Problem: f(a(),n__b(),X) -> f(X,X,X) c() -> a() c() -> b() b() -> n__b() activate(n__b()) -> b() activate(X) -> X Proof: Unfolding Processor: loop length: 4 terms: f(c(),c(),c()) f(c(),b(),c()) f(c(),n__b(),c()) f(a(),n__b(),c()) context: [] substitution: Qed