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