In combinatorics, one can sometimes get an *algorithmic proof*, which loosely has the following form:

-The proof moves through stages

-An invariant is shown to hold by induction from previous stages

-The algorithm is shown to terminate

-The invariant holding at termination implies the desired claim.

Perhaps the best example I know of is an algorithmic proof of Konig's theorem, which in a sense is just a max-flow/min-cut algorithm. In some sense, most induction proofs fit this mold.

The above example runs in polynomial time. Are there good examples of algorithmic/induction proofs that take *super-polynomial* time to prove things that don't obviously need such induction?

That is, I *don't* want Ackermann-like recurrences, or anything that is "brute-force". Further, I'm not looking for super-polynomial time algorithms that solve instances of problems, but rather am looking for super-polynomial time algorithms that prove a theorem of some sort (eg. like a combinatorial max-min theorem in the above example).