eground 3.2.5
Read a set of clauses and determine if it can be grounded (i.e. is either already ground or has no
non-constant function symbols). If this is the case, print sufficiently many ground instances of the
clauses to guarantee that a ground refutation can be found for unsatisfiable clause sets.
Options
-h--help
Print a short description of program usage and options.
--version
Print the version number of the program.
-v--verbose[=<arg>]
Verbose comments on the progress of the program by printing technical information to stderr. 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.
-s--silent
Equivalent to --output-level=0.
-l <arg>
--output-level=<arg>
Select an output level, greater values imply 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
Print a short statistical summary of clauses read and generated.
-R--resources-info
Give some information about the resources used by the system. You will usually get CPU time
information. On systems returning more information with the rusage() system call, you will also
get information about memory consumption.
--suppress-result
Suppress actual printing of the result, just give a short message about success. Useful mainly for
test runs.
--lop-in
Set E-LOP as the input format. If no input format is selected by this or one of the following
options, 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).
--tptp-out
Print TPTP-2 format instead of E-LOP.
--tptp-format
Equivalent to --tptp-in and --tptp-out.
--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>]
Tune the clausification algorithm to introduces definitions for subformulae to avoid exponential
blow-up. The optional argument is a fudge factor that determines when definitions are introduced.
0 disables definitions completely. The default works well. The option without the optional
argument is equivalent to --definitional-cnf=24.
--miniscope-limit[=<arg>]
Set 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>]
Determine 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
Do not check if clauses are subsumed by previously encountered unit clauses.
-r--no-unit-resolution
Do not perform forward-unit-resolution on new clauses.
-t--no-tautology-detection
Do not perform tautology deletion on new clauses.
-m <arg>
--memory-limit=<arg>
Limit 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>]
Limit 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>]
Limit 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, try 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>
Give 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
Use global purity constraints to restrict the number of instantiations done.
-C--local-constraints
Use 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
Fix the preamble to include only the maximum variable index, to compensate for MiniSAT's
problematic interpretation of the DIMAC syntax.
Install Now
PNG Icons