MAYBE
MAYBE
TRS:
 {
                 cons(X1, X2) -> n__cons(X1, X2),
                          0() -> n__0(),
                      zeros() -> cons(0(), n__zeros()),
                      zeros() -> n__zeros(),
                    U11(tt()) -> tt(),
                    U21(tt()) -> tt(),
                    U31(tt()) -> tt(),
                    U42(tt()) -> tt(),
                isNatIList(V) -> U31(isNatList(activate(V))),
       isNatIList(n__zeros()) -> tt(),
  isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
                  activate(X) -> X,
         activate(n__zeros()) -> zeros(),
             activate(n__0()) -> 0(),
       activate(n__length(X)) -> length(X),
            activate(n__s(X)) -> s(X),
    activate(n__cons(X1, X2)) -> cons(X1, X2),
           activate(n__nil()) -> nil(),
                U41(tt(), V2) -> U42(isNatIList(activate(V2))),
                    U52(tt()) -> tt(),
   isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
          isNatList(n__nil()) -> tt(),
                U51(tt(), V2) -> U52(isNatList(activate(V2))),
                 U62(tt(), L) -> s(length(activate(L))),
                isNat(n__0()) -> tt(),
         isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
              isNat(n__s(V1)) -> U21(isNat(activate(V1))),
              U61(tt(), L, N) -> U62(isNat(activate(N)), activate(L)),
                         s(X) -> n__s(X),
                    length(X) -> n__length(X),
           length(cons(N, L)) -> U61(isNatList(activate(L)), activate(L), N),
                length(nil()) -> 0(),
                        nil() -> n__nil()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                   cons(X1, X2) -> n__cons(X1, X2),
                            0() -> n__0(),
                        zeros() -> cons(0(), n__zeros()),
                        zeros() -> n__zeros(),
                      U11(tt()) -> tt(),
                      U21(tt()) -> tt(),
                      U31(tt()) -> tt(),
                      U42(tt()) -> tt(),
                  isNatIList(V) -> U31(isNatList(activate(V))),
         isNatIList(n__zeros()) -> tt(),
    isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
                    activate(X) -> X,
           activate(n__zeros()) -> zeros(),
               activate(n__0()) -> 0(),
         activate(n__length(X)) -> length(X),
              activate(n__s(X)) -> s(X),
      activate(n__cons(X1, X2)) -> cons(X1, X2),
             activate(n__nil()) -> nil(),
                  U41(tt(), V2) -> U42(isNatIList(activate(V2))),
                      U52(tt()) -> tt(),
     isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
            isNatList(n__nil()) -> tt(),
                  U51(tt(), V2) -> U52(isNatList(activate(V2))),
                   U62(tt(), L) -> s(length(activate(L))),
                  isNat(n__0()) -> tt(),
           isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
                isNat(n__s(V1)) -> U21(isNat(activate(V1))),
                U61(tt(), L, N) -> U62(isNat(activate(N)), activate(L)),
                           s(X) -> n__s(X),
                      length(X) -> n__length(X),
             length(cons(N, L)) ->
    U61(isNatList(activate(L)), activate(L), N),
                  length(nil()) -> 0(),
                          nil() -> n__nil()
   }
  Fail