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