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.