NO Problem: a(x) -> b(x) b(b(c(x))) -> c(a(c(a(a(x))))) c(c(x)) -> x Proof: Nonconfluence Processor: terms: b(b(x109)) *<- b(b(c(c(x109)))) ->* b(c(b(b(b(b(x109)))))) Qed