Fischer and Rabin proved a superexponential bound $2^{2^{cn}}$ for the worst-case length of a proof of a proposition of length $n$ in Presburger arithmetic.  The result is in

>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.

Are there any explicit positive lower bounds for the constant $c>0$ in their estimate?

This was asked [on MSE](https://math.stackexchange.com/questions/4994818/explicit-bound-for-superexponential-estimate-for-presburger-arithmetic) without input.