eprover

Automated theorem prover for first-order logic with equality

brewmacoslinux

Try with needOr install directly

About

Theorem prover for full first-order logic with equality

eprovereprover-ho

Prove a theorem from a TPTP format file$ eprover --auto problem.p

Check satisfiability with time limit of 10 seconds$ eprover --cpu-limit=10 input.tptp

Generate proof output in verbose mode$ eprover -v --proof=1 theorem.p