otter 3.3f-1.1 (amd64 binary) in ubuntu precise

 OTTER is an automated theorem prover for equational logic developed
 at Argonne National Laboratory.
 .
 OTTER's inference rules are based on resolution and paramodulation,
 and it includes facilities for term rewriting, term orderings,
 Knuth-Bendix completion, weighting, and strategies for directing and
 restricting searches for proofs. OTTER can also be used as a symbolic
 calculator and has an embedded equational programming system.