MAYBE
MAYBE
TRS:
 {
           zeros() -> cons(0()),
         U12(tt()) -> U13(isNatList()),
  isNatIListKind() -> tt(),
  isNatIListKind() -> U51(isNatKind()),
         U11(tt()) -> U12(isNatIListKind()),
         U13(tt()) -> tt(),
       isNatList() -> tt(),
       isNatList() -> U81(isNatKind()),
         U22(tt()) -> U23(isNat()),
       isNatKind() -> tt(),
       isNatKind() -> U61(isNatIListKind()),
       isNatKind() -> U71(isNatKind()),
         U21(tt()) -> U22(isNatKind()),
         U23(tt()) -> tt(),
           isNat() -> U11(isNatIListKind()),
           isNat() -> tt(),
           isNat() -> U21(isNatKind()),
         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(),
      isNatIList() -> tt(),
      isNatIList() -> U31(isNatIListKind()),
      isNatIList() -> U41(isNatKind()),
         U52(tt()) -> tt(),
         U51(tt()) -> U52(isNatIListKind()),
         U61(tt()) -> tt(),
         U71(tt()) -> tt(),
         U82(tt()) -> U83(isNatIListKind()),
         U81(tt()) -> U82(isNatKind()),
         U83(tt()) -> U84(isNatIListKind()),
         U84(tt()) -> U85(isNat()),
         U85(tt()) -> U86(isNatList()),
         U86(tt()) -> tt(),
         U92(tt()) -> U93(isNat()),
         U91(tt()) -> U92(isNatIListKind()),
         U93(tt()) -> U94(isNatKind()),
         U94(tt()) -> s(length(L)),
   length(cons(N)) -> U91(isNatList()),
     length(nil()) -> 0()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
             zeros() -> cons(0()),
           U12(tt()) -> U13(isNatList()),
    isNatIListKind() -> tt(),
    isNatIListKind() -> U51(isNatKind()),
           U11(tt()) -> U12(isNatIListKind()),
           U13(tt()) -> tt(),
         isNatList() -> tt(),
         isNatList() -> U81(isNatKind()),
           U22(tt()) -> U23(isNat()),
         isNatKind() -> tt(),
         isNatKind() -> U61(isNatIListKind()),
         isNatKind() -> U71(isNatKind()),
           U21(tt()) -> U22(isNatKind()),
           U23(tt()) -> tt(),
             isNat() -> U11(isNatIListKind()),
             isNat() -> tt(),
             isNat() -> U21(isNatKind()),
           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(),
        isNatIList() -> tt(),
        isNatIList() -> U31(isNatIListKind()),
        isNatIList() -> U41(isNatKind()),
           U52(tt()) -> tt(),
           U51(tt()) -> U52(isNatIListKind()),
           U61(tt()) -> tt(),
           U71(tt()) -> tt(),
           U82(tt()) -> U83(isNatIListKind()),
           U81(tt()) -> U82(isNatKind()),
           U83(tt()) -> U84(isNatIListKind()),
           U84(tt()) -> U85(isNat()),
           U85(tt()) -> U86(isNatList()),
           U86(tt()) -> tt(),
           U92(tt()) -> U93(isNat()),
           U91(tt()) -> U92(isNatIListKind()),
           U93(tt()) -> U94(isNatKind()),
           U94(tt()) -> s(length(L)),
     length(cons(N)) -> U91(isNatList()),
       length(nil()) -> 0()
   }
  Fail