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