SYNOPSIS
prover9 [options] < input-file > output-fileprover9 [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.
AUTHOR
prover9 was written by William McCune <[email protected]>This manual page was written by Peter Collingbourne <[email protected]>, for the Debian project (but may be used by others).