-h
--help
- Print a short description of program usage and options.
-V
--version
- Print the version number of the prover. Please include this with all bug
reports (if any).
-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.
-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, 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).
-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 asimple, 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. This feature is under
development, so far only level 0 and 1 are operational. By default The
proof object will be provided in TPTP-3 or LOP syntax, depending on input
format and explicit settings. The following option will suppress normal
output of the proof object in favour of a graphial representation. The
short form or the long form without the optional argument is equivalent to
--proof-object=1.
--proof-statistics
- Print various statistics of the proof object.
--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.
-d
--full-deriv
- Include all derived formuas/clauses in the proof graph/proof object, not
just the ones contributing to the actual proof.
--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.
--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.
--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.
--pcl-terms-compressed
- Print terms in the PCL output in shared representation.
--pcl-compact
- Print PCL steps without additional spaces for formatting (safes disk space
for large protocols).
--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.
--print-statistics
- Print the inference statistics (only relevant for output level <=1,
otherwise they are printed automatically.
-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.
-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.
--print-sat-info
- Print additional information (clause number, weight, etc) as a comment for
clauses from the semi-saturated end system.
--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.
--syntax-only
- Stop after parsing, i.e. only check if the input can be parsed
correcly.
--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').
--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.
--print-pid
- Print the process id of the prover as a comment after option
processing.
--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.
--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.
-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).
--cpu-limit[=<arg>]
- Limit the 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. 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, MacOS-X, and GNU/Linux. 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.
--soft-cpu-limit[=<arg>]
- Limit the cpu time the prover should spend in the main saturation phase.
The prover will then terminate gracefully, i.e. it will perform
post-processing, filtering and printing of unprocessed clauses, if these
options are selected. Note that for some filtering options (in particular
those which perform full subsumption), the post-processing time may well
be larger than the saturation time. This option is particularly useful if
you want to use E as a preprocessor or lemma generator in a larger system.
The option without the optional argument is equivalent to
--soft-cpu-limit=290.
-R
--resources-info
- Give some information about the resources used by the prover. 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.
--print-strategy
- Print a representation of all search parameters and their setting. Then
terminate.
--parse-strategy=<arg>
- Parse the previously printed representation of strategy and set all proof
search parameters accordingly.
-C <arg>
--processed-clauses-limit=<arg>
- Set the maximal number of clauses to process (i.e. the number of
traversals of the main-loop).
-P <arg>
--processed-set-limit=<arg>
- Set the maximal size of the set of processed clauses. This differs from
the previous option in that redundant and back-simplified processed
clauses are not counted.
-U <arg>
--unprocessed-limit=<arg>
- Set the maximal size of the set of unprocessed clauses. This is a
termination condition, not something to use to control the deletion of bad
clauses. Compare --delete-bad-limit.
-T <arg>
--total-clause-set-limit=<arg>
- Set the maximal size of the set of all clauses. See previous option.
--generated-limit=<arg>
- Set the maximal number of generated clauses before the proof search stops.
This is a reasonable (though not great) estimate of the work done.
--tb-insert-limit=<arg>
- Set the maximal number of of term bank term top insertions. This is a
reasonable (though not great) estimate of the work done.
--answers[=<arg>]
- Set the maximal number of answers to print for existentially quantified
questions. Without this option, the prover terminates after the first
answer found. If the value is different from 1, the prover is no longer
guaranteed to terminate, even if there is a finite number of answers. The
option without the optional argument is equivalent to
--answers=2147483647.
--conjectures-are-questions
- Treat all conjectures as questions to be answered. This is a wart
necessary because CASC-J6 has categories requiring answers, but does not
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 non-equational ones.
--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.
--pcl-out
- Set PCL as the proof object output format.
--tptp-in
- Set 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.
--tptp2-in
- Synonymous with --tptp-in.
--tptp2-out
- Synonymous with --tptp-out.
--tptp2-format
- Synonymous with --tptp-format.
--tstp-in
- Set TPTP-3 as the input format (Note that TPTP-3 syntax is still under
development, and the version in E may not be fully conforming at all
times. E works on all TPTP 6.3.0 FOF and CNF files (including
includes).
--tstp-out
- Print output clauses in TPTP-3 syntax. In particular, for output levels
>=2, write 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 determine settings for proof search.
--auto-schedule[=<arg>]
- Use the (experimental) strategy scheduling. This will try 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. Optional argument is the number of CPUs on which the
schedule is going to be executed on. By default, the schedule is executed
on a single core. To execute on all cores of a system set the argument to
'Auto', but note that thiswill use all reported cores (even efficiency
cores, if available). The option without the optional argument is
equivalent to --auto-schedule=1.
--force-preproc-sched=<arg>
- When autoscheduling is used, make sure that preprocessing schedule is
inserted in the search categories
--serialize-schedule=<arg>
- Convert parallel auto-schedule into serialized one.
--satauto-schedule[=<arg>]
- Use strategy scheduling without SInE, thus maintaining completeness. The
option without the optional argument is equivalent to
--satauto-schedule=1.
--no-preprocessing
- Do not 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. Unless
limited by one of the following options, it will also unfold equational
definitions.
--eq-unfold-limit=<arg>
- During preprocessing, limit 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 try unfolding of equational definitions if the
problem has more than this limit of clauses.
--no-eq-unfolding
- During preprocessing, abstain from unfolding (and removing) equational
definitions.
--goal-defs[=<arg>]
- Introduce Twee-style equational definitions for ground terms in conjecture
clauses. The argument can be All or Neg, which will only consider ground
terms from negative literals (to be implemented). The option without the
optional argument is equivalent to --goal-defs=All.
--goal-subterm-defs
- Introduce 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>]
- Apply SInE to prune the unprocessed axioms with the specified filter.
'Auto' will automatically pick a filter. The option without the optional
argument is equivalent to --sine=Auto.
--rel-pruning-level[=<arg>]
- Perform relevancy pruning up to the given level on the unprocessed axioms.
The option without the optional argument is equivalent to
--rel-pruning-level=3.
--presat-simplify
- Before proper saturation do a complete interreduction of the proof
state.
--ac-handling[=<arg>]
- Select AC handling mode, i.e. determine 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'. The option without the optional argument is equivalent
to --ac-handling=KeepUnits.
--ac-non-aggressive
- Do AC resolution on negative literals only on processing (by default, AC
resolution is done after clause creation). Only effective if AC handling
is not disabled.
-W <arg>
--literal-selection-strategy=<arg>
- Choose a strategy for selection of negative literals. There are two
special values for this option: NoSelection will select no literal (i.e.
perform normal superposition) and NoGeneration will inhibit 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
- Don't perform any generating inferences (equivalent to
--literal-selection-strategy=NoGeneration).
--select-on-processing-only
- Perform literal selection at processing time only (i.e. select only in the
_given clause_), not before clause evaluation. This is relevant because
many clause selection heuristics give special consideration to maximal or
selected literals.
-i
--inherit-paramod-literals
- Always select the negative literals a previous inference paramodulated
into (if possible). If no such literal exists, select as dictated by the
selection strategy.
-j
--inherit-goal-pm-literals
- In a goal (all negative clause), always select the negative literals a
previous inference paramodulated into (if possible). If no such literal
exists, select as dictated by the selection strategy.
--inherit-conjecture-pm-literals
- In a conjecture-derived clause, always select the negative literals a
previous inference paramodulated into (if possible). If no such literal
exists, select as dictated by the selection strategy.
--selection-pos-min=<arg>
- Set a lower limit for the number of positive literals a clause must have
to be eligible for literal selection.
--selection-pos-max=<arg>
- Set a upper limit for the number of positive literals a clause can have to
be eligible for literal selection.
--selection-neg-min=<arg>
- Set a lower limit for the number of negative literals a clause must have
to be eligible for literal selection.
--selection-neg-max=<arg>
- Set a upper limit for the number of negative literals a clause can have to
be eligible for literal selection.
--selection-all-min=<arg>
- Set a lower limit for the number of literals a clause must have to be
eligible for literal selection.
--selection-all-max=<arg>
- Set an upper limit for the number of literals a clause must have to be
eligible for literal selection.
--selection-weight-min=<arg>
- Set the minimum weight a clause must have to be eligible for literal
selection.
--prefer-initial-clauses
- Always process all initial clauses first.
-x <arg>
--expert-heuristic=<arg>
- Select one of the clause selection heuristics. Currently at least
available: Auto, Weight, StandardWeight, RWeight, FIFO, LIFO, Uniq,
UseWatchlist. For a full list check HEURISTICS/che_proofcontrol.c. Auto is
recommended if you only want to find a proof. It is special in that it
will also set some additional options. To have optimal performance, you
also should specify -tAuto to select a good term ordering. 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 using the
option -H (see below).
--filter-orphans-limit[=<arg>]
- Orphans are unprocessed clauses where one of the parents has been removed
by back-simolification. They are redundant and usually removed lazily
(i.e. only when they are selected for processing). With this option you
can select a limit on back-simplified clauses after which orphans will be
eagerly deleted. The option without the optional argument is equivalent to
--filter-orphans-limit=100.
--forward-contract-limit[=<arg>]
- Set a limit on the number of processed clauses after which the unprocessed
clause set will be re-simplified and reweighted. The option without the
optional argument is equivalent to
--forward-contract-limit=80000.
--delete-bad-limit[=<arg>]
- Set the number of storage units after which bad clauses are deleted
without further consideration. This causes the prover to be potentially
incomplete, but will allow you to limit the maximum amount of memory used
fairly well. The prover will tell you if a proof attempt failed due to the
incompleteness introduced by this option. It is recommended to set this
limit significantly higher than --filter-limit or
--filter-copies-limit. If you select -xAuto and set a memory
limit, the prover will determine a good value automatically. The option
without the optional argument is equivalent to
--delete-bad-limit=1500000.
--assume-completeness
- There are various way (e.g. the next few options) to configure the prover
to be strongly incomplete in the general case. E will detect when such an
option is selected and return corresponding exit states (i.e. it will not
claim satisfiability just because it ran out of unprocessed clauses). If
you _know_ that for your class of problems the selected strategy is still
complete, use this option to tell the system that this is the case.
--assume-incompleteness
- This option instructs the prover to assume incompleteness (typically
because the axiomatization already is incomplete because axioms have been
filtered before they are handed to the system.
--disable-eq-factoring
- Disable equality factoring. This makes the prover incomplete for general
non-Horn problems, but helps for some specialized classes. It is not
necessary to disable equality factoring for Horn problems, as Horn clauses
are not factored anyways.
--disable-paramod-into-neg-units
- Disable paramodulation into negative unit clause. This makes the prover
incomplete in the general case, but helps for some specialized
classes.
--condense
- Enable condensing for the given clause. Condensing replaces a clause by a
more general factor (if such a factor exists).
--condense-aggressive
- Enable condensing for the given and newly generated clauses.
--disable-given-clause-fw-contraction
- Disable simplification and subsumption of the newly selected given clause
(clauses are still simplified when they are generated). In general, this
breaks some basic assumptions of the DISCOUNT loop proof search procedure.
However, there are some problem classes in which this simplifications
empirically never occurs. In such cases, we can save significant overhead.
The option _should_ work in all cases, but is not expected to improve
things in most cases.
--simul-paramod
- Use simultaneous paramodulation to implement superposition. Default is to
use plain paramodulation.
--oriented-simul-paramod
- Use simultaneous paramodulation for oriented from-literals. This is an
experimental feature.
--supersimul-paramod
- Use supersimultaneous paramodulation to implement superposition. Default
is to use plain paramodulation.
--oriented-supersimul-paramod
- Use supersimultaneous paramodulation for oriented from-literals. This is
an experimental feature.
--split-clauses[=<arg>]
- Determine which clauses should be subject to splitting. The argument is
the binary 'OR' of values for the desired classes:
- 1:
- Horn clauses
- 2:
- Non-Horn clauses
- 4:
- Negative clauses
- 8:
- Positive clauses
- 16:
- Clauses with both positive and negative literals
- Each set bit adds that class to the set of clauses which will be split.
The option without the optional argument is equivalent to
--split-clauses=7.
--split-method=<arg>
- Determine how to treat ground literals in splitting. The argument is
either '0' to denote no splitting of ground literals (they are all
assigned to the first split clause produced), '1' to denote that all
ground literals should form a single new clause, or '2', in which case
ground literals are treated as usual and are all split off into individual
clauses.
--split-aggressive
- Apply splitting to new clauses (after simplification) and before
evaluation. By default, splitting (if activated) is only performed on
selected clauses.
--split-reuse-defs
- If possible, reuse previous definitions for splitting.
-t <arg>
--term-ordering=<arg>
- Select an ordering type (currently Auto, LPO, LPO4, KBO or KBO6).
-tAuto is suggested, in particular with -xAuto. KBO and KBO6
are different implementations of the same ordering, KBO6 is usually faster
and has had more testing. Similarly, LPO4 is a new, equivalent but
superior implementation of LPO.
-w <arg>
--order-weight-generation=<arg>
- Select a method for the generation of weights for use with the term
ordering. Run 'eprover -w none' for a list of options.
--order-weights=<arg>
- Describe a (partial) assignments of weights to function symbols for term
orderings (in particular, KBO). You can specify a list of weights of the
form 'f1:w1,f2:w2, ...'. Since a total weight assignment is needed, E will
_first_ apply any weight generation scheme specified (or the default one),
and then modify the weights as specified. Note that E performs only very
basic sanity checks, so you probably can specify weights that break KBO
constraints.
-G <arg>
--order-precedence-generation=<arg>
- Select a method for the generation of a precedence for use with the term
ordering. Run 'eprover -G none' for a list of options.
--prec-pure-conj[=<arg>]
- Set a weight for symbols that occur in conjectures only to determinewhere
to place it in the precedence. This value is used for a roughpre-order,
the normal schemes only sort within symbols with the sameoccurrence
modifier. The option without the optional argument is equivalent to
--prec-pure-conj=10.
--prec-conj-axiom[=<arg>]
- Set a weight for symbols that occur in both conjectures and axiomsto
determine where to place it in the precedence. This value is used for a
rough pre-order, the normal schemes only sort within symbols with the same
occurrence modifier. The option without the optional argument is
equivalent to --prec-conj-axiom=5.
--prec-pure-axiom[=<arg>]
- Set a weight for symbols that occur in axioms only to determine where to
place it in the precedence. This value is used for a rough pre-order, the
normal schemes only sort within symbols with the same occurrence modifier.
The option without the optional argument is equivalent to
--prec-pure-axiom=2.
--prec-skolem[=<arg>]
- Set a weight for Skolem symbols to determine where to place it in the
precedence. This value is used for a rough pre-order, the normal schemes
only sort within symbols with the same occurrence modifier. The option
without the optional argument is equivalent to
--prec-skolem=2.
--prec-defpred[=<arg>]
- Set a weight for introduced predicate symbols (usually via definitional
CNF or clause splitting) to determine where to place it in the precedence.
This value is used for a rough pre-order, the normal schemes only sort
within symbols with the same occurrence modifier. The option without the
optional argument is equivalent to --prec-defpred=2.
-c <arg>
--order-constant-weight=<arg>
- Set a special weight > 0 for constants in the term ordering. By
default, constants are treated like other function symbols.
--precedence[=<arg>]
- Describe a (partial) precedence for the term ordering used for the proof
attempt. You can specify a comma-separated list of precedence chains,
where a precedence chain is a list of function symbols (which all have to
appear in the proof problem), connected by >, <, or =. If this
option is used in connection with --order-precedence-generation,
the partial ordering will be completed using the selected method,
otherwise the prover runs with a non-ground-total ordering. The option
without the optional argument is equivalent to --precedence=.
--lpo-recursion-limit[=<arg>]
- Set a depth limit for LPO comparisons. Most comparisons do not need more
than 10 or 20 levels of recursion. By default, recursion depth is limited
to 1000 to avoid stack overflow problems. If the limit is reached, the
prover assumes that the terms are uncomparable. Smaller values make the
comparison attempts faster, but less exact. Larger values have the
opposite effect. Values up to 20000 should be save on most operating
systems. If you run into segmentation faults while using LPO or LPO4,
first try to set this limit to a reasonable value. If the problem
persists, send a bug report ;-) The option without the optional argument
is equivalent to --lpo-recursion-limit=100.
--restrict-literal-comparisons
- Make all literals uncomparable in the term ordering (i.e. do not use the
term ordering 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 still
is incomplete for the equational case, but pretty useless anyways).
--literal-comparison=<arg>
- Modify how literal comparisons are done. 'None' is equivalent to the
previous option, 'Normal' uses the normal lifting of the term ordering,
'TFOEqMax' uses the equivalent of a transfinite ordering deciding on the
predicate symbol and making equational literals maximal (note that this
setting makes the prover incomplere), and 'TFOEqMin' modifies this by
making equational symbols minimal.
--sos-uses-input-types
- If input is TPTP format, use TPTP conjectures for initializing the Set of
Support. If not in TPTP format, use E-LOP queries (clauses of the form
?-l(X),...,m(Y)). Normally, all negative clauses are used. Please note
that most E heuristics do not use this information at all, it is currently
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, i.e. replace the original clause with the result of an
equality resolution inference on this 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 this literal. Unless I
am 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 to selected clauses. 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. By default, E prefers specialized
demodulators. This affects in which order the rewrite index is
traversed.
-F <arg>
--forward-demod-level=<arg>
- Set the desired level for rewriting of unprocessed clauses. A value of 0
means no rewriting, 1 indicates to use rules (orientable equations) only,
2 indicates 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 try to equationally subsume a
single new clause. Default is to search for a single position.
--satcheck-proc-interval[=<arg>]
- Enable periodic SAT checking at the given interval of main loop
non-trivial processed clauses. The option without the optional argument is
equivalent to --satcheck-proc-interval=5000.
--satcheck-gen-interval[=<arg>]
- Enable periodic SAT checking whenever the total proof state size increases
by the given limit. The option without the optional argument is equivalent
to --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). The option without
the optional argument is equivalent to
--satcheck-ttinsert-interval=5000000.
--satcheck[=<arg>]
- Set the grounding strategy for periodic SAT checking. Note that to enable
SAT checking, it is also necessary to set the interval with one of the
previous two options. The option without the optional argument is
equivalent to --satcheck=FirstConst.
--satcheck-decision-limit[=<arg>]
- Set the number of decisions allowed for each run of the SAT solver. If the
option is not given, the built-in value is 10000. Use -1 to allow
unlimited decision. The option without the optional argument is equivalent
to --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 for a file containing clauses to be watched for during the
saturation process. If a clause is generated that subsumes a watchlist
clause, the subsumed clause is removed from the watchlist. The prover will
terminate when the watchlist is empty. If you want to use the watchlist
for guiding the proof, put the empty clause onto the list and use the
built-in clause selection heuristic 'UseWatchlist' (or build a heuristic
yourself using the priority functions 'PreferWatchlist' and
'DeferWatchlist'). Use the argument 'Use inline watchlist type' (or no
argument) and 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. The option without the optional argument is equivalent
to --watchlist='Use inline watchlist type'.
--static-watchlist[=<arg>]
- This is identical to the previous option, but subsumed clauses willnot be
removed from the watchlist (and hence the prover will not terminate if all
watchlist clauses have been subsumed. This may be more useful for
heuristic guidance. The option without the optional argument is equivalent
to --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 are
evaluated. This is particularly useful if heuristic evaluation is very
expensive, e.g. via externally connected neural networks.
--conventional-subsumption
- Equivalent to --subsumption-indexing=None.
--subsumption-indexing=<arg>
- Determine choice of 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 the feature types used for indexing. Choices are "None"
to disable FV-indexing, "AC" for AC compatible features (the
default) (literal number and symbol counts), "SS" for set
subsumption compatible features (symbol depth), and "All" for
all features.Unless you want to measure the effects of the different
features, I suggest you stick with the default.
--fvindex-maxfeatures[=<arg>]
- Set the maximum initial number of symbols for feature computation.
Depending on the feature selection, a value of X here will convert into
2X+2 features (for set subsumption features), 2X+4 features (for
AC-compatible features) or 4X+6 features (if all features are used, the
default). Note that the actually used set of features may be smaller than
this if the signature does not contain enough symbols.For the Perm and
PermOpt version, this is _also_ used to set the maximum depth of the
feature vector index. Yes, I should probably make this into two separate
options. If you select a small value here, you should probably not use
"Direct" for the --subsumption-indexing option. The
option without the optional argument is equivalent to
--fvindex-maxfeatures=200.
--fvindex-slack[=<arg>]
- Set the number of slots reserved in the index for function symbols that
may be introduced into the signature later, e.g. by splitting. If no new
symbols are introduced, this just wastes time and memory. If PermOpt is
chosen, the slackness slots will be deleted from the index anyways, but
will still waste (a little) time in computing feature vectors. The option
without the optional argument is equivalent to
--fvindex-slack=0.
--rw-bw-index[=<arg>]
- Select fingerprint function for backwards rewrite index.
"NoIndex" will disable paramodulation indexing. For a list of
the other values run 'eprover --pm-index=none'. FPX
functions will use a fingerprint of X positions, the letters disambiguate
between different fingerprints with the same sample size. The option
without the optional argument is equivalent to
--rw-bw-index=FP7.
--pm-from-index[=<arg>]
- Select fingerprint function for the index for paramodulation from indexed
clauses. "NoIndex" will disable paramodulation indexing. For a
list of the other values run 'eprover --pm-index=none'. FPX
functionswill use a fingerprint of X positions, the letters disambiguate
between different fingerprints with the same sample size. The option
without the optional argument is equivalent to
--pm-from-index=FP7.
--pm-into-index[=<arg>]
- Select fingerprint function for the index for paramodulation into the
indexed clauses. "NoIndex" will disable paramodulation indexing.
For a list of the other values run 'eprover
--pm-index=none'. FPX functionswill use a fingerprint of X
positions, the letters disambiguate between different fingerprints with
the same sample size. The option without the optional argument is
equivalent to --pm-into-index=FP7.
--fp-index[=<arg>]
- Select fingerprint function for all fingerprint indices. See above. The
option without the optional argument is equivalent to
--fp-index=FP7.
--fp-no-size-constr
- Disable usage of size constraints for matching with fingerprint
indexing.
--pdt-no-size-constr
- Disable usage of size constraints for matching with perfect discrimination
trees indexing.
--pdt-no-age-constr
- Disable usage of age constraints for matching with perfect discrimination
trees indexing.
--detsort-rw
- Sort set of clauses eliminated by backward rewriting using a total
syntactic ordering.
--detsort-new
- Sort set of newly generated and backward simplified clauses using a total
syntactic ordering.
-D <arg>
--define-weight-function=<arg>
- Define
- a weight function (see manual for details). Later definitions
- override previous definitions.
-H <arg>
--define-heuristic=<arg>
- Define a clause selection heuristic (see manual for details). Later
definitions override previous definitions.
--free-numbers
- Treat numbers (strings of decimal digits) as normal free function symbols
in the input. By default, number now are supposed to denote domain
constants and to be implicitly different from each other.
--free-objects
- Treat object identifiers (strings in 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
from numbers, unless those are declared to be free).
--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.
--fool-unroll=<arg>
- Enable or disable FOOL unrolling. Useful for some SH problems.
--old-cnf[=<arg>]
- As the previous option, but use the classical, well-tested clausification
algorithm as opposed to the newewst one which avoides some algorithmic
pitfalls and hence works better on some exotic formulae. The two may
produce slightly different (but equisatisfiable) clause normal forms. The
option without the optional argument is equivalent to
--old-cnf=24.
--miniscope-limit[=<arg>]
- Set the limit of sub-formula-size to miniscope. The build-indefault is
256. Only applies to the new (default) clausification algorithm The option
without the optional argument is equivalent to
--miniscope-limit=2147483648.
--print-types
- Print the type of every term. Useful for debugging purposes.
--app-encode
- Encodes terms in the proof state using applicative encoding, prints
encoded input problem and exits.
--arg-cong=<arg>
- Turns on ArgCong inference rule. Excepts an argument "all" or
"max" that applies the rule to all or only literals that are
eligible for resolution.
--neg-ext=<arg>
- Turns on NegExt inference rule. Excepts an argument "all" or
"max" that applies the rule to all or only literals that are
eligible for resolution.
--pos-ext=<arg>
- Turns on PosExt inference rule. Excepts an argument "all" or
"max" that applies the rule to all or only literals that are
eligible for resolution.
--ext-sup-max-depth=<arg>
- Sets the maximal proof depth of the clause which will be considered for
Ext-family of inferences. Negative value disables the rule.
--inverse-recognition
- Enables the recognition of injective function symbols. If such a symbol is
recognized, 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 by axiomatization of inverse function.
--lift-lambdas=<arg>
- Should the lambdas be replaced by named fuctions?
--eta-normalize=<arg>
- Which form of eta normalization to 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 lambda symbol in KBO.
--kbo-db-weight=<arg>
- Weight of DB var in KBO.
--eliminate-leibniz-eq=<arg>
- Maximal proof depth of the clause on which Leibniz equality elimination
should be applied; -1 disaables 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 which is going to be scanned for
occurrences of 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.
--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
copmuting the next unifier.
--classification-timeout-portion=<arg>
- Which percentage (from 1 to 99) of the total CPU time will be devoted to
problem classification?
--preinstantiate-induction=<arg>
- Abstract unit clauses coming from 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 symbol after it occurs in <arg> clauses Set
<arg> to -1 disable this limit
--pred-elim=<arg>
- Turn predicate elimination on or off
--pred-elim-max-occs=<arg>
- Stop tracking symbol after it occurs in <arg> clauses Set
<arg> to -1 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.
--pred-elim-ignore-conj-syms=<arg>
- Disable eliminating symbols that occur in the conjecture.
Copyright 1998-2023 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
The original copyright holder can be contacted via email or as
Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik
Lerchenstrasse 1 70174 Stuttgart Germany