A “natural” decidable problem not in $\mathsf{NP}$? [duplicate]

Question

This question already has an answer here:

• NP-Hard problems that are not in NP but decidable 2 answers

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.

Answer 1

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.

Answer 2

a variation of Posts Correspondence Problem for bounded length input (but not the standard "bounded" version eg in Garey/Johnson that is called "bounded PCP" that limits the number of blocks in the solution to the cardinality of the block set) is complete for NEXPSpace and therefore larger than NP which is properly in Pspace. [1]

ie let there also be an input parameter $n$ specified in binary that determines the maximal length of the PCP answer. this is apparently complete for NEXPSpace via a straightfwd proof. havent seen a proof in the literature. it proceeds in a way similar to the construction relating it to TMs in [2]

note that all problems that are known to be larger than NP are also larger than PSpace. otherwise it (a proof of a language that is not in NP but is still in PSpace) might be something close to a coNP$\neq$NP and therefore also P$\neq$NP proof (because P is closed under complement), or resolve some other "nearby" currently open complexity class separation.

[1] Decidable restrictions of the Post Correspondence Problem

[2] A polynomial reduction from any NP-complete problem to bounded PCP