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.
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.