Problem:
 a() -> c()
 a() -> f(c())
 f(x) -> f(g(x))

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