1E(1)                             User Commands                            E(1)
2
3
4

NAME

6       E     -    manual    page    for    E    2.6-DEBUG    Floral    Guranse
7       (ab0ade87bb070b853105f79bf59e8fc27f915b4f)
8

SYNOPSIS

10       eprover [options] [files]
11

DESCRIPTION

13       E 2.6-DEBUG "Floral Guranse"
14
15       Read a set of first-order clauses and formulae and try to refute it.
16

OPTIONS

18       -h
19
20       --help
21
22              Print a short description of program usage and options.
23
24       -V
25
26       --version
27
28              Print the version number of the prover. Please include this with
29              all bug reports (if any).
30
31       -v
32
33       --verbose[=<arg>]
34
35              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
42       -o <arg>
43
44       --output-file=<arg>
45
46              Redirect output into the named file.
47
48       -s
49
50       --silent
51
52              Equivalent to --output-level=0.
53
54       -l <arg>
55
56       --output-level=<arg>
57
58              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
66       -p
67
68       --proof-object[=<arg>]
69
70              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
84       --proof-graph[=<arg>]
85
86              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
94       -d
95
96       --full-deriv
97
98              Include all derived formuas/clauses in the proof graph/proof ob‐
99              ject, not just the ones contributing to the actual proof.
100
101       --force-deriv[=<arg>]
102
103              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
110       --record-gcs
111
112              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
116       --training-examples[=<arg>]
117
118              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
125       --pcl-terms-compressed
126
127              Print terms in the PCL output in shared representation.
128
129       --pcl-compact
130
131              Print  PCL steps without additional spaces for formatting (safes
132              disk space for large protocols).
133
134       --pcl-shell-level[=<arg>]
135
136              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
143       --print-statistics
144
145              Print  the  inference statistics (only relevant for output level
146              0, otherwise they are printed automatically.
147
148       -0
149
150       --print-detailed-statistics
151
152              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
156       -S
157
158       --print-saturated[=<arg>]
159
160              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
176       --print-sat-info
177
178              Print additional information (clause number, weight, etc)  as  a
179              comment for clauses from the semi-saturated end system.
180
181       --filter-saturated[=<arg>]
182
183       Filter the
184              (semi-) saturated clause sets after terminating the
185
186              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
196       --prune
197
198              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
204       --cnf
205
206              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
213       --print-pid
214
215              Print the process id of the prover as  a  comment  after  option
216              processing.
217
218       --print-version
219
220              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
224       --error-on-empty
225
226              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
233       -m <arg>
234
235       --memory-limit=<arg>
236
237              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
249       --cpu-limit[=<arg>]
250
251              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
263       --soft-cpu-limit[=<arg>]
264
265              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
276       -R
277
278       --resources-info
279
280              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
285       --print-strategy
286
287              Print a representation of all search parameters and  their  set‐
288              ting. Then terminate.
289
290       -C <arg>
291
292       --processed-clauses-limit=<arg>
293
294              Set the maximal number of clauses to process (i.e. the number of
295              traversals of the main-loop).
296
297       -P <arg>
298
299       --processed-set-limit=<arg>
300
301              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
305       -U <arg>
306
307       --unprocessed-limit=<arg>
308
309              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
313       -T <arg>
314
315       --total-clause-set-limit=<arg>
316
317              Set the maximal size of the set of all clauses. See previous op‐
318              tion.
319
320       --generated-limit=<arg>
321
322              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
326       --tb-insert-limit=<arg>
327
328              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
331       --answers[=<arg>]
332
333              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
340       --conjectures-are-questions
341
342              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
346       -n
347
348       --eqn-no-infix
349
350              In LOP, print equations in prefix notation equal(x,y).
351
352       -e
353
354       --full-equational-rep
355
356              In  LOP.  print  all  literals as equations, even non-equational
357              ones.
358
359       --lop-in
360
361              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
367       --pcl-out
368
369              Set PCL as the proof object output format.
370
371       --tptp-in
372
373              Set TPTP-2 as the input format (but note that includes are still
374              handled according to TPTP-3 semantics).
375
376       --tptp-out
377
378              Print  TPTP  format instead of E-LOP. Implies --eqn-no-infix and
379              will ignore --full-equational-rep.
380
381       --tptp-format
382
383              Equivalent to --tptp-in and --tptp-out.
384
385       --tptp2-in
386
387              Synonymous with --tptp-in.
388
389       --tptp2-out
390
391              Synonymous with --tptp-out.
392
393       --tptp2-format
394
395              Synonymous with --tptp-format.
396
397       --tstp-in
398
399              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
404       --tstp-out
405
406              Print output clauses in TPTP-3 syntax. In particular, for output
407              levels >=2, write derivations as TPTP-3 derivations.
408
409       --tstp-format
410
411              Equivalent to --tstp-in and --tstp-out.
412
413       --tptp3-in
414
415              Synonymous with --tstp-in.
416
417       --tptp3-out
418
419              Synonymous with --tstp-out.
420
421       --tptp3-format
422
423              Synonymous with --tstp-format.
424
425       --auto
426
427              Automatically determine  settings  for  proof  search.  This  is
428              equivalent to -xAuto -tAuto --sine=Auto.
429
430       --satauto
431
432              Automatically  determine  settings  for proof/saturation search.
433              This is equivalent to -xAuto -tAuto.
434
435       --autodev
436
437              Automatically determine settings for proof  search  (development
438              version).    This   is   equivalent   to   -xAutoDev   -tAutoDev
439              --sine=Auto.
440
441       --satautodev
442
443              Automatically determine  settings  for  proof/saturation  search
444              (development  version).  This  is  equivalent to -xAutoDev -tAu‐
445              toDev.
446
447       --auto-schedule
448
449              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
454       --satauto-schedule
455
456              Use  the  (experimental)  strategy scheduling without SInE, thus
457              maintaining completeness.
458
459       --schedule-kind=<arg>
460
461              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
465       --no-preprocessing
466
467              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
473       --eq-unfold-limit=<arg>
474
475              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
480       --eq-unfold-maxclauses=<arg>
481
482              During  preprocessing, don't try unfolding of equational defini‐
483              tions if the problem has more than this limit of clauses.
484
485       --no-eq-unfolding
486
487              During preprocessing,  abstain  from  unfolding  (and  removing)
488              equational definitions.
489
490       --sine[=<arg>]
491
492              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
496       --rel-pruning-level[=<arg>]
497
498              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
502       --presat-simplify
503
504              Before  proper  saturation  do  a complete interreduction of the
505              proof state.
506
507       --ac-handling[=<arg>]
508
509              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
515       --ac-non-aggressive
516
517              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
521       -W <arg>
522
523       --literal-selection-strategy=<arg>
524
525              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
535       --no-generation
536
537              Don't perform any generating inferences  (equivalent  to  --lit‐
538              eral-selection-strategy=NoGeneration).
539
540       --select-on-processing-only
541
542              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
547       -i
548
549       --inherit-paramod-literals
550
551              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
555       -j
556
557       --inherit-goal-pm-literals
558
559              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
564       --inherit-conjecture-pm-literals
565
566              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
571       --selection-pos-min=<arg>
572
573              Set a lower limit for the number of positive literals  a  clause
574              must have to be eligible for literal selection.
575
576       --selection-pos-max=<arg>
577
578              Set  a  upper limit for the number of positive literals a clause
579              can have to be eligible for literal selection.
580
581       --selection-neg-min=<arg>
582
583              Set a lower limit for the number of negative literals  a  clause
584              must have to be eligible for literal selection.
585
586       --selection-neg-max=<arg>
587
588              Set  a  upper limit for the number of negative literals a clause
589              can have to be eligible for literal selection.
590
591       --selection-all-min=<arg>
592
593              Set a lower limit for the number of literals a clause must  have
594              to be eligible for literal selection.
595
596       --selection-all-max=<arg>
597
598              Set an upper limit for the number of literals a clause must have
599              to be eligible for literal selection.
600
601       --selection-weight-min=<arg>
602
603              Set the minimum weight a clause must have  to  be  eligible  for
604              literal selection.
605
606       --prefer-initial-clauses
607
608              Always process all initial clauses first.
609
610       -x <arg>
611
612       --expert-heuristic=<arg>
613
614              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
625       --filter-orphans-limit[=<arg>]
626
627              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
635       --forward-contract-limit[=<arg>]
636
637              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
642       --delete-bad-limit[=<arg>]
643
644              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
655       --assume-completeness
656
657              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
665       --assume-incompleteness
666
667              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
671       --disable-eq-factoring
672
673              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
678       --disable-paramod-into-neg-units
679
680              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
684       --condense
685
686              Enable  condensing  for  the given clause. Condensing replaces a
687              clause by a more general factor (if such a factor exists).
688
689       --condense-aggressive
690
691              Enable condensing for the given and newly generated clauses.
692
693       --disable-given-clause-fw-contraction
694
695              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
704       --simul-paramod
705
706              Use  simultaneous paramodulation to implement superposition. De‐
707              fault is to use plain paramodulation.
708
709       --oriented-simul-paramod
710
711              Use simultaneous paramodulation for oriented from-literals. This
712              is an experimental feature.
713
714       --supersimul-paramod
715
716              Use supersimultaneous paramodulation to implement superposition.
717              Default is to use plain paramodulation.
718
719       --oriented-supersimul-paramod
720
721              Use supersimultaneous paramodulation for oriented from-literals.
722              This is an experimental feature.
723
724       --split-clauses[=<arg>]
725
726              Determine  which clauses should be subject to splitting. The ar‐
727              gument is the binary 'OR' of values for the desired classes:
728
729       1:     Horn clauses
730
731       2:     Non-Horn clauses
732
733       4:     Negative clauses
734
735       8:     Positive clauses
736
737       16:    Clauses with both positive and negative literals
738
739              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
743       --split-method=<arg>
744
745              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
752       --split-aggressive
753
754              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
758       --split-reuse-defs
759
760              If possible, reuse previous definitions for splitting.
761
762       -t <arg>
763
764       --term-ordering=<arg>
765
766              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
772       -w <arg>
773
774       --order-weight-generation=<arg>
775
776              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
779       --order-weights=<arg>
780
781              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
790       -G <arg>
791
792       --order-precedence-generation=<arg>
793
794              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
797       --prec-pure-conj[=<arg>]
798
799              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
805       --prec-conj-axiom[=<arg>]
806
807              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
814       --prec-pure-axiom[=<arg>]
815
816              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
822       --prec-skolem[=<arg>]
823
824              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
830       --prec-defpred[=<arg>]
831
832              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
839       -c <arg>
840
841       --order-constant-weight=<arg>
842
843              Set a special weight > 0 for constants in the term ordering.  By
844              default, constants are treated like other function symbols.
845
846       --precedence[=<arg>]
847
848              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
858       --lpo-recursion-limit[=<arg>]
859
860              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
872       --restrict-literal-comparisons
873
874              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
881       --literal-comparison=<arg>
882
883              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
890       --sos-uses-input-types
891
892              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
900       --destructive-er
901
902              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
907       --strong-destructive-er
908
909              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
915       --destructive-er-aggressive
916
917              Apply destructive equality resolution  to  all  newly  generated
918              clauses, not just to selected clauses. Implies --destructive-er.
919
920       --forward-context-sr
921
922              Apply  contextual simplify-reflect with processed clauses to the
923              given clause.
924
925       --forward-context-sr-aggressive
926
927              Apply contextual simplify-reflect with processed clauses to  new
928              clauses.  Implies --forward-context-sr.
929
930       --backward-context-sr
931
932              Apply  contextual simplify-reflect with the given clause to pro‐
933              cessed clauses.
934
935       -g
936
937       --prefer-general-demodulators
938
939              Prefer general demodulators. By default, E  prefers  specialized
940              demodulators.  This affects in which order the rewrite  index is
941              traversed.
942
943       -F <arg>
944
945       --forward-demod-level=<arg>
946
947              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
952       --strong-rw-inst
953
954              Instantiate unbound variables in matching potential demodulators
955              with a small constant terms.
956
957       -u
958
959       --strong-forward-subsumption
960
961              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
965       --satcheck-proc-interval[=<arg>]
966
967              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
971       --satcheck-gen-interval[=<arg>]
972
973              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
977       --satcheck-ttinsert-interval[=<arg>]
978
979              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
984       --satcheck[=<arg>]
985
986              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
991       --satcheck-decision-limit[=<arg>]
992
993              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
998       --satcheck-normalize-const
999
1000              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
1004       --satcheck-normalize-unproc
1005
1006              Enable  re-simplification  (heuristic  re-revaluation) of unpro‐
1007              cessed clauses before grounding for SAT checking.
1008
1009       --watchlist[=<arg>]
1010
1011              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
1026       --static-watchlist[=<arg>]
1027
1028              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
1035       --no-watchlist-simplification
1036
1037              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
1041       --conventional-subsumption
1042
1043              Equivalent to --subsumption-indexing=None.
1044
1045       --subsumption-indexing=<arg>
1046
1047              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
1053       --fvindex-featuretypes=<arg>
1054
1055              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
1062       --fvindex-maxfeatures[=<arg>]
1063
1064              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
1078       --fvindex-slack[=<arg>]
1079
1080              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
1088       --rw-bw-index[=<arg>]
1089
1090              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
1098       --pm-from-index[=<arg>]
1099
1100              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
1108       --pm-into-index[=<arg>]
1109
1110              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
1118       --fp-index[=<arg>]
1119
1120              Select  fingerprint  function  for  all fingerprint indices. See
1121              above. The option without the optional argument is equivalent to
1122              --fp-index=FP7.
1123
1124       --fp-no-size-constr
1125
1126              Disable  usage of size constraints for matching with fingerprint
1127              indexing.
1128
1129       --pdt-no-size-constr
1130
1131              Disable usage of size constraints for matching with perfect dis‐
1132              crimination trees indexing.
1133
1134       --pdt-no-age-constr
1135
1136              Disable  usage of age constraints for matching with perfect dis‐
1137              crimination trees indexing.
1138
1139       --detsort-rw
1140
1141              Sort set of clauses eliminated by backward rewriting using a to‐
1142              tal syntactic ordering.
1143
1144       --detsort-new
1145
1146              Sort  set of newly generated and backward simplified clauses us‐
1147              ing a total syntactic ordering.
1148
1149       -D <arg>
1150
1151       --define-weight-function=<arg>
1152
1153       Define
1154              a weight function (see manual for details). Later definitions
1155
1156              override previous definitions.
1157
1158       -H <arg>
1159
1160       --define-heuristic=<arg>
1161
1162              Define a clause selection heuristic (see  manual  for  details).
1163              Later definitions override previous definitions.
1164
1165       --free-numbers
1166
1167              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
1172       --free-objects
1173
1174              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
1180       --definitional-cnf[=<arg>]
1181
1182              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
1189       --old-cnf[=<arg>]
1190
1191              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
1198       --miniscope-limit[=<arg>]
1199
1200              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
1205       --print-types
1206
1207              Print the type of every term. Useful for debugging purposes.
1208
1209       --app-encode
1210
1211              Encodes  terms  in  the  proof state using applicative encoding,
1212              prints encoded input problem and exits.
1213
1214       --arg-cong=<arg>
1215
1216              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
1220       --neg-ext=<arg>
1221
1222              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
1226       --pos-ext=<arg>
1227
1228              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
1232       --ext-sup-max-depth=<arg>
1233
1234              Sets the maximal proof depth of the clause which will be consid‐
1235              ered for ExtSup inferences. Negative value disables the rule.
1236
1237       --inverse-recognition
1238
1239              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
1243       --replace-inj-defs
1244
1245              After  CNF  and before saturation, replaces all clauses that are
1246              definitions  of injectivity by axiomatization of  inverse  func‐
1247              tion.
1248

REPORTING BUGS

1250       Report  bugs  to <schulz@eprover.org>. Please include the following, if
1251       possible:
1252
1253       * The version of the package as reported by eprover --version.
1254
1255       * The operating system and version.
1256
1257       * The exact command line that leads to the unexpected behaviour.
1258
1259       * A description of what you expected and what actually happend.
1260
1261       * 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
1267       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
1271       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
1276       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
1281       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
1287       The original copyright holder can be contacted via email or as
1288
1289       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Rote‐
1290       buehlplatz 41 70178 Stuttgart Germany
1291
1292
1293
1294E 2.6-DEBUG Floral Guranse (ab0adeJ8a7nbuba0r7y0b2805232105f79bf59e8fc27f915b4f)     E(1)
Impressum