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