Your company here — click to reach over 10,000 unique daily visitors

epclextract - Man Page

manual page for epclextract 3.1.0-DEBUG


epclextract [options] [files]


epclextract 3.1.0-DEBUG

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 required 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 happened.

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


May 2024 epclextract 3.1.0-DEBUG