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

WWW: http://www-unix.mcs.anl.gov/AR/otter/