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