Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Otter and Mace2
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.