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