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.