co.combinatorics - Examples of Super-polynomial time algorithmic/induction proofs?

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).