clauses(sos).

% candidate

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

end_of_list.

clauses(goals).

x ^ (y v z) = (x ^ y) v (x ^ z) # answer(distributivity).

end_of_list.