OTTER (Organized Techniques for Theorem-proving and Effective Research[1]) is an automated theorem prover developed by William McCune at Argonne National Laboratory in Illinois.

Otter was the first widely distributed, high-performance theorem prover for first-order logic, and it pioneered a number of important implementation techniques.

Otter is based on resolution and paramodulation, constrained by term orderings similar to those in the superposition calculus.

[2] Otter also pioneered the use of efficient term indexing techniques to speed up the search for inference partners in large clause sets.

However, "NEITHER THE UNITED STATES GOVERNMENT NOR ANY AGENCY THEREOF [...] REPRESENTS THAT ITS USE WOULD NOT INFRINGE PRIVATELY OWNED RIGHTS.