---
name: "epclextract"
section: "1"
platform: "linux"
package: "eprover"
version: "3.2.5+ds-1"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/epclextract"
---

# epclextract(1)

manual page for epclextract 3.2.5

## NAME

epclextract - manual page for epclextract 3.2.5

## SYNOPSIS

**epclextract** \[*options*\] \[*files*\]

## 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*.

## 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.

## COPYRIGHT

Copyright 1998-2024 by Stephan Schulz, schulz@eprover.org, and the E contributors (see DOC/CONTRIBUTORS).

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