"Natural" decidable problems known not to be in NP. Every time I teach NP-Completeness, students ask "are there any problems that are known to not belong to NP?"

How would you answer?  I usually give them an undecidable problem as an example, but this often doesn't turn out well: (a) if I give them the Halting Problem they think it's some dumb corner case, and (b) if I give them Diophantine Equations they don't see why it's not in NP (you can check solutions in poly-time... just plug them in!  I have a hard time disabusing them of this approach.)

I'd like to give them something like QBF as an example, but there is no proven separation.

Suggestions?
One possibility is a problem that is EXPSPACE-complete. NP is trivially in PSPACE, which is strictly contained in EXPSPACE. One problem that is EXPSPACE-complete is deciding whether a regular expression that allows exponentiation is all of $\Sigma^*$.