GenServer that orchestrates the proof search for a single session.

On start_proof, seeds the root branch into the ETS work queue, spawns N worker processes, and sets a timeout timer. 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.