NO

Problem:
 p(x) -> q(x)
 p(x) -> r(x)
 q(x) -> s(p(x))
 r(x) -> s(p(x))
 s(x) -> f(p(x))

Proof:
 Unfolding Processor:
  loop length: 2
  terms:
   p(x3)
   q(x3)
  context: s([])
  substitution:
   x3 -> x3
  Qed