assign(max_seconds, 30).

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


formulas(sos).

x * (x \ y) = y.
x \ (x * y) = y.
(x / y) * y = x.
(x * y) / y = x.

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

end_of_list.

formulas(goals).

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

end_of_list.