["SETHEO - A High-Perormance Theorem Prover for First-Order

Logic", Reinhold Letz et al, J Automated Reasoning

8(2):183-212 (1992)].