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.