LP, the Larch Prover -- The statistics-level setting

The statistics-level setting controls the amount of statistics that LP records about its operation.


<set-statistics-level-command> ::= set statistics-level <number>


set statistics-level 3


The statistics-level setting is an integer between 0 and 3; 2 is the default. LP gathers increasingly many statistics at each level, as follows.
Summary statistics only: total running time and memory usage, including the number of garbage collections.
Detailed statistics about the time spent, both successfully and unsuccessfully, attempting to orient formulas into rewrite rules, to apply rewrite rules, to apply deduction rules, and to unify terms (in response to the critical-pairs command). Also, the time spent controlling LP's inference mechanisms.
The number of successful applications of each rewrite and deduction rule, as well as the number of nontrivial critical pairs involving each rewrite rule.
The number of attempted applications of each rewrite rule. Level 3 imposes a considerable computational burden, for example, up to 10% in some applications.