(VAR x y)
(RULES
  f(a,f(a,f(a,f(x,b)))) -> f(f(a,f(a,f(a,x))),b)
  f(f(f(a,x),b),b) -> f(f(a,f(f(x,b),b)),b)
)