% Case 2:  u != x * y & u != y * x 

formulas(assumptions).

   % general lemmas (proved)

   (x * y = u * v) -> ( Prefix(x,u) | Prefix(u,x) | x = u ) # label("Lemma 1").

   Prefix(x,y) -> Shorter(x,y) # label("Lemma 2").

   % hypothesis

   Power(U * U1,X).
   Power(U * U2,Y).
   U = X * U3.
   U = Y * U4.
   -Shorter(U, X * Y).
   U != X * Y.          % Case 2 assumption
   U != Y * X.          % Case 2 assumption
   U = (X * Y) * U5.    % Lemma Case2a
   U = (Y * X) * U6.    % Lemma Case2b

   % negation of the conclusion

   X * Y != Y * X.      % Case 2

end_of_list.
