formulas(assumptions). E * x = x. x * E = x. x' * x = E. x * x' = E. (x * y) * z = x * (y * z). end_of_list. formulas(goals). x * y = y * x. end_of_list.