I think it shows even theorem proving oracles can have a sense of humor.

I know, I know. Don't anthropomorphize AIs. They hate it when you do that.