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