Provided by: eprover_3.0.03+ds-1_amd64 
NAME
E - manual page for E 3.0.03-DEBUG Shangri-La (c4e0c2473db4601a3316eb3ecf2bd50ab810f10a)
SYNOPSIS
eprover [options] [files]
DESCRIPTION
E 3.0.03-DEBUG "Shangri-La"
Read a set of first-order clauses and formulae and try to refute it.
OPTIONS
-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.
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.
COPYRIGHT
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
E 3.0.03-DEBUG Shangri-La (c4e0c2473db4601Decembere2023d50ab810f10a) E(1)