Problem:
 a(x) -> b(b(b(x)))
 a(x) -> c(x)
 b(x) -> b(x)

Proof:
 Nonconfluence Processor:
  terms: c(f3()) *<- a(f3()) ->* b(b(b(f3())))
  Qed