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.