Input TRS:
    1: U11(tt()) -> s(length(L))
    2: and(tt()) -> X
    3: zeros() -> cons(|0|())
    4: isNat() -> tt()
    5: isNat() -> isNatList()
    6: isNat() -> isNat()
    7: isNatIList() -> isNatList()
    8: isNatIList() -> tt()
    9: isNatIList() -> and(isNat())
    10: isNatList() -> tt()
    11: isNatList() -> and(isNat())
    12: length(nil()) -> |0|()
    13: length(cons(N)) -> U11(and(isNatList()))
Extra variable in rule 2.
NO