formulas(sos).

% Nonassociative Ring

  x + 0 = x.
  x + -x = 0.
  (x + y) + z = x + (y + z).
  x + y = y + x.

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

%%%%%%%%%%%%%%%%%%%%%%%

  (x * x) * y = x * (x * y) # label(left).
% (x * y) * x = x * (y * x) # label(flexible).

end_of_list.

formulas(goals).

  (y * x) * x = y * (x * x) # label(right).

end_of_list.