assign(max_seconds, 300).

list(weights).
weight(x') = weight(x).
weight(x v (y v (z v u))) = 1000.
weight(x ^ (y ^ (z ^ u))) = 1000.
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.