NO Problem: a() -> a() f(b(),x) -> b() f(x,a()) -> a() Proof: Ground Confluence Processor: not UNC by decision procedure. (shallow, linear)