NAME

       prover9 - resolution/paramodulation theorem prover

SYNOPSIS

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

DESCRIPTION

       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.

OPTIONS

       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.

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.

AUTHOR

       prover9 was written by William McCune <mccune@cs.unm.edu>

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

                                         August 12, 2007                               PROVER9(1)