Next I'll tell you how to generate invariants with universal quantifiers by using an interpolating prover, straight from the "best paper" at TACAS.
And now some off topic stuff.
Since we are talking about puzzles, here's another one I saw recently. It was previously featured on xkcd and it is also featured by one of the toilets in the CASL. It didn't excite me before I saw the (intentionally) wrong solution of Terence Tao. The fact that the error is so subtle made me think that I got the correct answer in the first place by accident :)