Why doesn't the decision problem for Presburger arithmetic demonstrate that $\mathsf{P} \neq \mathsf{NP}$

Question

From Wikipedia's article on Presburger arithmetic:

Then Fischer and Rabin (1974) proved that any decision algorithm for Presburger arithmetic has a worst-case runtime of at least $2^{2^{cn}}$, for some constant $c>0$. Hence, the decision problem for Presburger arithmetic is an example of a decision problem that has been proved to require more than exponential run time.

(The referenced paper is Michael J. Fischer and Michael O. Rabin, Super-Exponential Complexity of Presburger Arithmetic, Proceedings of the SIAM-AMS Symposium in Applied Mathematics 7 (1974), pp.27–41)

Some other source: "Quantifier-free Boolean Algebra with Presburger Arithmetic is NP-Complete" (Viktor Kuncak, Technical Report MIT-CSAIL-TR-2007-001, MIT CSAIL, January 2007.)

So an $\mathsf{NP}$ problem that is proved to require more than exponential time. Why doesn't this establish that $\mathsf{P} \neq \mathsf{NP}$.

Answer 1

The doubly exponential worse case runtime for deciding Presburger arithmetic theorems occurs only when nested quantifiers are used. Since the paper describes a quantifier-free version of Presburger arithmetic, the doubly exponential lower bound does not apply. We're left with the singly-exponential runtime upper-bound known for all NP-complete problems and an unknown lower-bound, leaving the P = NP question unresolved.