Tarski's high school algebra problem

Problem

Consider the signature with a constant $1$ and binary operations $+$, $\cdot$ and exponentiation $x^y$, interpreted in the positive integers. Let $\mathrm{HSI}$ be the following eleven identities:

1. $x + y \approx y + x$ and $(x + y) + z \approx x + (y + z)$;
2. $x \cdot 1 \approx x$, $x \cdot y \approx y \cdot x$ and $(x \cdot y) \cdot z \approx x \cdot (y \cdot z)$;
3. $x \cdot (y + z) \approx x \cdot y + x \cdot z$;
4. $1^x \approx 1$, $x^1 \approx x$, $x^{y + z} \approx x^y \cdot x^z$, $(x \cdot y)^z \approx x^z \cdot y^z$ and $(x^y)^z \approx x^{y \cdot z}$.

The problem asks whether every identity in this signature that holds in the positive integers can be derived from $\mathrm{HSI}$ in equational logic.