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