(VAR x ) (RULES a -> b f(a,b) -> f(a,a) f(b,a) -> f(a,a) f(a,a) -> c g(x) -> f(x,x) f(b,a) -> c f(a,b) -> c f(b,b) -> f(a,a) f(b,b) -> c )