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