epclextract man page

epclextract — manual page for epclextract 1.9.1-001


epclextract [options] [files]


epclextract 1.9.1-001

Read an PCL2 protocol and print the steps necessary for proving the clauses in "proof", "final", or "extract" steps.




Print a short description of program usage and options.



Print the version number of the program.



Verbose comments on the progress of the program. The short form or the long form without the optional argument is equivalent to --verbose=1.



Do a fast extract. With this option the program understands only a subset of PCL and assumes that all "proof" and "final" steps are at the end of the protocoll.



Pass comments found in the input through to the output while reading input.



Print special "begin" and "end"comments around the proof object, as requiered by the CASC MIX* class.



Don't extract, print back all steps (actually, it treats all steps as proof steps). Useful as a syntax checker, or if you want to convert PCL to TSTP with the next option.


Print proof protocol in TSTP syntax (default is PCL).


Synonymous with --tstp-out.

-o <arg>


Redirect output into the named file.



Equivalent to --output-level=0.

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.


epclextract 1.9.1-001 September 2016