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.6-DEBUG Floral Guranse
7

SYNOPSIS

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

DESCRIPTION

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

REPORTING BUGS

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

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