NO Problem: f(f(x,y),z) -> f(x,f(y,z)) f(x,y) -> f(y,x) Proof: Containment Processor: loop length: 1 terms: f(x,y) context: [] substitution: x -> y y -> x Qed