GenServer that orchestrates the proof search for a single session.

On start_proof, arms the deadline, then builds the root branch in a supervised task and spawns N workers once it lands. Workers report back as idle when their queue empties; once all workers stall the Manager triggers iterative deepening by incrementing the gamma and prim-subst limits and waking the parked branches. The final proof result is returned synchronously to the caller of start_proof.

The deadline is enforced against the wall clock at the head of every callback, not by the :timeout message alone — see on_deadline/3. Every step this process runs on a proof's behalf must therefore stay bounded, or it defers the deadline it is meant to enforce.