MAYBE
MAYBE
TRS:
 {
                mark(and(X1, X2)) -> active(and(mark(X1), mark(X2))),
                       mark(tt()) -> active(tt()),
               mark(isNatList(X)) -> active(isNatList(X)),
              mark(isNatIList(X)) -> active(isNatIList(X)),
                   mark(isNat(X)) -> active(isNat(X)),
                        mark(0()) -> active(0()),
                       mark(s(X)) -> active(s(mark(X))),
                  mark(length(X)) -> active(length(mark(X))),
                    mark(zeros()) -> active(zeros()),
               mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                      mark(nil()) -> active(nil()),
               mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))),
                  mark(uTake1(X)) -> active(uTake1(mark(X))),
     mark(uTake2(X1, X2, X3, X4)) -> active(uTake2(mark(X1), X2, X3, X4)),
            mark(uLength(X1, X2)) -> active(uLength(mark(X1), X2)),
             active(and(tt(), T)) -> mark(T),
    active(isNatList(cons(N, L))) -> mark(and(isNat(N), isNatList(L))),
         active(isNatList(nil())) -> mark(tt()),
   active(isNatList(take(N, IL))) -> mark(and(isNat(N), isNatIList(IL))),
           active(isNatIList(IL)) -> mark(isNatList(IL)),
      active(isNatIList(zeros())) -> mark(tt()),
  active(isNatIList(cons(N, IL))) -> mark(and(isNat(N), isNatIList(IL))),
               active(isNat(0())) -> mark(tt()),
              active(isNat(s(N))) -> mark(isNat(N)),
         active(isNat(length(L))) -> mark(isNatList(L)),
       active(length(cons(N, L))) ->
  mark(uLength(and(isNat(N), isNatList(L)), L)),
                  active(zeros()) -> mark(cons(0(), zeros())),
            active(take(0(), IL)) -> mark(uTake1(isNatIList(IL))),
  active(take(s(M), cons(N, IL))) ->
  mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)),
             active(uTake1(tt())) -> mark(nil()),
   active(uTake2(tt(), M, N, IL)) -> mark(cons(N, take(M, IL))),
         active(uLength(tt(), L)) -> mark(s(length(L))),
                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),
               isNatList(mark(X)) -> isNatList(X),
             isNatList(active(X)) -> isNatList(X),
              isNatIList(mark(X)) -> isNatIList(X),
            isNatIList(active(X)) -> isNatIList(X),
                   isNat(mark(X)) -> isNat(X),
                 isNat(active(X)) -> isNat(X),
                       s(mark(X)) -> s(X),
                     s(active(X)) -> s(X),
                  length(mark(X)) -> length(X),
                length(active(X)) -> length(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),
               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),
                  uTake1(mark(X)) -> uTake1(X),
                uTake1(active(X)) -> uTake1(X),
     uTake2(X1, X2, X3, mark(X4)) -> uTake2(X1, X2, X3, X4),
   uTake2(X1, X2, X3, active(X4)) -> uTake2(X1, X2, X3, X4),
     uTake2(X1, X2, mark(X3), X4) -> uTake2(X1, X2, X3, X4),
   uTake2(X1, X2, active(X3), X4) -> uTake2(X1, X2, X3, X4),
     uTake2(X1, mark(X2), X3, X4) -> uTake2(X1, X2, X3, X4),
   uTake2(X1, active(X2), X3, X4) -> uTake2(X1, X2, X3, X4),
     uTake2(mark(X1), X2, X3, X4) -> uTake2(X1, X2, X3, X4),
   uTake2(active(X1), X2, X3, X4) -> uTake2(X1, X2, X3, X4),
            uLength(X1, mark(X2)) -> uLength(X1, X2),
          uLength(X1, active(X2)) -> uLength(X1, X2),
            uLength(mark(X1), X2) -> uLength(X1, X2),
          uLength(active(X1), X2) -> uLength(X1, X2)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                  mark(and(X1, X2)) -> active(and(mark(X1), mark(X2))),
                         mark(tt()) -> active(tt()),
                 mark(isNatList(X)) -> active(isNatList(X)),
                mark(isNatIList(X)) -> active(isNatIList(X)),
                     mark(isNat(X)) -> active(isNat(X)),
                          mark(0()) -> active(0()),
                         mark(s(X)) -> active(s(mark(X))),
                    mark(length(X)) -> active(length(mark(X))),
                      mark(zeros()) -> active(zeros()),
                 mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                        mark(nil()) -> active(nil()),
                 mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))),
                    mark(uTake1(X)) -> active(uTake1(mark(X))),
       mark(uTake2(X1, X2, X3, X4)) -> active(uTake2(mark(X1), X2, X3, X4)),
              mark(uLength(X1, X2)) -> active(uLength(mark(X1), X2)),
               active(and(tt(), T)) -> mark(T),
      active(isNatList(cons(N, L))) -> mark(and(isNat(N), isNatList(L))),
           active(isNatList(nil())) -> mark(tt()),
     active(isNatList(take(N, IL))) -> mark(and(isNat(N), isNatIList(IL))),
             active(isNatIList(IL)) -> mark(isNatList(IL)),
        active(isNatIList(zeros())) -> mark(tt()),
    active(isNatIList(cons(N, IL))) -> mark(and(isNat(N), isNatIList(IL))),
                 active(isNat(0())) -> mark(tt()),
                active(isNat(s(N))) -> mark(isNat(N)),
           active(isNat(length(L))) -> mark(isNatList(L)),
         active(length(cons(N, L))) ->
    mark(uLength(and(isNat(N), isNatList(L)), L)),
                    active(zeros()) -> mark(cons(0(), zeros())),
              active(take(0(), IL)) -> mark(uTake1(isNatIList(IL))),
    active(take(s(M), cons(N, IL))) ->
    mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M, N, IL)),
               active(uTake1(tt())) -> mark(nil()),
     active(uTake2(tt(), M, N, IL)) -> mark(cons(N, take(M, IL))),
           active(uLength(tt(), L)) -> mark(s(length(L))),
                  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),
                 isNatList(mark(X)) -> isNatList(X),
               isNatList(active(X)) -> isNatList(X),
                isNatIList(mark(X)) -> isNatIList(X),
              isNatIList(active(X)) -> isNatIList(X),
                     isNat(mark(X)) -> isNat(X),
                   isNat(active(X)) -> isNat(X),
                         s(mark(X)) -> s(X),
                       s(active(X)) -> s(X),
                    length(mark(X)) -> length(X),
                  length(active(X)) -> length(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),
                 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),
                    uTake1(mark(X)) -> uTake1(X),
                  uTake1(active(X)) -> uTake1(X),
       uTake2(X1, X2, X3, mark(X4)) -> uTake2(X1, X2, X3, X4),
     uTake2(X1, X2, X3, active(X4)) -> uTake2(X1, X2, X3, X4),
       uTake2(X1, X2, mark(X3), X4) -> uTake2(X1, X2, X3, X4),
     uTake2(X1, X2, active(X3), X4) -> uTake2(X1, X2, X3, X4),
       uTake2(X1, mark(X2), X3, X4) -> uTake2(X1, X2, X3, X4),
     uTake2(X1, active(X2), X3, X4) -> uTake2(X1, X2, X3, X4),
       uTake2(mark(X1), X2, X3, X4) -> uTake2(X1, X2, X3, X4),
     uTake2(active(X1), X2, X3, X4) -> uTake2(X1, X2, X3, X4),
              uLength(X1, mark(X2)) -> uLength(X1, X2),
            uLength(X1, active(X2)) -> uLength(X1, X2),
              uLength(mark(X1), X2) -> uLength(X1, X2),
            uLength(active(X1), X2) -> uLength(X1, X2)
   }
  Fail