Prover9

This is Prover9, an automated theorem prover and model finder for first-order logic with equality.

This clone is based on the version LADR-2017-11A provided by Bob Veroff, the most recent version in August 2018.

Readme first

Prover9, Mace4, and Related Programs.

To compile, see README.make.

See

http://www.cs.unm.edu/~mccune/prover9/

for the HTML manual, examples, and updates.