Problem: F(x,C(x)) -> A() F(x,x) -> B() a() -> g(C(a())) g(x) -> x Proof: Nonconfluence Processor: terms: B() *<- F(a(),C(a())) ->* A() Qed