It takes programs from a restricted language in which all programs provably terminate. It doesn't take arbitrary programs and search for termination proofs relative to a powerful proof system. There's, um... a really really really LARGE difference.
Based on the way that sort of termination proof usually works, I'd guess there are some simple tree ordinals which grow faster than that language, and that a program based on them would defeat the winner, but I haven't looked into it in detail so it's only a guess.
