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 (z ^ ((x ^ (y v z)) v (y ^ z)))) = x ^ (y v (x ^ z))  # label(H2).
  x ^ (y v (z ^ (y v (x ^ (z v (x ^ y)))))) = x ^ (y v (x ^ z))  # label(H3).

  A ^ (B v (C ^ ((A ^ (B v C)) v (B ^ C)))) != A ^ (B v (A ^ C))  # label(H2_denial).
% A ^ (B v (C ^ (B v (A ^ (C v (A ^ B)))))) != A ^ (B v (A ^ C))  # label(H3_denial).

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

% x v (y ^ (z v (x ^ (z v y)))) = x v (y ^ (x v z))              # label(H55).
% x ^ (y v ((x v y) ^ (z v (x ^ y)))) = x ^ (y v z)              # label(H58).

% A v (B ^ (C v (A ^ (C v B)))) != A v (B ^ (A v C))              # label(H55_denial).
% A ^ (B v ((A v B) ^ (C v (A ^ B)))) != A ^ (B v C)              # label(H58_denial).

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

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

% A ^ (B v (A ^ (C v (A ^ B)))) != A ^ (B v C)                    # label(H68_denial).
% (A ^ (C v (A ^ B))) v (A ^ (B v (A ^ C))) != A ^ (B v C)        # label(H69_denial).

end_of_list.
