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