Major Section: CHECKPOINTS
By evaluating (print-checkpoints t) one can get trace-like information
about prover functions, including time summaries, printed to the screen
during a proof. To turn off this feature, evaluate
(print-checkpoints nil). Also See checkpoints.