1E(1) User Commands E(1)
2
6 E - manual page for E 2.3-DEBUG Gielle
7
9 eprover [options] [files]
10
12 E 2.3-DEBUG "Gielle"
13 Read a set of first-order clauses and formulae and try to refute it.
15
17 -h
18 --help
20 Print a short description of program usage and options.
22 -V
24 --version
26 Print the version number of the prover. Please include this with
28 all bug reports (if any).
29 -v
31 --verbose[=<arg>]
33 Verbose comments on the progress of the program. This differs
35 from the output level (below) in that technical information is
36 printed to stderr, while the output level determines which logi‐
37 cal manipulations of the clauses are printed to stdout. The
38 short form or the long form without the optional argument is
39 equivalent to --verbose=1.
40 -o <arg>
42 --output-file=<arg>
44 Redirect output into the named file.
46 -s
48 --silent
50 Equivalent to --output-level=0.
52 -l <arg>
54 --output-level=<arg>
56 Select an output level, greater values imply more verbose out‐
58 put. Level 0 produces nearly no output, level 1 will output each
59 clause as it is processed, level 2 will output generating infer‐
60 ences, level 3 will give a full protocol including rewrite steps
61 and level 4 will include some internal clause renamings. Levels
62 >= 2 also imply PCL2 or TSTP formats (which can be post-pro‐
63 cessed with suitable tools).
64 -p
66 --proof-object[=<arg>]
68 Generate (and print, in case of success) an internal proof
70 object. Level 0 will not build a proof object, level 1 will
71 build a simple, compact proof object that only contains infer‐
72 ence rules and dependencies, level 2 will build a proof object
73 where inferences are unambiguously described by giving inference
74 positions, and level 3 will expand this to a proof object where
75 all intermediate results are explicit. This feature is under
76 development, so far only level 0 and 1 are operational. The
77 short form or the long form without the optional argument is
78 equivalent to --proof-object=1.
79 --proof-graph[=<arg>]
81 Generate (and print, in case of success) an internal proof
83 object in the form of a GraphViz dot graph. The optional argu‐
84 ment can be 1 (nodes are labelled with just name of the clause),
85 2 (nodes are labelled with just the TPTP clause/formula) or 3
86 (nodes also labelled with source/inference record. The option
87 without the optional argument is equivalent to --proof-graph=3.
88 -d
90 --full-deriv
92 Include all derived formuas/clauses in the proof graph/proof
94 object, not just the ones contributing to the actual proof.
95 --force-deriv[=<arg>]
97 Force output of the derivation even in cases where the prover
99 terminates in an indeterminate state. By default, the derivia‐
100 tion of all processed clauses is included in the derivation
101 object. With value 2, derivation of all clauses will be printed
102 The option without the optional argument is equivalent to
103 --force-deriv=1.
104 --record-gcs
106 Record given-clause selection as separate (pseudo-)inferences
108 and preserve the form of given clauses evaluated and selected
109 via archiving for analysis and possibly machine learning.
110 --training-examples[=<arg>]
112 Generate and process training examples from the proof search
114 object. Implies --record-gcs. The argument is a binary or of
115 the desired processig. Bit zero prints positive exampels. Bit 1
116 prints negative examples. Additional selectors will be added
117 later. The option without the optional argument is equivalent to
118 --training-examples=1.
119 --pcl-terms-compressed
121 Print terms in the PCL output in shared representation.
123 --pcl-compact
125 Print PCL steps without additional spaces for formatting (safes
127 disk space for large protocols).
128 --pcl-shell-level[=<arg>]
130 Determines level to which clauses and formulas are suppressed in
132 the output. Level 0 will print all, level 1 will only print ini‐
133 tial clauses/formulas, level 2 will print no clauses or axioms.
134 All levels will still print the dependency graph. The option
135 without the optional argument is equivalent to
136 --pcl-shell-level=1.
137 --print-statistics
139 Print the inference statistics (only relevant for output level
141 0, otherwise they are printed automatically.
142 -0
144 --print-detailed-statistics
146 Print data about the proof state that is potentially expensive
148 to collect. Includes number of term cells and number of rewrite
149 steps.
150 -S
152 --print-saturated[=<arg>]
154 Print the (semi-) saturated clause sets after terminating the
156 saturation process. The argument given describes which parts
157 should be printed in which order. Legal characters are
158 'teigEIGaA', standing for type declarations, processed positive
159 units, processed negative units, processed non-units, unpro‐
160 cessed positive units, unprocessed negative units, unprocessed
161 non-units, and two types of additional equality axioms, respec‐
162 tively. Equality axioms will only be printed if the original
163 specification contained real equality. In this case, 'a'
164 requests axioms in which a separate substitutivity axiom is
165 given for each argument position of a function or predicate sym‐
166 bol, while 'A' requests a single substitutivity axiom (covering
167 all positions) for each symbol. The short form or the long form
168 without the optional argument is equivalent to --print-satu‐
169 rated=eigEIG.
170 --print-sat-info
172 Print additional information (clause number, weight, etc) as a
174 comment for clauses from the semi-saturated end system.
175 --filter-saturated[=<arg>]
177 Filter the
179 (semi-) saturated clause sets after terminating the
180 saturation process. The argument is a string describing which
182 operations to take (and in which order). Options are 'u' (remove
183 all clauses with more than one literal), 'c' (delete all but one
184 copy of identical clauses, 'n', 'r', 'f' (forward contraction,
185 unit-subsumption only, no rewriting, rewriting with rules only,
186 full rewriting, respectively), and 'N', 'R' and 'F' (as their
187 lower case counterparts, but with non-unit-subsumption enabled
188 as well). The option without the optional argument is equivalent
189 to --filter-saturated=Fc.
190 --prune
192 Stop after relevancy pruning, SInE pruning, and output of the
194 initial clause- and formula set. This will automatically set
195 output level to 4 so that the pruned problem specification is
196 printed. Note that the desired pruning methods must still be
197 specified (e.g. '--sine=Auto').
198 --cnf
200 Convert the input problem into clause normal form and print it.
202 This is (nearly) equivalent to '--print-saturated=eigEIG --pro‐
203 cessed-clauses-limit=0' and will by default perform some usually
204 useful simplifications. You can additionally specify e.g.
205 '--no-preprocessing' if you want just the result of CNF transla‐
206 tion.
207 --print-pid
209 Print the process id of the prover as a comment after option
211 processing.
212 --print-version
214 Print the version number of the prover as a comment after option
216 processing. Note that unlike -version, the prover will not ter‐
217 minate, but proceed normally.
218 --error-on-empty
220 Return with an error code if the input file contains no clauses.
222 Formally, the empty clause set (as an empty conjunction of
223 clauses) is trivially satisfiable, and E will treat any empty
224 input set as satisfiable. However, in composite systems this is
225 more often a sign that something went wrong. Use this option to
226 catch such bugs.
227 -m <arg>
229 --memory-limit=<arg>
231 Limit the memory the prover may use. The argument is the allowed
233 amount of memory in MB. If you use the argument 'Auto', the sys‐
234 tem will try to figure out the amount of physical memory of your
235 machine and claim most of it. This option may not work every‐
236 where, due to broken and/or strange behaviour of setrlimit() in
237 some UNIX implementations, and due to the fact that I know of no
238 portable way to figure out the physical memory in a machine.
239 Both the option and the 'Auto' version do work under all tested
240 versions of Solaris and GNU/Linux. Due to problems with limit
241 data types, it is currently impossible to set a limit of more
242 than 2 GB (2048 MB).
243 --cpu-limit[=<arg>]
245 Limit the cpu time the prover should run. The optional argument
247 is the CPU time in seconds. The prover will terminate immedi‐
248 ately after reaching the time limit, regardless of internal
249 state. This option may not work everywhere, due to broken and/or
250 strange behaviour of setrlimit() in some UNIX implementations.
251 It does work under all tested versions of Solaris, HP-UX, Mac‐
252 OS-X, and GNU/Linux. As a side effect, this option will inhibit
253 core file writing. Please note that if you use both --cpu-limit
254 and --soft-cpu-limit, the soft limit has to be smaller than the
255 hard limit to have any effect. The option without the optional
256 argument is equivalent to --cpu-limit=300.
257 --soft-cpu-limit[=<arg>]
259 Limit the cpu time the prover should spend in the main satura‐
261 tion phase. The prover will then terminate gracefully, i.e. it
262 will perform post-processing, filtering and printing of unpro‐
263 cessed clauses, if these options are selected. Note that for
264 some filtering options (in particular those which perform full
265 subsumption), the post-processing time may well be larger than
266 the saturation time. This option is particularly useful if you
267 want to use E as a preprocessor or lemma generator in a larger
268 system. The option without the optional argument is equivalent
269 to --soft-cpu-limit=290.
270 -R
272 --resources-info
274 Give some information about the resources used by the prover.
276 You will usually get CPU time information. On systems returning
277 more information with the rusage() system call, you will also
278 get information about memory consumption.
279 -C <arg>
281 --processed-clauses-limit=<arg>
283 Set the maximal number of clauses to process (i.e. the number of
285 traversals of the main-loop).
286 -P <arg>
288 --processed-set-limit=<arg>
290 Set the maximal size of the set of processed clauses. This dif‐
292 fers from the previous option in that redundant and back-simpli‐
293 fied processed clauses are not counted.
294 -U <arg>
296 --unprocessed-limit=<arg>
298 Set the maximal size of the set of unprocessed clauses. This is
300 a termination condition, not something to use to control the
301 deletion of bad clauses. Compare --delete-bad-limit.
302 -T <arg>
304 --total-clause-set-limit=<arg>
306 Set the maximal size of the set of all clauses. See previous
308 option.
309 --generated-limit=<arg>
311 Set the maximal number of generated clauses before the proof
313 search stops. This is a reasonable (though not great) estimate
314 of the work done.
315 --tb-insert-limit=<arg>
317 Set the maximal number of of term bank term top insertions. This
319 is a reasonable (though not great) estimate of the work done.
320 --answers[=<arg>]
322 Set the maximal number of answers to print for existentially
324 quantified questions. Without this option, the prover terminates
325 after the first answer found. If the value is different from 1,
326 the prover is no longer guaranteed to terminate, even if there
327 is a finite number of answers. The option without the optional
328 argument is equivalent to --answers=2147483647.
329 --conjectures-are-questions
331 Treat all conjectures as questions to be answered. This is a
333 wart necessary because CASC-J6 has categories requiring answers,
334 but does not yet support the 'question' type for formulas.
335 -n
337 --eqn-no-infix
339 In LOP, print equations in prefix notation equal(x,y).
341 -e
343 --full-equational-rep
345 In LOP. print all literals as equations, even non-equational
347 ones.
348 --lop-in
350 Set E-LOP as the input format. If no input format is selected by
352 this or one of the following options, E will guess the input
353 format based on the first token. It will almost always correctly
354 recognize TPTP-3, but it may misidentify E-LOP files that use
355 TPTP meta-identifiers as logical symbols.
356 --pcl-out
358 Set PCL as the proof object output format.
360 --tptp-in
362 Set TPTP-2 as the input format (but note that includes are still
364 handled according to TPTP-3 semantics).
365 --tptp-out
367 Print TPTP format instead of E-LOP. Implies --eqn-no-infix and
369 will ignore --full-equational-rep.
370 --tptp-format
372 Equivalent to --tptp-in and --tptp-out.
374 --tptp2-in
376 Synonymous with --tptp-in.
378 --tptp2-out
380 Synonymous with --tptp-out.
382 --tptp2-format
384 Synonymous with --tptp-format.
386 --tstp-in
388 Set TPTP-3 as the input format (Note that TPTP-3 syntax is still
390 under development, and the version in E may not be fully con‐
391 forming at all times. E works on all TPTP 6.3.0 FOF and CNF
392 files (including includes).
393 --tstp-out
395 Print output clauses in TPTP-3 syntax. In particular, for output
397 levels >=2, write derivations as TPTP-3 derivations.
398 --tstp-format
400 Equivalent to --tstp-in and --tstp-out.
402 --tptp3-in
404 Synonymous with --tstp-in.
406 --tptp3-out
408 Synonymous with --tstp-out.
410 --tptp3-format
412 Synonymous with --tstp-format.
414 --auto
416 Automatically determine settings for proof search. This is
418 equivalent to -xAuto -tAuto --sine=Auto.
419 --satauto
421 Automatically determine settings for proof/saturation search.
423 This is equivalent to -xAuto -tAuto.
424 --autodev
426 Automatically determine settings for proof search (development
428 version). This is equivalent to -xAutoDev -tAutoDev
429 --sine=Auto.
430 --satautodev
432 Automatically determine settings for proof/saturation search
434 (development version). This is equivalent to -xAutoDev -tAu‐
435 toDev.
436 --auto-schedule
438 Use the (experimental) strategy scheduling. This will try sev‐
440 eral different fully specified search strategies (aka
441 "Auto-Modes"), one after the other, until a proof or saturation
442 is found, or the time limit is exceeded.
443 --satauto-schedule
445 Use the (experimental) strategy scheduling without SInE, thus
447 maintaining completeness.
448 --no-preprocessing
450 Do not perform preprocessing on the initial clause set. Prepro‐
452 cessing currently removes tautologies and orders terms, literals
453 and clauses in a certain ("canonical") way before anything else
454 happens. Unless limited by one of the following options, it will
455 also unfold equational definitions.
456 --eq-unfold-limit=<arg>
458 During preprocessing, limit unfolding (and removing) of equa‐
460 tional definitions to those where the expanded definition is at
461 most the given limit bigger (in terms of standard weight) than
462 the defined term.
463 --eq-unfold-maxclauses=<arg>
465 During preprocessing, don't try unfolding of equational defini‐
467 tions if the problem has more than this limit of clauses.
468 --no-eq-unfolding
470 During preprocessing, abstain from unfolding (and removing)
472 equational definitions.
473 --sine[=<arg>]
475 Apply SInE to prune the unprocessed axioms with the specified
477 filter. 'Auto' will automatically pick a filter. The option
478 without the optional argument is equivalent to --sine=Auto.
479 --rel-pruning-level[=<arg>]
481 Perform relevancy pruning up to the given level on the unpro‐
483 cessed axioms. The option without the optional argument is
484 equivalent to --rel-pruning-level=3.
485 --presat-simplify
487 Before proper saturation do a complete interreduction of the
489 proof state.
490 --ac-handling[=<arg>]
492 Select AC handling mode, i.e. determine what to do with redun‐
494 dant AC tautologies. The default is equivalent to 'DiscardAll',
495 the other possible values are 'None' (to disable AC handling),
496 'KeepUnits', and 'KeepOrientable'. The option without the
497 optional argument is equivalent to --ac-handling=KeepUnits.
498 --ac-non-aggressive
500 Do AC resolution on negative literals only on processing (by
502 default, AC resolution is done after clause creation). Only
503 effective if AC handling is not disabled.
504 -W <arg>
506 --literal-selection-strategy=<arg>
508 Choose a strategy for selection of negative literals. There are
510 two special values for this option: NoSelection will select no
511 literal (i.e. perform normal superposition) and NoGeneration
512 will inhibit all generating inferences. For a list of the other
513 (hopefully self-documenting) values run 'eprover -W none'. There
514 are two variants of each strategy. The one prefixed with 'P'
515 will allow paramodulation into maximal positive literals in
516 addition to paramodulation into maximal selected negative liter‐
517 als.
518 --no-generation
520 Don't perform any generating inferences (equivalent to --lit‐
522 eral-selection-strategy=NoGeneration).
523 --select-on-processing-only
525 Perform literal selection at processing time only (i.e. select
527 only in the _given clause_), not before clause evaluation. This
528 is relevant because many clause selection heuristics give spe‐
529 cial consideration to maximal or selected literals.
530 -i
532 --inherit-paramod-literals
534 Always select the negative literals a previous inference
536 paramodulated into (if possible). If no such literal exists,
537 select as dictated by the selection strategy.
538 -j
540 --inherit-goal-pm-literals
542 In a goal (all negative clause), always select the negative lit‐
544 erals a previous inference paramodulated into (if possible). If
545 no such literal exists, select as dictated by the selection
546 strategy.
547 --inherit-conjecture-pm-literals
549 In a conjecture-derived clause, always select the negative lit‐
551 erals a previous inference paramodulated into (if possible). If
552 no such literal exists, select as dictated by the selection
553 strategy.
554 --selection-pos-min=<arg>
556 Set a lower limit for the number of positive literals a clause
558 must have to be eligible for literal selection.
559 --selection-pos-max=<arg>
561 Set a upper limit for the number of positive literals a clause
563 can have to be eligible for literal selection.
564 --selection-neg-min=<arg>
566 Set a lower limit for the number of negative literals a clause
568 must have to be eligible for literal selection.
569 --selection-neg-max=<arg>
571 Set a upper limit for the number of negative literals a clause
573 can have to be eligible for literal selection.
574 --selection-all-min=<arg>
576 Set a lower limit for the number of literals a clause must have
578 to be eligible for literal selection.
579 --selection-all-max=<arg>
581 Set an upper limit for the number of literals a clause must have
583 to be eligible for literal selection.
584 --selection-weight-min=<arg>
586 Set the minimum weight a clause must have to be eligible for
588 literal selection.
589 --prefer-initial-clauses
591 Always process all initial clauses first.
593 -x <arg>
595 --expert-heuristic=<arg>
597 Select one of the clause selection heuristics. Currently at
599 least available: Auto, Weight, StandardWeight, RWeight, FIFO,
600 LIFO, Uniq, UseWatchlist. For a full list check HEURIS‐
601 TICS/che_proofcontrol.c. Auto is recommended if you only want to
602 find a proof. It is special in that it will also set some addi‐
603 tional options. To have optimal performance, you also should
604 specify -tAuto to select a good term ordering. LIFO is unfair
605 and will make the prover incomplete. Uniq is used internally and
606 is not very useful in most cases. You can define more heuristics
607 using the option -H (see below).
608 --filter-orphans-limit[=<arg>]
610 Orphans are unprocessed clauses where one of the parents has
612 been removed by back-simolification. They are redundant and usu‐
613 ally removed lazily (i.e. only when they are selected for pro‐
614 cessing). With this option you can select a limit on back-sim‐
615 plified clauses after which orphans will be eagerly deleted.
616 The option without the optional argument is equivalent to --fil‐
617 ter-orphans-limit=100.
618 --forward-contract-limit[=<arg>]
620 Set a limit on the number of processed clauses after which the
622 unprocessed clause set will be re-simplified and reweighted.
623 The option without the optional argument is equivalent to --for‐
624 ward-contract-limit=80000.
625 --delete-bad-limit[=<arg>]
627 Set the number of storage units after which bad clauses are
629 deleted without further consideration. This causes the prover to
630 be potentially incomplete, but will allow you to limit the maxi‐
631 mum amount of memory used fairly well. The prover will tell you
632 if a proof attempt failed due to the incompleteness introduced
633 by this option. It is recommended to set this limit signifi‐
634 cantly higher than --filter-limit or --filter-copies-limit. If
635 you select -xAuto and set a memory limit, the prover will deter‐
636 mine a good value automatically. The option without the optional
637 argument is equivalent to --delete-bad-limit=1500000.
638 --assume-completeness
640 There are various way (e.g. the next few options) to configure
642 the prover to be strongly incomplete in the general case. E will
643 detect when such an option is selected and return corresponding
644 exit states (i.e. it will not claim satisfiability just because
645 it ran out of unprocessed clauses). If you _know_ that for your
646 class of problems the selected strategy is still complete, use
647 this option to tell the system that this is the case.
648 --assume-incompleteness
650 This option instructs the prover to assume incompleteness (typi‐
652 cally because the axiomatization already is incomplete because
653 axioms have been filtered before they are handed to the system.
654 --disable-eq-factoring
656 Disable equality factoring. This makes the prover incomplete for
658 general non-Horn problems, but helps for some specialized
659 classes. It is not necessary to disable equality factoring for
660 Horn problems, as Horn clauses are not factored anyways.
661 --disable-paramod-into-neg-units
663 Disable paramodulation into negative unit clause. This makes the
665 prover incomplete in the general case, but helps for some spe‐
666 cialized classes.
667 --condense
669 Enable condensing for the given clause. Condensing replaces a
671 clause by a more general factor (if such a factor exists).
672 --condense-aggressive
674 Enable condensing for the given and newly generated clauses.
676 --disable-given-clause-fw-contraction
678 Disable simplification and subsumption of the newly selected
680 given clause (clauses are still simplified when they are gener‐
681 ated). In general, this breaks some basic assumptions of the
682 DISCOUNT loop proof search procedure. However, there are some
683 problem classes in which this simplifications empirically never
684 occurs. In such cases, we can save significant overhead. The
685 option _should_ work in all cases, but is not expected to
686 improve things in most cases.
687 --simul-paramod
689 Use simultaneous paramodulation to implement superposition.
691 Default is to use plain paramodulation.
692 --oriented-simul-paramod
694 Use simultaneous paramodulation for oriented from-literals. This
696 is an experimental feature.
697 --split-clauses[=<arg>]
699 Determine which clauses should be subject to splitting. The
701 argument is the binary 'OR' of values for the desired classes:
702 1: Horn clauses
704 2: Non-Horn clauses
706 4: Negative clauses
708 8: Positive clauses
710 16: Clauses with both positive and negative literals
712 Each set bit adds that class to the set of clauses which will be
714 split. The option without the optional argument is equivalent
715 to --split-clauses=7.
716 --split-method=<arg>
718 Determine how to treat ground literals in splitting. The argu‐
720 ment is either '0' to denote no splitting of ground literals
721 (they are all assigned to the first split clause produced), '1'
722 to denote that all ground literals should form a single new
723 clause, or '2', in which case ground literals are treated as
724 usual and are all split off into individual clauses.
725 --split-aggressive
727 Apply splitting to new clauses (after simplification) and before
729 evaluation. By default, splitting (if activated) is only per‐
730 formed on selected clauses.
731 --split-reuse-defs
733 If possible, reuse previous definitions for splitting.
735 -t <arg>
737 --term-ordering=<arg>
739 Select an ordering type (currently Auto, LPO, LPO4, KBO or
741 KBO6). -tAuto is suggested, in particular with -xAuto. KBO and
742 KBO6 are different implementations of the same ordering, KBO6 is
743 usually faster and has had more testing. Similarly, LPO4 is a
744 new, equivalent but superior implementation of LPO.
745 -w <arg>
747 --order-weight-generation=<arg>
749 Select a method for the generation of weights for use with the
751 term ordering. Run 'eprover -w none' for a list of options.
752 --order-weights=<arg>
754 Describe a (partial) assignments of weights to function symbols
756 for term orderings (in particular, KBO). You can specify a list
757 of weights of the form 'f1:w1,f2:w2, ...'. Since a total weight
758 assignment is needed, E will _first_ apply any weight generation
759 scheme specified (or the default one), and then modify the
760 weights as specified. Note that E performs only very basic san‐
761 ity checks, so you probably can specify weights that break KBO
762 constraints.
763 -G <arg>
765 --order-precedence-generation=<arg>
767 Select a method for the generation of a precedence for use with
769 the term ordering. Run 'eprover -G none' for a list of options.
770 -c <arg>
772 --order-constant-weight=<arg>
774 Set a special weight > 0 for constants in the term ordering. By
776 default, constants are treated like other function symbols.
777 --precedence[=<arg>]
779 Describe a (partial) precedence for the term ordering used for
781 the proof attempt. You can specify a comma-separated list of
782 precedence chains, where a precedence chain is a list of func‐
783 tion symbols (which all have to appear in the proof problem),
784 connected by >, <, or =. If this option is used in connection
785 with --order-precedence-generation, the partial ordering will be
786 completed using the selected method, otherwise the prover runs
787 with a non-ground-total ordering. The option without the
788 optional argument is equivalent to --precedence=.
789 --lpo-recursion-limit[=<arg>]
791 Set a depth limit for LPO comparisons. Most comparisons do not
793 need more than 10 or 20 levels of recursion. By default, recur‐
794 sion depth is limited to 1000 to avoid stack overflow problems.
795 If the limit is reached, the prover assumes that the terms are
796 uncomparable. Smaller values make the comparison attempts
797 faster, but less exact. Larger values have the opposite effect.
798 Values up to 20000 should be save on most operating systems. If
799 you run into segmentation faults while using LPO or LPO4, first
800 try to set this limit to a reasonable value. If the problem per‐
801 sists, send a bug report ;-) The option without the optional
802 argument is equivalent to --lpo-recursion-limit=100.
803 --restrict-literal-comparisons
805 Make all literals uncomparable in the term ordering (i.e. do not
807 use the term ordering to restrict paramodulation, equality reso‐
808 lution and factoring to certain literals. This is necessary to
809 make Set-of-Support-strategies complete for the non-equational
810 case (It still is incomplete for the equational case, but pretty
811 useless anyways).
812 --sos-uses-input-types
814 If input is TPTP format, use TPTP conjectures for initializing
816 the Set of Support. If not in TPTP format, use E-LOP queries
817 (clauses of the form ?-l(X),...,m(Y)). Normally, all negative
818 clauses are used. Please note that most E heuristics do not use
819 this information at all, it is currently only useful for certain
820 parameter settings (including the SimulateSOS priority func‐
821 tion).
822 --destructive-er
824 Allow destructive equality resolution inferences on pure-vari‐
826 able literals of the form X!=Y, i.e. replace the original clause
827 with the result of an equality resolution inference on this lit‐
828 eral.
829 --strong-destructive-er
831 Allow destructive equality resolution inferences on literals of
833 the form X!=t (where X does not occur in t), i.e. replace the
834 original clause with the result of an equality resolution infer‐
835 ence on this literal. Unless I am brain-dead, this maintains
836 completeness, although the proof is rather tricky.
837 --destructive-er-aggressive
839 Apply destructive equality resolution to all newly generated
841 clauses, not just to selected clauses. Implies --destructive-er.
842 --forward-context-sr
844 Apply contextual simplify-reflect with processed clauses to the
846 given clause.
847 --forward-context-sr-aggressive
849 Apply contextual simplify-reflect with processed clauses to new
851 clauses. Implies --forward-context-sr.
852 --backward-context-sr
854 Apply contextual simplify-reflect with the given clause to pro‐
856 cessed clauses.
857 -g
859 --prefer-general-demodulators
861 Prefer general demodulators. By default, E prefers specialized
863 demodulators. This affects in which order the rewrite index is
864 traversed.
865 -F <arg>
867 --forward-demod-level=<arg>
869 Set the desired level for rewriting of unprocessed clauses. A
871 value of 0 means no rewriting, 1 indicates to use rules (ori‐
872 entable equations) only, 2 indicates full rewriting with rules
873 and instances of unorientable equations. Default behavior is 2.
874 --strong-rw-inst
876 Instantiate unbound variables in matching potential demodulators
878 with a small constant terms.
879 -u
881 --strong-forward-subsumption
883 Try multiple positions and unit-equations to try to equationally
885 subsume a single new clause. Default is to search for a single
886 position.
887 --satcheck-proc-interval[=<arg>]
889 Enable periodic SAT checking at the given interval of main loop
891 non-trivial processed clauses. The option without the optional
892 argument is equivalent to --satcheck-proc-interval=5000.
893 --satcheck-gen-interval[=<arg>]
895 Enable periodic SAT checking whenever the total proof state size
897 increases by the given limit. The option without the optional
898 argument is equivalent to --satcheck-gen-interval=10000.
899 --satcheck-ttinsert-interval[=<arg>]
901 Enable periodic SAT checking whenever the number of term tops
903 insertions matches the given limit (which grows exponentially).
904 The option without the optional argument is equivalent to
905 --satcheck-ttinsert-interval=5000000.
906 --satcheck[=<arg>]
908 Set the grounding strategy for periodic SAT checking. Note that
910 to enable SAT checking, it is also necessary to set the interval
911 with one of the previous two options. The option without the
912 optional argument is equivalent to --satcheck=FirstConst.
913 --satcheck-decision-limit[=<arg>]
915 Set the number of decisions allowed for each run of the SAT
917 solver. If the option is not given, the built-in value is 10000.
918 Use -1 to allow unlimited decision. The option without the
919 optional argument is equivalent to --satcheck-deci‐
920 sion-limit=100.
921 --satcheck-normalize-const
923 Use the current normal form (as recorded in the termbank rewrite
925 cache) of the selected constant as the term for the grounding
926 substitution.
927 --satcheck-normalize-unproc
929 Enable re-simplification (heuristic re-revaluation) of unpro‐
931 cessed clauses before grounding for SAT checking.
932 --watchlist[=<arg>]
934 Give the name for a file containing clauses to be watched for
936 during the saturation process. If a clause is generated that
937 subsumes a watchlist clause, the subsumed clause is removed from
938 the watchlist. The prover will terminate when the watchlist is
939 empty. If you want to use the watchlist for guiding the proof,
940 put the empty clause onto the list and use the built-in clause
941 selection heuristic 'UseWatchlist' (or build a heuristic your‐
942 self using the priority functions 'PreferWatchlist' and 'Defer‐
943 Watchlist'). Use the argument 'Use inline watchlist type' (or no
944 argument) and the special clause type 'watchlist' if you want to
945 put watchlist clauses into the normal input stream. This is only
946 supported for TPTP input formats. The option without the
947 optional argument is equivalent to --watchlist='Use inline
948 watchlist type'.
949 --static-watchlist[=<arg>]
951 This is identical to the previous option, but subsumed clauses
953 willnot be removed from the watchlist (and hence the prover will
954 not terminate if all watchlist clauses have been subsumed. This
955 may be more useful for heuristic guidance. The option without
956 the optional argument is equivalent to --static-watchlist='Use
957 inline watchlist type'.
958 --no-watchlist-simplification
960 By default, the watchlist is brought into normal form with
962 respect to the current processed clause set and certain simpli‐
963 fications. This option disables simplification for the watch‐
964 list.
965 --conventional-subsumption
967 Equivalent to --subsumption-indexing=None.
969 --subsumption-indexing=<arg>
971 Determine choice of indexing for (most) subsumption operations.
973 Choices are 'None' for naive subsumption, 'Direct' for direct
974 mapped FV-Indexing, 'Perm' for permuted FV-Indexing and 'Per‐
975 mOpt' for permuted FV-Indexing with deletion of (suspected)
976 non-informative features. Default behaviour is 'Perm'.
977 --fvindex-featuretypes=<arg>
979 Select the feature types used for indexing. Choices are "None"
981 to disable FV-indexing, "AC" for AC compatible features (the
982 default) (literal number and symbol counts), "SS" for set sub‐
983 sumption compatible features (symbol depth), and "All" for all
984 features.Unless you want to measure the effects of the different
985 features, I suggest you stick with the default.
986 --fvindex-maxfeatures[=<arg>]
988 Set the maximum initial number of symbols for feature computa‐
990 tion. Depending on the feature selection, a value of X here
991 will convert into 2X+2 features (for set subsumption features),
992 2X+4 features (for AC-compatible features) or 4X+6 features (if
993 all features are used, the default). Note that the actually used
994 set of features may be smaller than this if the signature does
995 not contain enough symbols.For the Perm and PermOpt version,
996 this is _also_ used to set the maximum depth of the feature vec‐
997 tor index. Yes, I should probably make this into two separate
998 options. If you select a small value here, you should probably
999 not use "Direct" for the --subsumption-indexing option. The
1000 option without the optional argument is equivalent to --fvin‐
1001 dex-maxfeatures=200.
1002 --fvindex-slack[=<arg>]
1004 Set the number of slots reserved in the index for function sym‐
1006 bols that may be introduced into the signature later, e.g. by
1007 splitting. If no new symbols are introduced, this just wastes
1008 time and memory. If PermOpt is chosen, the slackness slots will
1009 be deleted from the index anyways, but will still waste (a lit‐
1010 tle) time in computing feature vectors. The option without the
1011 optional argument is equivalent to --fvindex-slack=0.
1012 --rw-bw-index[=<arg>]
1014 Select fingerprint function for backwards rewrite index. "NoIn‐
1016 dex" will disable paramodulation indexing. For a list of the
1017 other values run 'eprover --pm-index=none'. FPX functions will
1018 use a fingerprint of X positions, the letters disambiguate
1019 between different fingerprints with the same sample size. The
1020 option without the optional argument is equivalent to
1021 --rw-bw-index=FP7.
1022 --pm-from-index[=<arg>]
1024 Select fingerprint function for the index for paramodulation
1026 from indexed clauses. "NoIndex" will disable paramodulation
1027 indexing. For a list of the other values run 'eprover
1028 --pm-index=none'. FPX functionswill use a fingerprint of X posi‐
1029 tions, the letters disambiguate between different fingerprints
1030 with the same sample size. The option without the optional argu‐
1031 ment is equivalent to --pm-from-index=FP7.
1032 --pm-into-index[=<arg>]
1034 Select fingerprint function for the index for paramodulation
1036 into the indexed clauses. "NoIndex" will disable paramodulation
1037 indexing. For a list of the other values run 'eprover
1038 --pm-index=none'. FPX functionswill use a fingerprint of X posi‐
1039 tions, the letters disambiguate between different fingerprints
1040 with the same sample size. The option without the optional argu‐
1041 ment is equivalent to --pm-into-index=FP7.
1042 --fp-index[=<arg>]
1044 Select fingerprint function for all fingerprint indices. See
1046 above. The option without the optional argument is equivalent to
1047 --fp-index=FP7.
1048 --fp-no-size-constr
1050 Disable usage of size constraints for matching with fingerprint
1052 indexing.
1053 --pdt-no-size-constr
1055 Disable usage of size constraints for matching with perfect dis‐
1057 crimination trees indexing.
1058 --pdt-no-age-constr
1060 Disable usage of age constraints for matching with perfect dis‐
1062 crimination trees indexing.
1063 --detsort-rw
1065 Sort set of clauses eliminated by backward rewriting using a
1067 total syntactic ordering.
1068 --detsort-new
1070 Sort set of newly generated and backward simplified clauses
1072 using a total syntactic ordering.
1073 -D <arg>
1075 --define-weight-function=<arg>
1077 Define
1079 a weight function (see manual for details). Later definitions
1080 override previous definitions.
1082 -H <arg>
1084 --define-heuristic=<arg>
1086 Define a clause selection heuristic (see manual for details).
1088 Later definitions override previous definitions.
1089 --free-numbers
1091 Treat numbers (strings of decimal digits) as normal free func‐
1093 tion symbols in the input. By default, number now are supposed
1094 to denote domain constants and to be implicitly different from
1095 each other.
1096 --free-objects
1098 Treat object identifiers (strings in double quotes) as normal
1100 free function symbols in the input. By default, object identi‐
1101 fiers now represent domain objects and are implicitly different
1102 from each other (and from numbers, unless those are declared to
1103 be free).
1104 --definitional-cnf[=<arg>]
1106 Tune the clausification algorithm to introduces definitions for
1108 subformulae to avoid exponential blow-up. The optional argument
1109 is a fudge factor that determines when definitions are intro‐
1110 duced. 0 disables definitions completely. The default works
1111 well. The option without the optional argument is equivalent to
1112 --definitional-cnf=24.
1113 --old-cnf[=<arg>]
1115 As the previous option, but use the classical, well-tested
1117 clausification algorithm as opposed to the newewst one which
1118 avoides some algorithmic pitfalls and hence works better on some
1119 exotic formulae. The two may produce slightly different (but
1120 equisatisfiable) clause normal forms. The option without the
1121 optional argument is equivalent to --old-cnf=24.
1122 --miniscope-limit[=<arg>]
1124 Set the limit of sub-formula-size to miniscope. The build-inde‐
1126 fault is 256. Only applies to the new (default) clausification
1127 algorithm The option without the optional argument is equivalent
1128 to --miniscope-limit=2147483648.
1129 --print-types
1131 Print the type of every term. Useful for debugging purposes.
1133 --app-encode
1135 Encodes terms in the proof state using applicative encoding,
1137 prints encoded input problem and exits.
1138
1140 Report bugs to <schulz@eprover.org>. Please include the following, if
1141 possible:
1142 * The version of the package as reported by eprover --version.
1144 * The operating system and version.
1146 * The exact command line that leads to the unexpected behaviour.
1148 * A description of what you expected and what actually happend.
1150 * If possible all input files necessary to reproduce the bug.
1152
1154 Copyright 1998-2019 by Stephan Schulz, schulz@eprover.org, and the E
1155 contributors (see DOC/CONTRIBUTORS).
1156 This program is a part of the distribution of the equational theorem
1158 prover E. You can find the latest version of the E distribution as well
1159 as additional information at http://www.eprover.org
1160 This program is free software; you can redistribute it and/or modify it
1162 under the terms of the GNU General Public License as published by the
1163 Free Software Foundation; either version 2 of the License, or (at your
1164 option) any later version.
1165 This program is distributed in the hope that it will be useful, but
1167 WITHOUT ANY WARRANTY; without even the implied warranty of MER‐
1168 CHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
1169 Public License for more details.
1170 You should have received a copy of the GNU General Public License along
1172 with this program (it should be contained in the top level directory of
1173 the distribution in the file COPYING); if not, write to the Free Soft‐
1174 ware Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
1175 02111-1307 USA
1176 The original copyright holder can be contacted via email or as
1178 Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Rote‐
1180 buehlplatz 41 70178 Stuttgart Germany
1181E 2.3-DEBUG Gielle April 2019 E(1)