eprover

E(1)                             User Commands                            E(1)



NAME
       E - manual page for E 1.9 Sourenee

SYNOPSIS
       eprover [options] [files]

DESCRIPTION
       E 1.9 "Sourenee"

       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 build a proof object, level 1 will
              build a simple, compact proof object that only contains
              inference rules and dependencies, level 2 will build a proof
              object where inferences are unambiguously described by giving
              inference positions, and level 3 will expand this to a proof
              object where all intermediate results are explicit. This feature
              is under development, so far only level 0 and 1 are operational.
              The short form or the long form without the optional argument is
              equivalent to --proof-object=1.

       --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 TPTP
              clause/formula) or 2 (nodesalso labelled with source/inference
              record. The option without the optional argument is equivalent
              to --proof-graph=2.

       --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
              0, 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
              'eigEIGaA', standing for 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.

       --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.

       -C <arg>

       --processed-clauses-limit=<arg>

              Set the maximal number of clauses to process (i.e. the number of
              traversals of the main-loop).

       --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.

       -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.

       -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.

       --tptp-in

              Parse TPTP-2 format instead of E-LOP (but note that includes are
              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

              Parse TPTP-3 format instead of E-LOP (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 3.0.1 input files
              (including includes).

       --tstp-out

              Print output clauses in TPTP-3 syntax. In particular, for output
              levels >=2, write derivations as TPTP-3 derivations (default is
              PCL).

       --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. This is
              equivalent to -xAuto -tAuto --sine=Auto.

       --satauto

              Automatically determine settings for proof/saturation search.
              This is equivalent to -xAuto -tAuto.

       --autodev

              Automatically determine settings for proof search (development
              version).  This is equivalent to -xAutoDev -tAutoDev
              --sine=Auto.

       --satautodev

              Automatically determine settings for proof/saturation search
              (development version). This is equivalent to -xAutoDev
              -tAutoDev.

       --auto-schedule

              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.

       --satauto-schedule

              Use the (experimental) strategy scheduling without SInE, thus
              maintaining completeness.

       --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.

       --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.

       -j

       --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-limit[=<arg>]

              Set the limit on the number of 'storage units' in the proof
              state, after which the set of unprocessed clauses will be
              filtered against the processed clauses to eliminate redundant
              clauses. As of E 0.7, a 'storage unit' is approximately one
              byte, however, storage is estimated in an abstract way,
              independent of hardware or memory allocation library, and the
              storage estimate is only an approximation. The option without
              the optional argument is equivalent to --filter-limit=1000000.

       --filter-copies-limit[=<arg>]

              Set the number of storage units in new unprocessed clauses after
              which the set of unprocessed clauses will be filtered for
              equivalent copies of clauses (see above). As this operation is
              cheaper, you may want to set this limit lower than
              --filter-limit. The option without the optional argument is
              equivalent to --filter-copies-limit=800000.

       --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. This is an experimental
              feature.

       --oriented-simul-paramod

              Use simultaneous 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.

       --reweight-limit[=<arg>]

              Set the number of new unprocessed clauses after which the set of
              unprocessed clauses will be reevaluated. The option without the
              optional argument is equivalent to --reweight-limit=30000.

       -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
              KBO1 are different implementations of the same ordering, KBO is
              usually faster and has had more testing. Similarly, LPO4 is an
              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.

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

       --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.

       --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.

       --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'.

       --no-watchlist-simplification

              Normally, that watchlist is brought into normal form with
              respect to the current processed clause set and certain
              simplifications. This option disables this behaviour.

       --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.

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 happend.

       * If possible all input files necessary to reproduce the bug.

COPYRIGHT
       Copyright 1998-2014 by Stephan Schulz, schulz@eprover.org

       You can find the latest version of E and 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 as

       Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik
       Rotebuehlplatz 41 70178 Stuttgart Germany



E 1.9 Sourenee                     July 2015                              E(1)