clauses(sos).

% candidate

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

end_of_list.

formulas(goals).

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

end_of_list.