y = y.
y = y.
(x v (v ^ ((x ^ z) v (x ^ u)))) ^ (w v ((x v v6) ^ (x v v7))) = x.
(x v (v ^ ((x ^ z) v (x ^ u)))) ^ (v7 v ((x v w) ^ (x v v6))) = x.
% rewriter lattice.rules: rewrote 4 terms with 42 rewrite steps in 0.01 seconds.