LP, the Larch Prover -- Hints on making proofs go faster

When LP seems too slow, use the statistics command to find out which activities are consuming a lot of time. If rewriting (particularly, unsuccessful rewriting) is costly, try one of the following.

Immunize facts that you know are irreducible. LP will not waste time trying to reduce them.
Deactivate rewrite rules that are needed only occasionally.
Make definitions passive and apply them manually.
Avoid big terms, especially with associative-commutative operators. Seek different axiomatizations or proof strategies if they occur.

If ordering is costly, put ordering constraints in the registry, particularly if you have declared many operators. It may also help to put ordering constraints in the registry prior to a proof by cases to save the cost of having LP rediscover these constraints in each of the cases.

If unification or critical pairing is costly, try to use smaller rule lists as arguments to the critical-pairs command. Also, try to avoid computing critical pairs between rewrite rules that contain subterms such as t1 /\ t2 /\ ... /\ t5, with multiple occurrences of the same associative-commutative operator.