EGROUND(1)

📦
version 3.5.1 · 8 versions
, in ubuntu stonking

🌸 EGROUND(1) — the eground girlie manual 💅

okay so bestie, welcome to EGROUND(1), the user-commands corner of the manual, where we talk about eground — manual page for eground 3.5.1. yes the version number is in the title AND in the body, she contains multitudes. 🎀

✨ SYNOPSIS ✨

eground [options] [files]

like. that's it. that's the whole vibe. [options] and [files], slay. 🦋

💖 DESCRIPTION 💖

hi bestie so this is eground 3.5.1 👑

What she does: you hand her a set of clauses and she figures out whether that set can be grounded — meaning it's either already ground, or it has no non-constant function symbols. (iykyk 🧚)

And if that IS the case? She prints sufficiently many ground instances of the clauses to guarantee that a ground refutation can be found for unsatisfiable clause sets. periodt. 💅

🎀 Options 🎀

okay bestie here's the whole roster, no skips, no cuts, every single one:

  • -h, --help — Prints a short description of program usage and options. the "help me pls" button 🫶
  • --version — Prints the version number of the program. ✨
  • -v, --verbose[=<arg>] — verbose commentary on how the program is doing, printing technical info to stderr. the short form, or the long form with no optional argument, is the same as --verbose=1. hot pink narration mode 💖
  • -o <arg>, --output-file=<arg> — redirects the output into the named file. 📁
  • -s, --silent — same as --output-level=0. shhh 🤫
  • -l <arg>, --output-level=<arg> — picks an output level, and bigger values mean more verbose output. Level 0 produces nearly no output except for the final clauses, level 1 produces minimal additional output. Higher levels are without meaning in eground (I think). 💀
  • --print-statistics — prints a short statistical summary of clauses read and generated. 📊
  • -R, --resources-info — gives some info about the resources the system used. you'll usually get CPU time info. on systems that return more info from the rusage() system call, you'll also get memory consumption info. 🧮
  • --suppress-result — suppress the actual printing of the result, just gives a short message about success. mainly useful for test runs. 🙈
  • --lop-in — sets E-LOP as the input format. if no input format is selected by this option or one of the following ones, E will guess the input format based on the first token. It will almost always correctly recognize TPTP-3, but it may misidentify E-LOP files that use TPTP meta-identifiers as logical symbols. ⚠️
  • --tptp-in — parse TPTP-2 format instead of E-LOP (except includes, which are handles as in TPTP-3, as TPTP-2 include syntax is considered harmful). bestie that's literally what it says 😭
  • --tptp-out — print TPTP-2 format instead of E-LOP. 🖨️
  • --tptp-format — equivalent to --tptp-in and --tptp-out. both at once, icon behavior
  • --tptp2-in — synonymous with --tptp-in.
  • --tptp2-out — synonymous with --tptp-out.
  • --tptp2-format — synonymous with --tptp-format.
  • --tstp-in — parse TPTP-3 format instead of E-LOP. (Note that TPTP-3 syntax is still under development, and the version implemented may not be fully conformant at all times. It works on all TPTP 3.0.1 input files (including includes). 👀
  • --tstp-out — print output clauses in TPTP-3 syntax. ✨
  • --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.
  • -d, --dimacs — print output in the DIMACS format suitable for many propositional provers. 🧩
  • --definitional-cnf[=<arg>] — tunes the clausification algorithm to introduce definitions for subformulae so we avoid 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 without the optional argument is equivalent to --definitional-cnf=24. 🍓
  • --miniscope-limit[=<arg>] — sets the limit of variables to miniscope per input formula. the build-in default is 1000. only applies to the new (default) clausification algorithm. the option without the optional argument is equivalent to --miniscope-limit=2147483648. 🔢
  • --split-tries[=<arg>] — determines the number of tries for splitting. if 0, no splitting is performed. if 1, only variable-disjoint splits are done. otherwise, up to the desired number of variable permutations is tried to find a splitting subset. the option without the optional argument is equivalent to --split-tries=1. 🪓
  • -U, --no-unit-subsumption — does not check if clauses are subsumed by previously encountered unit clauses. 🚫
  • -r, --no-unit-resolution — does not perform forward-unit-resolution on new clauses. 🚫
  • -t, --no-tautology-detection — does not perform tautology deletion on new clauses. 🚫
  • -m <arg>, --memory-limit=<arg> — limits the memory the system may use. the argument is the allowed amount of memory in MB. this option may not work everywhere, due to broken and/or strange behaviour of setrlimit() in some UNIX implementations. it does work under all tested versions of Solaris and GNU/Linux. 💾
  • --cpu-limit[=<arg>] — limits the cpu time the program should run. the optional argument is the CPU time in seconds. the program will terminate immediately after reaching the time limit, regardless of internal state. this option may not work everywhere, due to broken and/or strange behaviour of setrlimit() in some UNIX implementations. It does work under all tested versions of Solaris, HP-UX and GNU/Linux. as a side effect, this option will inhibit core file writing. the option without the optional argument is equivalent to --cpu-limit=300. ⏰
  • --soft-cpu-limit[=<arg>] — limits the cpu time spend in grounding. after the time expires, the prover will print an partial system. the option without the optional argument is equivalent to --soft-cpu-limit=310. 🕰️
  • -i, --add-one-instance — if the grounding procedure runs out of time or memory, tries to add at least one instance of each clause to the set. this might fail for really large clause sets, since the reserve memory kept for this purpose may be insufficient. 😬
  • -g <arg>, --give-up=<arg> — gives up early if the problem is unlikely to be reasonably small. if run without constraints, the program will give up if the clause with the largest number of instances will be expanded into more than this number of instances. if run with constraints, the program keeps a running count and will terminate if the estimated total number of clauses would exceed this value. a value of 0 will leave this test disabled. 🏳️
  • -c, --constraints — uses global purity constraints to restrict the number of instantiations done. 🔒
  • -C, --local-constraints — uses local purity constraints to further restrict the number of instantiations done. implies the previous option. Not yet implemented! Note to self: Split clauses need to get fresh variables if this is to work! 🙃
  • -M, --fix-minisat — fixes the preamble to include only the maximum variable index, to compensate for MiniSAT's problematic interpretation of the DIMAC syntax. 🛠️

😤 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 bestie please actually include these, it's giving "help me help you" 🫶

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, bestie.)

The original copyright holder can be contacted via email or as

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

okay that's the whole page bestie, you ate that 💅✨

this version of the page is eground 3.5.1, dated August 2026, and it lives in the manual under the name EGROUND(1). k bye 🦋💖🌸
📦 where this page comes from