eproof_ram man page

eproof_ram — manual page for eproof_ram PROVER/eproof_ram


eproof_ram [options] <file1> ...



Eproof_ram is a wrapper around E and epclextract. It will run E with output level 4 (full output of all potentially proof-relevant inferences) and pipe the output through epclextract to provide a proof derivation or a derivation of all clauses in the saturated proof state.

Eproof_ram will intercept the command line arguments and interpret certain options as described below. All other options and arguments are  passed on to eprover or epclextract, as appropriate. See those tools help pages for the supported options.

In particular, eproof_ram will automatically do a close approximation of 'the right thing' (tm) with the options describing input- and output formats.


Print a short description of program usage and options.
Print the version numbers of eprover and epclextract used by this instance of eproof. Please include this with all bug reports (if any).

Reporting Bugs

Report bugs to <schulz@eprover.org>. Please include the following, if possible:

* The version of the package as reported by eprover --version.

* The operating system and version.

* The exact command line that leads to the unexpected behaviour.

* A description of what you expected and what actually happend.

* If possible all input files necessary to reproduce the bug.


August 2017 eproof_ram PROVER/eproof_ram User Commands