E_LTB_RUNNER(1)

💖 E_LTB_RUNNER — the manual page, bestie edition 💖

okay so. This is the manual page for E_LTB_RUNNER(1) — that's the thing you're reading rn, and also the little program it's about. Strap in. 🎀

✨ NAME ✨

e_ltb_runner — manual page for e_ltb_runner 3.5.1 Countess Grey

🌸 SYNOPSIS 🌸

e_ltb_runner [options] [Batchfile] [PATH_TO_EPROVER]

🦋 DESCRIPTION 🦋

e_ltb_runner 3.5.1 "Countess Grey" 💅

She reads a CASC LTB batch specification file and processes it. That's the whole job. Iconic behaviour, honestly. ✨

---

👑 OPTIONS 👑

• -h / --help — prints a short lil description of how to use the program and what the options do. Baby's first flag. 🫶
• -V / --version — prints the version number of the prover. bestie, PLEASE include this with all bug reports (if any). It's literally the number one thing we need. 😭
• -v / --verbose[=<arg>] — verbose comments on the progress of the program. NOT the same as the output level (that's down below, keep reading 👀): this one prints technical info to stderr, while the output level controls which logical manipulations of the clauses get 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. Classic. 🎀
• -d <arg> / --output-dir=<arg> — directory for individual problem output files. Default is the current working directory. (Yes, that's where you already are. No cap.)
• --variants27 — handles different variants for each problem base name, as required for CASC-27. This is a very specific hack. It said what it said. 💀
• --variants28 — handles different variants for each problem base name, as required for CASC-28 (without higher-order support). Also a very specific hack. ✨
• --variants28-ho — handles different variants for each problem base name, as required for CASC-28, including the TH0-variant. Very specific hack. Heads up: this one requires eprover-ho for the third variant. 🫶
• --variants28-25 — handles different variants for each problem base name, as required for CASC-28, but runs E-2.5 (prerelease) as the base prover. This is a really very specific hack, existing so that E 2.5 — the CASC-J10 LTB winner, hello?? 👑 — can compete in CASC-28. It requires manual installation of the eprover-2.5 binary in the StarExec package. Manual. Installation. You've been warned. 😭
• --variantsj11 — handles different variants for each problem base name, as required for CASC-J11. See above. ⬆️
• -i / --interactive — for each batch file, drops you into interactive mode after it processes the batch problems. Interactive mode lets you process additional jobs with respect to the loaded axioms set. Jobs come in via stdin and print to stdout. 💅
• -s / --silent — equivalent to --output-level=0. The quiet luxury option. 🤫
• -l <arg> / --output-level=<arg> — pick an output level; bigger values mean more verbose output. The levels, ranked:
  1. Level 0 produces nearly no output.
  2. Level 1 will output each clause as it is processed.
  3. Level 2 will output generating inferences.
  4. Level 3 will give a full protocol including rewrite steps.
  5. Level 4 will include some internal clause renamings.

Levels >= 2 also imply PCL2 or TSTP formats (which can be post-processed with suitable tools). So level 4 really is the main character. ✨

• -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 happened.
• If possible all input files necessary to reproduce the bug.

like fr fr, all of that. It makes the fix happen so much faster bestie. 🫶

---

💜 COPYRIGHT 💜

Copyright 1998-2026 by Stephan Schulz, schulz@eprover.org, and the E contributors (see DOC/CONTRIBUTORS).

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

We welcome bug reports and even reasonable questions. If the prover behaves in an unexpected way, please include the following information:

• What did you observe?
• What did you expect?
• The output of eprover --version
• The full commandline that lead to the unexpected behaviour
• The input file(s) that lead to the unexpected behaviour

Most bug reports should be send to <schulz@eprover.org>. Bug reports with respect to the HO-version should be send to or at least copied to <jasmin.blanchette@gmail.com>. Please remember that this is an unpaid volunteer service. 🙏 (be nice, they're doing this for free)

The original copyright holder can be contacted via email or as

Stephan Schulz
DHBW Stuttgart
Fakultaet Technik Informatik
Lerchenstrasse 1
70174 Stuttgart
Germany

---

and that's the whole page bestie 🎀 go forth, process those batch files, and remember: --version in every bug report or it didn't happen 💅

e_ltb_runner 3.5.1 Countess Grey — August 2026 — E_LTB_RUNNER(1) ✨🦋🌸 that's the version, the date, and the manual section, all tucked into one cute lil sign-off, periodt. 💖