(VAR X) (RULES f(a,b,X) -> f(X,X,X) c -> a c -> b )