MAYBE
MAYBE
TRS:
 {
                    mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                             mark(0()) -> active(0()),
                         mark(zeros()) -> active(zeros()),
                          mark(U12(X)) -> active(U12(mark(X))),
                    mark(isNatList(X)) -> active(isNatList(X)),
                     mark(U11(X1, X2)) -> active(U11(mark(X1), X2)),
                            mark(tt()) -> active(tt()),
                          mark(U22(X)) -> active(U22(mark(X))),
                        mark(isNat(X)) -> active(isNat(X)),
                     mark(U21(X1, X2)) -> active(U21(mark(X1), X2)),
                          mark(U32(X)) -> active(U32(mark(X))),
                     mark(U31(X1, X2)) -> active(U31(mark(X1), X2)),
                     mark(U42(X1, X2)) -> active(U42(mark(X1), X2)),
                 mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3)),
                          mark(U43(X)) -> active(U43(mark(X))),
                   mark(isNatIList(X)) -> active(isNatIList(X)),
                     mark(U52(X1, X2)) -> active(U52(mark(X1), X2)),
                 mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)),
                          mark(U53(X)) -> active(U53(mark(X))),
                     mark(U62(X1, X2)) -> active(U62(mark(X1), X2)),
                 mark(U61(X1, X2, X3)) -> active(U61(mark(X1), X2, X3)),
                          mark(U63(X)) -> active(U63(mark(X))),
                            mark(s(X)) -> active(s(mark(X))),
                       mark(length(X)) -> active(length(mark(X))),
                     mark(U71(X1, X2)) -> active(U71(mark(X1), X2)),
                           mark(nil()) -> active(nil()),
                          mark(U81(X)) -> active(U81(mark(X))),
                    mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))),
             mark(U91(X1, X2, X3, X4)) -> active(U91(mark(X1), X2, X3, X4)),
                     mark(and(X1, X2)) -> active(and(mark(X1), X2)),
               mark(isNatIListKind(X)) -> active(isNatIListKind(X)),
                    mark(isNatKind(X)) -> active(isNatKind(X)),
                    cons(X1, mark(X2)) -> cons(X1, X2),
                  cons(X1, active(X2)) -> cons(X1, X2),
                    cons(mark(X1), X2) -> cons(X1, X2),
                  cons(active(X1), X2) -> cons(X1, X2),
                       active(zeros()) -> mark(cons(0(), zeros())),
                     active(U12(tt())) -> mark(tt()),
       active(isNatList(cons(V1, V2))) ->
  mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)),
              active(isNatList(nil())) -> mark(tt()),
       active(isNatList(take(V1, V2))) ->
  mark(U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)),
                 active(U11(tt(), V1)) -> mark(U12(isNatList(V1))),
                     active(U22(tt())) -> mark(tt()),
                    active(isNat(0())) -> mark(tt()),
                  active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)),
             active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)),
                 active(U21(tt(), V1)) -> mark(U22(isNat(V1))),
                     active(U32(tt())) -> mark(tt()),
                  active(U31(tt(), V)) -> mark(U32(isNatList(V))),
                 active(U42(tt(), V2)) -> mark(U43(isNatIList(V2))),
             active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2)),
                     active(U43(tt())) -> mark(tt()),
                 active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)),
      active(isNatIList(cons(V1, V2))) ->
  mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)),
           active(isNatIList(zeros())) -> mark(tt()),
                 active(U52(tt(), V2)) -> mark(U53(isNatList(V2))),
             active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2)),
                     active(U53(tt())) -> mark(tt()),
                 active(U62(tt(), V2)) -> mark(U63(isNatIList(V2))),
             active(U61(tt(), V1, V2)) -> mark(U62(isNat(V1), V2)),
                     active(U63(tt())) -> mark(tt()),
            active(length(cons(N, L))) ->
  mark(
      U71(
         and(
            and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))
         ), L
      )
  ),
                 active(length(nil())) -> mark(0()),
                  active(U71(tt(), L)) -> mark(s(length(L))),
                     active(U81(tt())) -> mark(nil()),
                 active(take(0(), IL)) ->
  mark(U81(and(isNatIList(IL), isNatIListKind(IL)))),
       active(take(s(M), cons(N, IL))) ->
  mark(
      U91(
         and(
            and(isNatIList(IL), isNatIListKind(IL)),
            and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
         ), IL, M, N
      )
  ),
           active(U91(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))),
                  active(and(tt(), X)) -> mark(X),
  active(isNatIListKind(cons(V1, V2))) ->
  mark(and(isNatKind(V1), isNatIListKind(V2))),
       active(isNatIListKind(zeros())) -> mark(tt()),
         active(isNatIListKind(nil())) -> mark(tt()),
  active(isNatIListKind(take(V1, V2))) ->
  mark(and(isNatKind(V1), isNatIListKind(V2))),
                active(isNatKind(0())) -> mark(tt()),
              active(isNatKind(s(V1))) -> mark(isNatKind(V1)),
         active(isNatKind(length(V1))) -> mark(isNatIListKind(V1)),
                          U12(mark(X)) -> U12(X),
                        U12(active(X)) -> U12(X),
                    isNatList(mark(X)) -> isNatList(X),
                  isNatList(active(X)) -> isNatList(X),
                     U11(X1, mark(X2)) -> U11(X1, X2),
                   U11(X1, active(X2)) -> U11(X1, X2),
                     U11(mark(X1), X2) -> U11(X1, X2),
                   U11(active(X1), X2) -> U11(X1, X2),
                          U22(mark(X)) -> U22(X),
                        U22(active(X)) -> U22(X),
                        isNat(mark(X)) -> isNat(X),
                      isNat(active(X)) -> isNat(X),
                     U21(X1, mark(X2)) -> U21(X1, X2),
                   U21(X1, active(X2)) -> U21(X1, X2),
                     U21(mark(X1), X2) -> U21(X1, X2),
                   U21(active(X1), X2) -> U21(X1, X2),
                          U32(mark(X)) -> U32(X),
                        U32(active(X)) -> U32(X),
                     U31(X1, mark(X2)) -> U31(X1, X2),
                   U31(X1, active(X2)) -> U31(X1, X2),
                     U31(mark(X1), X2) -> U31(X1, X2),
                   U31(active(X1), X2) -> U31(X1, X2),
                     U42(X1, mark(X2)) -> U42(X1, X2),
                   U42(X1, active(X2)) -> U42(X1, X2),
                     U42(mark(X1), X2) -> U42(X1, X2),
                   U42(active(X1), X2) -> U42(X1, X2),
                 U41(X1, X2, mark(X3)) -> U41(X1, X2, X3),
               U41(X1, X2, active(X3)) -> U41(X1, X2, X3),
                 U41(X1, mark(X2), X3) -> U41(X1, X2, X3),
               U41(X1, active(X2), X3) -> U41(X1, X2, X3),
                 U41(mark(X1), X2, X3) -> U41(X1, X2, X3),
               U41(active(X1), X2, X3) -> U41(X1, X2, X3),
                          U43(mark(X)) -> U43(X),
                        U43(active(X)) -> U43(X),
                   isNatIList(mark(X)) -> isNatIList(X),
                 isNatIList(active(X)) -> isNatIList(X),
                     U52(X1, mark(X2)) -> U52(X1, X2),
                   U52(X1, active(X2)) -> U52(X1, X2),
                     U52(mark(X1), X2) -> U52(X1, X2),
                   U52(active(X1), X2) -> U52(X1, X2),
                 U51(X1, X2, mark(X3)) -> U51(X1, X2, X3),
               U51(X1, X2, active(X3)) -> U51(X1, X2, X3),
                 U51(X1, mark(X2), X3) -> U51(X1, X2, X3),
               U51(X1, active(X2), X3) -> U51(X1, X2, X3),
                 U51(mark(X1), X2, X3) -> U51(X1, X2, X3),
               U51(active(X1), X2, X3) -> U51(X1, X2, X3),
                          U53(mark(X)) -> U53(X),
                        U53(active(X)) -> U53(X),
                     U62(X1, mark(X2)) -> U62(X1, X2),
                   U62(X1, active(X2)) -> U62(X1, X2),
                     U62(mark(X1), X2) -> U62(X1, X2),
                   U62(active(X1), X2) -> U62(X1, X2),
                 U61(X1, X2, mark(X3)) -> U61(X1, X2, X3),
               U61(X1, X2, active(X3)) -> U61(X1, X2, X3),
                 U61(X1, mark(X2), X3) -> U61(X1, X2, X3),
               U61(X1, active(X2), X3) -> U61(X1, X2, X3),
                 U61(mark(X1), X2, X3) -> U61(X1, X2, X3),
               U61(active(X1), X2, X3) -> U61(X1, X2, X3),
                          U63(mark(X)) -> U63(X),
                        U63(active(X)) -> U63(X),
                            s(mark(X)) -> s(X),
                          s(active(X)) -> s(X),
                       length(mark(X)) -> length(X),
                     length(active(X)) -> length(X),
                     U71(X1, mark(X2)) -> U71(X1, X2),
                   U71(X1, active(X2)) -> U71(X1, X2),
                     U71(mark(X1), X2) -> U71(X1, X2),
                   U71(active(X1), X2) -> U71(X1, X2),
                          U81(mark(X)) -> U81(X),
                        U81(active(X)) -> U81(X),
                    take(X1, mark(X2)) -> take(X1, X2),
                  take(X1, active(X2)) -> take(X1, X2),
                    take(mark(X1), X2) -> take(X1, X2),
                  take(active(X1), X2) -> take(X1, X2),
             U91(X1, X2, X3, mark(X4)) -> U91(X1, X2, X3, X4),
           U91(X1, X2, X3, active(X4)) -> U91(X1, X2, X3, X4),
             U91(X1, X2, mark(X3), X4) -> U91(X1, X2, X3, X4),
           U91(X1, X2, active(X3), X4) -> U91(X1, X2, X3, X4),
             U91(X1, mark(X2), X3, X4) -> U91(X1, X2, X3, X4),
           U91(X1, active(X2), X3, X4) -> U91(X1, X2, X3, X4),
             U91(mark(X1), X2, X3, X4) -> U91(X1, X2, X3, X4),
           U91(active(X1), X2, X3, X4) -> U91(X1, X2, X3, X4),
                     and(X1, mark(X2)) -> and(X1, X2),
                   and(X1, active(X2)) -> and(X1, X2),
                     and(mark(X1), X2) -> and(X1, X2),
                   and(active(X1), X2) -> and(X1, X2),
               isNatIListKind(mark(X)) -> isNatIListKind(X),
             isNatIListKind(active(X)) -> isNatIListKind(X),
                    isNatKind(mark(X)) -> isNatKind(X),
                  isNatKind(active(X)) -> isNatKind(X)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                      mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(0()) -> active(0()),
                           mark(zeros()) -> active(zeros()),
                            mark(U12(X)) -> active(U12(mark(X))),
                      mark(isNatList(X)) -> active(isNatList(X)),
                       mark(U11(X1, X2)) -> active(U11(mark(X1), X2)),
                              mark(tt()) -> active(tt()),
                            mark(U22(X)) -> active(U22(mark(X))),
                          mark(isNat(X)) -> active(isNat(X)),
                       mark(U21(X1, X2)) -> active(U21(mark(X1), X2)),
                            mark(U32(X)) -> active(U32(mark(X))),
                       mark(U31(X1, X2)) -> active(U31(mark(X1), X2)),
                       mark(U42(X1, X2)) -> active(U42(mark(X1), X2)),
                   mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3)),
                            mark(U43(X)) -> active(U43(mark(X))),
                     mark(isNatIList(X)) -> active(isNatIList(X)),
                       mark(U52(X1, X2)) -> active(U52(mark(X1), X2)),
                   mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)),
                            mark(U53(X)) -> active(U53(mark(X))),
                       mark(U62(X1, X2)) -> active(U62(mark(X1), X2)),
                   mark(U61(X1, X2, X3)) -> active(U61(mark(X1), X2, X3)),
                            mark(U63(X)) -> active(U63(mark(X))),
                              mark(s(X)) -> active(s(mark(X))),
                         mark(length(X)) -> active(length(mark(X))),
                       mark(U71(X1, X2)) -> active(U71(mark(X1), X2)),
                             mark(nil()) -> active(nil()),
                            mark(U81(X)) -> active(U81(mark(X))),
                      mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))),
               mark(U91(X1, X2, X3, X4)) -> active(U91(mark(X1), X2, X3, X4)),
                       mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                 mark(isNatIListKind(X)) -> active(isNatIListKind(X)),
                      mark(isNatKind(X)) -> active(isNatKind(X)),
                      cons(X1, mark(X2)) -> cons(X1, X2),
                    cons(X1, active(X2)) -> cons(X1, X2),
                      cons(mark(X1), X2) -> cons(X1, X2),
                    cons(active(X1), X2) -> cons(X1, X2),
                         active(zeros()) -> mark(cons(0(), zeros())),
                       active(U12(tt())) -> mark(tt()),
         active(isNatList(cons(V1, V2))) ->
    mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)),
                active(isNatList(nil())) -> mark(tt()),
         active(isNatList(take(V1, V2))) ->
    mark(U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)),
                   active(U11(tt(), V1)) -> mark(U12(isNatList(V1))),
                       active(U22(tt())) -> mark(tt()),
                      active(isNat(0())) -> mark(tt()),
                    active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)),
               active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)),
                   active(U21(tt(), V1)) -> mark(U22(isNat(V1))),
                       active(U32(tt())) -> mark(tt()),
                    active(U31(tt(), V)) -> mark(U32(isNatList(V))),
                   active(U42(tt(), V2)) -> mark(U43(isNatIList(V2))),
               active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2)),
                       active(U43(tt())) -> mark(tt()),
                   active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)),
        active(isNatIList(cons(V1, V2))) ->
    mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)),
             active(isNatIList(zeros())) -> mark(tt()),
                   active(U52(tt(), V2)) -> mark(U53(isNatList(V2))),
               active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2)),
                       active(U53(tt())) -> mark(tt()),
                   active(U62(tt(), V2)) -> mark(U63(isNatIList(V2))),
               active(U61(tt(), V1, V2)) -> mark(U62(isNat(V1), V2)),
                       active(U63(tt())) -> mark(tt()),
              active(length(cons(N, L))) ->
    mark(
        U71(
           and(
              and(isNatList(L), isNatIListKind(L)),
              and(isNat(N), isNatKind(N))
           ), L
        )
    ),
                   active(length(nil())) -> mark(0()),
                    active(U71(tt(), L)) -> mark(s(length(L))),
                       active(U81(tt())) -> mark(nil()),
                   active(take(0(), IL)) ->
    mark(U81(and(isNatIList(IL), isNatIListKind(IL)))),
         active(take(s(M), cons(N, IL))) ->
    mark(
        U91(
           and(
              and(isNatIList(IL), isNatIListKind(IL)),
              and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))
           ), IL, M, N
        )
    ),
             active(U91(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))),
                    active(and(tt(), X)) -> mark(X),
    active(isNatIListKind(cons(V1, V2))) ->
    mark(and(isNatKind(V1), isNatIListKind(V2))),
         active(isNatIListKind(zeros())) -> mark(tt()),
           active(isNatIListKind(nil())) -> mark(tt()),
    active(isNatIListKind(take(V1, V2))) ->
    mark(and(isNatKind(V1), isNatIListKind(V2))),
                  active(isNatKind(0())) -> mark(tt()),
                active(isNatKind(s(V1))) -> mark(isNatKind(V1)),
           active(isNatKind(length(V1))) -> mark(isNatIListKind(V1)),
                            U12(mark(X)) -> U12(X),
                          U12(active(X)) -> U12(X),
                      isNatList(mark(X)) -> isNatList(X),
                    isNatList(active(X)) -> isNatList(X),
                       U11(X1, mark(X2)) -> U11(X1, X2),
                     U11(X1, active(X2)) -> U11(X1, X2),
                       U11(mark(X1), X2) -> U11(X1, X2),
                     U11(active(X1), X2) -> U11(X1, X2),
                            U22(mark(X)) -> U22(X),
                          U22(active(X)) -> U22(X),
                          isNat(mark(X)) -> isNat(X),
                        isNat(active(X)) -> isNat(X),
                       U21(X1, mark(X2)) -> U21(X1, X2),
                     U21(X1, active(X2)) -> U21(X1, X2),
                       U21(mark(X1), X2) -> U21(X1, X2),
                     U21(active(X1), X2) -> U21(X1, X2),
                            U32(mark(X)) -> U32(X),
                          U32(active(X)) -> U32(X),
                       U31(X1, mark(X2)) -> U31(X1, X2),
                     U31(X1, active(X2)) -> U31(X1, X2),
                       U31(mark(X1), X2) -> U31(X1, X2),
                     U31(active(X1), X2) -> U31(X1, X2),
                       U42(X1, mark(X2)) -> U42(X1, X2),
                     U42(X1, active(X2)) -> U42(X1, X2),
                       U42(mark(X1), X2) -> U42(X1, X2),
                     U42(active(X1), X2) -> U42(X1, X2),
                   U41(X1, X2, mark(X3)) -> U41(X1, X2, X3),
                 U41(X1, X2, active(X3)) -> U41(X1, X2, X3),
                   U41(X1, mark(X2), X3) -> U41(X1, X2, X3),
                 U41(X1, active(X2), X3) -> U41(X1, X2, X3),
                   U41(mark(X1), X2, X3) -> U41(X1, X2, X3),
                 U41(active(X1), X2, X3) -> U41(X1, X2, X3),
                            U43(mark(X)) -> U43(X),
                          U43(active(X)) -> U43(X),
                     isNatIList(mark(X)) -> isNatIList(X),
                   isNatIList(active(X)) -> isNatIList(X),
                       U52(X1, mark(X2)) -> U52(X1, X2),
                     U52(X1, active(X2)) -> U52(X1, X2),
                       U52(mark(X1), X2) -> U52(X1, X2),
                     U52(active(X1), X2) -> U52(X1, X2),
                   U51(X1, X2, mark(X3)) -> U51(X1, X2, X3),
                 U51(X1, X2, active(X3)) -> U51(X1, X2, X3),
                   U51(X1, mark(X2), X3) -> U51(X1, X2, X3),
                 U51(X1, active(X2), X3) -> U51(X1, X2, X3),
                   U51(mark(X1), X2, X3) -> U51(X1, X2, X3),
                 U51(active(X1), X2, X3) -> U51(X1, X2, X3),
                            U53(mark(X)) -> U53(X),
                          U53(active(X)) -> U53(X),
                       U62(X1, mark(X2)) -> U62(X1, X2),
                     U62(X1, active(X2)) -> U62(X1, X2),
                       U62(mark(X1), X2) -> U62(X1, X2),
                     U62(active(X1), X2) -> U62(X1, X2),
                   U61(X1, X2, mark(X3)) -> U61(X1, X2, X3),
                 U61(X1, X2, active(X3)) -> U61(X1, X2, X3),
                   U61(X1, mark(X2), X3) -> U61(X1, X2, X3),
                 U61(X1, active(X2), X3) -> U61(X1, X2, X3),
                   U61(mark(X1), X2, X3) -> U61(X1, X2, X3),
                 U61(active(X1), X2, X3) -> U61(X1, X2, X3),
                            U63(mark(X)) -> U63(X),
                          U63(active(X)) -> U63(X),
                              s(mark(X)) -> s(X),
                            s(active(X)) -> s(X),
                         length(mark(X)) -> length(X),
                       length(active(X)) -> length(X),
                       U71(X1, mark(X2)) -> U71(X1, X2),
                     U71(X1, active(X2)) -> U71(X1, X2),
                       U71(mark(X1), X2) -> U71(X1, X2),
                     U71(active(X1), X2) -> U71(X1, X2),
                            U81(mark(X)) -> U81(X),
                          U81(active(X)) -> U81(X),
                      take(X1, mark(X2)) -> take(X1, X2),
                    take(X1, active(X2)) -> take(X1, X2),
                      take(mark(X1), X2) -> take(X1, X2),
                    take(active(X1), X2) -> take(X1, X2),
               U91(X1, X2, X3, mark(X4)) -> U91(X1, X2, X3, X4),
             U91(X1, X2, X3, active(X4)) -> U91(X1, X2, X3, X4),
               U91(X1, X2, mark(X3), X4) -> U91(X1, X2, X3, X4),
             U91(X1, X2, active(X3), X4) -> U91(X1, X2, X3, X4),
               U91(X1, mark(X2), X3, X4) -> U91(X1, X2, X3, X4),
             U91(X1, active(X2), X3, X4) -> U91(X1, X2, X3, X4),
               U91(mark(X1), X2, X3, X4) -> U91(X1, X2, X3, X4),
             U91(active(X1), X2, X3, X4) -> U91(X1, X2, X3, X4),
                       and(X1, mark(X2)) -> and(X1, X2),
                     and(X1, active(X2)) -> and(X1, X2),
                       and(mark(X1), X2) -> and(X1, X2),
                     and(active(X1), X2) -> and(X1, X2),
                 isNatIListKind(mark(X)) -> isNatIListKind(X),
               isNatIListKind(active(X)) -> isNatIListKind(X),
                      isNatKind(mark(X)) -> isNatKind(X),
                    isNatKind(active(X)) -> isNatKind(X)
   }
  Fail