folderol Prover for first-order logic. Derived from the Standard ML implementation of Lawrence C Paulson, here