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>
Examples
set statistics-level 3
Usage
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.
- 0
-
Summary statistics only: total running time and memory usage, including the
number of garbage collections.
- 1
-
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.
- 2
-
The number of successful applications of each rewrite and deduction rule, as
well as the number of nontrivial critical pairs involving each rewrite rule.
- 3
-
The number of attempted applications of each rewrite rule. Level 3 imposes a
considerable computational burden, for example, up to 10% in some applications.