In this case, we have the much simpler equational theory of positive integers under addition, multiplication, and exponentiation, which does not include any quantifiers. In fact, Gurevič showed that this theory is decidable [0]. On the other hand, Gurevič later showed that this theory is not finitely axiomatizable [1], so an infinite (but still computable) set of axioms is needed to fully characterize the theory.
[0] R. Gurevič, Equational theory of positive numbers with exponentiation, 1985, https://doi.org/10.2307/2044966
[1] R. Gurevič, Equational theory of positive numbers with exponentiation is not finitely axiomatizable, 1990, https://doi.org/10.1016/0168-0072(90)90049-8