1E_LTB_RUNNER(1)                  User Commands                 E_LTB_RUNNER(1)
2
3
4

NAME

6       e_ltb_runner - manual page for e_ltb_runner 2.3-DEBUG Gielle
7

SYNOPSIS

9       e_ltb_runner [options] [files]
10

DESCRIPTION

12       e_ltb_runner 2.3-DEBUG "Gielle"
13
14       Read a CASC 26 LTB batch specification file and process it.
15

OPTIONS

17       -h
18
19       --help
20
21              Print a short description of program usage and options.
22
23       -V
24
25       --version
26
27              Print the version number of the prover. Please include this with
28              all bug reports (if any).
29
30       -v
31
32       --verbose[=<arg>]
33
34              Verbose comments on the progress of the  program.  This  differs
35              from  the  output level (below) in that technical information is
36              printed to stderr, while the output level determines which logi‐
37              cal  manipulations  of  the  clauses  are printed to stdout. The
38              short form or the long form without  the  optional  argument  is
39              equivalent to --verbose=1.
40
41       -o <arg>
42
43       --output-file=<arg>
44
45              Redirect output into the named file.
46
47       -d <arg>
48
49       --output-dir=<arg>
50
51              Directory  for  individual  problem output files. Default is the
52              current working directory.
53
54       -i
55
56       --interactive
57
58              For each batch file, enter  interactive  mode  after  processing
59              batch the batch problems. Interactive mode allows the processing
60              of additional jobs with respect to the loaded axioms  set.  Jobs
61              are entered via stdin and print to stdout.
62
63       -s
64
65       --silent
66
67              Equivalent to --output-level=0.
68
69       -l <arg>
70
71       --output-level=<arg>
72
73              Select  an  output level, greater values imply more verbose out‐
74              put. Level 0 produces nearly no output, level 1 will output each
75              clause as it is processed, level 2 will output generating infer‐
76              ences, level 3 will give a full protocol including rewrite steps
77              and  level 4 will include some internal clause renamings. Levels
78              >= 2 also imply PCL2 or TSTP formats  (which  can  be  post-pro‐
79              cessed with suitable tools).
80
81       -w <arg>
82
83       --wtc-limit=<arg>
84
85              Set the global wall-clock limit for each batch (if any).
86

REPORTING BUGS

88       Report  bugs  to <schulz@eprover.org>. Please include the following, if
89       possible:
90
91       * The version of the package as reported by eprover --version.
92
93       * The operating system and version.
94
95       * The exact command line that leads to the unexpected behaviour.
96
97       * A description of what you expected and what actually happend.
98
99       * If possible all input files necessary to reproduce the bug.
100

102       Copyright 1998-2019 by Stephan Schulz, schulz@eprover.org,  and  the  E
103       contributors (see DOC/CONTRIBUTORS).
104
105       This  program  is  a part of the distribution of the equational theorem
106       prover E. You can find the latest version of the E distribution as well
107       as additional information at http://www.eprover.org
108
109       This program is free software; you can redistribute it and/or modify it
110       under the terms of the GNU General Public License as published  by  the
111       Free  Software Foundation; either version 2 of the License, or (at your
112       option) any later version.
113
114       This program is distributed in the hope that it  will  be  useful,  but
115       WITHOUT  ANY  WARRANTY;  without  even  the  implied  warranty  of MER‐
116       CHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  General
117       Public License for more details.
118
119       You should have received a copy of the GNU General Public License along
120       with this program (it should be contained in the top level directory of
121       the  distribution in the file COPYING); if not, write to the Free Soft‐
122       ware  Foundation,  Inc.,  59  Temple  Place,  Suite  330,  Boston,   MA
123       02111-1307 USA
124
125       The original copyright holder can be contacted via email or as
126
127       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Rote‐
128       buehlplatz 41 70178 Stuttgart Germany
129
130
131
132e_ltb_runner 2.3-DEBUG Gielle     April 2019                   E_LTB_RUNNER(1)
Impressum