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