.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.49.2.
.TH EPCLEXTRACT "1" "July 2022" "epclextract 2.6" "User Commands"
.SH NAME
epclextract \- manual page for epclextract 2.6
.SH SYNOPSIS
.B epclextract
[\fI\,options\/\fR] [\fI\,files\/\fR]
.SH DESCRIPTION
epclextract 2.6
.PP
Read an PCL2 protocol and print the steps necessary for proving the clauses in "proof", "final", or "extract" steps.
.PP
Options
.HP
\fB\-h\fR
.HP
\fB\-\-help\fR
.IP
Print a short description of program usage and options.
.HP
\fB\-V\fR
.HP
\fB\-\-version\fR
.IP
Print the version number of the program.
.HP
\fB\-v\fR
.HP
\fB\-\-verbose[=\fR<arg>]
.IP
Verbose comments on the progress of the program. The short form or the
long form without the optional argument is equivalent to \fB\-\-verbose\fR=\fI\,1\/\fR.
.HP
\fB\-f\fR
.HP
\fB\-\-fast\-extract\fR
.IP
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.
.HP
\fB\-C\fR
.HP
\fB\-\-forward\-comments\fR
.IP
Pass comments found in the input through to the output while reading
input.
.HP
\fB\-c\fR
.HP
\fB\-\-competition\-framing\fR
.IP
Print special "begin" and "end"comments around the proof object, as
required by the CASC MIX* class.
.HP
\fB\-n\fR
.HP
\fB\-\-no\-extract\fR
.IP
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.
.HP
\fB\-\-tstp\-out\fR
.IP
Print proof protocol in TSTP syntax (default is PCL).
.HP
\fB\-\-tptp3\-out\fR
.IP
Synonymous with \fB\-\-tstp\-out\fR.
.HP
\fB\-o\fR <arg>
.HP
\fB\-\-output\-file=\fR<arg>
.IP
Redirect output into the named file.
.HP
\fB\-s\fR
.HP
\fB\-\-silent\fR
.IP
Equivalent to \fB\-\-output\-level\fR=\fI\,0\/\fR.
.SH "REPORTING BUGS"
.PP
Report bugs to <schulz@eprover.org>. Please include the following, if
possible:
.PP
* The version of the package as reported by \fBeprover \-\-version\fR.
.PP
* The operating system and version.
.PP
* The exact command line that leads to the unexpected behaviour.
.PP
* A description of what you expected and what actually happened.
.PP
* If possible all input files necessary to reproduce the bug.
.SH COPYRIGHT
Copyright 1998\-2021 by Stephan Schulz, schulz@eprover.org,
and the E contributors (see DOC/CONTRIBUTORS).
.PP
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
.PP
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.
.PP
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.
.PP
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
.PP
The original copyright holder can be contacted via email or as
.PP
Stephan Schulz
DHBW Stuttgart
Fakultaet Technik
Informatik
Rotebuehlplatz 41
70178 Stuttgart
Germany