assign(max_seconds, 120).

formulas(sos).

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

end_of_list.

formulas(goals).

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

end_of_list.