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.

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

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

% Denial

A ^ B = A.
A' v B' != A'.

end_of_list.
