assign(max_seconds, 30).

% Prove that (x*y)*(z*u) = (x*z)*(y*u) implies (x(yz))((uv)w) = (x(uz)) 
% ((yv)w) in cancellation groupoids with an idempotent or under (gL)  
% but not in general.

formulas(sos).

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

end_of_list.

formulas(sos).

  (x * y) * (z * u) = (x * z) * (y * u).

% e * e = e.

end_of_list.

formulas(goals).

  (x * (y * z)) * ((u * v) * w) = (x * (u * z)) * ((y * v) * w).

end_of_list.

