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