(VAR x)
(RULES
  f(a, f(a, x)) -> f(f(a, a), a)
)
(COMMENT NFP & ~CR)