CeTA: 1: error when switching from the TRS
and(true) -> X
if(true) -> X
if(false) -> Y
add(0) -> X
and(false) -> false
add(s) -> s
first(0,X) -> nil
first(s,cons) -> cons
from -> cons

to the initial DP problem
dependency pairs: 

rewrite system:
and(true) -> X
if(true) -> X
if(false) -> Y
add(0) -> X
and(false) -> false
add(s) -> s
first(0,X) -> nil
first(s,cons) -> cons
from -> cons

the DP-transformation is not applied correctly.
the TRS is not well-formed
the variable X occurs only in the right-hand side of rule and(true) -> X