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