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.

% This is a Mace4 input, so we can assume lattices are finite
% and include 0 and 1.  This doesn't speed up Mace4 in this
% case; it just forces the top to be 1 and the bottom to be 0.

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

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

% (x ^ y) v (x ^ z) = x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z))))   # label(H18).
% A ^ (B v (A ^ C)) != A ^ (B v (C ^ (B v (A ^ (C v (A ^ B))))))  # label(H3_denial).

% x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (x ^ y))))         # label(H76).
% A ^ (B v C) != (A ^ (C v (A ^ B))) v (A ^ (B v (A ^ C)))        # label(H69_denial).

% x ^ (y v (z ^ (x v u))) = x ^ ((x ^ (y v (x ^ z))) v (z ^ u))   # label(H79).
% A ^ (B v C) != (A ^ (C v (A ^ B))) v (A ^ (B v (A ^ C)))        # label(H69_denial).

  (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y)))         # label(H82).
  A ^ (B v (A ^ C)) != A ^ (B v (C ^ (B v (A ^ (C v (A ^ B))))))  # label(H3_denial).

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

end_of_list.
