Otter and Mace2

Otter is an automated theorem prover for first-order and equational logic, and Mace2 searches for finite models and counterexamples.

Otter/Mace2 are no longer being actively developed, and maintenance and support minimal.

We recommend using Otter/Mace2's successor Prover9/Mace4 instead.