A proof that ran in seconds last week now runs overnight, or never finishes at all. The project question is not which engine flag to try first; it is what to measure, which reduction to apply, and when to stop and call the result inconclusive. This topic gives that project view: diagnose from numbers, split properties and parameters, and hold every run inside a budget that reports timeouts as inconclusive, never as passes.
Lesson | After it you can... |
|---|---|
Collect cone size, depth progress, and engine state, then pick the right action. | |
Replace one monolithic property with layered ones and climb a parameter ladder. | |
Set per-property budgets and report every timeout as inconclusive. |
Suggested order: top to bottom. Diagnose before you tune: most slow proofs are fixed by measuring first. The tactic lessons in the engines section carry the how; these lessons carry the when and the how-much.
The cone size per property, the depth reached against time, and what the engine reports: the diagnosis starts from those three, not from a new flag.