assign(order, kbo).

formulas(sos).

% Ring Theory (associative)

x + 0 = x.
x + (-x) = 0.
(x + y) + z = x + (y + z).
x + y = y + x.

x * (y + z) = (x * y) + (x * z).
(x + z) * y = (x * y) + (z * y).

(x * y) * z = x * (y * z).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

x * (x * x) = x.  % hypothesis  xxx=x

A * B != B * A.   % denial of commutativity

end_of_list.