assign(max_seconds, 30). formulas(sos). (x * e) * x = x. x * (x * y) = y. (x * y) * (z * u) = (x * z) * (y * u). ((x * x) * x) * x = e. x * (x \ y) = y. x \ (x * y) = y. (x / y) * y = x. (x * y) / y = x. end_of_list. formulas(goals). ((x * y) * z) * u = ((u * y) * z) * x. end_of_list.