assign(max_seconds, 300).
assign(constant_weight, 0).

list(weights).
weight(x') = weight(x).
end_of_list.

formulas(sos).

% candidate

x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (y ^ (x v u))))) # label(H78).

end_of_list.

formulas(goals).

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

end_of_list.
