Prover9-Mace4-v05B

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

Prover9 is the successor of the Otter prover. The program comes for different operating systems and a Mac version is also available.