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