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__take(X1, X2)) -> take(X1, X2),
             activate(n__0()) -> 0(),
       activate(n__length(X)) -> length(X),
            activate(n__s(X)) -> s(X),
   activate(n__isNatIList(X)) -> isNatIList(X),
    activate(n__cons(X1, X2)) -> cons(X1, X2),
           activate(n__nil()) -> nil(),
    activate(n__isNatList(X)) -> isNatList(X),
        activate(n__isNat(X)) -> isNat(X),
     activate(n__and(X1, X2)) -> and(X1, X2),
                 U11(tt(), L) -> s(length(activate(L))),
                        nil() -> n__nil(),
                    U21(tt()) -> nil(),
          U31(tt(), IL, M, N) ->
  cons(activate(N), n__take(activate(M), activate(IL))),
                  and(X1, X2) -> n__and(X1, X2),
                 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__take(V1, V2)) ->
  and(isNat(activate(V1)), n__isNatIList(activate(V2))),
   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))),
                 take(X1, X2) -> n__take(X1, X2),
                take(0(), IL) -> U21(isNatIList(IL)),
      take(s(M), cons(N, IL)) ->
  U31(
     and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))),
     activate(IL), M, N
  )
 }
 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__take(X1, X2)) -> take(X1, X2),
               activate(n__0()) -> 0(),
         activate(n__length(X)) -> length(X),
              activate(n__s(X)) -> s(X),
     activate(n__isNatIList(X)) -> isNatIList(X),
      activate(n__cons(X1, X2)) -> cons(X1, X2),
             activate(n__nil()) -> nil(),
      activate(n__isNatList(X)) -> isNatList(X),
          activate(n__isNat(X)) -> isNat(X),
       activate(n__and(X1, X2)) -> and(X1, X2),
                   U11(tt(), L) -> s(length(activate(L))),
                          nil() -> n__nil(),
                      U21(tt()) -> nil(),
            U31(tt(), IL, M, N) ->
    cons(activate(N), n__take(activate(M), activate(IL))),
                    and(X1, X2) -> n__and(X1, X2),
                   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__take(V1, V2)) ->
    and(isNat(activate(V1)), n__isNatIList(activate(V2))),
     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))),
                   take(X1, X2) -> n__take(X1, X2),
                  take(0(), IL) -> U21(isNatIList(IL)),
        take(s(M), cons(N, IL)) ->
    U31(
       and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))),
       activate(IL), M, N
    )
   }
  Fail