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