set(auto).

assign(constant_weight, 0).

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.

% Unique Complementation (UC)

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

% Denial of property x ^ y = x ==> x' v y' = x

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

% Huntington implications

 x v y != x v z | x v (y ^ z) = x v y                      # label(SD_join).
% x v y != x v z | x ^ (y v z) = (x ^ y) v (x ^ z)          # label(CD_join).
% x v y != x v z | x ^ ((x ^ y) v z) = (x ^ y) v (x ^ z)    # label(CM_join).

end_of_list.
