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.

