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.5-DEBUG Avongrove
7

SYNOPSIS

9       e_ltb_runner [options] [Batchfile] [PATH_TO_EPROVER]
10

DESCRIPTION

12       e_ltb_runner 2.5-DEBUG "Avongrove"
13
14       Read a CASC 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       --variants27
55
56              Handle different variants for each problem base name as required
57              for CASC-27. This is very specific hack.
58
59       -i
60
61       --interactive
62
63              For  each  batch  file,  enter interactive mode after processing
64              batch the batch problems. Interactive mode allows the processing
65              of  additional  jobs with respect to the loaded axioms set. Jobs
66              are entered via stdin and print to stdout.
67
68       -s
69
70       --silent
71
72              Equivalent to --output-level=0.
73
74       -l <arg>
75
76       --output-level=<arg>
77
78              Select an output level, greater values imply more  verbose  out‐
79              put. Level 0 produces nearly no output, level 1 will output each
80              clause as it is processed, level 2 will output generating infer‐
81              ences, level 3 will give a full protocol including rewrite steps
82              and level 4 will include some internal clause renamings.  Levels
83              >=  2  also  imply  PCL2 or TSTP formats (which can be post-pro‐
84              cessed with suitable tools).
85
86       -w <arg>
87
88       --wtc-limit=<arg>
89
90              Set the global wall-clock limit for each batch (if any).
91

REPORTING BUGS

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

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