assign(max_seconds, 30). assign(eq_defs, fold). formulas(sos). % Nonassociative Ring x + 0 = x. x + -x = 0. (x + y) + z = x + (y + z). x + y = y + x. x * (y + z) = (x * y) + (x * z). (x + y) * z = (x * z) + (y * z). %%%%%%%%%%%%%%%%%%%%%%% associator(x,y,z) = ((x * y) * z) + -(x * (y * z)). %%%%%%%%%%%%%%%%%%%%%%% (x * x) * y = x * (x * y) # label(left). (x * y) * x = x * (y * x) # label(flexible). end_of_list. formulas(goals). (y * x) * x = y * (x * x) # label(right). end_of_list.