Consider the identity $C$ $$(x+y)\times(y+z)=(x\times y)+(y\times z).$$
Is the problem of determining whether an identity is a consequence of $C$ in universal algebra a polynomial time problem? This problem is in PSPACE since if $p=q$ is a consequence of $C$, then the terms $p$ and $q$ must have the same length and $q$ can be obtained from $p$ by just repeatedly replacing the operation $+$ with $\times$ and vice versa.
Algebras that satisfy identity $C$ are precisely the algebraic structures that can be used to produce commuting one-dimensional cellular automata (these cellular automata have two dimensions of time).
Note: We do not assume that the operations $+,\times$ are associative, commutative, or distributive in any way.
- Moore, Cristopher; Boykett, Timothy. Commuting cellular automata. Complex Systems 11 (1997), no. 1, 55–64.