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