[CJefferson]

I agree. I've produced x^8 algorithms, which are already completely useless for all practical applications.

If a proof has 10,000 statements, we already couldnt generate it with an x^8 algorithm.