PTTP is a theorem-prover for the first-order predicate calculus
that uses the model elimination inference procedure and iterative
deepening search.  Input formulas are compiled by PTTP for direct
execution by Prolog, so individual inference operations are fast.