EPCLEXTRACT(1)                   User Commands                  EPCLEXTRACT(1)

       epclextract - manual page for epclextract 1.9

       epclextract [options] [files]

       epclextract 1.9

       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



              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.

       Report bugs to <schulz@eprover.org>. Please include the following, if

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

       Copyright 1998-2014 by Stephan Schulz, schulz@eprover.org

       This program is a part of the support structure for the E equational
       theorem prover. 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
       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

       The original copyright holder can be contacted as

       Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik
       Rotebuehlplatz 41 70178 Stuttgart Germany

epclextract 1.9                    July 2015                    EPCLEXTRACT(1)