set(auto). assign(nest_penalty, 2). assign(max_weight, 25). assign(max_seconds, 3600). set(x_proofs). clauses(sos). % lattice theory x v y = y v x. (x v y) v z = x v (y v z). x ^ y = y ^ x. (x ^ y) ^ z = x^ (y ^ z). x ^ (x v y) = x. x v (x ^ y) = x. end_of_list.