Tree Proof Generator Update
I've spent some more time on the Tree Proof Generator. The algorithm is now a lot faster, more information is displayed during calculation, and there are new buttons to control the drawing.
This formula (the last one on the Examples page) is quite interesting: After the quantifiers have all been dealt with, there are 36 formulas on the tree that have to be broken down by the truth-functional rules. I let it run for several hours. When finally Mozilla ran out of memory it had developed just 25 of those 36 formulas, building a tree with 179797 nodes!
I've got that formula from David Bostock's very fine book "Intermediate Logic", where he says that "the tedium of writing out a completed tableau" for this formula would be "very considerable" (p.177). Indeed.