% 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).

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.

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.