 0

Only user interactions and the final results of commands.
 1

The creation and deletion of facts: how many new facts have been asserted, when
facts are deleted because they reduce to true, when application of a
deduction rule yields a nontrivial result, when a nontrivial critical pair or
instantiation has been added to the system, and when a deduction rule is
normalized to a set of formulas.
Also, the size of the system at regular intervals, and when a critical pair
computation is abandoned because a theorem has been proved.
 2

Ordering actions: when a formula is oriented into a rewrite rule, when a
rewrite rule is turned back into a formula because its left side was reduced,
when the registry is extended, and when an incompatible formula cannot be
oriented.
Also, the size of the system at more frequent intervals.
 3

Reduction actions: a formula, deduction rule, or the right side of a rewrite
rule has been reduced as a result of adding a new rewrite rule to the system.
Also, the accumulated running time at periodic intervals.
 4

Internormalization actions: processing new facts (by normalizing them and
applying deduction rules), applying new rewrite rules, orienting formulas into
rewrite rules, and computing critical pairs during completion. Also,
postponing the orientation of formulas because of their size or because they
cannot be oriented using the current registry.
 5

Detailed information about critical pairs, deduction rules, and instantiations:
instantiations that leave a formula, rewrite rule, or deduction rule unchanged;
instantiations and the results of deduction rules that reduce to true, and
unreduced critical pair equations along with their normal forms.
 6

Successful application of a rewrite rule (debugging information). The output
produced at this and higher trace levels is not particularly well coordinated
with the output produced by lower trace levels.
 7

Attempted application of a rewrite rule (debugging information).
 8

Times at which the events reported at levels 6 and 7 occur.