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