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.