e_ltb_runner

E_LTB_RUNNER(1)                  User Commands                 E_LTB_RUNNER(1)



NAME
       e_ltb_runner - manual page for e_ltb_runner 1.9 Sourenee

SYNOPSIS
       e_ltb_runner [options] [files]

DESCRIPTION
       e_ltb_runner 1.9 "Sourenee"

       Read a CASC 24 LTB batch specification file and process it.

OPTIONS
       -h

       --help

              Print a short description of program usage and options.

       -V

       --version

              Print the version number of the prover. Please include this with
              all bug reports (if any).

       -v

       --verbose[=<arg>]

              Verbose comments on the progress of the program. This differs
              from the output level (below) in that technical information is
              printed to stderr, while the output level determines which
              logical manipulations of the clauses are printed to stdout. The
              short form or the long form without the optional argument is
              equivalent to --verbose=1.

       -o <arg>

       --output-file=<arg>

              Redirect output into the named file.

       -i

       --interactive

              For each batch file, enter interactive mode after processing
              batch the batch problems. Interactive mode allows the processing
              of additional jobs with respect to the loaded axioms set. Jobs
              are entered via stdin and print to stdout.

       -s

       --silent

              Equivalent to --output-level=0.

       -l <arg>

       --output-level=<arg>

              Select an output level, greater values imply more verbose
              output. Level 0 produces nearly no output, level 1 will output
              each clause as it is processed, level 2 will output generating
              inferences, level 3 will give a full protocol including rewrite
              steps and level 4 will include some internal clause renamings.
              Levels >= 2 also imply PCL2 or TSTP formats (which can be
              post-processed with suitable tools).

       -w <arg>

       --wtc-limit=<arg>

              Set the global wall-clock limit for each batch (if any).

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

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

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

       You can find the latest version of E and 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

       The original copyright holder can be contacted as

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



e_ltb_runner 1.9 Sourenee          July 2015                   E_LTB_RUNNER(1)