
% Prove that x*(y*(y*x)) = y*x  implies y*(y*x) = x*y in quasigroups  
% but not in cancellative groupoids.


formulas(sos).

  x * y = x * z -> y = z.
  y * x = z * x -> y = z.

end_of_list.

formulas(sos).

  x * (y * (y * x)) = y * x.

end_of_list.

formulas(goals).

  y * (y * x) = x * y.

end_of_list.

