Problem: f(c()) -> g(c()) g(c()) -> f(c()) c() -> d() Proof: Nonconfluence Processor: terms: f(d()) *<- f(c()) ->* g(d()) Qed