MAYBE
MAYBE
TRS:
 {
           zeros() -> cons(0()),
         U12(tt()) -> tt(),
       isNatList() -> tt(),
       isNatList() -> U51(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(),
   length(cons(N)) -> U61(and(and(isNatList()))),
     length(nil()) -> 0(),
         U61(tt()) -> s(length(L)),
         and(tt()) -> X,
  isNatIListKind() -> tt(),
  isNatIListKind() -> and(isNatKind()),
       isNatKind() -> tt(),
       isNatKind() -> isNatIListKind(),
       isNatKind() -> isNatKind()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
             zeros() -> cons(0()),
           U12(tt()) -> tt(),
         isNatList() -> tt(),
         isNatList() -> U51(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(),
     length(cons(N)) -> U61(and(and(isNatList()))),
       length(nil()) -> 0(),
           U61(tt()) -> s(length(L)),
           and(tt()) -> X,
    isNatIListKind() -> tt(),
    isNatIListKind() -> and(isNatKind()),
         isNatKind() -> tt(),
         isNatKind() -> isNatIListKind(),
         isNatKind() -> isNatKind()
   }
  Fail