Provided by: prover9_0.0.200911a-2.1build1_amd64 bug


       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.

       -h     View a list of command-line options.

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

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


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


       prover9 was written by William McCune <>

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

                                         August 12, 2007                               PROVER9(1)