assign(max_seconds, 30). assign(constant_weight, 0). formulas(sos). % candidate x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). end_of_list. formulas(goals). all x all y (x ^ y = x -> x' v y' = x'). % order reversibility end_of_list.