Running Prover9

The standard way of running Prover9 is to (1) prepare an input file containing the logical specification of a conjecture and the search parameters, (2) issue a command that runs Prover9 on the input file and produces an output file, (3) look at the output, and (4) maybe run Prover9 again with different search parameters.

Nearly all of the information in this manual applies also when using a graphical user interface.

An Input File

Here is an input file; assume it is named subset_trans.in.
(Use a plain text editor, not a word processor, to create input files.)

formulas(sos).
  all x all y (subset(x,y) <-> (all z (member(z,x) -> member(z,y)))).
end_of_list.

formulas(goals).
  all x all y all z (subset(x,y) & subset(y,z) -> subset(x,z)).
end_of_list.

A Basic Prover9 Command

Here is a command to run Prover9 on the preceding file and send the output to a file called subset_trans.out.

prover9 -f subset_trans.in > subset_trans.out

When you run the preceding command, a message like the following should appear immediately on your screen.

-------- Proof 1 -------- 
THEOREM PROVED
------ process 3666 exit (max_proofs) ------

The output file subset_trans.out should contain the proof (and a lot of other information about the job).

Taking Input from Standard Input

Prover9 jobs can be run in a slightly different way, taking input from "standard input" instead of a named file, as follows.

prover9 < subset_trans.in > subset_trans.out2

The disadvantage of using this method is that the name of the input file is not given in the output file.

More Than One Input File

The input can occur in more than one file:

prover9 -f subset.in trans.in > subset_trans.out3

All arguments after the "-f" are taken as input filenames, and there can be as many as you like. When multiple filnames are given on the command line, a list of objects (clauses, formulas, or terms) cannot be split across more than one file.

Time Limit on the Command Line

Prover9 also accepts a time limit, in seconds, on the command line. The following command limits the job to about 10 seconds.

prover9 -t 10 -f subset_trans.in > subset_trans.out4

If "-t" and "-f" are both in the command, the "-t" must occur first.

Getting Statistics During the Search

This section applies to Unix-like systems only.

If a Prover9 process is running in the background, one can tell it to send search statistics (without killing the job) to the output file sending a "USR1" signal to the process. For example,

% prover9 -f p3a.in > p3a.outb &
    [1] 31613
% kill -USR1 31613
    A report (17.75 seconds) has been sent to the output.

Calling Prover9 From Another Program

If Prover9 is called from another program (e.g., a shell script, a Perl script, or a Python script), Prover9's exit codes can tell the other program the reason Prover9 terminates. The following table shows the exit codes.

Exit Code	Reason for Termination
0 (MAX_PROOFS)	The specified number of proofs (max_proofs) was found.
1 (FATAL)	A fatal error occurred (user's syntax error or Prover9's bug).
2 (SOS_EMPTY)	Prover9 ran out of things to do (sos list exhausted).
3 (MAX_MEGS)	The max_megs (memory limit) parameter was exceeded.
4 (MAX_SECONDS)	The max_seconds parameter was exceeded.
5 (MAX_GIVEN)	The max_given parameter was exceeded.
6 (MAX_KEPT)	The max_kept parameter was exceeded.
7 (ACTION)	A Prover9 action terminated the search.
101 (SIGINT)	Prover9 received an interrupt signal.
102 (SIGSEGV)	Prover9 crashed, most probably due to a bug.

The calling program will probably want to look in Prover9's output, for example, to extract a proof. See the page on Prover9 output files.