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