E has several different output levels, controlled by the option -l or --output-level. Level 0 prints nearly no output except for the result. Level 1 is intended to give humans a somewhat readable impression of what is going on inside the inference engine. Levels 3 to 6 output increasingly more information about the inside processes in PCL2 format. At level 4 and above, a (large) superset of the proof inferences is printed. You can use the epclextract utility in E/PROVER/ to extract a simple proof object.
In Level 0 and 1, everything E prints is either a clause that is implied by the original axioms, or a comment (or, very often, both).
In silent mode (--output-level=0, -s or --silent), E will not print any output during saturation. It will print a one-line comment documenting the state of the proof search after termination. The following possibilities exist:
Ensuring the completeness of a prover is much harder than ensuring correctness. Moreover, proofs can easily be checked by analyzing the output of the prover, while such a check for the absence of proofs is rarely possible. I do believe that the current version of E is both correct and complete13 but my belief in the former is stronger than my belief in the later…...
…and the user is expected to know which limit he selected.
This is roughly equivalent to Otter’s SOS empty message.
If you run E without selection an output level (or by setting it explicitly to 1), E will print each non-tautological, non-subsumed clause it processes as a comment. It will also print a hash (’#’) for each clause it tries to process but can prove to be superfluous.
This mode gives some indication of progress, and as the output is fairly restricted, does not slow the prover down too much.
For any output level greater than 0, E will also print statistical information about the proof search and final clause sets. The data should be fairly self-explaining.
At output levels greater that 1, E prints certain inferences in PCL2 format14. At level 2, it only prints generating inferences. At level 4, it prints all generating and modifying inferences, and at level 6 it also prints PCL steps giving a lot of insight into the internal operation of the inference engine. This protocol is fairly readable and, from level 4 on can be used to check the proof with the utility checkproof provided with the distribution.
There are two additional kinds of information E can provide beyond the normal output during proof search: Statistical information and final clause sets (with additional information).
First, E can give you some technical information about the conditions it runs under.
The option --print-pid will make E printing its process id as a comment, in the format # Pid: XXX, where XXX is an integer number. This is useful if you want to send signals to the prover (in particular, if you want to terminate the prover) to control it from the outside.
The option -R (--resources-info) will make E print a summary of used system resources after graceful termination:
Most operating systems do not provide a valid value for the resident set size and other memory-related resources, so you should probably not depend on the last value to carry any meaningful information. The time information is required by most standards and should be useful for all tested operating systems.
E can be used not only as a prover, but as a normalizer for formulae or as a lemma generator. In this cases, you will not only want to know if E found a proof, but also need some or all of the derived clauses, possibly with statistical information for filtering. This is supported with the --print-saturated and --print-sat-info options for E.
The option --print-saturated takes as its argument a string of letters, each of which represents a part of the total set of clauses E knows about. The following table contains the meaning of the individual letters:
e | Processed positive unit clauses (Equations). |
i | Processed negative unit clauses (Inequations). |
g | Processed non-unit clauses (except for the empty clause, which, if present, is printed separately). The above three sets are interreduced and all selected inferences between them have been computed. |
E | Unprocessed positive unit clauses. |
I | Unprocessed negative unit clauses. |
G | Unprocessed non-unit clause (this set may contain the empty clause in very rare cases). |
a | Print equality axioms (if equality is present in the problem). This letter prints axioms for reflexivity, symmetry, and transitivity, and a set of substitutivity axioms, one for each argument position of every function symbol and predicate symbol. |
A | As a, but print a single substitutivity axiom covering all positions for each symbol. |
The short form, -S, is equivalent to --print-saturated=eigEIG. If the option --print-sat-info is set, then each of the clauses is followed by a comment of the form # info(id, pd, pl, sc, cd, nl, no, nv). The following table explains the meaning of these values:
id | Clause ident (probably only useful internally) |
pd | Depth of the derivation graph for this clause |
pl | Number of nodes in the derivation grap |
sc | Symbol count (function symbols and variables) |
cd | Depth of the deepest term in the clause |
nl | Number of literals in the clause |
no | Number of variable occurences |
nv | Number of different variables |