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