MAYBE
MAYBE
TRS:
 {
                 cons(X1, X2) -> n__cons(X1, X2),
                          0() -> n__0(),
                      zeros() -> cons(0(), n__zeros()),
                      zeros() -> n__zeros(),
                         s(X) -> n__s(X),
                    length(X) -> n__length(X),
           length(cons(N, L)) ->
  U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)),
                length(nil()) -> 0(),
                  activate(X) -> X,
         activate(n__zeros()) -> zeros(),
             activate(n__0()) -> 0(),
       activate(n__length(X)) -> length(activate(X)),
            activate(n__s(X)) -> s(activate(X)),
   activate(n__isNatIList(X)) -> isNatIList(X),
    activate(n__cons(X1, X2)) -> cons(activate(X1), X2),
           activate(n__nil()) -> nil(),
    activate(n__isNatList(X)) -> isNatList(X),
        activate(n__isNat(X)) -> isNat(X),
                 U11(tt(), L) -> s(length(activate(L))),
                 and(tt(), X) -> activate(X),
                     isNat(X) -> n__isNat(X),
                isNat(n__0()) -> tt(),
         isNat(n__length(V1)) -> isNatList(activate(V1)),
              isNat(n__s(V1)) -> isNat(activate(V1)),
                 isNatList(X) -> n__isNatList(X),
   isNatList(n__cons(V1, V2)) ->
  and(isNat(activate(V1)), n__isNatList(activate(V2))),
          isNatList(n__nil()) -> tt(),
                isNatIList(X) -> n__isNatIList(X),
                isNatIList(V) -> isNatList(activate(V)),
       isNatIList(n__zeros()) -> tt(),
  isNatIList(n__cons(V1, V2)) ->
  and(isNat(activate(V1)), n__isNatIList(activate(V2))),
                        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(),
                           s(X) -> n__s(X),
                      length(X) -> n__length(X),
             length(cons(N, L)) ->
    U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)),
                  length(nil()) -> 0(),
                    activate(X) -> X,
           activate(n__zeros()) -> zeros(),
               activate(n__0()) -> 0(),
         activate(n__length(X)) -> length(activate(X)),
              activate(n__s(X)) -> s(activate(X)),
     activate(n__isNatIList(X)) -> isNatIList(X),
      activate(n__cons(X1, X2)) -> cons(activate(X1), X2),
             activate(n__nil()) -> nil(),
      activate(n__isNatList(X)) -> isNatList(X),
          activate(n__isNat(X)) -> isNat(X),
                   U11(tt(), L) -> s(length(activate(L))),
                   and(tt(), X) -> activate(X),
                       isNat(X) -> n__isNat(X),
                  isNat(n__0()) -> tt(),
           isNat(n__length(V1)) -> isNatList(activate(V1)),
                isNat(n__s(V1)) -> isNat(activate(V1)),
                   isNatList(X) -> n__isNatList(X),
     isNatList(n__cons(V1, V2)) ->
    and(isNat(activate(V1)), n__isNatList(activate(V2))),
            isNatList(n__nil()) -> tt(),
                  isNatIList(X) -> n__isNatIList(X),
                  isNatIList(V) -> isNatList(activate(V)),
         isNatIList(n__zeros()) -> tt(),
    isNatIList(n__cons(V1, V2)) ->
    and(isNat(activate(V1)), n__isNatIList(activate(V2))),
                          nil() -> n__nil()
   }
  Fail