MAYBE
MAYBE
TRS:
 {
              zeros() -> cons(0()),
            U12(tt()) -> tt(),
          isNatList() -> tt(),
          isNatList() -> U51(and(isNatKind())),
          isNatList() -> U61(and(isNatKind())),
            U11(tt()) -> U12(isNatList()),
            U22(tt()) -> tt(),
              isNat() -> U11(isNatIListKind()),
              isNat() -> tt(),
              isNat() -> U21(isNatKind()),
            U21(tt()) -> U22(isNat()),
            U32(tt()) -> tt(),
            U31(tt()) -> U32(isNatList()),
            U42(tt()) -> U43(isNatIList()),
            U41(tt()) -> U42(isNat()),
            U43(tt()) -> tt(),
         isNatIList() -> tt(),
         isNatIList() -> U31(isNatIListKind()),
         isNatIList() -> U41(and(isNatKind())),
            U52(tt()) -> U53(isNatList()),
            U51(tt()) -> U52(isNat()),
            U53(tt()) -> tt(),
            U62(tt()) -> U63(isNatIList()),
            U61(tt()) -> U62(isNat()),
            U63(tt()) -> tt(),
      length(cons(N)) -> U71(and(and(isNatList()))),
        length(nil()) -> 0(),
            U71(tt()) -> s(length(L)),
            U81(tt()) -> nil(),
            U91(tt()) -> cons(N),
            and(tt()) -> X,
     isNatIListKind() -> tt(),
     isNatIListKind() -> and(isNatKind()),
          isNatKind() -> tt(),
          isNatKind() -> isNatIListKind(),
          isNatKind() -> isNatKind(),
        take(0(), IL) -> U81(and(isNatIList())),
  take(s(M), cons(N)) -> U91(and(and(isNatIList())))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                zeros() -> cons(0()),
              U12(tt()) -> tt(),
            isNatList() -> tt(),
            isNatList() -> U51(and(isNatKind())),
            isNatList() -> U61(and(isNatKind())),
              U11(tt()) -> U12(isNatList()),
              U22(tt()) -> tt(),
                isNat() -> U11(isNatIListKind()),
                isNat() -> tt(),
                isNat() -> U21(isNatKind()),
              U21(tt()) -> U22(isNat()),
              U32(tt()) -> tt(),
              U31(tt()) -> U32(isNatList()),
              U42(tt()) -> U43(isNatIList()),
              U41(tt()) -> U42(isNat()),
              U43(tt()) -> tt(),
           isNatIList() -> tt(),
           isNatIList() -> U31(isNatIListKind()),
           isNatIList() -> U41(and(isNatKind())),
              U52(tt()) -> U53(isNatList()),
              U51(tt()) -> U52(isNat()),
              U53(tt()) -> tt(),
              U62(tt()) -> U63(isNatIList()),
              U61(tt()) -> U62(isNat()),
              U63(tt()) -> tt(),
        length(cons(N)) -> U71(and(and(isNatList()))),
          length(nil()) -> 0(),
              U71(tt()) -> s(length(L)),
              U81(tt()) -> nil(),
              U91(tt()) -> cons(N),
              and(tt()) -> X,
       isNatIListKind() -> tt(),
       isNatIListKind() -> and(isNatKind()),
            isNatKind() -> tt(),
            isNatKind() -> isNatIListKind(),
            isNatKind() -> isNatKind(),
          take(0(), IL) -> U81(and(isNatIList())),
    take(s(M), cons(N)) -> U91(and(and(isNatIList())))
   }
  Fail