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