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