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.