Problem: f(g(x,a(),b())) -> x p(a()) -> c() g(f(h(c(),d())),x,y) -> h(p(x),q(x)) q(b()) -> d() Proof: Nonconfluence Processor: terms: f(h(p(a()),q(a()))) *<- f(g(f(h(c(),d())),a(),b())) ->* f(h(c(),d())) Qed