Wolfgang Schwarz

Oh Dear

I just noticed that my tree prover fails on this simple formula! This is a good opportunity to rewrite the part of the script that does the proving and implement some shortcuts, and maybe some "loop detection".