A left distributive algebra is a set $A$ together with a binary operation, $\cdot$, satisfying $a\cdot(b\cdot c)=(a\cdot b)\cdot(a\cdot c)$.
One important example of left distributive algebras arises in set theory. For $\lambda$ a limit cardinal let $\mathcal{E}_\lambda$ be the set of elementary embeddings $j: V_\lambda\rightarrow V_\lambda$. Suppose $\lambda$ is such that $\mathcal{E}_\lambda\not=\emptyset$ (this is a very large cardinal axiom, called "rank-into-rank" or more precisely "$I_3$"). Then for $j, k\in \mathcal{E}_\lambda$, we can define $$j\cdot k=\bigcup_{\alpha<\lambda}j(k\cap V_\alpha)$$ where we view $k$ as a set of ordered pairs, so that $k\subset V_{\lambda+1}$. Then it turns out that $j\cdot k\in\mathcal{E}_\lambda$ and that $(\mathcal{E}_\lambda, \cdot)$ is a left distributive algebra. Fixing $j\in\mathcal{E}_\lambda$ and letting $\mathcal{A}_j$ be the closure of $\{j\}$ in $\mathcal{E}_\lambda$, Laver (1992, http://www.sciencedirect.com/science/article/pii/000187089290016E#) proved that $\mathcal{A}_j$ is the free left distributive algebra on one generator. He also showed (under the assumption that such a $j$ exists, that is, $I_3$) that the word problem for the free left distributive algebra on one generator is decidable.
There has been extensive work on the strength of various results around left distributive algebras. My question is about this last point:
Is it known (within ZFC) if the word problem for the free left distributive algebra with one generator is decidable?
Since the only proof of decidability I know of uses the normal form theorem, I suspect the answer is no, but I haven't been able to find out myself.
Note: I've tagged this "universal algebra" as that seemed the most relevant algebraic tag. If there is a better tag, or if this tag is just too irrelevant, feel free to replace/remove it.