Man Linux: Main Page and Category List

NAME

       E - The Equational Theorem Prover User Manual

SYNOPSIS

       eprover [options] [files]
       eproof [options] [files]

DESCRIPTION

       E 1.0-004 "Temi"

       eprover  reads  a  set of first-order clauses and formulae and tries to
       refute it.

       eproof is a wrapper script that calls eprover and then runs epclextract
       on its output to construct a proof.

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

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

       --print-statistics

              Print the inference statistics (only relevant for  output  level
              0, otherwise they are printed automatically.

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

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

       --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 datatypes, 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  postprocessing 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).

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

       --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 the next option is set, it will
              also unfold equational definitions.

       --no-eq-unfolding

              During preprocessing,  abstain  from  unfolding  (and  removing)
              equational definitions.

       --ac-handling[=<arg>]

              Select  AC  handling  mode.  Preselected  is ’DiscardAll’, other
              options 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.

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

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

       --simplify-with-unprocessed-units[=<arg>]

              Determine  whether  to  use   unprocessed   unit   clauses   for
              simplify-reflect  (unit-cutting)  and unit subsumption. Possible
              values are ’NoSimplify’ for strict DISCOUNT loop,  ’TopSimplify’
              to   use   unprocessed   units   at   the  top  level  only,  or
              ’FullSimplify’ to use positive units even within equations.  The
              option   without   the   optional   argument  is  equivalent  to
              --simplify-with-unprocessed-units=TopSimplify.

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

              Use  the  new  clausification algorithm that possibly introduces
              definitions for subformulas to avoid exponential  blow-up.  This
              is  now  the  default.   The optional argument is a fudge factor
              that determines when a  definition  is  introduced.  0  disables
              definitions,  the  default  works  well.  The option without the
              optional argument is equivalent to --definitional-cnf=24.

AUTHOR

       Stephan Schulz <schulz@eprover.org>

COPYRIGHT

       Copyright 1998-2006 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 (I4)
       Technische Universitaet Muenchen
       Institut fuer Informatik
       Boltzmannstrasse 3
       85748 Garching bei Muenchen
       Germany

SEE ALSO

       eground(1), epclextract(1),
       PDF  manual  /usr/share/doc/eprover/eprover.pdf.gz  for a more detailed
       description.