epclextract - manual page for epclextract 3.2.5

Copyright

This program is a part of the distribution of the equational theorem prover E. You can find the latest
version of the E distribution as well as additional information at http://www.eprover.org

This program is free software; you can redistribute it and/or modify it under the terms of the GNU
General Public License as published by the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even
the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
License for more details.

You should have received a copy of the GNU General Public License along with this program (it should be
contained in the top level directory of the distribution in the file COPYING); if not, write to the Free
Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

We welcome bug reports and even reasonable questions. If the prover behaves in an unexpected way, please
include the following information:

- What did you observe? - What did you expect? - The output of `eprover --version` - The full
commandline that lead to the unexpected behaviour - The input file(s) that lead to the unexpected
behaviour

Most bug reports should be send to <schulz@eprover.org>. Bug reports with respect to the HO-version
should be send to or at least copied to <jasmin.blanchette@gmail.com>. Please remember that this is an
unpaid volunteer service.

The original copyright holder can be contacted via email or as

Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Lerchenstrasse 1 70174 Stuttgart Germany

epclextract 3.2.5 October 2024 EPCLEXTRACT(1)

Description

       epclextract 3.2.5

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

       Options

       -h--help

              Print a short description of program usage and options.

       -V--version

              Print the version number of the program.

       -v--verbose[=<arg>]

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

       -f--fast-extract

              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.

       -C--forward-comments

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

       -c--competition-framing

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

       -n--no-extract

              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.

       --tstp-out

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

       --tptp3-out

              Synonymous with --tstp-out.

       -o <arg>

       --output-file=<arg>

              Redirect output into the named file.

       -s--silent

              Equivalent to --output-level=0.

Name

       epclextract - manual page for epclextract 3.2.5

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.