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


formulas(sos).

all x all y all z (x * y = x * z -> y = z).

all x all y all z (y * x = z * x -> y = z).

end_of_list.

clauses(sos).

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

end_of_list.

clauses(goals).

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

end_of_list.