Take a set $S$ and an associative binary operation $*:S \times S \rightarrow S$ such that there exists an element $e$ such that $x * x = e$ for any $x \in S$. Can we conclude that the operation is commutative?
This question was inspired while trying to prove easy algebra statements with SPASS. The original problem supposed that $S$ was a group and $e$ the identity, but I tried to remove hypotheses and found out that the statement remains true if we simply suppose that $e$ is a left/right identity for the binary operation (still assuming that this operation is associative). Trying to remove this hypothesis made the saturation process diverge. I suppose that a counterexample exists and probably SPASS is not running with optimal settings, but I don't know how to find one.
I believe this is a counterexample.
$$ \begin{array} {r|r r r r r} * & a & b & c & d \\ \hline a & a & a & a & a \\ b & a & a & a & a \\ c & a & d & a & a \\ d & a & a & a & a \\ \end{array} $$
The hardest part is checking associativity, but a little thought reveals that $(x * y) * z = x * (y * z)$ is always $a$ (think about what $x * y$ can be and what that tells you about $(x * y) * z$).