A "natural" decidable problem not in $\mathsf{NP}$? Are there any "natural" examples of decidable problems that are definitively known not to be in NP?  The decidable languages I know of that are not contained in NP are usually derived from the time hierarchy theorem, which produces "artificial" languages based on diagonalization.
From an answer to a related question on NP-hard problems which are not contained in NP: probably the most natural example is determining whether two regular expressions (including the Kleene star for arbitrary repetition, and a squaring operation to allow compact expressions of very large fixed numbers of repetitions) are equivalent. The resulting problem is EXPSPACE complete. Because EXPSPACE contains NEXP, which contains NP strictly (by the time hierarchy theorem), this is a decideable problem which is not in NP.