(VAR x0)
(RULES
  a -> a
  a -> b
  a -> f(a, a)
  f(b, b) -> f(a, a)
  f(x0, a) -> f(a, b)
)
(COMMENT -f "a:0 b:0 f:2" -r 5 "UN & ~UNC & ~SN")