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