MAYBE
MAYBE
TRS:
 {
          zeros() -> cons(0()),
        U11(tt()) -> tt(),
        U21(tt()) -> tt(),
        U31(tt()) -> tt(),
        U42(tt()) -> tt(),
     isNatIList() -> tt(),
     isNatIList() -> U31(isNatList()),
     isNatIList() -> U41(isNat()),
        U41(tt()) -> U42(isNatIList()),
        U52(tt()) -> tt(),
      isNatList() -> tt(),
      isNatList() -> U51(isNat()),
        U51(tt()) -> U52(isNatList()),
        U62(tt()) -> s(length(L)),
          isNat() -> tt(),
          isNat() -> U11(isNatList()),
          isNat() -> U21(isNat()),
        U61(tt()) -> U62(isNat()),
  length(cons(N)) -> U61(isNatList()),
    length(nil()) -> 0()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
            zeros() -> cons(0()),
          U11(tt()) -> tt(),
          U21(tt()) -> tt(),
          U31(tt()) -> tt(),
          U42(tt()) -> tt(),
       isNatIList() -> tt(),
       isNatIList() -> U31(isNatList()),
       isNatIList() -> U41(isNat()),
          U41(tt()) -> U42(isNatIList()),
          U52(tt()) -> tt(),
        isNatList() -> tt(),
        isNatList() -> U51(isNat()),
          U51(tt()) -> U52(isNatList()),
          U62(tt()) -> s(length(L)),
            isNat() -> tt(),
            isNat() -> U11(isNatList()),
            isNat() -> U21(isNat()),
          U61(tt()) -> U62(isNat()),
    length(cons(N)) -> U61(isNatList()),
      length(nil()) -> 0()
   }
  Fail