CeTA: 1: error when switching from the TRS 2nd(cons(X)) -> 2nd(cons1(X,X1)) 2nd(cons1(X,cons(Y))) -> Y from(X) -> cons(X) to the initial DP problem dependency pairs: 2nd#(cons(X)) -> 2nd#(cons1(X,X1)) rewrite system: 2nd(cons(X)) -> 2nd(cons1(X,X1)) 2nd(cons1(X,cons(Y))) -> Y from(X) -> cons(X) the DP-transformation is not applied correctly. the TRS is not well-formed the variable X1 occurs only in the right-hand side of rule 2nd(cons(X)) -> 2nd(cons1(X,X1))