set(auto).

clauses(sos).

% Lattice Theory

x v y = y v x.
x ^ y = y ^ x.
(x v y) v z = x v (y v z).
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (x v y) = x.
x v (x ^ y) = x.

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

(x ^ (y v (x ^ z))) v (x ^ (z v (x ^ y))) = x ^ (z v y) # label(H69).

% Denial of Modularity

(A v B) ^ (A v C) != A v (C ^ (A v B)) # answer(Modularity).

end_of_list.
