Updates
The new tree prover has now replaced the old one at /logik/trees. I'm still grateful for all kinds of feedback, even if it's just letting me know that it works on your machine. Unlike the old version, which has retired to /logik/oldtrees/, the new one certainly doesn't work any more with Internet Explorer on the Mac and Netscape 4. If you're still using these browsers, you should really consider switching to Mozilla (or, on MacOS Classic, WaMCom).
I've tested the prover on the first 40 Pelletier problems. It solves them all in less than 10 seconds, except problem 34 and problem 38, which take much longer (I haven't been patient enough to see how long). Some improvements are still turned off, but I haven't checked what difference they would make. I don't know any systematic testcase for invalid formulas, but from those I've tried the only ones it didn't catch were formulas whose refutation requires an infinite domain, like this one.
In case anyone's interested, there have also been minor updates of Beta-Blogger and Digital recently, and a not so minor update of Postbote will come very soon.