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.