Presburger arithmetic: is it known to be in $EXPSPACE \setminus EXP$? My understanding of the Presburger arithmetic decision problem is that it requires doubly-exponential time, but only singly-exponential space, meaning that it is in $EXPSPACE \setminus EXP$.  Obviously, if this set is not empty, then $P \subsetneq PSPACE$, solving a major open problem, so my understanding is probably wrong.  Where did my reasoning fail?
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.