NO Problem: a() -> a() f(b(),a()) -> f(a(),b()) f(x,a()) -> b() Proof: Nonconfluence Processor: terms: f(a(),b()) *<- f(b(),a()) ->* b() Qed