E(1)

✨ E(1) ✨

Bestie, this is the manual page for E version 3.5.1 “Countess Grey” (facc36eaf92d70896d830140efc4382df9e8dcdb). It's giving prover main character energy and I'm obsessed. 💅

💖 NAME 💖

E — manual page for E 3.5.1 Countess Grey (facc36eaf92d70896d830140efc4382df9e8dcdb).

🌈 SYNOPSIS 🌈

# 🦋 DESCRIPTION 🦋

<purple>E 3.5.1 “Countess Grey”</purple>

Read a set of first-order (or, in the `-ho-version`, higher-order) clauses and formulae and try to prove the conjecture (if given) or show the set unsatisfiable. <pink>No cap, that's the whole vibe.</pink> ✨

# 💅 OPTIONS 💅

Okay bestie, here's the option buffet. One bullet per glow-up, all the facts intact. 👑

- **`-h`, `--help`** — Prints a short description of program usage and options. <mint>Iconic for when you're lost.</mint>
- **`-V`, `--version`** — Prints the version number of the prover. <yellow>Please include this with all bug reports (if any) 💀.</yellow>
- **`-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`. <lavender>iykyk.</lavender>
- **`-o <arg>`, `--output-file=<arg>`** — Redirect output into the named file. <blue>Bye bye terminal spam.</blue>
- **`-s`, `--silent`** — Equivalent to `--output-level=0`. <purple>Shhh 🤫.</purple>
- **`-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). <hotpink>Pick your chaos level.</hotpink>
- **`-p`, `--proof-object[=<arg>]`** — Generate (and print, in case of success) an internal proof object. Level `0` will not print a proof object, level `1` will build a simple, compact proof object that only contains inference rules and dependencies, level `2` will build a proof object where inferences are unambiguously described by giving inference positions, and level `3` will expand this to a proof object where all intermediate results are explicit. <red>This feature is under development, so far only level `0` and `1` are operational.</red> The proof object will be provided in TPTP-3 or PCL syntax, depending on input format and explicit settings. The `--proof-graph` option will suppress normal output of the proof object in favour of a graphical representation. The short form or the long form without the optional argument is equivalent to `--proof-object=1`. <rainbow>Slay but stay safe.</rainbow>
- **`--proof-graph[=<arg>]`** — Generate (and print, in case of success) an internal proof object in the form of a GraphViz dot graph. The optional argument can be `1` (nodes are labelled with just the name of the clause/formula), `2` (nodes are labelled with the TPTP clause/formula) or `3` (nodes also labelled with source/inference record). The option without the optional argument is equivalent to `--proof-graph=3`. <cyan>GraphViz girlies rise.</cyan> 📈
- **`--proof-statistics`** — Print various statistics of the proof object. <mint>Numbers, but make it proof.</mint>
- **`-d`, `--full-deriv`** — Include all derived formuas/clauses in the proof graph/proof object, not just the ones contributing to the actual proof. <peach>All the receipts, not just the winning ones.</peach>
- **`--force-deriv[=<arg>]`** — Force output of the derivation even in cases where the prover terminates in an indeterminate state. By default, the deriviation of all processed clauses is included in the derivation object. With argument `2`, the derivation of all clauses will be printed. The option without the optional argument is equivalent to `--force-deriv=1`. <yellow>Force it? Okay, main character.</yellow>
- **`--record-gcs`** — Record given-clause selection as separate (pseudo-)inferences and preserve the form of given clauses evaluated and selected via archiving for analysis and possibly machine learning. <purple>ML girlies, this one's for you.</purple> 🤖
- **`--training-examples[=<arg>]`** — Generate and process training examples from the proof search object. Implies `--record-gcs`. The argument is a binary or of the desired processing. Bit zero prints positive exampels. Bit 1 prints negative examples. Additional selectors will be added later. The option without the optional argument is equivalent to `--training-examples=1`. <green>Training era.</green> 🏋️
- **`--pcl-terms-compressed`** — Print terms in the PCL output in shared representation. <blue>Compressed, but make it readable.</blue>
- **`--pcl-compact`** — Print PCL steps without additional spaces for formatting (safes disk space for large protocols). <pink>Disk space is precious, bestie.</pink>
- **`--pcl-shell-level[=<arg>]`** — Determines level to which clauses and formulas are suppressed in the output. Level `0` will print all, level `1` will only print initial clauses/formulas, level `2` will print no clauses or axioms. All levels will still print the dependency graph. The option without the optional argument is equivalent to `--pcl-shell-level=1`. <lavender>Shell level = vibe check for output.</lavender>
- **`--print-statistics`** — Print the inference statistics (only relevant for output level `<=1`, otherwise they are printed automatically). <cyan>Stats o'clock.</cyan> ⏰
- **`-0`, `--print-detailed-statistics`** — Print data about the proof state that is potentially expensive to collect. Includes number of term cells and number of rewrite steps. This implies the previous option. <red>Expensive but worth it?</red> 💸
- **`-S`, `--print-saturated[=<arg>]`** — Print the (semi-) saturated clause sets after terminating the saturation process. The argument given describes which parts should be printed in which order. Legal characters are `'teigEIGaA'`, standing for type declarations, processed positive units, processed negative units, processed non-units, unprocessed positive units, unprocessed negative units, unprocessed non-units, and two types of additional equality axioms, respectively. Equality axioms will only be printed if the original specification contained real equality. In this case, `'a'` requests axioms in which a separate substitutivity axiom is given for each argument position of a function or predicate symbol, while `'A'` requests a single substitutivity axiom (covering all positions) for each symbol. The short form or the long form without the optional argument is equivalent to `--print-saturated=eigEIG`. <rainbow>Alphabet soup, but make it logic.</rainbow> 🔤
- **`--print-sat-info`** — Print additional information (clause number, weight, etc) as a comment for clauses from the semi-saturated end system. <mint>Extra commentary, because why not.</mint>
- **`--filter-saturated[=<arg>]`** — Filter the (semi-) saturated clause sets after terminating the saturation process. The argument is a string describing which operations to take (and in which order). Options are `'u'` (remove all clauses with more than one literal), `'c'` (delete all but one copy of identical clauses, `'n'`, `'r'`, `'f'` (forward contraction, unit-subsumption only, no rewriting, rewriting with rules only, full rewriting, respectively), and `'N'`, `'R'` and `'F'` (as their lower case counterparts, but with non-unit-subsumption enabled as well). The option without the optional argument is equivalent to `--filter-saturated=Fc`. <peach>Filter it like a photo, but for clauses.</peach> 📸
- **`--syntax-only`** — Stop after parsing, i.e. only check if the input can be parsed correcly. <yellow>Just a vibe check on syntax.</yellow>
- **`--print-formulas`** — If the syntax checks out, print back an include-expanded all formula-version of the peoblem, then terminate. <blue>Print it and dip.</blue>
- **`--prune`** — Stop after relevancy pruning, SInE pruning, and output of the initial clause- and formula set. This will automatically set output level to `4` so that the pruned problem specification is printed. Note that the desired pruning methods must still be specified (e.g. `'--sine=Auto'`). <purple>Prune it, then show the receipts.</purple>
- **`--cnf`** — Convert the input problem into clause normal form and print it. This is (nearly) equivalent to `'--print-saturated=eigEIG --processed-clauses-limit=0'` and will by default perform some usually useful simplifications. You can additionally specify e.g. `'--no-preprocessing'` if you want just the result of CNF translation. <cyan>CNF glow-up.</cyan>
- **`--print-pid`** — Print the process id of the prover as a comment after option processing. <mint>PID, but as a comment.</mint>
- **`--print-version`** — Print the version number of the prover as a comment after option processing. Note that unlike `-version`, the prover will not terminate, but proceed normally. <hotpink>Version peek, no exit.</hotpink>
- **`--error-on-empty`** — Return with an error code if the input file contains no clauses. Formally, the empty clause set (as an empty conjunction of clauses) is trivially satisfiable, and E will treat any empty input set as satisfiable. However, in composite systems this is more often a sign that something went wrong. Use this option to catch such bugs. <red>Bug catcher energy.</red> 🐛
- **`-m <arg>`, `--memory-limit=<arg>`** — Limit the memory the prover may use. The argument is the allowed amount of memory in MB. If you use the argument `'Auto'`, the system will try to figure out the amount of physical memory of your machine and claim most of it. This option may not work everywhere, due to broken and/or strange behaviour of `setrlimit()` in some UNIX implementations, and due to the fact that I know of no portable way to figure out the physical memory in a machine. Both the option and the `'Auto'` version do work under all tested versions of Solaris and GNU/Linux. Due to problems with limit data types, it is currently impossible to set a limit of more than 2 GB (2048 MB). <yellow>Memory limits: complicated, but we move.</yellow> 🧠
- **`--cpu-limit[=<arg>]`** — Limit the (per core) cpu time the prover should run. The optional argument is the CPU time in seconds. The prover will terminate immediately after reaching the time limit, regardless of internal state. As a side effect, this option will inhibit core file writing. Please note that if you use both `--cpu-limit` and `--soft-cpu-limit`, the soft limit has to be smaller than the hard limit to have any effect. The option without the optional argument is equivalent to `--cpu-limit=300`. <peach>Time's up, bestie.</peach> ⏳
- **`--soft-cpu-limit[=<arg>]`** — *and the description for this one is coming in part 2, bestie, stay tuned 💖*

...which lowkey means the prover gets told "girl, wrap it up" and then it **terminates gracefully** — like, it'll still do post-processing, filtering, and printing of unprocessed clauses, *if* those options are selected. But bestie, fair warning: for some filtering options (especially the ones doing full subsumption), the post-processing time can absolutely be **bigger** than the saturation time. 🙈 This one is chef's kiss if you're using E as a preprocessor or lemma generator inside some bigger system. And the version with no optional argument? That's the same as `--soft-cpu-limit=290`. Periodt.

---

- **`-R`, `--resources-info`** — spills the tea on what resources the prover used. Usually you get CPU time info; on systems that hand back more with the `rusage()` system call, you also get the memory consumption deets. 👑

- **`--select-strategy=<arg>`** — pick one of the built-in strategies and it sets all the proof search parameters accordingly. One-stop glow-up. ✨

- **`--print-strategy[=<arg>]`** — prints a representation of *all* search parameters and their settings for a given strategy, then peaces out (terminates). No argument? It prints the current strategy. Two reserved names for you: `'>all-strats<'` gets you a description of every built-in strategy, and `'>all-names<'` gets you a list of all the strategy names. No optional argument = `--print-strategy=>current-strategy<`.

- **`--parse-strategy=<arg>`** — takes a previously printed representation of a strategy and sets all proof search parameters accordingly. The come-back-around. 🦋

- **`-C <arg>`, `--processed-clauses-limit=<arg>`** — the max number of clauses to process, like, literally the number of traversals of the main-loop.

- **`-P <arg>`, `--processed-set-limit=<arg>`** — max size of the set of processed clauses. Different from the last one because redundant and back-simplified processed clauses **don't** get counted.

- **`-U <arg>`, `--unprocessed-limit=<arg>`** — max size of the set of unprocessed clauses. Heads up: this is a *termination condition*, not a knob for controlling deletion of bad clauses. For that vibe, compare `--delete-bad-limit`.

- **`-T <arg>`, `--total-clause-set-limit=<arg>`** — max size of the set of *all* clauses. Same energy as the previous option, just the whole squad.

- **`--generated-limit=<arg>`** — max number of generated clauses before the proof search stops. It's a reasonable (though ngl, not great) estimate of the work done.

- **`--tb-insert-limit=<arg>`** — max number of term bank term top insertions. Again: reasonable (though not great) estimate of the work done.

- **`--answers[=<arg>]`** — sets the max number of answers to print for existentially quantified questions. Without it, the prover stops after the *first* answer it finds. And okay so ⚠️ if the value is anything other than `1`, the prover is **no longer guaranteed to terminate**, even if there's a finite number of answers. No optional argument = `--answers=2147483647`.

- **`--conjectures-are-questions`** — treats all conjectures as questions to be answered. The original calls it a wart, and honestly? It is, but it's a *necessary* wart: CASC-J6 has categories that require answers but doesn't yet support the `'question'` type for formulas. 💀

- **`-n`, `--eqn-no-infix`** — in LOP, print equations in prefix notation: `equal(x,y)`.

- **`-e`, `--full-equational-rep`** — in LOP. print all literals as equations, even the non-equational ones. (yes the original has a period there, we respect the source 🫶)

- **`--print-oriented-eqlits-as-rules`** — prints oriented equational literals as rules, using `->` in place of `=`.

- **`--lop-in`** — sets E-LOP as the input format. If no input format is picked by this or one of the following options, E guesses based on the first token. It'll almost always correctly recognize TPTP-3, but it *may* misidentify E-LOP files that use TPTP meta-identifiers as logical symbols. So like, usually iconic, occasionally messy.

- **`--pcl-out`** — sets PCL as the proof object output format.

- **`--tptp-in`** — sets TPTP-2 as the input format (but note that includes are still handled according to TPTP-3 semantics 👀).

- **`--tptp-out`** — print TPTP format instead of E-LOP. Implies `--eqn-no-infix` and will ignore `--full-equational-rep`.

- **`--tptp-format`** — equivalent to `--tptp-in` and `--tptp-out` together.

- **`--tptp2-in`** — synonymous with `--tptp-in`.

- **`--tptp2-out`** — synonymous with `--tptp-out`.

- **`--tptp2-format`** — synonymous with `--tptp-format`.

- **`--tstp-in`** — sets TPTP-3 as the input format. Real talk: TPTP-3 syntax is still under development, so any given version in E may not be fully conforming at all times. That said, E works on all TPTP 8.2.0 FOF and CNF files (including includes). 💅

- **`--tstp-out`** — prints output clauses in TPTP-3 syntax. In particular, for output levels >=2, it writes derivations as TPTP-3 derivations.

- **`--tstp-format`** — equivalent to `--tstp-in` and `--tstp-out`.

- **`--tptp3-in`** — synonymous with `--tstp-in`.

- **`--tptp3-out`** — synonymous with `--tstp-out`.

- **`--tptp3-format`** — synonymous with `--tstp-format`.

- **`--auto`** — automatically determines the settings for proof search. Let it cook. 🔥

- **`--auto-schedule[=<arg>]`** — uses the (experimental!) strategy scheduling. It tries several different fully specified search strategies (aka "Auto-Modes"), one after the other, until a proof or saturation is found, or the time limit is exceeded. The optional argument is the number of CPUs the schedule gets run on. By default it runs on a single core. Wanna run on all cores of a system? Set the argument to `'Auto'` — but ⚠️ note that this uses *all* reported cores, even the low-performance efficiency cores, if they're available on the hardware platform and reported by the OS. No optional argument = `--auto-schedule=1`.

- **`--force-preproc-sched=<arg>`** — when autoscheduling is used, makes sure the preprocessing schedule gets inserted in the search categories. 💖

- **`--serialize-schedule=<arg>`** — converts a parallel auto-schedule into a serialized one.

- **`--satauto-schedule[=<arg>]`** — uses strategy scheduling *without* SInE, so it maintains completeness. No optional argument = `--satauto-schedule=1`.

- **`--no-preprocessing`** — doesn't perform preprocessing on the initial clause set. Preprocessing currently removes tautologies and orders terms, literals and clauses in a certain ("canonical") way before anything else happens. And unless it's limited by one of the following options, it'll also unfold equational definitions.

- **`--eq-unfold-limit=<arg>`** — during preprocessing, limits unfolding (and removing) of equational definitions to those where the expanded definition is at most the given limit bigger (in terms of standard weight) than the defined term.

- **`--eq-unfold-maxclauses=<arg>`** — during preprocessing, don't even *try* unfolding equational definitions if the problem has more than this limit of clauses. Know your limits, bestie.

- **`--no-eq-unfolding`** — during preprocessing, abstains from unfolding (and removing) equational definitions.

- **`--goal-defs[=<arg>]`** — introduces Twee-style equational definitions for ground terms in conjecture clauses. The argument can be `None`, `All` or `Neg` — and `Neg` will only consider ground terms from negative literals in the CNF (to be implemented). No optional argument = `--goal-defs=All`.

- **`--goal-subterm-defs`** — introduces goal definitions for *all* conjecture ground subterms. The default is to only introduce them for the maximal (with respect to the subterm relation) ground terms in conjecture clauses (to be implemented).

- **`--sine[=<arg>]`** — applies SInE to prune the unprocessed axioms with the specified filter. `'Auto'` will automatically pick a filter. No optional argument = `--sine=Auto`.

- **`--rel-pruning-level[=<arg>]`** — performs relevancy pruning up to the given level on the unprocessed axioms. No optional argument = `--rel-pruning-level=3`.

- **`--presat-simplify[=<arg>]`** — before proper saturation, does a complete interreduction of the proof state. No optional argument = `--presat-simplify=true`.

- **`--ac-handling[=<arg>]`** — selects the AC handling mode, i.e. decides what to do with redundant AC tautologies. The default is equivalent to `'DiscardAll'`; the other possible values are `'None'` (to disable AC handling), `'KeepUnits'`, and `'KeepOrientable'`. No optional argument = `--ac-handling=KeepUnits`.

- **`--ac-non-aggressive`** — does AC resolution on negative literals *only on processing* (by default, AC resolution is done after clause creation). Only effective if AC handling isn't disabled.

- **`-W <arg>`, `--literal-selection-strategy=<arg>`** — chooses a strategy for selection of negative literals. Two special values live here: `NoSelection` selects no literal (i.e. performs normal superposition) and `NoGeneration` inhibits all generating inferences. For a list of the other (hopefully self-documenting) values, run `eprover -W none`. There are two variants of each strategy — the one prefixed with `'P'` will allow paramodulation into maximal *positive* literals in addition to paramodulation into maximal *selected negative* literals.

- **`--no-generation`** — doesn't perform any generating inferences (equivalent to `--literal-selection-strategy=NoGeneration`).

- **`--select-on-processing-only`** — performs literal selection at processing time only (i.e. selects only in the _given clause_), not before clause evaluation. This matters because many clause selection heuristics give special consideration to maximal or selected literals.

- **`-i`, `--inherit-paramod-literals`** — always selects the negative literals a previous inference paramodulated into (if possible). If there's no such literal, it selects as dictated by the selection strategy.

- **`-j`, `--inherit-goal-pm-literals`** —

Okay so I'm literally mid-sentence from the last part, so let's just pick it up: in a goal (which is an all-negative clause, bestie), **always** select the negative literals that a previous inference paramodulated into — if that's even possible 💅. And if no such literal exists? Then you just select whatever the selection strategy tells you to select. That's it, that's the whole vibe.

- **`--inherit-conjecture-pm-literals`** — same energy as above but for a clause that came from a conjecture: always select the negative literals a previous inference paramodulated into (if possible). And if there's no such literal lying around, fall back to whatever the selection strategy says. No notes ✨

- **`--selection-pos-min=<arg>`** — sets a *lower* limit on how many positive literals a clause has to have before it's even eligible for literal selection. Too few positives? Not invited to the party 🎀

- **`--selection-pos-max=<arg>`** — sets an *upper* limit on how many positive literals a clause can have and still be eligible for literal selection. My girl is not beating the too-many-positives allegations 🙈

- **`--selection-neg-min=<arg>`** — lower limit on the number of **negative** literals a clause must have to be eligible for literal selection.

- **`--selection-neg-max=<arg>`** — upper limit on the number of **negative** literals a clause can have to be eligible for literal selection.

- **`--selection-all-min=<arg>`** — lower limit on the total number of literals (all of them, periodt) a clause must have to be eligible for literal selection.

- **`--selection-all-max=<arg>`** — upper limit on the total number of literals a clause must have to be eligible for literal selection. (Yeah, the original really does say the upper limit is a "must have" — I'm just the messenger 🫶)

- **`--selection-weight-min=<arg>`** — sets the minimum *weight* a clause needs before it's eligible for literal selection.

- **`--prefer-initial-clauses`** — always process all the initial clauses first. First come, first served, main character energy 👑

- **`-x <arg>`**, **`--expert-heuristic=<arg>`** — pick one of the clause selection heuristics. Currently there's at least: `Auto`, `Weight`, `StandardWeight`, `RWeight`, `FIFO`, `LIFO`, `Uniq`, `UseWatchlist`. For the *full* list, go check `HEURISTICS/che_proofcontrol.c` 👀. `Auto` is what you want if you literally just want a proof found — it's special because it also sets some extra options for you. And heads up: for optimal performance you should also pass `-tAuto` so you get a good term ordering. Now the tea:
  - `LIFO` is **unfair** and will make the prover **incomplete** 💀
  - `Uniq` is used internally and is not very useful in most cases.
  - You can define more heuristics yourself with the option `-H` (more on that below).

- **`--filter-orphans-limit[=<arg>]`** — okay so *orphans* are unprocessed clauses where one of the parents got removed by back-simplification. They're redundant and usually get removed lazily (meaning: only when something selects them for processing). With this option you set a limit on back-simplified clauses — once you hit it, orphans get deleted **eagerly** instead. Giving the option with no argument is the same as `--filter-orphans-limit=100`.

- **`--forward-contract-limit[=<arg>]`** — sets a limit on the number of processed clauses; once you pass it, the unprocessed clause set gets re-simplified and reweighted 🔁. No argument? That's the same as `--forward-contract-limit=80000`.

- **`--delete-bad-limit[=<arg>]`** — sets the number of storage units after which bad clauses get deleted with no further consideration. Fair warning: this makes the prover **potentially incomplete** 😭 — but it lets you cap the maximum amount of memory used pretty well. The prover *will* tell you if a proof attempt failed because of the incompleteness this option introduces, so at least it's honest. It's recommended to set this limit significantly higher than `--filter-limit` or `--filter-copies-limit`. And if you pick `-xAuto` and set a memory limit, the prover will figure out a good value for this automatically 💖. No argument means `--delete-bad-limit=1500000`.

- **`--assume-completeness`** — there are various ways (like, say, the next few options) to configure the prover to be *strongly incomplete* in the general case. E will notice when one of those gets selected and return the corresponding exit states (i.e. it will **not** claim satisfiability just because it ran out of unprocessed clauses). But if you *_know_* that for your class of problems the strategy you picked is still complete, use this option to tell the system that's the case. Trust fall 🫶

- **`--assume-incompleteness`** — this one tells the prover to assume incompleteness (typically because the axiomatization already *is* incomplete, since axioms got filtered before they were ever handed to the system).

- **`--disable-eq-factoring`** — disables equality factoring. This makes the prover **incomplete for general non-Horn problems**, but it helps for some specialized classes. And ngl, you don't need to disable equality factoring for Horn problems — Horn clauses aren't factored anyway, so there'd be nothing to turn off 🌸

- **`--disable-paramod-into-neg-units`** — disables paramodulation into negative unit clauses. Makes the prover **incomplete in the general case**, but helps for some specialized classes.

- **`--condense`** — enables condensing for the given clause. Condensing swaps a clause out for a more general factor, if such a factor exists. Glow up ✨

- **`--condense-aggressive`** — enables condensing for the given clause **and** for newly generated clauses. No chill, all condense.

- **`--disable-given-clause-fw-contraction`** — disables simplification and subsumption of the newly selected given clause (clauses still get simplified when they're generated, don't worry). In general this breaks some basic assumptions of the `DISCOUNT` loop proof search procedure 😬. That said, there are some problem classes where this simplification empirically never happens at all — and in those cases you save significant overhead. The option *_should_* work in all cases, but it's not expected to improve things in most cases. So, like, proceed with caution bestie.

- **`--simul-paramod`** — use simultaneous paramodulation to implement superposition. The default is to use plain paramodulation.

- **`--oriented-simul-paramod`** — use simultaneous paramodulation for oriented from-literals. This is an **experimental feature** 🧪 no cap.

- **`--supersimul-paramod`** — use supersimultaneous paramodulation to implement superposition. Again, the default is plain paramodulation.

- **`--oriented-supersimul-paramod`** — use supersimultaneous paramodulation for oriented from-literals. Also an **experimental feature** 🦋

- **`--split-clauses[=<arg>]`** — decides which clauses get subjected to splitting. The argument is the binary `'OR'` of the values for the classes you want:
  - `1`: Horn clauses
  - `2`: Non-Horn clauses
  - `4`: Negative clauses
  - `8`: Positive clauses
  - `16`: Clauses with both positive and negative literals

  Every set bit adds that class to the set of clauses that will be split 🎀. Option with no argument = `--split-clauses=7`.

- **`--split-method=<arg>`** — decides how ground literals get treated when splitting. The argument is either `'0'` for no splitting of ground literals (they all get assigned to the first split clause that's produced), `'1'` meaning all ground literals should form a single new clause, or `'2'`, where ground literals are treated as usual and all get split off into individual clauses.

- **`--split-aggressive`** — apply splitting to new clauses (after simplification) and before evaluation. By default, splitting (if it's activated at all) only happens on selected clauses.

- **`--split-reuse-defs`** — if it's possible, reuse previous definitions for splitting. Recycle, queen ♻️

- **`--disequality-decomposition[=<arg>]`** — enables the disequality decomposition inference. The optional argument is the maximal literal number of clauses considered for the inference. No argument = `--disequality-decomposition=1024`.

- **`--disequality-decomp-maxarity[=<arg>]`** — limits disequality decomposition to function symbols with at most the given arity. No argument = `--disequality-decomp-maxarity=1`.

- **`-t <arg>`**, **`--term-ordering=<arg>`** — select an ordering type (currently `Auto`, `LPO`, `LPO4`, `KBO` or `KBO6`). `-tAuto` is the suggested one, especially alongside `-xAuto` 👑. For the record: `KBO` and `KBO6` are different implementations of the *same* ordering, and `KBO6` is usually faster and has had way more testing. Similarly, `LPO4` is a new, equivalent but superior implementation of `LPO`. Upgrades, we love to see it 💅

- **`-w <arg>`**, **`--order-weight-generation=<arg>`** — select a method for generating weights for use with the term ordering. Wanna see the list of options? Run `eprover -w none` 🏃

- **`--order-weights=<arg>`** — describes a (partial) assignment of weights to function symbols for term orderings (in particular, `KBO`). You can give a list of weights in the form `'f1:w1,f2:w2, ...'`. Since a *total* weight assignment is what's actually needed, E will **first** apply whatever weight generation scheme you specified (or the default one), and *then* modify the weights as you specified. Real talk though: E only performs very basic sanity checks here, so you probably *can* specify weights that break `KBO` constraints 🫠

- **`-G <arg>`**, **`--order-precedence-generation=<arg>`** — select a method for generating a precedence for use with the term ordering. For the list of options, run `eprover -G none`.

- **`--prec-pure-conj[=<arg>]`** — sets a weight for symbols that occur **only in conjectures**, which is used to determine where to place them in the precedence. This value is used for a rough pre-order — the normal schemes only sort *within* symbols that share the same occurrence modifier. No argument = `--prec-pure-conj=10`.

- **`--prec-conj-axiom[=<arg>]`** — sets a weight for symbols that occur in **both conjectures and axioms**, to determine where to place them in the precedence. Same deal: this value is used for a rough pre-order, and the normal schemes only sort within symbols with the same occurrence modifier. No argument = `--prec-conj-axiom=5`.

- **`--prec-pure-axiom[=<arg>]`** — sets a weight for symbols that occur **only in axioms**, to determine where to place them in the precedence. Again: rough pre-order value, and the normal schemes only sort within symbols with the same occurrence modifier. No argument = `--prec-pure-axiom=2`.

- **`--prec-skolem[=<arg>]`**

Set a weight for <hotpink>Skolem symbols</hotpink> so the prover knows where to slot them into the precedence. This value only does a rough pre-order — the normal schemes sort *within* symbols that have the same occurrence modifier. Leave the optional argument off and it's the same as `--prec-skolem=2`. ✨

- **`--prec-defpred[=<arg>]`** — set a weight for the predicate symbols that get introduced (usually through definitional CNF or clause splitting) so the prover knows where to drop them in the precedence. Same energy as above: rough pre-order only, and the normal schemes only sort among symbols sharing the same occurrence modifier. Skip the optional argument and you get `--prec-defpred=2`. 🎀

- **`-c <arg>`**, **`--order-constant-weight=<arg>`** — set a special weight `> 0` for constants in the term ordering. Default vibe is that constants are just regular function symbols like everyone else. 🌸

- **`--precedence[=<arg>]`** — describe a (partial) precedence for the term ordering used in the proof attempt, bestie. You hand it a comma-separated list of precedence chains, and each chain is a list of function symbols (all of which **have** to show up in the proof problem) glued together with `>`, `<`, or `=`. If you pair this with `--order-precedence-generation`, the partial ordering gets completed using whichever method you picked — otherwise the prover runs with a non-ground-total ordering. No optional argument means it's the same as `--precedence=`. 👑

- **`--lpo-recursion-limit[=<arg>]`** — depth limit for LPO comparisons. Most comparisons don't need more than 10 or 20 levels of recursion. By default the recursion depth is capped at `1000` so you don't blow your stack. If the limit is hit, the prover just assumes the terms are uncomparable. Smaller values = faster comparisons but less exact; bigger values = the opposite. Values up to `20000` should be safe on most operating systems. If you're catching segmentation faults while running LPO or LPO4, first try setting this limit to something reasonable. And if the problem *still* persists, send a bug report `;-)`. No optional argument = `--lpo-recursion-limit=100`. 💀

- **`--restrict-literal-comparisons`** — makes every literal uncomparable in the term ordering, i.e. the term ordering is no longer used to restrict paramodulation, equality resolution and factoring to certain literals. This is necessary to make Set-of-Support strategies **complete** for the non-equational case. (It's still incomplete for the equational case, but it's pretty useless anyways.)

- **`--literal-comparison=<arg>`** — change up how literal comparisons happen. `'None'` is the same as the previous option, `'Normal'` uses the normal lifting of the term ordering, `'TFOEqMax'` uses the equivalent of a transfinite ordering that decides on the predicate symbol and makes equational literals maximal (heads up: this setting makes the prover **incomplete** 😭), and `'TFOEqMin'` twists that by making equational symbols minimal.

- **`--sos-uses-input-types`** — if the input is TPTP format, use TPTP conjectures to initialize the Set of Support. If it's not TPTP, use E-LOP queries (clauses shaped like `?-l(X),...,m(Y)`). Normally, all negative clauses get used. Just so you know: most E heuristics don't touch this information at all, and right now it's only useful for certain parameter settings (including the `SimulateSOS` priority function). 🙈

- **`--destructive-er`** — allow destructive equality resolution inferences on pure-variable literals of the form `X!=Y`, meaning the original clause gets replaced by the result of an equality resolution inference on that literal.

- **`--strong-destructive-er`** — allow destructive equality resolution inferences on literals of the form `X!=t` (where `X` does not occur in `t`), i.e. replace the original clause with the result of an equality resolution inference on that literal. Unless the author is brain-dead, this maintains completeness — although the proof is rather tricky. 🧚

- **`--destructive-er-aggressive`** — apply destructive equality resolution to **all** newly generated clauses, not just selected ones. Implies `--destructive-er`.

- **`--forward-context-sr`** — apply contextual simplify-reflect with processed clauses to the given clause.

- **`--forward-context-sr-aggressive`** — apply contextual simplify-reflect with processed clauses to new clauses. Implies `--forward-context-sr`.

- **`--backward-context-sr`** — apply contextual simplify-reflect with the given clause to processed clauses.

- **`-g`**, **`--prefer-general-demodulators`** — prefer general demodulators. Default is that E prefers specialized demodulators. This decides the order in which the rewrite index gets traversed. 🦋

- **`-F <arg>`**, **`--forward-demod-level=<arg>`** — set the desired level for rewriting of unprocessed clauses. `0` means no rewriting, `1` says use rules (orientable equations) only, `2` says full rewriting with rules and instances of unorientable equations. Default behavior is `2`.

- **`--demod-under-lambda=<arg>`** — demodulate **closed** subterms under lambdas.

- **`--strong-rw-inst`** — instantiate unbound variables in matching potential demodulators with a small constant terms.

- **`-u`**, **`--strong-forward-subsumption`** — try multiple positions and unit-equations to equationally subsume a single new clause. Default is to search for a single position.

- **`--satcheck-proc-interval[=<arg>]`** — enable periodic SAT checking every time you hit the given interval of main loop non-trivial processed clauses. No optional argument = `--satcheck-proc-interval=5000`. ⭐

- **`--satcheck-gen-interval[=<arg>]`** — enable periodic SAT checking whenever the total proof state size grows by the given limit. No optional argument = `--satcheck-gen-interval=10000`.

- **`--satcheck-ttinsert-interval[=<arg>]`** — enable periodic SAT checking whenever the number of term tops insertions matches the given limit (which grows exponentially, iconic 💅). No optional argument = `--satcheck-ttinsert-interval=5000000`.

- **`--satcheck[=<arg>]`** — set the grounding strategy for periodic SAT checking. Note that to actually turn SAT checking on, you *also* have to set the interval with one of the interval options above. No optional argument = `--satcheck=FirstConst`.

- **`--satcheck-decision-limit[=<arg>]`** — set how many decisions each run of the SAT solver gets. If you don't pass the option, the built-in value is `10000`. Use `-1` for unlimited decisions. No optional argument = `--satcheck-decision-limit=100`.

- **`--satcheck-normalize-const`** — use the current normal form (as recorded in the termbank rewrite cache) of the selected constant as the term for the grounding substitution.

- **`--satcheck-normalize-unproc`** — enable re-simplification (heuristic re-revaluation) of unprocessed clauses before grounding for SAT checking.

- **`--watchlist[=<arg>]`** — give the name of a file full of clauses to be watched during the saturation process. If a clause gets generated that subsumes a watchlist clause, the subsumed clause gets removed from the watchlist. The prover terminates once the watchlist is empty. If you want the watchlist to *guide* the proof, put the empty clause on the list and use the built-in clause selection heuristic `'UseWatchlist'` (or build your own heuristic with the priority functions `'PreferWatchlist'` and `'DeferWatchlist'`). Use the argument `'Use inline watchlist type'` (or no argument) plus the special clause type `watchlist` if you want to put watchlist clauses into the normal input stream — this is only supported for TPTP input formats. No optional argument = `--watchlist='Use inline watchlist type'`.

- **`--static-watchlist[=<arg>]`** — identical to the previous option, but subsumed clauses are **not** removed from the watchlist (so the prover will not terminate once all watchlist clauses have been subsumed). This may be more useful for heuristic guidance. No optional argument = `--static-watchlist='Use inline watchlist type'`. ⚠️

- **`--no-watchlist-simplification`** — by default, the watchlist is brought into normal form with respect to the current processed clause set and certain simplifications. This option disables simplification for the watchlist. 🍓

- **`--fw-subsumption-aggressive`** — perform forward subsumption on newly generated clauses *before* they get evaluated. Especially useful when heuristic evaluation is very expensive, e.g. through externally connected neural networks. 🔥

- **`--conventional-subsumption`** — equivalent to `--subsumption-indexing=None`.

- **`--subsumption-indexing=<arg>`** — pick the indexing for (most) subsumption operations. Choices are `'None'` for naive subsumption, `'Direct'` for direct mapped FV-Indexing, `'Perm'` for permuted FV-Indexing, and `'PermOpt'` for permuted FV-Indexing with deletion of (suspected) non-informative features. Default behaviour is `'Perm'`.

- **`--fvindex-featuretypes=<arg>`** — select which feature types get used for indexing. Choices are `"None"` to disable FV-indexing, `"AC"` for AC compatible features (literal number and symbol counts — this is the default), `"SS"` for set subsumption compatible features (symbol depth), and `"All"` for all features. Unless you want to measure the effects of the different features, the author suggests you just stick with the default. 🌈

- **`--fvindex-maxfeatures[=<arg>]`**

okay so continuing the option tea, no interruption, we're just gonna keep going 💅

- **`--fvindex-maxfeatures[=<arg>]`** — sets the max initial number of symbols used for feature computation. Depending on which feature selection you rock, a value of X here converts into `2X+2` features (set subsumption features), `2X+4` features (AC-compatible features), or `4X+6` features (if you use all the features, which is the default). Heads up though: the set of features you actually end up using can be *smaller* than that if your signature doesn't have enough symbols in it. And for the `Perm` and `PermOpt` versions, this is <italic>also</italic> what sets the max depth of the feature vector index. Yes, the author says they should probably make this into two separate options, their words not mine 😭. If you pick a small value here, you probs shouldn't use `"Direct"` for the `--subsumption-indexing` option. The option with no optional argument is the same as `--fvindex-maxfeatures=200`.

- **`--fvindex-slack[=<arg>]`** — sets how many slots you reserve in the index for function symbols that might get introduced into the signature later, like when something splits. If no new symbols show up, this just wastes time and memory, sorry bestie. And if `PermOpt` is the chosen one, the slackness slots get deleted from the index anyway, but still waste (a little) time when computing feature vectors. The option with no optional argument is the same as `--fvindex-slack=0`.

- **`--rw-bw-index[=<arg>]`** — picks the fingerprint function for the backwards rewrite index. `"NoIndex"` disables paramodulation indexing. For the full list of other values, go run `eprover --pm-index=none`. `FPX` functions use a fingerprint of X positions, and the letters tell apart different fingerprints that happen to have the same sample size. The option with no optional argument is the same as `--rw-bw-index=FP7`.

- **`--pm-from-index[=<arg>]`** — picks the fingerprint function for the index for paramodulation *from* indexed clauses. `"NoIndex"` disables paramodulation indexing. For a list of the other values, run `eprover --pm-index=none`. `FPX` functions use a fingerprint of X positions, and the letters disambiguate between different fingerprints with the same sample size. The option with no optional argument is the same as `--pm-from-index=FP7`.

- **`--pm-into-index[=<arg>]`** — picks the fingerprint function for the index for paramodulation *into* the indexed clauses. `"NoIndex"` disables paramodulation indexing. For the list of other values, run `eprover --pm-index=none`. `FPX` functions use a fingerprint of X positions, letters disambiguate between fingerprints with the same sample size. The option with no optional argument is the same as `--pm-into-index=FP7`.

- **`--fp-index[=<arg>]`** — picks the fingerprint function for *all* the fingerprint indices. See above 👆. The option with no optional argument is the same as `--fp-index=FP7`.

- **`--fp-no-size-constr`** — turns OFF using size constraints for matching with fingerprint indexing. bye size constraints ✨

- **`--pdt-no-size-constr`** — turns OFF using size constraints for matching with perfect discrimination trees indexing.

- **`--pdt-no-age-constr`** — turns OFF using age constraints for matching with perfect discrimination trees indexing.

- **`--detsort-rw`** — sorts the set of clauses that got eliminated by backward rewriting, using a total syntactic ordering.

- **`--detsort-new`** — sorts the set of newly generated and backward simplified clauses using a total syntactic ordering.

- **`-D <arg>`**, **`--define-weight-function=<arg>`** — define a weight function (check the manual for the details). Later definitions override earlier ones. no pressure 🫶

- **`-H <arg>`**, **`--define-heuristic=<arg>`** — define a clause selection heuristic (the manual has the deets). Later definitions override earlier definitions, periodt.

- **`--free-numbers`** — treats numbers (strings of decimal digits) as normal free function symbols in the input. By default, numbers are now supposed to denote domain constants and to be implicitly different from each other.

- **`--free-objects`** — treats object identifiers (strings inside double quotes) as normal free function symbols in the input. By default, object identifiers now represent domain objects and are implicitly different from each other (and different from numbers too, unless those numbers are declared to be free).

- **`--definitional-cnf[=<arg>]`** — tunes the clausification algorithm so it introduces definitions for subformulae, avoiding exponential blow-up. The optional argument is a fudge factor that decides when definitions get introduced. `0` disables definitions completely. The default works well. The option with no optional argument is the same as `--definitional-cnf=24`.

- **`--fool-unroll=<arg>`** — enable or disable FOOL unrolling. Useful for some SH problems, iykyk.

- **`--miniscope-limit[=<arg>]`** — sets the limit of sub-formula-size to miniscope. The built-in default is `256`. Only applies to the new (default) clausification algorithm. The option with no optional argument is the same as `--miniscope-limit=2147483648`.

- **`--print-types`** — prints the type of every term. useful for debugging, iconic for chaos 👑

- **`--app-encode`** — encodes terms in the proof state using applicative encoding, prints the encoded input problem, and exits.

- **`--arg-cong=<arg>`** — turns on the ArgCong inference rule. Takes an argument `"all"` or `"max"`, which applies the rule to all literals, or only to literals eligible for resolution.

- **`--neg-ext=<arg>`** — turns on the NegExt inference rule. Takes an argument `"all"` or `"max"` that applies the rule to all literals, or only to those eligible for resolution.

- **`--pos-ext=<arg>`** — turns on the PosExt inference rule. Takes an argument `"all"` or `"max"` that applies the rule to all literals, or only to those eligible for resolution.

- **`--ext-sup-max-depth=<arg>`** — sets the maximal proof depth of the clause that will be considered for the Ext-family of inferences. A negative value disables the rule.

- **`--inverse-recognition`** — enables recognition of injective function symbols. If such a symbol gets recognized, the existence of the inverse function is asserted by adding a corresponding axiom.

- **`--replace-inj-defs`** — after CNF and before saturation, replaces all clauses that are definitions of injectivity with the axiomatization of the inverse function.

- **`--lift-lambdas=<arg>`** — should the lambdas be replaced by named functions? 🤔

- **`--eta-normalize=<arg>`** — which form of eta normalization do we perform?

- **`--ho-order-kind=<arg>`** — do we use simple LFHO order, or a more advanced Boolean free lambda-KBO?

- **`--cnf-lambda-to-forall=<arg>`** — do we turn equations of the form `^X.s (!)= ^X.t` into `(?)!X. s (!)= t` ?

- **`--kbo-lam-weight=<arg>`** — weight of the lambda symbol in KBO.

- **`--kbo-db-weight=<arg>`** — weight of the DB var in KBO.

- **`--eliminate-leibniz-eq=<arg>`** — maximal proof depth of the clause on which Leibniz equality elimination should be applied; `-1` disables Leibniz equality elimination altogether.

- **`--unroll-formulas-only=<arg>`** — set to `true` if you want only formulas to be recognized as definitions during CNF. Default is `true`.

- **`--prim-enum-mode=<arg>`** — choose the mode of primitive enumeration.

- **`--prim-enum-max-depth=<arg>`** — maximal proof depth of a clause on which primitive enumeration is applied. `-1` disables primitive enumeration.

- **`--inst-choice-max-depth=<arg>`** — maximal proof depth of a clause that is going to be scanned for occurrences of a defined choice symbol. `-1` disables scanning for choice symbols.

- **`--local-rw=<arg>`** — enable/disable local rewriting: if the clause is of the form `s != t | C`, where `s > t`, rewrite all occurrences of `s` with `t` in `C`.

- **`--prune-args=<arg>`** — enable/disable pruning arguments of applied variables.

- **`--func-proj-limit=<arg>`** — maximal number of functional projections.

- **`--imit-limit=<arg>`** — maximal number of imitations.

- **`--ident-limit=<arg>`** — maximal number of identifications.

- **`--elim-limit=<arg>`** — maximal number of eliminations.

- **`--unif-mode=<arg>`** — set the mode of unification: either `single` or `multi`.

- **`--pattern-oracle=<arg>`** — turn the pattern oracle on or off.

- **`--fixpoint-oracle=<arg>`** — turn the pattern oracle on or off. (yes bestie it literally says pattern oracle again, that's the original's vibe, I'm not touching it 🙈)

- **`--max-unifiers=<arg>`** — maximal number of imitations.

- **`--max-unif-steps=<arg>`** — maximal number of variable bindings that can be done in one single call to computing the next unifier.

- **`--classification-timeout-portion=<arg>`** — which percentage (from `1` to `99`) of the total CPU time gets devoted to problem classification?

- **`--preinstantiate-induction=<arg>`** — abstract unit clauses coming from the conjecture and use the abstractions to instantiate clauses that look like the ones coming from induction axioms.

- **`--bce=<arg>`** — turn blocked clause elimination on or off.

- **`--bce-max-occs=<arg>`** — stop tracking a symbol after it occurs in `<arg>` clauses. Set `<arg>` to `-1` to disable this limit.

- **`--pred-elim=<arg>`** — turn predicate elimination on or off.

- **`--pred-elim-max-occs=<arg>`** — stop tracking a symbol after it occurs in `<arg>` clauses. Set `<arg>` to `-1` to disable this limit.

- **`--pred-elim-tolerance=<arg>`** — tolerance for predicate elimination measures.

- **`--pred-elim-recognize-gates=<arg>`** — turn gate recognition for predicate elimination on or off.

- **`--pred-elim-force-mu-decrease=<arg>`** — require that the square number of distinct free variables decreases when doing predicate elimination. Helps avoid creating huge clauses. (iconic anti-bloat behavior honestly)

- **`--pred-elim-ignore-conj-syms=<arg>`** — disable eliminating symbols that occur in the conjecture.

---

# 💌 REPORTING BUGS 💌

found a bug? spill the tea to `<schulz@eprover.org>`. Please include the following if you possibly can:

1. The version of the package, as reported by `eprover --version`.

2. The operating system and its version.

3. The *exact* command line that leads to the unexpected behaviour.

4. A description of what you expected and what actually happened.

5. If possible, all the input files necessary to reproduce the bug.

# 📜 COPYRIGHT 📜

Okay bestie, gather round, legal-but-make-it-cute time 💖

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

This program is a part of the distribution of the <purple>equational theorem prover E</purple>. You can find the latest version of the E distribution as well as additional information at <cyan>http://www.eprover.org</cyan> ✨

---

## 🫶 the license bit (it's giving freedom)

This program is **free software**; you can redistribute it and/or modify it under the terms of the <green>GNU General Public License</green> as published by the <blue>Free Software Foundation</blue>; either **version 2** of the License, or (at your option) **any later version**. slay 🎀

This program is distributed in the hope that it will be useful, but <red>WITHOUT ANY WARRANTY</red>; without even the implied warranty of <red>MERCHANTABILITY</red> or <red>FITNESS FOR A PARTICULAR PURPOSE</red>. 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:

Free Software Foundation, Inc. 59 Temple Place, Suite 330 Boston, MA 02111-1307 USA

---

## 🐛 bug reports & questions (we actually want them, no cap)

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

- 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 <hotpink>`schulz@eprover.org`</hotpink>. Bug reports with respect to the **HO-version** should be send to or at least copied to <hotpink>`jasmin.blanchette@gmail.com`</hotpink>.

> 🫶 Please remember that this is an <italic>unpaid volunteer service</italic>. Be nice, these people are doing it for the love of the game 💅

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, we made it to the end 🦋🌸 thank you for reading with me — this was **E 3.5.1 Countess Grey** (`facc36e...`), from **August 2026**, and yes she ate, she's iconic, and she's `E(1)` to the very last line 👑💜