(VAR x)
(RULES
   f(x,x) -> x
   f(x,e) -> x
   f(e,x) -> x
   f(x,i(x)) -> e
   f(i(x),x) -> e
)
(COMMENT p.30 of Kapur/Narendran/Otto, IC 1990)