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.

% Complement

x v x' = 1.
x ^ x' = 0.

% UC Lattice

x v y != 1 | x ^ y != 0 | x' = y.

% Modularity

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

% x v (y ^ (x v z)) = x v (z ^ (x v y)) # label(Modularity2).

% Denial of Distributivity

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

end_of_list.
