% *****************************************************
% M3 => M4, pure
% *****************************************************

assign(order, kbo).

% helpful in this case
set(para_from_small).

% hint matchers can be deleted by weight
set(limit_hint_matchers).

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 * (x * z)) = ((x * y) * x) * z # label("M3").

end_of_list.

formulas(goals).

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

end_of_list.

formulas(hints).

   % assign these clauses high weight if they appear

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

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

end_of_list.
