NOTE: The PROVER9 files linked in below assume you have installed the version of June 2006B ("LADR-June-2006B"). Our files may not work with later versions (e.g., they will not work with the August-2006A version or later, since the flags we set for the June-2006B version are no longer valid in the August-2006A version).
You can download a gzipped tarball of the June 2006B version of PROVER9 by following one of these links:
You will need to expand the Unix/Mac archive and compile the program yourself; the Windows version comes only as a binary, without sources.
If the above URLs are unavailable, a local copy for Unix/Mac can be obtained at the following URL:
Assuming that you have installed the above version of PROVER9, you can download the input and output files linked in below and process them. The standard command-line syntax for running PROVER9 is:
prover9 < theorem.in
or, if you want to append PROVER9's output to a file:
prover9 < theorem.in > theorem.out
If you need further help in running PROVER9, you can consult the manual that goes with the June 2006B version of PROVER9, which can be viewed at the following location:
(A local copy in tar/gzipped format can be downloaded here.)
Similarly, one can use MACE4 to find models of the axioms used in the proof of each theorem. This provides a finite verification of the consistency of the axioms and definitions. The standard command-line syntax for running MACE4 is (unless otherwise noted):
mace4 -c -N 8 -p 1 < model.in
or, if you want to append MACE4's output to a file,
mace4 -c -N 8 -p 1 < model.in > model.out