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