set(auto).

assign(constant_weight, 0).
assign(max_weight, 25).
assign(max_literals, 1).

terms(weights).
x' = x.
end_of_list.

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 (and a commuted variant)

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

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

% x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (x v (z ^ u))))        # label(H1).
 x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z))))  # label(H2).
% x ^ (y v (x ^ z)) = x ^ (y v (z ^ (y v (x ^ (z v (x ^ y))))))  # label(H3).
% x v (y ^ (x v z)) = x v (y ^ (z v (x ^ (z v y))))              # label(H55).
% x ^ (y v z) = x ^ (y v ((x v y) ^ (z v (x ^ y))))              # label(H58).

% Denial

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

end_of_list.
