formulas(assumptions). (x * y) * z = x * (y * z). % There is a left identity element, and every element has a left inverse. exists e ((all x (e * x = x)) & (all x exists y (y * x = e))). % So far, we have group theory. Now, state that % there are two noncommuting elements. exists a exists b (a * b != b * a). end_of_list.