Presburger arithmetic: is it known to be in $EXPSPACE \setminus EXP$?
The problem of determining whether a sentence of Presburger arithmetic is true is in between 2-NEXP and 2-EXPSPACE. When the number of quantifier alternations is fixed and at least two, the problem is in between NEXP and EXPSPACE. The existential fragment is NP-complete. For more details, see e.g. Christoph Haase, Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy, CSL/LICS 2014.