Problem:
f(X) -> f(c())
c() -> b()
Proof:
Containment Processor: loop length: 1
terms:
f(X)
context: []
substitution:
X -> c()
Qed