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. clauses(sos). x ^ (y v (z ^ (x v u))) = x ^ ((x ^ (y v (x ^ z))) v (z ^ u)) # label(H79). A ^ (B v (C ^ (B v D))) != A ^ (B v (C ^ (D v (A ^ B)))) # answer(H76). end_of_list.