assign(max_seconds, 30).

formulas(sos).

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

end_of_list.

formulas(goals).

x ^ (y v (z ^ u)) = x ^ (y v (z ^ (y v (u ^ (y v z))))) # answer(H34).

end_of_list.