formulas(goals).

x * y = y * x -> (exists z (Power(x,z) & Power(y,z)))
   # label("Commutation Lemma").

end_of_list.

