prover9 man page

prover9 — resolution/paramodulation theorem prover


prover9 [options] < input-file > output-file
prover9 [options] -f input-file > output-file


This manual page documents briefly the prover9 command.

prover9 is an automated theorem prover for first-order and equational logic. It is a successor of the otter(1) prover.  prover9 uses the inference techniques of ordered resolution and paramodulation with literal selection.


A summary of options is included below.


View a list of command-line options.


Enables an experimental enhanced auto-mode.  For more information consult the prover9 manual.


Fully parenthesize output.

-t n

Constrain the search to last about n seconds.  For UNIX-like systems, the `user CPU' time is used.

-f file

Take input from file instead of from standard input.

See Also

mace4(1), otter(1).
On Debian systems, the manual is found in the prover9-doc package, at /usr/share/doc/prover9-doc/manual/index.html.


prover9 was written by William McCune <>

This manual page was written by Peter Collingbourne <>, for the Debian project (but may be used by others).

Referenced By

mace4(1), prover9-clausefilter(1), prover9-clausetester(1), prover9-interpfilter(1), prover9-prooftrans(1), prover9-rewriter(1).

August 12, 2007