Messages about expensive use of the tau-system
During a proof you may see a message such as the following.
TIME-TRACKER-NOTE [:TAU]: Elapsed runtime in tau is 4.95 secs; see :DOC time-tracker-tau.
Just below a proof summary you may see a message such as the following.
TIME-TRACKER-NOTE [:TAU]: For the proof above, the total runtime spent in the tau system was 30.01 seconds. See :DOC time-tracker-tau.
Both of these messages are intended to let you know that certain prover heuristics (see tau-system) may be slowing proofs down more than they are helping. If you are satisfied with the prover's performance, you may ignore these messages or even turn them off by disabling time-tracking entirely (see time-tracker). Otherwise, here are some actions that you can take to solve such a performance problem.
The simplest solution is to disable the tau-system, in either of the following equivalent ways.
(in-theory (disable (:executable-counterpart tau-system))) (in-theory (disable (tau-system)))
But if you want to leave the tau-system enabled, you could investigate the
possibility is that the tau-system is causing an expensive
(in-theory (disable (:executable-counterpart foo))) (in-theory (disable (:e foo))) (in-theory (disable (foo)))
As a result, the tau-system will be weakened, but perhaps only negligibly.
A more sophisticated solution is to record values of the