% *****************************************************
% M1 => M2, unconstrained
% *****************************************************

assign(order, kbo).

% no given selection preference for hint matchers
assign(hints_part,0).

formulas(sos).

   x * rs(x,y) = y   # label("right solvable").
   rs(x, x * y) = y  # label("right solution is unique").
   ls(x,y) * y = x   # label("left solvable").
   ls(x * y, y) = x  # label("left solution is unique").

   1 * x = x         # label("left identity").
   x * 1 = x         # label("right identity").

   (x * y) * (z * x) = (x * (y * z)) * x # label("M1").

end_of_list.

formulas(goals).

   ((x * y) * z) * y = x * (y * (z * y)) # label("M2").

end_of_list.

formulas(hints).

   % label these clauses if they appear

   x * (y * (x * z)) = ((x * y) * x) * z # label("M3").

   x * ((y * z) * x) = (x * y) * (z * x) # label("M4").

end_of_list.
