Otter is an automated deduction system (theorem prover) for
first-order logic with equality developed at Argonne National
Laboratories.