CeTA: 1: error when switching from the TRS tail(cons(X)) -> Y if(true) -> X if(false) -> Y primes -> sieve(from(s(s(0)))) from(X) -> cons(X) head(cons(X)) -> X filter(s(s(X)),cons(Y)) -> if(divides(s(s(X)),Y)) sieve(cons(X)) -> cons(X) to the initial DP problem dependency pairs: filter#(s(s(X)),cons(Y)) -> if#(divides(s(s(X)),Y)) primes# -> from#(s(s(0))) primes# -> sieve#(from(s(s(0)))) rewrite system: tail(cons(X)) -> Y if(true) -> X if(false) -> Y primes -> sieve(from(s(s(0)))) from(X) -> cons(X) head(cons(X)) -> X filter(s(s(X)),cons(Y)) -> if(divides(s(s(X)),Y)) sieve(cons(X)) -> cons(X) the DP-transformation is not applied correctly. the TRS is not well-formed the variable Y occurs only in the right-hand side of rule tail(cons(X)) -> Y