(VAR x)
(RULES
  f(a, f(x, a)) -> f(a, f(f(a, a), a))
)
(COMMENT UN & ~UNC)