This is the command prover9 that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
PROGRAM:
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.
Use prover9 online using onworks.net services