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