MAYBE
MAYBE
TRS:
 {
              zeros() -> cons(0()),
           U102(tt()) -> U103(isNatIListKind()),
          isNatKind() -> tt(),
          isNatKind() -> U71(isNatIListKind()),
          isNatKind() -> U81(isNatKind()),
           U101(tt()) -> U102(isNatKind()),
           U103(tt()) -> U104(isNatIListKind()),
     isNatIListKind() -> tt(),
     isNatIListKind() -> U51(isNatKind()),
     isNatIListKind() -> U61(isNatKind()),
           U104(tt()) -> U105(isNat()),
           U105(tt()) -> U106(isNatIList()),
              isNat() -> tt(),
              isNat() -> U11(isNatIListKind()),
              isNat() -> U21(isNatKind()),
           U106(tt()) -> tt(),
         isNatIList() -> tt(),
         isNatIList() -> U31(isNatIListKind()),
         isNatIList() -> U41(isNatKind()),
            U12(tt()) -> U13(isNatList()),
            U11(tt()) -> U12(isNatIListKind()),
           U112(tt()) -> U113(isNat()),
           U111(tt()) -> U112(isNatIListKind()),
           U113(tt()) -> U114(isNatKind()),
           U114(tt()) -> s(length(L)),
      length(cons(N)) -> U111(isNatList()),
        length(nil()) -> 0(),
            U13(tt()) -> tt(),
          isNatList() -> U101(isNatKind()),
          isNatList() -> tt(),
          isNatList() -> U91(isNatKind()),
           U122(tt()) -> nil(),
           U121(tt()) -> U122(isNatIListKind()),
           U132(tt()) -> U133(isNat()),
           U131(tt()) -> U132(isNatIListKind()),
           U133(tt()) -> U134(isNatKind()),
           U134(tt()) -> U135(isNat()),
           U135(tt()) -> U136(isNatKind()),
           U136(tt()) -> cons(N),
            U22(tt()) -> U23(isNat()),
            U21(tt()) -> U22(isNatKind()),
            U23(tt()) -> tt(),
            U32(tt()) -> U33(isNatList()),
            U31(tt()) -> U32(isNatIListKind()),
            U33(tt()) -> tt(),
            U42(tt()) -> U43(isNatIListKind()),
            U41(tt()) -> U42(isNatKind()),
            U43(tt()) -> U44(isNatIListKind()),
            U44(tt()) -> U45(isNat()),
            U45(tt()) -> U46(isNatIList()),
            U46(tt()) -> tt(),
            U52(tt()) -> tt(),
            U51(tt()) -> U52(isNatIListKind()),
            U62(tt()) -> tt(),
            U61(tt()) -> U62(isNatIListKind()),
            U71(tt()) -> tt(),
            U81(tt()) -> tt(),
            U92(tt()) -> U93(isNatIListKind()),
            U91(tt()) -> U92(isNatKind()),
            U93(tt()) -> U94(isNatIListKind()),
            U94(tt()) -> U95(isNat()),
            U95(tt()) -> U96(isNatList()),
            U96(tt()) -> tt(),
        take(0(), IL) -> U121(isNatIList()),
  take(s(M), cons(N)) -> U131(isNatIList())
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                zeros() -> cons(0()),
             U102(tt()) -> U103(isNatIListKind()),
            isNatKind() -> tt(),
            isNatKind() -> U71(isNatIListKind()),
            isNatKind() -> U81(isNatKind()),
             U101(tt()) -> U102(isNatKind()),
             U103(tt()) -> U104(isNatIListKind()),
       isNatIListKind() -> tt(),
       isNatIListKind() -> U51(isNatKind()),
       isNatIListKind() -> U61(isNatKind()),
             U104(tt()) -> U105(isNat()),
             U105(tt()) -> U106(isNatIList()),
                isNat() -> tt(),
                isNat() -> U11(isNatIListKind()),
                isNat() -> U21(isNatKind()),
             U106(tt()) -> tt(),
           isNatIList() -> tt(),
           isNatIList() -> U31(isNatIListKind()),
           isNatIList() -> U41(isNatKind()),
              U12(tt()) -> U13(isNatList()),
              U11(tt()) -> U12(isNatIListKind()),
             U112(tt()) -> U113(isNat()),
             U111(tt()) -> U112(isNatIListKind()),
             U113(tt()) -> U114(isNatKind()),
             U114(tt()) -> s(length(L)),
        length(cons(N)) -> U111(isNatList()),
          length(nil()) -> 0(),
              U13(tt()) -> tt(),
            isNatList() -> U101(isNatKind()),
            isNatList() -> tt(),
            isNatList() -> U91(isNatKind()),
             U122(tt()) -> nil(),
             U121(tt()) -> U122(isNatIListKind()),
             U132(tt()) -> U133(isNat()),
             U131(tt()) -> U132(isNatIListKind()),
             U133(tt()) -> U134(isNatKind()),
             U134(tt()) -> U135(isNat()),
             U135(tt()) -> U136(isNatKind()),
             U136(tt()) -> cons(N),
              U22(tt()) -> U23(isNat()),
              U21(tt()) -> U22(isNatKind()),
              U23(tt()) -> tt(),
              U32(tt()) -> U33(isNatList()),
              U31(tt()) -> U32(isNatIListKind()),
              U33(tt()) -> tt(),
              U42(tt()) -> U43(isNatIListKind()),
              U41(tt()) -> U42(isNatKind()),
              U43(tt()) -> U44(isNatIListKind()),
              U44(tt()) -> U45(isNat()),
              U45(tt()) -> U46(isNatIList()),
              U46(tt()) -> tt(),
              U52(tt()) -> tt(),
              U51(tt()) -> U52(isNatIListKind()),
              U62(tt()) -> tt(),
              U61(tt()) -> U62(isNatIListKind()),
              U71(tt()) -> tt(),
              U81(tt()) -> tt(),
              U92(tt()) -> U93(isNatIListKind()),
              U91(tt()) -> U92(isNatKind()),
              U93(tt()) -> U94(isNatIListKind()),
              U94(tt()) -> U95(isNat()),
              U95(tt()) -> U96(isNatList()),
              U96(tt()) -> tt(),
          take(0(), IL) -> U121(isNatIList()),
    take(s(M), cons(N)) -> U131(isNatIList())
   }
  Fail