assign(max_seconds, 60).

assign(max_weight, 25).

assign(constant_weight, 0).

assign(nest_penalty, 2).

formulas(sos).

% candidate

x ^ (y v (x ^ z)) = x ^ (y v (x ^ ((x ^ y) v (z ^ (x v y))))) # label(H7).

end_of_list.

formulas(goals).

all x all y (x ^ y = x -> x' v y' = x').  % order reversibility

end_of_list.
