1E(1) User Commands E(1)
2
6 E - manual page for E 2.6-DEBUG Floral Guranse
7 (ab0ade87bb070b853105f79bf59e8fc27f915b4f)
8
10 eprover [options] [files]
11
13 E 2.6-DEBUG "Floral Guranse"
14 Read a set of first-order clauses and formulae and try to refute it.
16
18 -h
19 --help
21 Print a short description of program usage and options.
23 -V
25 --version
27 Print the version number of the prover. Please include this with
29 all bug reports (if any).
30 -v
32 --verbose[=<arg>]
34 Verbose comments on the progress of the program. This differs
36 from the output level (below) in that technical information is
37 printed to stderr, while the output level determines which logi‐
38 cal manipulations of the clauses are printed to stdout. The
39 short form or the long form without the optional argument is
40 equivalent to --verbose=1.
41 -o <arg>
43 --output-file=<arg>
45 Redirect output into the named file.
47 -s
49 --silent
51 Equivalent to --output-level=0.
53 -l <arg>
55 --output-level=<arg>
57 Select an output level, greater values imply more verbose out‐
59 put. Level 0 produces nearly no output, level 1 will output each
60 clause as it is processed, level 2 will output generating infer‐
61 ences, level 3 will give a full protocol including rewrite steps
62 and level 4 will include some internal clause renamings. Levels
63 >= 2 also imply PCL2 or TSTP formats (which can be post-pro‐
64 cessed with suitable tools).
65 -p
67 --proof-object[=<arg>]
69 Generate (and print, in case of success) an internal proof ob‐
71 ject. Level 0 will not print a proof object, level 1 will build
72 asimple, compact proof object that only contains inference rules
73 and dependencies, level 2 will build a proof object where infer‐
74 ences are unambiguously described by giving inference positions,
75 and level 3 will expand this to a proof object where all inter‐
76 mediate results are explicit. This feature is under development,
77 so far only level 0 and 1 are operational. By default The proof
78 object will be provided in TPTP-3 or LOP syntax, depending on
79 input format and explicit settings. The following option will
80 suppress normal output of the proof object in favour of a
81 graphial representation. The short form or the long form without
82 the optional argument is equivalent to --proof-object=1.
83 --proof-graph[=<arg>]
85 Generate (and print, in case of success) an internal proof ob‐
87 ject in the form of a GraphViz dot graph. The optional argument
88 can be 1 (nodes are labelled with just the name of the
89 clause/formula), 2 (nodes are labelled with the TPTP clause/for‐
90 mula) or 3 (nodes also labelled with source/inference record.
91 The option without the optional argument is equivalent to
92 --proof-graph=3.
93 -d
95 --full-deriv
97 Include all derived formuas/clauses in the proof graph/proof ob‐
99 ject, not just the ones contributing to the actual proof.
100 --force-deriv[=<arg>]
102 Force output of the derivation even in cases where the prover
104 terminates in an indeterminate state. By default, the derivia‐
105 tion of all processed clauses is included in the derivation ob‐
106 ject. With value 2, derivation of all clauses will be printed
107 The option without the optional argument is equivalent to
108 --force-deriv=1.
109 --record-gcs
111 Record given-clause selection as separate (pseudo-)inferences
113 and preserve the form of given clauses evaluated and selected
114 via archiving for analysis and possibly machine learning.
115 --training-examples[=<arg>]
117 Generate and process training examples from the proof search ob‐
119 ject. Implies --record-gcs. The argument is a binary or of the
120 desired processig. Bit zero prints positive exampels. Bit 1
121 prints negative examples. Additional selectors will be added
122 later. The option without the optional argument is equivalent to
123 --training-examples=1.
124 --pcl-terms-compressed
126 Print terms in the PCL output in shared representation.
128 --pcl-compact
130 Print PCL steps without additional spaces for formatting (safes
132 disk space for large protocols).
133 --pcl-shell-level[=<arg>]
135 Determines level to which clauses and formulas are suppressed in
137 the output. Level 0 will print all, level 1 will only print ini‐
138 tial clauses/formulas, level 2 will print no clauses or axioms.
139 All levels will still print the dependency graph. The option
140 without the optional argument is equivalent to
141 --pcl-shell-level=1.
142 --print-statistics
144 Print the inference statistics (only relevant for output level
146 0, otherwise they are printed automatically.
147 -0
149 --print-detailed-statistics
151 Print data about the proof state that is potentially expensive
153 to collect. Includes number of term cells and number of rewrite
154 steps.
155 -S
157 --print-saturated[=<arg>]
159 Print the (semi-) saturated clause sets after terminating the
161 saturation process. The argument given describes which parts
162 should be printed in which order. Legal characters are
163 'teigEIGaA', standing for type declarations, processed positive
164 units, processed negative units, processed non-units, unpro‐
165 cessed positive units, unprocessed negative units, unprocessed
166 non-units, and two types of additional equality axioms, respec‐
167 tively. Equality axioms will only be printed if the original
168 specification contained real equality. In this case, 'a' re‐
169 quests axioms in which a separate substitutivity axiom is given
170 for each argument position of a function or predicate symbol,
171 while 'A' requests a single substitutivity axiom (covering all
172 positions) for each symbol. The short form or the long form
173 without the optional argument is equivalent to --print-satu‐
174 rated=eigEIG.
175 --print-sat-info
177 Print additional information (clause number, weight, etc) as a
179 comment for clauses from the semi-saturated end system.
180 --filter-saturated[=<arg>]
182 Filter the
184 (semi-) saturated clause sets after terminating the
185 saturation process. The argument is a string describing which
187 operations to take (and in which order). Options are 'u' (remove
188 all clauses with more than one literal), 'c' (delete all but one
189 copy of identical clauses, 'n', 'r', 'f' (forward contraction,
190 unit-subsumption only, no rewriting, rewriting with rules only,
191 full rewriting, respectively), and 'N', 'R' and 'F' (as their
192 lower case counterparts, but with non-unit-subsumption enabled
193 as well). The option without the optional argument is equivalent
194 to --filter-saturated=Fc.
195 --prune
197 Stop after relevancy pruning, SInE pruning, and output of the
199 initial clause- and formula set. This will automatically set
200 output level to 4 so that the pruned problem specification is
201 printed. Note that the desired pruning methods must still be
202 specified (e.g. '--sine=Auto').
203 --cnf
205 Convert the input problem into clause normal form and print it.
207 This is (nearly) equivalent to '--print-saturated=eigEIG --pro‐
208 cessed-clauses-limit=0' and will by default perform some usually
209 useful simplifications. You can additionally specify e.g.
210 '--no-preprocessing' if you want just the result of CNF transla‐
211 tion.
212 --print-pid
214 Print the process id of the prover as a comment after option
216 processing.
217 --print-version
219 Print the version number of the prover as a comment after option
221 processing. Note that unlike -version, the prover will not ter‐
222 minate, but proceed normally.
223 --error-on-empty
225 Return with an error code if the input file contains no clauses.
227 Formally, the empty clause set (as an empty conjunction of
228 clauses) is trivially satisfiable, and E will treat any empty
229 input set as satisfiable. However, in composite systems this is
230 more often a sign that something went wrong. Use this option to
231 catch such bugs.
232 -m <arg>
234 --memory-limit=<arg>
236 Limit the memory the prover may use. The argument is the allowed
238 amount of memory in MB. If you use the argument 'Auto', the sys‐
239 tem will try to figure out the amount of physical memory of your
240 machine and claim most of it. This option may not work every‐
241 where, due to broken and/or strange behaviour of setrlimit() in
242 some UNIX implementations, and due to the fact that I know of no
243 portable way to figure out the physical memory in a machine.
244 Both the option and the 'Auto' version do work under all tested
245 versions of Solaris and GNU/Linux. Due to problems with limit
246 data types, it is currently impossible to set a limit of more
247 than 2 GB (2048 MB).
248 --cpu-limit[=<arg>]
250 Limit the cpu time the prover should run. The optional argument
252 is the CPU time in seconds. The prover will terminate immedi‐
253 ately after reaching the time limit, regardless of internal
254 state. This option may not work everywhere, due to broken and/or
255 strange behaviour of setrlimit() in some UNIX implementations.
256 It does work under all tested versions of Solaris, HP-UX,
257 MacOS-X, and GNU/Linux. As a side effect, this option will in‐
258 hibit core file writing. Please note that if you use both
259 --cpu-limit and --soft-cpu-limit, the soft limit has to be
260 smaller than the hard limit to have any effect. The option
261 without the optional argument is equivalent to --cpu-limit=300.
262 --soft-cpu-limit[=<arg>]
264 Limit the cpu time the prover should spend in the main satura‐
266 tion phase. The prover will then terminate gracefully, i.e. it
267 will perform post-processing, filtering and printing of unpro‐
268 cessed clauses, if these options are selected. Note that for
269 some filtering options (in particular those which perform full
270 subsumption), the post-processing time may well be larger than
271 the saturation time. This option is particularly useful if you
272 want to use E as a preprocessor or lemma generator in a larger
273 system. The option without the optional argument is equivalent
274 to --soft-cpu-limit=290.
275 -R
277 --resources-info
279 Give some information about the resources used by the prover.
281 You will usually get CPU time information. On systems returning
282 more information with the rusage() system call, you will also
283 get information about memory consumption.
284 --print-strategy
286 Print a representation of all search parameters and their set‐
288 ting. Then terminate.
289 -C <arg>
291 --processed-clauses-limit=<arg>
293 Set the maximal number of clauses to process (i.e. the number of
295 traversals of the main-loop).
296 -P <arg>
298 --processed-set-limit=<arg>
300 Set the maximal size of the set of processed clauses. This dif‐
302 fers from the previous option in that redundant and back-simpli‐
303 fied processed clauses are not counted.
304 -U <arg>
306 --unprocessed-limit=<arg>
308 Set the maximal size of the set of unprocessed clauses. This is
310 a termination condition, not something to use to control the
311 deletion of bad clauses. Compare --delete-bad-limit.
312 -T <arg>
314 --total-clause-set-limit=<arg>
316 Set the maximal size of the set of all clauses. See previous op‐
318 tion.
319 --generated-limit=<arg>
321 Set the maximal number of generated clauses before the proof
323 search stops. This is a reasonable (though not great) estimate
324 of the work done.
325 --tb-insert-limit=<arg>
327 Set the maximal number of of term bank term top insertions. This
329 is a reasonable (though not great) estimate of the work done.
330 --answers[=<arg>]
332 Set the maximal number of answers to print for existentially
334 quantified questions. Without this option, the prover terminates
335 after the first answer found. If the value is different from 1,
336 the prover is no longer guaranteed to terminate, even if there
337 is a finite number of answers. The option without the optional
338 argument is equivalent to --answers=2147483647.
339 --conjectures-are-questions
341 Treat all conjectures as questions to be answered. This is a
343 wart necessary because CASC-J6 has categories requiring answers,
344 but does not yet support the 'question' type for formulas.
345 -n
347 --eqn-no-infix
349 In LOP, print equations in prefix notation equal(x,y).
351 -e
353 --full-equational-rep
355 In LOP. print all literals as equations, even non-equational
357 ones.
358 --lop-in
360 Set E-LOP as the input format. If no input format is selected by
362 this or one of the following options, E will guess the input
363 format based on the first token. It will almost always correctly
364 recognize TPTP-3, but it may misidentify E-LOP files that use
365 TPTP meta-identifiers as logical symbols.
366 --pcl-out
368 Set PCL as the proof object output format.
370 --tptp-in
372 Set TPTP-2 as the input format (but note that includes are still
374 handled according to TPTP-3 semantics).
375 --tptp-out
377 Print TPTP format instead of E-LOP. Implies --eqn-no-infix and
379 will ignore --full-equational-rep.
380 --tptp-format
382 Equivalent to --tptp-in and --tptp-out.
384 --tptp2-in
386 Synonymous with --tptp-in.
388 --tptp2-out
390 Synonymous with --tptp-out.
392 --tptp2-format
394 Synonymous with --tptp-format.
396 --tstp-in
398 Set TPTP-3 as the input format (Note that TPTP-3 syntax is still
400 under development, and the version in E may not be fully con‐
401 forming at all times. E works on all TPTP 6.3.0 FOF and CNF
402 files (including includes).
403 --tstp-out
405 Print output clauses in TPTP-3 syntax. In particular, for output
407 levels >=2, write derivations as TPTP-3 derivations.
408 --tstp-format
410 Equivalent to --tstp-in and --tstp-out.
412 --tptp3-in
414 Synonymous with --tstp-in.
416 --tptp3-out
418 Synonymous with --tstp-out.
420 --tptp3-format
422 Synonymous with --tstp-format.
424 --auto
426 Automatically determine settings for proof search. This is
428 equivalent to -xAuto -tAuto --sine=Auto.
429 --satauto
431 Automatically determine settings for proof/saturation search.
433 This is equivalent to -xAuto -tAuto.
434 --autodev
436 Automatically determine settings for proof search (development
438 version). This is equivalent to -xAutoDev -tAutoDev
439 --sine=Auto.
440 --satautodev
442 Automatically determine settings for proof/saturation search
444 (development version). This is equivalent to -xAutoDev -tAu‐
445 toDev.
446 --auto-schedule
448 Use the (experimental) strategy scheduling. This will try sev‐
450 eral different fully specified search strategies (aka
451 "Auto-Modes"), one after the other, until a proof or saturation
452 is found, or the time limit is exceeded.
453 --satauto-schedule
455 Use the (experimental) strategy scheduling without SInE, thus
457 maintaining completeness.
458 --schedule-kind=<arg>
460 Choose a schedule kind that is more optimized for different pur‐
462 poses: CASC is optimized for general-purpose theorem proving,
463 while SH is optimized for theorem low-timeout theorem proving.
464 --no-preprocessing
466 Do not perform preprocessing on the initial clause set. Prepro‐
468 cessing currently removes tautologies and orders terms, literals
469 and clauses in a certain ("canonical") way before anything else
470 happens. Unless limited by one of the following options, it will
471 also unfold equational definitions.
472 --eq-unfold-limit=<arg>
474 During preprocessing, limit unfolding (and removing) of equa‐
476 tional definitions to those where the expanded definition is at
477 most the given limit bigger (in terms of standard weight) than
478 the defined term.
479 --eq-unfold-maxclauses=<arg>
481 During preprocessing, don't try unfolding of equational defini‐
483 tions if the problem has more than this limit of clauses.
484 --no-eq-unfolding
486 During preprocessing, abstain from unfolding (and removing)
488 equational definitions.
489 --sine[=<arg>]
491 Apply SInE to prune the unprocessed axioms with the specified
493 filter. 'Auto' will automatically pick a filter. The option
494 without the optional argument is equivalent to --sine=Auto.
495 --rel-pruning-level[=<arg>]
497 Perform relevancy pruning up to the given level on the unpro‐
499 cessed axioms. The option without the optional argument is
500 equivalent to --rel-pruning-level=3.
501 --presat-simplify
503 Before proper saturation do a complete interreduction of the
505 proof state.
506 --ac-handling[=<arg>]
508 Select AC handling mode, i.e. determine what to do with redun‐
510 dant AC tautologies. The default is equivalent to 'DiscardAll',
511 the other possible values are 'None' (to disable AC handling),
512 'KeepUnits', and 'KeepOrientable'. The option without the op‐
513 tional argument is equivalent to --ac-handling=KeepUnits.
514 --ac-non-aggressive
516 Do AC resolution on negative literals only on processing (by de‐
518 fault, AC resolution is done after clause creation). Only effec‐
519 tive if AC handling is not disabled.
520 -W <arg>
522 --literal-selection-strategy=<arg>
524 Choose a strategy for selection of negative literals. There are
526 two special values for this option: NoSelection will select no
527 literal (i.e. perform normal superposition) and NoGeneration
528 will inhibit all generating inferences. For a list of the other
529 (hopefully self-documenting) values run 'eprover -W none'. There
530 are two variants of each strategy. The one prefixed with 'P'
531 will allow paramodulation into maximal positive literals in ad‐
532 dition to paramodulation into maximal selected negative liter‐
533 als.
534 --no-generation
536 Don't perform any generating inferences (equivalent to --lit‐
538 eral-selection-strategy=NoGeneration).
539 --select-on-processing-only
541 Perform literal selection at processing time only (i.e. select
543 only in the _given clause_), not before clause evaluation. This
544 is relevant because many clause selection heuristics give spe‐
545 cial consideration to maximal or selected literals.
546 -i
548 --inherit-paramod-literals
550 Always select the negative literals a previous inference
552 paramodulated into (if possible). If no such literal exists, se‐
553 lect as dictated by the selection strategy.
554 -j
556 --inherit-goal-pm-literals
558 In a goal (all negative clause), always select the negative lit‐
560 erals a previous inference paramodulated into (if possible). If
561 no such literal exists, select as dictated by the selection
562 strategy.
563 --inherit-conjecture-pm-literals
565 In a conjecture-derived clause, always select the negative lit‐
567 erals a previous inference paramodulated into (if possible). If
568 no such literal exists, select as dictated by the selection
569 strategy.
570 --selection-pos-min=<arg>
572 Set a lower limit for the number of positive literals a clause
574 must have to be eligible for literal selection.
575 --selection-pos-max=<arg>
577 Set a upper limit for the number of positive literals a clause
579 can have to be eligible for literal selection.
580 --selection-neg-min=<arg>
582 Set a lower limit for the number of negative literals a clause
584 must have to be eligible for literal selection.
585 --selection-neg-max=<arg>
587 Set a upper limit for the number of negative literals a clause
589 can have to be eligible for literal selection.
590 --selection-all-min=<arg>
592 Set a lower limit for the number of literals a clause must have
594 to be eligible for literal selection.
595 --selection-all-max=<arg>
597 Set an upper limit for the number of literals a clause must have
599 to be eligible for literal selection.
600 --selection-weight-min=<arg>
602 Set the minimum weight a clause must have to be eligible for
604 literal selection.
605 --prefer-initial-clauses
607 Always process all initial clauses first.
609 -x <arg>
611 --expert-heuristic=<arg>
613 Select one of the clause selection heuristics. Currently at
615 least available: Auto, Weight, StandardWeight, RWeight, FIFO,
616 LIFO, Uniq, UseWatchlist. For a full list check HEURIS‐
617 TICS/che_proofcontrol.c. Auto is recommended if you only want to
618 find a proof. It is special in that it will also set some addi‐
619 tional options. To have optimal performance, you also should
620 specify -tAuto to select a good term ordering. LIFO is unfair
621 and will make the prover incomplete. Uniq is used internally and
622 is not very useful in most cases. You can define more heuristics
623 using the option -H (see below).
624 --filter-orphans-limit[=<arg>]
626 Orphans are unprocessed clauses where one of the parents has
628 been removed by back-simolification. They are redundant and usu‐
629 ally removed lazily (i.e. only when they are selected for pro‐
630 cessing). With this option you can select a limit on back-sim‐
631 plified clauses after which orphans will be eagerly deleted.
632 The option without the optional argument is equivalent to --fil‐
633 ter-orphans-limit=100.
634 --forward-contract-limit[=<arg>]
636 Set a limit on the number of processed clauses after which the
638 unprocessed clause set will be re-simplified and reweighted.
639 The option without the optional argument is equivalent to --for‐
640 ward-contract-limit=80000.
641 --delete-bad-limit[=<arg>]
643 Set the number of storage units after which bad clauses are
645 deleted without further consideration. This causes the prover to
646 be potentially incomplete, but will allow you to limit the maxi‐
647 mum amount of memory used fairly well. The prover will tell you
648 if a proof attempt failed due to the incompleteness introduced
649 by this option. It is recommended to set this limit signifi‐
650 cantly higher than --filter-limit or --filter-copies-limit. If
651 you select -xAuto and set a memory limit, the prover will deter‐
652 mine a good value automatically. The option without the optional
653 argument is equivalent to --delete-bad-limit=1500000.
654 --assume-completeness
656 There are various way (e.g. the next few options) to configure
658 the prover to be strongly incomplete in the general case. E will
659 detect when such an option is selected and return corresponding
660 exit states (i.e. it will not claim satisfiability just because
661 it ran out of unprocessed clauses). If you _know_ that for your
662 class of problems the selected strategy is still complete, use
663 this option to tell the system that this is the case.
664 --assume-incompleteness
666 This option instructs the prover to assume incompleteness (typi‐
668 cally because the axiomatization already is incomplete because
669 axioms have been filtered before they are handed to the system.
670 --disable-eq-factoring
672 Disable equality factoring. This makes the prover incomplete for
674 general non-Horn problems, but helps for some specialized
675 classes. It is not necessary to disable equality factoring for
676 Horn problems, as Horn clauses are not factored anyways.
677 --disable-paramod-into-neg-units
679 Disable paramodulation into negative unit clause. This makes the
681 prover incomplete in the general case, but helps for some spe‐
682 cialized classes.
683 --condense
685 Enable condensing for the given clause. Condensing replaces a
687 clause by a more general factor (if such a factor exists).
688 --condense-aggressive
690 Enable condensing for the given and newly generated clauses.
692 --disable-given-clause-fw-contraction
694 Disable simplification and subsumption of the newly selected
696 given clause (clauses are still simplified when they are gener‐
697 ated). In general, this breaks some basic assumptions of the
698 DISCOUNT loop proof search procedure. However, there are some
699 problem classes in which this simplifications empirically never
700 occurs. In such cases, we can save significant overhead. The op‐
701 tion _should_ work in all cases, but is not expected to improve
702 things in most cases.
703 --simul-paramod
705 Use simultaneous paramodulation to implement superposition. De‐
707 fault is to use plain paramodulation.
708 --oriented-simul-paramod
710 Use simultaneous paramodulation for oriented from-literals. This
712 is an experimental feature.
713 --supersimul-paramod
715 Use supersimultaneous paramodulation to implement superposition.
717 Default is to use plain paramodulation.
718 --oriented-supersimul-paramod
720 Use supersimultaneous paramodulation for oriented from-literals.
722 This is an experimental feature.
723 --split-clauses[=<arg>]
725 Determine which clauses should be subject to splitting. The ar‐
727 gument is the binary 'OR' of values for the desired classes:
728 1: Horn clauses
730 2: Non-Horn clauses
732 4: Negative clauses
734 8: Positive clauses
736 16: Clauses with both positive and negative literals
738 Each set bit adds that class to the set of clauses which will be
740 split. The option without the optional argument is equivalent
741 to --split-clauses=7.
742 --split-method=<arg>
744 Determine how to treat ground literals in splitting. The argu‐
746 ment is either '0' to denote no splitting of ground literals
747 (they are all assigned to the first split clause produced), '1'
748 to denote that all ground literals should form a single new
749 clause, or '2', in which case ground literals are treated as
750 usual and are all split off into individual clauses.
751 --split-aggressive
753 Apply splitting to new clauses (after simplification) and before
755 evaluation. By default, splitting (if activated) is only per‐
756 formed on selected clauses.
757 --split-reuse-defs
759 If possible, reuse previous definitions for splitting.
761 -t <arg>
763 --term-ordering=<arg>
765 Select an ordering type (currently Auto, LPO, LPO4, KBO or
767 KBO6). -tAuto is suggested, in particular with -xAuto. KBO and
768 KBO6 are different implementations of the same ordering, KBO6 is
769 usually faster and has had more testing. Similarly, LPO4 is a
770 new, equivalent but superior implementation of LPO.
771 -w <arg>
773 --order-weight-generation=<arg>
775 Select a method for the generation of weights for use with the
777 term ordering. Run 'eprover -w none' for a list of options.
778 --order-weights=<arg>
780 Describe a (partial) assignments of weights to function symbols
782 for term orderings (in particular, KBO). You can specify a list
783 of weights of the form 'f1:w1,f2:w2, ...'. Since a total weight
784 assignment is needed, E will _first_ apply any weight generation
785 scheme specified (or the default one), and then modify the
786 weights as specified. Note that E performs only very basic san‐
787 ity checks, so you probably can specify weights that break KBO
788 constraints.
789 -G <arg>
791 --order-precedence-generation=<arg>
793 Select a method for the generation of a precedence for use with
795 the term ordering. Run 'eprover -G none' for a list of options.
796 --prec-pure-conj[=<arg>]
798 Set a weight for symbols that occur in conjectures only to de‐
800 terminewhere to place it in the precedence. This value is used
801 for a roughpre-order, the normal schemes only sort within sym‐
802 bols with the sameoccurance modifier. The option without the op‐
803 tional argument is equivalent to --prec-pure-conj=10.
804 --prec-conj-axiom[=<arg>]
806 Set a weight for symbols that occur in both conjectures and ax‐
808 iomsto determine where to place it in the precedence. This value
809 is used for a rough pre-order, the normal schemes only sort
810 within symbols with the same occurance modifier. The option
811 without the optional argument is equivalent to --prec-conj-ax‐
812 iom=5.
813 --prec-pure-axiom[=<arg>]
815 Set a weight for symbols that occur in axioms only to determine
817 where to place it in the precedence. This value is used for a
818 rough pre-order, the normal schemes only sort within symbols
819 with the same occurance modifier. The option without the op‐
820 tional argument is equivalent to --prec-pure-axiom=2.
821 --prec-skolem[=<arg>]
823 Set a weight for Skolem symbols to determine where to place it
825 in the precedence. This value is used for a rough pre-order, the
826 normal schemes only sort within symbols with the same occurance
827 modifier. The option without the optional argument is equivalent
828 to --prec-skolem=2.
829 --prec-defpred[=<arg>]
831 Set a weight for introduced predicate symbols (usually via defi‐
833 nitional CNF or clause splitting) to determine where to place it
834 in the precedence. This value is used for a rough pre-order, the
835 normal schemes only sort within symbols with the same occurance
836 modifier. The option without the optional argument is equivalent
837 to --prec-defpred=2.
838 -c <arg>
840 --order-constant-weight=<arg>
842 Set a special weight > 0 for constants in the term ordering. By
844 default, constants are treated like other function symbols.
845 --precedence[=<arg>]
847 Describe a (partial) precedence for the term ordering used for
849 the proof attempt. You can specify a comma-separated list of
850 precedence chains, where a precedence chain is a list of func‐
851 tion symbols (which all have to appear in the proof problem),
852 connected by >, <, or =. If this option is used in connection
853 with --order-precedence-generation, the partial ordering will be
854 completed using the selected method, otherwise the prover runs
855 with a non-ground-total ordering. The option without the op‐
856 tional argument is equivalent to --precedence=.
857 --lpo-recursion-limit[=<arg>]
859 Set a depth limit for LPO comparisons. Most comparisons do not
861 need more than 10 or 20 levels of recursion. By default, recur‐
862 sion depth is limited to 1000 to avoid stack overflow problems.
863 If the limit is reached, the prover assumes that the terms are
864 uncomparable. Smaller values make the comparison attempts
865 faster, but less exact. Larger values have the opposite effect.
866 Values up to 20000 should be save on most operating systems. If
867 you run into segmentation faults while using LPO or LPO4, first
868 try to set this limit to a reasonable value. If the problem per‐
869 sists, send a bug report ;-) The option without the optional ar‐
870 gument is equivalent to --lpo-recursion-limit=100.
871 --restrict-literal-comparisons
873 Make all literals uncomparable in the term ordering (i.e. do not
875 use the term ordering to restrict paramodulation, equality reso‐
876 lution and factoring to certain literals. This is necessary to
877 make Set-of-Support-strategies complete for the non-equational
878 case (It still is incomplete for the equational case, but pretty
879 useless anyways).
880 --literal-comparison=<arg>
882 Modify how literal comparisons are done. 'None' is equivalent to
884 the previous option, 'Normal' uses the normal lifting of the
885 term ordering, 'TFOEqMax' uses the equivalent of a transfinite
886 ordering deciding on the predicate symbol and making equational
887 literals maximal, and 'TFOEqMin' modifies this by making equa‐
888 tional symbols minimal.
889 --sos-uses-input-types
891 If input is TPTP format, use TPTP conjectures for initializing
893 the Set of Support. If not in TPTP format, use E-LOP queries
894 (clauses of the form ?-l(X),...,m(Y)). Normally, all negative
895 clauses are used. Please note that most E heuristics do not use
896 this information at all, it is currently only useful for certain
897 parameter settings (including the SimulateSOS priority func‐
898 tion).
899 --destructive-er
901 Allow destructive equality resolution inferences on pure-vari‐
903 able literals of the form X!=Y, i.e. replace the original clause
904 with the result of an equality resolution inference on this lit‐
905 eral.
906 --strong-destructive-er
908 Allow destructive equality resolution inferences on literals of
910 the form X!=t (where X does not occur in t), i.e. replace the
911 original clause with the result of an equality resolution infer‐
912 ence on this literal. Unless I am brain-dead, this maintains
913 completeness, although the proof is rather tricky.
914 --destructive-er-aggressive
916 Apply destructive equality resolution to all newly generated
918 clauses, not just to selected clauses. Implies --destructive-er.
919 --forward-context-sr
921 Apply contextual simplify-reflect with processed clauses to the
923 given clause.
924 --forward-context-sr-aggressive
926 Apply contextual simplify-reflect with processed clauses to new
928 clauses. Implies --forward-context-sr.
929 --backward-context-sr
931 Apply contextual simplify-reflect with the given clause to pro‐
933 cessed clauses.
934 -g
936 --prefer-general-demodulators
938 Prefer general demodulators. By default, E prefers specialized
940 demodulators. This affects in which order the rewrite index is
941 traversed.
942 -F <arg>
944 --forward-demod-level=<arg>
946 Set the desired level for rewriting of unprocessed clauses. A
948 value of 0 means no rewriting, 1 indicates to use rules (ori‐
949 entable equations) only, 2 indicates full rewriting with rules
950 and instances of unorientable equations. Default behavior is 2.
951 --strong-rw-inst
953 Instantiate unbound variables in matching potential demodulators
955 with a small constant terms.
956 -u
958 --strong-forward-subsumption
960 Try multiple positions and unit-equations to try to equationally
962 subsume a single new clause. Default is to search for a single
963 position.
964 --satcheck-proc-interval[=<arg>]
966 Enable periodic SAT checking at the given interval of main loop
968 non-trivial processed clauses. The option without the optional
969 argument is equivalent to --satcheck-proc-interval=5000.
970 --satcheck-gen-interval[=<arg>]
972 Enable periodic SAT checking whenever the total proof state size
974 increases by the given limit. The option without the optional
975 argument is equivalent to --satcheck-gen-interval=10000.
976 --satcheck-ttinsert-interval[=<arg>]
978 Enable periodic SAT checking whenever the number of term tops
980 insertions matches the given limit (which grows exponentially).
981 The option without the optional argument is equivalent to
982 --satcheck-ttinsert-interval=5000000.
983 --satcheck[=<arg>]
985 Set the grounding strategy for periodic SAT checking. Note that
987 to enable SAT checking, it is also necessary to set the interval
988 with one of the previous two options. The option without the op‐
989 tional argument is equivalent to --satcheck=FirstConst.
990 --satcheck-decision-limit[=<arg>]
992 Set the number of decisions allowed for each run of the SAT
994 solver. If the option is not given, the built-in value is 10000.
995 Use -1 to allow unlimited decision. The option without the op‐
996 tional argument is equivalent to --satcheck-decision-limit=100.
997 --satcheck-normalize-const
999 Use the current normal form (as recorded in the termbank rewrite
1001 cache) of the selected constant as the term for the grounding
1002 substitution.
1003 --satcheck-normalize-unproc
1005 Enable re-simplification (heuristic re-revaluation) of unpro‐
1007 cessed clauses before grounding for SAT checking.
1008 --watchlist[=<arg>]
1010 Give the name for a file containing clauses to be watched for
1012 during the saturation process. If a clause is generated that
1013 subsumes a watchlist clause, the subsumed clause is removed from
1014 the watchlist. The prover will terminate when the watchlist is
1015 empty. If you want to use the watchlist for guiding the proof,
1016 put the empty clause onto the list and use the built-in clause
1017 selection heuristic 'UseWatchlist' (or build a heuristic your‐
1018 self using the priority functions 'PreferWatchlist' and 'Defer‐
1019 Watchlist'). Use the argument 'Use inline watchlist type' (or no
1020 argument) and the special clause type 'watchlist' if you want to
1021 put watchlist clauses into the normal input stream. This is only
1022 supported for TPTP input formats. The option without the op‐
1023 tional argument is equivalent to --watchlist='Use inline watch‐
1024 list type'.
1025 --static-watchlist[=<arg>]
1027 This is identical to the previous option, but subsumed clauses
1029 willnot be removed from the watchlist (and hence the prover will
1030 not terminate if all watchlist clauses have been subsumed. This
1031 may be more useful for heuristic guidance. The option without
1032 the optional argument is equivalent to --static-watchlist='Use
1033 inline watchlist type'.
1034 --no-watchlist-simplification
1036 By default, the watchlist is brought into normal form with re‐
1038 spect to the current processed clause set and certain simplifi‐
1039 cations. This option disables simplification for the watchlist.
1040 --conventional-subsumption
1042 Equivalent to --subsumption-indexing=None.
1044 --subsumption-indexing=<arg>
1046 Determine choice of indexing for (most) subsumption operations.
1048 Choices are 'None' for naive subsumption, 'Direct' for direct
1049 mapped FV-Indexing, 'Perm' for permuted FV-Indexing and 'Per‐
1050 mOpt' for permuted FV-Indexing with deletion of (suspected)
1051 non-informative features. Default behaviour is 'Perm'.
1052 --fvindex-featuretypes=<arg>
1054 Select the feature types used for indexing. Choices are "None"
1056 to disable FV-indexing, "AC" for AC compatible features (the de‐
1057 fault) (literal number and symbol counts), "SS" for set subsump‐
1058 tion compatible features (symbol depth), and "All" for all fea‐
1059 tures.Unless you want to measure the effects of the different
1060 features, I suggest you stick with the default.
1061 --fvindex-maxfeatures[=<arg>]
1063 Set the maximum initial number of symbols for feature computa‐
1065 tion. Depending on the feature selection, a value of X here
1066 will convert into 2X+2 features (for set subsumption features),
1067 2X+4 features (for AC-compatible features) or 4X+6 features (if
1068 all features are used, the default). Note that the actually used
1069 set of features may be smaller than this if the signature does
1070 not contain enough symbols.For the Perm and PermOpt version,
1071 this is _also_ used to set the maximum depth of the feature vec‐
1072 tor index. Yes, I should probably make this into two separate
1073 options. If you select a small value here, you should probably
1074 not use "Direct" for the --subsumption-indexing option. The op‐
1075 tion without the optional argument is equivalent to --fvin‐
1076 dex-maxfeatures=200.
1077 --fvindex-slack[=<arg>]
1079 Set the number of slots reserved in the index for function sym‐
1081 bols that may be introduced into the signature later, e.g. by
1082 splitting. If no new symbols are introduced, this just wastes
1083 time and memory. If PermOpt is chosen, the slackness slots will
1084 be deleted from the index anyways, but will still waste (a lit‐
1085 tle) time in computing feature vectors. The option without the
1086 optional argument is equivalent to --fvindex-slack=0.
1087 --rw-bw-index[=<arg>]
1089 Select fingerprint function for backwards rewrite index. "NoIn‐
1091 dex" will disable paramodulation indexing. For a list of the
1092 other values run 'eprover --pm-index=none'. FPX functions will
1093 use a fingerprint of X positions, the letters disambiguate be‐
1094 tween different fingerprints with the same sample size. The op‐
1095 tion without the optional argument is equivalent to --rw-bw-in‐
1096 dex=FP7.
1097 --pm-from-index[=<arg>]
1099 Select fingerprint function for the index for paramodulation
1101 from indexed clauses. "NoIndex" will disable paramodulation in‐
1102 dexing. For a list of the other values run 'eprover --pm-in‐
1103 dex=none'. FPX functionswill use a fingerprint of X positions,
1104 the letters disambiguate between different fingerprints with the
1105 same sample size. The option without the optional argument is
1106 equivalent to --pm-from-index=FP7.
1107 --pm-into-index[=<arg>]
1109 Select fingerprint function for the index for paramodulation
1111 into the indexed clauses. "NoIndex" will disable paramodulation
1112 indexing. For a list of the other values run 'eprover --pm-in‐
1113 dex=none'. FPX functionswill use a fingerprint of X positions,
1114 the letters disambiguate between different fingerprints with the
1115 same sample size. The option without the optional argument is
1116 equivalent to --pm-into-index=FP7.
1117 --fp-index[=<arg>]
1119 Select fingerprint function for all fingerprint indices. See
1121 above. The option without the optional argument is equivalent to
1122 --fp-index=FP7.
1123 --fp-no-size-constr
1125 Disable usage of size constraints for matching with fingerprint
1127 indexing.
1128 --pdt-no-size-constr
1130 Disable usage of size constraints for matching with perfect dis‐
1132 crimination trees indexing.
1133 --pdt-no-age-constr
1135 Disable usage of age constraints for matching with perfect dis‐
1137 crimination trees indexing.
1138 --detsort-rw
1140 Sort set of clauses eliminated by backward rewriting using a to‐
1142 tal syntactic ordering.
1143 --detsort-new
1145 Sort set of newly generated and backward simplified clauses us‐
1147 ing a total syntactic ordering.
1148 -D <arg>
1150 --define-weight-function=<arg>
1152 Define
1154 a weight function (see manual for details). Later definitions
1155 override previous definitions.
1157 -H <arg>
1159 --define-heuristic=<arg>
1161 Define a clause selection heuristic (see manual for details).
1163 Later definitions override previous definitions.
1164 --free-numbers
1166 Treat numbers (strings of decimal digits) as normal free func‐
1168 tion symbols in the input. By default, number now are supposed
1169 to denote domain constants and to be implicitly different from
1170 each other.
1171 --free-objects
1173 Treat object identifiers (strings in double quotes) as normal
1175 free function symbols in the input. By default, object identi‐
1176 fiers now represent domain objects and are implicitly different
1177 from each other (and from numbers, unless those are declared to
1178 be free).
1179 --definitional-cnf[=<arg>]
1181 Tune the clausification algorithm to introduces definitions for
1183 subformulae to avoid exponential blow-up. The optional argument
1184 is a fudge factor that determines when definitions are intro‐
1185 duced. 0 disables definitions completely. The default works
1186 well. The option without the optional argument is equivalent to
1187 --definitional-cnf=24.
1188 --old-cnf[=<arg>]
1190 As the previous option, but use the classical, well-tested
1192 clausification algorithm as opposed to the newewst one which
1193 avoides some algorithmic pitfalls and hence works better on some
1194 exotic formulae. The two may produce slightly different (but eq‐
1195 uisatisfiable) clause normal forms. The option without the op‐
1196 tional argument is equivalent to --old-cnf=24.
1197 --miniscope-limit[=<arg>]
1199 Set the limit of sub-formula-size to miniscope. The build-inde‐
1201 fault is 256. Only applies to the new (default) clausification
1202 algorithm The option without the optional argument is equivalent
1203 to --miniscope-limit=2147483648.
1204 --print-types
1206 Print the type of every term. Useful for debugging purposes.
1208 --app-encode
1210 Encodes terms in the proof state using applicative encoding,
1212 prints encoded input problem and exits.
1213 --arg-cong=<arg>
1215 Turns on ArgCong inference rule. Excepts an argument "all" or
1217 "max" that applies the rule to all or only literals that are el‐
1218 igible for resolution.
1219 --neg-ext=<arg>
1221 Turns on NegExt inference rule. Excepts an argument "all" or
1223 "max" that applies the rule to all or only literals that are el‐
1224 igible for resolution.
1225 --pos-ext=<arg>
1227 Turns on PosExt inference rule. Excepts an argument "all" or
1229 "max" that applies the rule to all or only literals that are el‐
1230 igible for resolution.
1231 --ext-sup-max-depth=<arg>
1233 Sets the maximal proof depth of the clause which will be consid‐
1235 ered for ExtSup inferences. Negative value disables the rule.
1236 --inverse-recognition
1238 Enables the recognition of injective function symbols. If such a
1240 symbol is recognized, existence of the inverse function is as‐
1241 serted by adding a corresponding axiom.
1242 --replace-inj-defs
1244 After CNF and before saturation, replaces all clauses that are
1246 definitions of injectivity by axiomatization of inverse func‐
1247 tion.
1248
1250 Report bugs to <schulz@eprover.org>. Please include the following, if
1251 possible:
1252 * The version of the package as reported by eprover --version.
1254 * The operating system and version.
1256 * The exact command line that leads to the unexpected behaviour.
1258 * A description of what you expected and what actually happend.
1260 * If possible all input files necessary to reproduce the bug.
1262
1264 Copyright 1998-2021 by Stephan Schulz, schulz@eprover.org, and the E
1265 contributors (see DOC/CONTRIBUTORS).
1266 This program is a part of the distribution of the equational theorem
1268 prover E. You can find the latest version of the E distribution as well
1269 as additional information at http://www.eprover.org
1270 This program is free software; you can redistribute it and/or modify it
1272 under the terms of the GNU General Public License as published by the
1273 Free Software Foundation; either version 2 of the License, or (at your
1274 option) any later version.
1275 This program is distributed in the hope that it will be useful, but
1277 WITHOUT ANY WARRANTY; without even the implied warranty of MER‐
1278 CHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
1279 Public License for more details.
1280 You should have received a copy of the GNU General Public License along
1282 with this program (it should be contained in the top level directory of
1283 the distribution in the file COPYING); if not, write to the Free Soft‐
1284 ware Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
1285 02111-1307 USA
1286 The original copyright holder can be contacted via email or as
1288 Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Rote‐
1290 buehlplatz 41 70178 Stuttgart Germany
1291E 2.6-DEBUG Floral Guranse (ab0adeJ8a7nbuba0r7y0b2805232105f79bf59e8fc27f915b4f) E(1)