We consider a technique for liveness and termination proofs that reduces temporal proofs to verification conditions in uninterpreted first-order logic based on a suitable notion of a fair abstract lasso. It was previously shown that temporal prophecy makes the technique more powerful, essentially empowering it to prove termination of nested loops. In this paper we show that temporal prophecy is even more powerful than previously demonstrated: it can even prove termination of the Ackermann function, which is not primitive recursive, and essentially represents “infinitely-many” nested loops.