MAYBE
TRS:
 {                  mark(tt()) -> tt(),
                     mark(0()) -> 0(),
                    mark(s(X)) -> s(mark(X)),
               mark(length(X)) -> a__length(mark(X)),
                 mark(zeros()) -> a__zeros(),
            mark(cons(X1, X2)) -> cons(mark(X1), X2),
                   mark(nil()) -> nil(),
            mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
             mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
           mark(isNatIList(X)) -> a__isNatIList(X),
            mark(isNatList(X)) -> a__isNatList(X),
                mark(isNat(X)) -> a__isNat(X),
               mark(uTake1(X)) -> a__uTake1(mark(X)),
  mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
         mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                a__and(X1, X2) -> and(X1, X2),
               a__and(tt(), T) -> mark(T),
               a__isNatList(X) -> isNatList(X),
      a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
           a__isNatList(nil()) -> tt(),
     a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
             a__isNatIList(IL) -> a__isNatList(IL),
              a__isNatIList(X) -> isNatIList(X),
        a__isNatIList(zeros()) -> tt(),
    a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                   a__isNat(X) -> isNat(X),
                 a__isNat(0()) -> tt(),
                a__isNat(s(N)) -> a__isNat(N),
           a__isNat(length(L)) -> a__isNatList(L),
                    a__zeros() -> zeros(),
                    a__zeros() -> cons(0(), zeros()),
                  a__uTake1(X) -> uTake1(X),
               a__uTake1(tt()) -> nil(),
               a__take(X1, X2) -> take(X1, X2),
              a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
    a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
     a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
     a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
            a__uLength(X1, X2) -> uLength(X1, X2),
           a__uLength(tt(), L) -> s(a__length(mark(L))),
                  a__length(X) -> length(X),
         a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
 DP:
  Strict:
   {                  mark#(s(X)) -> mark#(X),
                 mark#(length(X)) -> mark#(X),
                 mark#(length(X)) -> a__length#(mark(X)),
                   mark#(zeros()) -> a__zeros#(),
              mark#(cons(X1, X2)) -> mark#(X1),
              mark#(take(X1, X2)) -> mark#(X1),
              mark#(take(X1, X2)) -> mark#(X2),
              mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)),
               mark#(and(X1, X2)) -> mark#(X1),
               mark#(and(X1, X2)) -> mark#(X2),
               mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
             mark#(isNatIList(X)) -> a__isNatIList#(X),
              mark#(isNatList(X)) -> a__isNatList#(X),
                  mark#(isNat(X)) -> a__isNat#(X),
                 mark#(uTake1(X)) -> mark#(X),
                 mark#(uTake1(X)) -> a__uTake1#(mark(X)),
    mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1),
    mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4),
           mark#(uLength(X1, X2)) -> mark#(X1),
           mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2),
                 a__and#(tt(), T) -> mark#(T),
        a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
        a__isNatList#(cons(N, L)) -> a__isNatList#(L),
        a__isNatList#(cons(N, L)) -> a__isNat#(N),
       a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
       a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
       a__isNatList#(take(N, IL)) -> a__isNat#(N),
               a__isNatIList#(IL) -> a__isNatList#(IL),
      a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
      a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
      a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                  a__isNat#(s(N)) -> a__isNat#(N),
             a__isNat#(length(L)) -> a__isNatList#(L),
                a__take#(0(), IL) -> a__isNatIList#(IL),
                a__take#(0(), IL) -> a__uTake1#(a__isNatIList(IL)),
      a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
      a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))),
      a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL),
      a__take#(s(M), cons(N, IL)) -> a__isNat#(N),
      a__take#(s(M), cons(N, IL)) -> a__isNat#(M),
      a__take#(s(M), cons(N, IL)) -> a__uTake2#(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
       a__uTake2#(tt(), M, N, IL) -> mark#(N),
             a__uLength#(tt(), L) -> mark#(L),
             a__uLength#(tt(), L) -> a__length#(mark(L)),
           a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
           a__length#(cons(N, L)) -> a__isNatList#(L),
           a__length#(cons(N, L)) -> a__isNat#(N),
           a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L)}
  Weak:
  {                  mark(tt()) -> tt(),
                      mark(0()) -> 0(),
                     mark(s(X)) -> s(mark(X)),
                mark(length(X)) -> a__length(mark(X)),
                  mark(zeros()) -> a__zeros(),
             mark(cons(X1, X2)) -> cons(mark(X1), X2),
                    mark(nil()) -> nil(),
             mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
              mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
            mark(isNatIList(X)) -> a__isNatIList(X),
             mark(isNatList(X)) -> a__isNatList(X),
                 mark(isNat(X)) -> a__isNat(X),
                mark(uTake1(X)) -> a__uTake1(mark(X)),
   mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
          mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                 a__and(X1, X2) -> and(X1, X2),
                a__and(tt(), T) -> mark(T),
                a__isNatList(X) -> isNatList(X),
       a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
            a__isNatList(nil()) -> tt(),
      a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
              a__isNatIList(IL) -> a__isNatList(IL),
               a__isNatIList(X) -> isNatIList(X),
         a__isNatIList(zeros()) -> tt(),
     a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                    a__isNat(X) -> isNat(X),
                  a__isNat(0()) -> tt(),
                 a__isNat(s(N)) -> a__isNat(N),
            a__isNat(length(L)) -> a__isNatList(L),
                     a__zeros() -> zeros(),
                     a__zeros() -> cons(0(), zeros()),
                   a__uTake1(X) -> uTake1(X),
                a__uTake1(tt()) -> nil(),
                a__take(X1, X2) -> take(X1, X2),
               a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
     a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
      a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
      a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
             a__uLength(X1, X2) -> uLength(X1, X2),
            a__uLength(tt(), L) -> s(a__length(mark(L))),
                   a__length(X) -> length(X),
          a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
  EDG:
   {
    (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
    (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
    (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
    (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
    (a__take#(s(M), cons(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
    (a__take#(s(M), cons(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
    (a__length#(cons(N, L)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
    (a__length#(cons(N, L)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
    (mark#(s(X)) -> mark#(X), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(s(X)) -> mark#(X), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(s(X)) -> mark#(X), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(zeros()) -> a__zeros#())
    (mark#(s(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
    (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
    (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(IL) -> a__isNatList#(IL))
    (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(length(L)) -> a__isNatList#(L))
    (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(N)) -> a__isNat#(N))
    (a__and#(tt(), T) -> mark#(T), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (a__and#(tt(), T) -> mark#(T), mark#(uLength(X1, X2)) -> mark#(X1))
    (a__and#(tt(), T) -> mark#(T), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (a__and#(tt(), T) -> mark#(T), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (a__and#(tt(), T) -> mark#(T), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (a__and#(tt(), T) -> mark#(T), mark#(uTake1(X)) -> mark#(X))
    (a__and#(tt(), T) -> mark#(T), mark#(isNat(X)) -> a__isNat#(X))
    (a__and#(tt(), T) -> mark#(T), mark#(isNatList(X)) -> a__isNatList#(X))
    (a__and#(tt(), T) -> mark#(T), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X2))
    (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X1))
    (a__and#(tt(), T) -> mark#(T), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (a__and#(tt(), T) -> mark#(T), mark#(take(X1, X2)) -> mark#(X2))
    (a__and#(tt(), T) -> mark#(T), mark#(take(X1, X2)) -> mark#(X1))
    (a__and#(tt(), T) -> mark#(T), mark#(cons(X1, X2)) -> mark#(X1))
    (a__and#(tt(), T) -> mark#(T), mark#(zeros()) -> a__zeros#())
    (a__and#(tt(), T) -> mark#(T), mark#(length(X)) -> a__length#(mark(X)))
    (a__and#(tt(), T) -> mark#(T), mark#(length(X)) -> mark#(X))
    (a__and#(tt(), T) -> mark#(T), mark#(s(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(zeros()) -> a__zeros#())
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(zeros()) -> a__zeros#())
    (mark#(and(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(zeros()) -> a__zeros#())
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X))
    (mark#(uLength(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
    (a__uLength#(tt(), L) -> mark#(L), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (a__uLength#(tt(), L) -> mark#(L), mark#(uLength(X1, X2)) -> mark#(X1))
    (a__uLength#(tt(), L) -> mark#(L), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (a__uLength#(tt(), L) -> mark#(L), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (a__uLength#(tt(), L) -> mark#(L), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (a__uLength#(tt(), L) -> mark#(L), mark#(uTake1(X)) -> mark#(X))
    (a__uLength#(tt(), L) -> mark#(L), mark#(isNat(X)) -> a__isNat#(X))
    (a__uLength#(tt(), L) -> mark#(L), mark#(isNatList(X)) -> a__isNatList#(X))
    (a__uLength#(tt(), L) -> mark#(L), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (a__uLength#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (a__uLength#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> mark#(X2))
    (a__uLength#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> mark#(X1))
    (a__uLength#(tt(), L) -> mark#(L), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (a__uLength#(tt(), L) -> mark#(L), mark#(take(X1, X2)) -> mark#(X2))
    (a__uLength#(tt(), L) -> mark#(L), mark#(take(X1, X2)) -> mark#(X1))
    (a__uLength#(tt(), L) -> mark#(L), mark#(cons(X1, X2)) -> mark#(X1))
    (a__uLength#(tt(), L) -> mark#(L), mark#(zeros()) -> a__zeros#())
    (a__uLength#(tt(), L) -> mark#(L), mark#(length(X)) -> a__length#(mark(X)))
    (a__uLength#(tt(), L) -> mark#(L), mark#(length(X)) -> mark#(X))
    (a__uLength#(tt(), L) -> mark#(L), mark#(s(X)) -> mark#(X))
    (mark#(length(X)) -> a__length#(mark(X)), a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L))
    (mark#(length(X)) -> a__length#(mark(X)), a__length#(cons(N, L)) -> a__isNat#(N))
    (mark#(length(X)) -> a__length#(mark(X)), a__length#(cons(N, L)) -> a__isNatList#(L))
    (mark#(length(X)) -> a__length#(mark(X)), a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
    (a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), a__and#(tt(), T) -> mark#(T))
    (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
    (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
    (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
    (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
    (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
    (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
    (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
    (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
    (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
    (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__uTake2#(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL))
    (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__isNat#(M))
    (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__isNat#(N))
    (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL))
    (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))))
    (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(0(), IL) -> a__uTake1#(a__isNatIList(IL)))
    (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(0(), IL) -> a__isNatIList#(IL))
    (a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
    (a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
    (a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(uTake1(X)) -> mark#(X))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(zeros()) -> a__zeros#())
    (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> mark#(X))
    (mark#(take(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (a__take#(s(M), cons(N, IL)) -> a__uTake2#(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL), a__uTake2#(tt(), M, N, IL) -> mark#(N))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(length(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(zeros()) -> a__zeros#())
    (mark#(and(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(uTake1(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X2), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4), a__uTake2#(tt(), M, N, IL) -> mark#(N))
    (a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
    (a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
    (mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)), a__and#(tt(), T) -> mark#(T))
    (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
    (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
    (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNat#(N))
    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNat#(N))
    (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
    (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__isNatList#(L))
    (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__isNat#(N))
    (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L))
    (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
    (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
    (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
    (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
    (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
    (a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L), a__uLength#(tt(), L) -> mark#(L))
    (a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L), a__uLength#(tt(), L) -> a__length#(mark(L)))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(length(X)) -> mark#(X))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(zeros()) -> a__zeros#())
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(zeros()) -> a__zeros#())
    (mark#(take(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(take(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(uTake1(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(uTake1(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
    (mark#(uTake1(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(uTake1(X)) -> mark#(X), mark#(zeros()) -> a__zeros#())
    (mark#(uTake1(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(uTake1(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(uTake1(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(uTake1(X)) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(uTake1(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(uTake1(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(uTake1(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(uTake1(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))
    (mark#(uTake1(X)) -> mark#(X), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(uTake1(X)) -> mark#(X), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(uTake1(X)) -> mark#(X), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(uTake1(X)) -> mark#(X), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(uTake1(X)) -> mark#(X), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNat#(N))
    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNat#(N))
    (mark#(length(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(length(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
    (mark#(length(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X)))
    (mark#(length(X)) -> mark#(X), mark#(zeros()) -> a__zeros#())
    (mark#(length(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1))
    (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2))
    (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (mark#(length(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(length(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
    (mark#(length(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (mark#(length(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (mark#(length(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
    (mark#(length(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(length(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))
    (mark#(length(X)) -> mark#(X), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (mark#(length(X)) -> mark#(X), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (mark#(length(X)) -> mark#(X), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (mark#(length(X)) -> mark#(X), mark#(uLength(X1, X2)) -> mark#(X1))
    (mark#(length(X)) -> mark#(X), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2), a__uLength#(tt(), L) -> mark#(L))
    (mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2), a__uLength#(tt(), L) -> a__length#(mark(L)))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(s(X)) -> mark#(X))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(length(X)) -> mark#(X))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(length(X)) -> a__length#(mark(X)))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(zeros()) -> a__zeros#())
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(take(X1, X2)) -> mark#(X1))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(take(X1, X2)) -> mark#(X2))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(and(X1, X2)) -> mark#(X2))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(isNatIList(X)) -> a__isNatIList#(X))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(isNatList(X)) -> a__isNatList#(X))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(uTake1(X)) -> mark#(X))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(uTake1(X)) -> a__uTake1#(mark(X)))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(uLength(X1, X2)) -> mark#(X1))
    (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
    (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
    (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
    (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
    (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
    (a__take#(s(M), cons(N, IL)) -> a__isNat#(M), a__isNat#(s(N)) -> a__isNat#(N))
    (a__take#(s(M), cons(N, IL)) -> a__isNat#(M), a__isNat#(length(L)) -> a__isNatList#(L))
   }
   SCCS:
    Scc:
     {                  mark#(s(X)) -> mark#(X),
                   mark#(length(X)) -> mark#(X),
                   mark#(length(X)) -> a__length#(mark(X)),
                mark#(cons(X1, X2)) -> mark#(X1),
                mark#(take(X1, X2)) -> mark#(X1),
                mark#(take(X1, X2)) -> mark#(X2),
                mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)),
                 mark#(and(X1, X2)) -> mark#(X1),
                 mark#(and(X1, X2)) -> mark#(X2),
                 mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
               mark#(isNatIList(X)) -> a__isNatIList#(X),
                mark#(isNatList(X)) -> a__isNatList#(X),
                    mark#(isNat(X)) -> a__isNat#(X),
                   mark#(uTake1(X)) -> mark#(X),
      mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1),
      mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4),
             mark#(uLength(X1, X2)) -> mark#(X1),
             mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2),
                   a__and#(tt(), T) -> mark#(T),
          a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
          a__isNatList#(cons(N, L)) -> a__isNatList#(L),
          a__isNatList#(cons(N, L)) -> a__isNat#(N),
         a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
         a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
         a__isNatList#(take(N, IL)) -> a__isNat#(N),
                 a__isNatIList#(IL) -> a__isNatList#(IL),
        a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
        a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
        a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                    a__isNat#(s(N)) -> a__isNat#(N),
               a__isNat#(length(L)) -> a__isNatList#(L),
                  a__take#(0(), IL) -> a__isNatIList#(IL),
        a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
        a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))),
        a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL),
        a__take#(s(M), cons(N, IL)) -> a__isNat#(N),
        a__take#(s(M), cons(N, IL)) -> a__isNat#(M),
        a__take#(s(M), cons(N, IL)) -> a__uTake2#(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
         a__uTake2#(tt(), M, N, IL) -> mark#(N),
               a__uLength#(tt(), L) -> mark#(L),
               a__uLength#(tt(), L) -> a__length#(mark(L)),
             a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
             a__length#(cons(N, L)) -> a__isNatList#(L),
             a__length#(cons(N, L)) -> a__isNat#(N),
             a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L)}
    SCC:
     Strict:
      {                  mark#(s(X)) -> mark#(X),
                    mark#(length(X)) -> mark#(X),
                    mark#(length(X)) -> a__length#(mark(X)),
                 mark#(cons(X1, X2)) -> mark#(X1),
                 mark#(take(X1, X2)) -> mark#(X1),
                 mark#(take(X1, X2)) -> mark#(X2),
                 mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)),
                  mark#(and(X1, X2)) -> mark#(X1),
                  mark#(and(X1, X2)) -> mark#(X2),
                  mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                mark#(isNatIList(X)) -> a__isNatIList#(X),
                 mark#(isNatList(X)) -> a__isNatList#(X),
                     mark#(isNat(X)) -> a__isNat#(X),
                    mark#(uTake1(X)) -> mark#(X),
       mark#(uTake2(X1, X2, X3, X4)) -> mark#(X1),
       mark#(uTake2(X1, X2, X3, X4)) -> a__uTake2#(mark(X1), X2, X3, X4),
              mark#(uLength(X1, X2)) -> mark#(X1),
              mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2),
                    a__and#(tt(), T) -> mark#(T),
           a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
           a__isNatList#(cons(N, L)) -> a__isNatList#(L),
           a__isNatList#(cons(N, L)) -> a__isNat#(N),
          a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
          a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
          a__isNatList#(take(N, IL)) -> a__isNat#(N),
                  a__isNatIList#(IL) -> a__isNatList#(IL),
         a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
         a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
         a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                     a__isNat#(s(N)) -> a__isNat#(N),
                a__isNat#(length(L)) -> a__isNatList#(L),
                   a__take#(0(), IL) -> a__isNatIList#(IL),
         a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
         a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))),
         a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL),
         a__take#(s(M), cons(N, IL)) -> a__isNat#(N),
         a__take#(s(M), cons(N, IL)) -> a__isNat#(M),
         a__take#(s(M), cons(N, IL)) -> a__uTake2#(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
          a__uTake2#(tt(), M, N, IL) -> mark#(N),
                a__uLength#(tt(), L) -> mark#(L),
                a__uLength#(tt(), L) -> a__length#(mark(L)),
              a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
              a__length#(cons(N, L)) -> a__isNatList#(L),
              a__length#(cons(N, L)) -> a__isNat#(N),
              a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L)}
     Weak:
     {                  mark(tt()) -> tt(),
                         mark(0()) -> 0(),
                        mark(s(X)) -> s(mark(X)),
                   mark(length(X)) -> a__length(mark(X)),
                     mark(zeros()) -> a__zeros(),
                mark(cons(X1, X2)) -> cons(mark(X1), X2),
                       mark(nil()) -> nil(),
                mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                 mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
               mark(isNatIList(X)) -> a__isNatIList(X),
                mark(isNatList(X)) -> a__isNatList(X),
                    mark(isNat(X)) -> a__isNat(X),
                   mark(uTake1(X)) -> a__uTake1(mark(X)),
      mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
             mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                    a__and(X1, X2) -> and(X1, X2),
                   a__and(tt(), T) -> mark(T),
                   a__isNatList(X) -> isNatList(X),
          a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
               a__isNatList(nil()) -> tt(),
         a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                 a__isNatIList(IL) -> a__isNatList(IL),
                  a__isNatIList(X) -> isNatIList(X),
            a__isNatIList(zeros()) -> tt(),
        a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                       a__isNat(X) -> isNat(X),
                     a__isNat(0()) -> tt(),
                    a__isNat(s(N)) -> a__isNat(N),
               a__isNat(length(L)) -> a__isNatList(L),
                        a__zeros() -> zeros(),
                        a__zeros() -> cons(0(), zeros()),
                      a__uTake1(X) -> uTake1(X),
                   a__uTake1(tt()) -> nil(),
                   a__take(X1, X2) -> take(X1, X2),
                  a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
        a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
         a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
         a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                a__uLength(X1, X2) -> uLength(X1, X2),
               a__uLength(tt(), L) -> s(a__length(mark(L))),
                      a__length(X) -> length(X),
             a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
     POLY:
      Argument Filtering:
       pi(uLength) = [0,1], pi(uTake2) = [0,1,2,3], pi(uTake1) = 0, pi(isNat) = [], pi(isNatList) = [], pi(isNatIList) = [], pi(and) = [0,1], pi(a__length#) = 0, pi(a__length) = 0, pi(a__uLength#) = 1, pi(a__uLength) = [0,1], pi(a__uTake2#) = 2, pi(a__uTake2) = [0,1,2,3], pi(a__take#) = 1, pi(a__take) = [0,1], pi(a__uTake1) = 0, pi(a__zeros) = [], pi(take) = [0,1], pi(nil) = [], pi(cons) = [0,1], pi(zeros) = [], pi(length) = 0, pi(s) = 0, pi(0) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__isNatIList#) = [], pi(a__isNatIList) = [], pi(a__isNatList#) = [], pi(a__isNatList) = [], pi(tt) = [], pi(a__and#) = 1, pi(a__and) = [0,1], pi(mark#) = 0, pi(mark) = 0
      Usable Rules:
       {}
      Interpretation:
       [a__isNat#] = 0,
       [a__isNatIList#] = 0,
       [a__isNatList#] = 0,
       [uTake2](x0, x1, x2, x3) = x0 + x1 + x2 + x3 + 1,
       [uLength](x0, x1) = x0 + x1,
       [and](x0, x1) = x0 + x1,
       [take](x0, x1) = x0 + x1 + 1,
       [cons](x0, x1) = x0 + x1,
       [a__and](x0, x1) = x0 + x1,
       [isNat] = 0,
       [isNatList] = 0,
       [isNatIList] = 0,
       [a__isNat] = 0,
       [a__isNatIList] = 0,
       [a__isNatList] = 0
      Strict:
       {                mark#(s(X)) -> mark#(X),
                   mark#(length(X)) -> mark#(X),
                   mark#(length(X)) -> a__length#(mark(X)),
                mark#(cons(X1, X2)) -> mark#(X1),
                 mark#(and(X1, X2)) -> mark#(X1),
                 mark#(and(X1, X2)) -> mark#(X2),
                 mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
               mark#(isNatIList(X)) -> a__isNatIList#(X),
                mark#(isNatList(X)) -> a__isNatList#(X),
                    mark#(isNat(X)) -> a__isNat#(X),
                   mark#(uTake1(X)) -> mark#(X),
             mark#(uLength(X1, X2)) -> mark#(X1),
             mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2),
                   a__and#(tt(), T) -> mark#(T),
          a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
          a__isNatList#(cons(N, L)) -> a__isNatList#(L),
          a__isNatList#(cons(N, L)) -> a__isNat#(N),
         a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
         a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
         a__isNatList#(take(N, IL)) -> a__isNat#(N),
                 a__isNatIList#(IL) -> a__isNatList#(IL),
        a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
        a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
        a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                    a__isNat#(s(N)) -> a__isNat#(N),
               a__isNat#(length(L)) -> a__isNatList#(L),
                  a__take#(0(), IL) -> a__isNatIList#(IL),
        a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
        a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))),
        a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL),
        a__take#(s(M), cons(N, IL)) -> a__isNat#(N),
        a__take#(s(M), cons(N, IL)) -> a__isNat#(M),
        a__take#(s(M), cons(N, IL)) -> a__uTake2#(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
         a__uTake2#(tt(), M, N, IL) -> mark#(N),
               a__uLength#(tt(), L) -> mark#(L),
               a__uLength#(tt(), L) -> a__length#(mark(L)),
             a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
             a__length#(cons(N, L)) -> a__isNatList#(L),
             a__length#(cons(N, L)) -> a__isNat#(N),
             a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L)}
      Weak:
       {                  mark(tt()) -> tt(),
                           mark(0()) -> 0(),
                          mark(s(X)) -> s(mark(X)),
                     mark(length(X)) -> a__length(mark(X)),
                       mark(zeros()) -> a__zeros(),
                  mark(cons(X1, X2)) -> cons(mark(X1), X2),
                         mark(nil()) -> nil(),
                  mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                   mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                 mark(isNatIList(X)) -> a__isNatIList(X),
                  mark(isNatList(X)) -> a__isNatList(X),
                      mark(isNat(X)) -> a__isNat(X),
                     mark(uTake1(X)) -> a__uTake1(mark(X)),
        mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
               mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                      a__and(X1, X2) -> and(X1, X2),
                     a__and(tt(), T) -> mark(T),
                     a__isNatList(X) -> isNatList(X),
            a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                 a__isNatList(nil()) -> tt(),
           a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                   a__isNatIList(IL) -> a__isNatList(IL),
                    a__isNatIList(X) -> isNatIList(X),
              a__isNatIList(zeros()) -> tt(),
          a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                         a__isNat(X) -> isNat(X),
                       a__isNat(0()) -> tt(),
                      a__isNat(s(N)) -> a__isNat(N),
                 a__isNat(length(L)) -> a__isNatList(L),
                          a__zeros() -> zeros(),
                          a__zeros() -> cons(0(), zeros()),
                        a__uTake1(X) -> uTake1(X),
                     a__uTake1(tt()) -> nil(),
                     a__take(X1, X2) -> take(X1, X2),
                    a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
          a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
           a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
           a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                  a__uLength(X1, X2) -> uLength(X1, X2),
                 a__uLength(tt(), L) -> s(a__length(mark(L))),
                        a__length(X) -> length(X),
               a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
      EDG:
       {
        (a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), a__and#(tt(), T) -> mark#(T))
        (a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L), a__uLength#(tt(), L) -> a__length#(mark(L)))
        (a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L), a__uLength#(tt(), L) -> mark#(L))
        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNat#(N))
        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNat#(N))
        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
        (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
        (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
        (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
        (a__uLength#(tt(), L) -> mark#(L), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (a__uLength#(tt(), L) -> mark#(L), mark#(uLength(X1, X2)) -> mark#(X1))
        (a__uLength#(tt(), L) -> mark#(L), mark#(uTake1(X)) -> mark#(X))
        (a__uLength#(tt(), L) -> mark#(L), mark#(isNat(X)) -> a__isNat#(X))
        (a__uLength#(tt(), L) -> mark#(L), mark#(isNatList(X)) -> a__isNatList#(X))
        (a__uLength#(tt(), L) -> mark#(L), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (a__uLength#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (a__uLength#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> mark#(X2))
        (a__uLength#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> mark#(X1))
        (a__uLength#(tt(), L) -> mark#(L), mark#(cons(X1, X2)) -> mark#(X1))
        (a__uLength#(tt(), L) -> mark#(L), mark#(length(X)) -> a__length#(mark(X)))
        (a__uLength#(tt(), L) -> mark#(L), mark#(length(X)) -> mark#(X))
        (a__uLength#(tt(), L) -> mark#(L), mark#(s(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X)))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> mark#(X1))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X)))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X))
        (mark#(uLength(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(length(X)) -> mark#(X), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (mark#(length(X)) -> mark#(X), mark#(uLength(X1, X2)) -> mark#(X1))
        (mark#(length(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))
        (mark#(length(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(length(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
        (mark#(length(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (mark#(length(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (mark#(length(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
        (mark#(length(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(length(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(length(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X)))
        (mark#(length(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
        (mark#(length(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNat#(N))
        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNat#(N))
        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
        (mark#(uTake1(X)) -> mark#(X), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (mark#(uTake1(X)) -> mark#(X), mark#(uLength(X1, X2)) -> mark#(X1))
        (mark#(uTake1(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))
        (mark#(uTake1(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(uTake1(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
        (mark#(uTake1(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
        (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(uTake1(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(uTake1(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X)))
        (mark#(uTake1(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
        (mark#(uTake1(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
        (a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
        (a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
        (a__and#(tt(), T) -> mark#(T), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (a__and#(tt(), T) -> mark#(T), mark#(uLength(X1, X2)) -> mark#(X1))
        (a__and#(tt(), T) -> mark#(T), mark#(uTake1(X)) -> mark#(X))
        (a__and#(tt(), T) -> mark#(T), mark#(isNat(X)) -> a__isNat#(X))
        (a__and#(tt(), T) -> mark#(T), mark#(isNatList(X)) -> a__isNatList#(X))
        (a__and#(tt(), T) -> mark#(T), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X2))
        (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X1))
        (a__and#(tt(), T) -> mark#(T), mark#(cons(X1, X2)) -> mark#(X1))
        (a__and#(tt(), T) -> mark#(T), mark#(length(X)) -> a__length#(mark(X)))
        (a__and#(tt(), T) -> mark#(T), mark#(length(X)) -> mark#(X))
        (a__and#(tt(), T) -> mark#(T), mark#(s(X)) -> mark#(X))
        (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
        (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
        (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
        (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(uLength(X1, X2)) -> mark#(X1))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(uTake1(X)) -> mark#(X))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(isNatList(X)) -> a__isNatList#(X))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(and(X1, X2)) -> mark#(X2))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(length(X)) -> a__length#(mark(X)))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(length(X)) -> mark#(X))
        (a__uTake2#(tt(), M, N, IL) -> mark#(N), mark#(s(X)) -> mark#(X))
        (a__take#(s(M), cons(N, IL)) -> a__isNat#(M), a__isNat#(length(L)) -> a__isNatList#(L))
        (a__take#(s(M), cons(N, IL)) -> a__isNat#(M), a__isNat#(s(N)) -> a__isNat#(N))
        (a__take#(s(M), cons(N, IL)) -> a__uTake2#(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL), a__uTake2#(tt(), M, N, IL) -> mark#(N))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(length(X)) -> mark#(X))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(length(X)) -> a__length#(mark(X)))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X2))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(uTake1(X)) -> mark#(X))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(uLength(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X2), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (a__length#(cons(N, L)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
        (a__length#(cons(N, L)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
        (a__take#(s(M), cons(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
        (a__take#(s(M), cons(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
        (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
        (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
        (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
        (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
        (mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2), a__uLength#(tt(), L) -> mark#(L))
        (mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2), a__uLength#(tt(), L) -> a__length#(mark(L)))
        (a__take#(s(M), cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
        (a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
        (mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)), a__and#(tt(), T) -> mark#(T))
        (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(N)) -> a__isNat#(N))
        (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(length(L)) -> a__isNatList#(L))
        (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(IL) -> a__isNatList#(IL))
        (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
        (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
        (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(length(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X)))
        (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
        (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(s(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(uLength(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X)))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2))
        (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
        (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
        (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
        (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
        (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
        (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
        (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
        (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
        (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
        (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
        (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
        (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
        (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
        (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
        (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
        (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
        (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
        (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
        (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
        (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
        (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
        (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__isNatList#(L))
        (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__isNat#(N))
        (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L))
        (mark#(length(X)) -> a__length#(mark(X)), a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
        (mark#(length(X)) -> a__length#(mark(X)), a__length#(cons(N, L)) -> a__isNatList#(L))
        (mark#(length(X)) -> a__length#(mark(X)), a__length#(cons(N, L)) -> a__isNat#(N))
        (mark#(length(X)) -> a__length#(mark(X)), a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L))
       }
       SCCS:
        Scc:
         {                mark#(s(X)) -> mark#(X),
                     mark#(length(X)) -> mark#(X),
                     mark#(length(X)) -> a__length#(mark(X)),
                  mark#(cons(X1, X2)) -> mark#(X1),
                   mark#(and(X1, X2)) -> mark#(X1),
                   mark#(and(X1, X2)) -> mark#(X2),
                   mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                 mark#(isNatIList(X)) -> a__isNatIList#(X),
                  mark#(isNatList(X)) -> a__isNatList#(X),
                      mark#(isNat(X)) -> a__isNat#(X),
                     mark#(uTake1(X)) -> mark#(X),
               mark#(uLength(X1, X2)) -> mark#(X1),
               mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2),
                     a__and#(tt(), T) -> mark#(T),
            a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
            a__isNatList#(cons(N, L)) -> a__isNatList#(L),
            a__isNatList#(cons(N, L)) -> a__isNat#(N),
           a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
           a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
           a__isNatList#(take(N, IL)) -> a__isNat#(N),
                   a__isNatIList#(IL) -> a__isNatList#(IL),
          a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
          a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
          a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                      a__isNat#(s(N)) -> a__isNat#(N),
                 a__isNat#(length(L)) -> a__isNatList#(L),
                 a__uLength#(tt(), L) -> mark#(L),
                 a__uLength#(tt(), L) -> a__length#(mark(L)),
               a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
               a__length#(cons(N, L)) -> a__isNatList#(L),
               a__length#(cons(N, L)) -> a__isNat#(N),
               a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L)}
        SCC:
         Strict:
          {                mark#(s(X)) -> mark#(X),
                      mark#(length(X)) -> mark#(X),
                      mark#(length(X)) -> a__length#(mark(X)),
                   mark#(cons(X1, X2)) -> mark#(X1),
                    mark#(and(X1, X2)) -> mark#(X1),
                    mark#(and(X1, X2)) -> mark#(X2),
                    mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                  mark#(isNatIList(X)) -> a__isNatIList#(X),
                   mark#(isNatList(X)) -> a__isNatList#(X),
                       mark#(isNat(X)) -> a__isNat#(X),
                      mark#(uTake1(X)) -> mark#(X),
                mark#(uLength(X1, X2)) -> mark#(X1),
                mark#(uLength(X1, X2)) -> a__uLength#(mark(X1), X2),
                      a__and#(tt(), T) -> mark#(T),
             a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
             a__isNatList#(cons(N, L)) -> a__isNatList#(L),
             a__isNatList#(cons(N, L)) -> a__isNat#(N),
            a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
            a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
            a__isNatList#(take(N, IL)) -> a__isNat#(N),
                    a__isNatIList#(IL) -> a__isNatList#(IL),
           a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
           a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
           a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                       a__isNat#(s(N)) -> a__isNat#(N),
                  a__isNat#(length(L)) -> a__isNatList#(L),
                  a__uLength#(tt(), L) -> mark#(L),
                  a__uLength#(tt(), L) -> a__length#(mark(L)),
                a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                a__length#(cons(N, L)) -> a__isNatList#(L),
                a__length#(cons(N, L)) -> a__isNat#(N),
                a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L)}
         Weak:
         {                  mark(tt()) -> tt(),
                             mark(0()) -> 0(),
                            mark(s(X)) -> s(mark(X)),
                       mark(length(X)) -> a__length(mark(X)),
                         mark(zeros()) -> a__zeros(),
                    mark(cons(X1, X2)) -> cons(mark(X1), X2),
                           mark(nil()) -> nil(),
                    mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                     mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                   mark(isNatIList(X)) -> a__isNatIList(X),
                    mark(isNatList(X)) -> a__isNatList(X),
                        mark(isNat(X)) -> a__isNat(X),
                       mark(uTake1(X)) -> a__uTake1(mark(X)),
          mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                 mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                        a__and(X1, X2) -> and(X1, X2),
                       a__and(tt(), T) -> mark(T),
                       a__isNatList(X) -> isNatList(X),
              a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                   a__isNatList(nil()) -> tt(),
             a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                     a__isNatIList(IL) -> a__isNatList(IL),
                      a__isNatIList(X) -> isNatIList(X),
                a__isNatIList(zeros()) -> tt(),
            a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                           a__isNat(X) -> isNat(X),
                         a__isNat(0()) -> tt(),
                        a__isNat(s(N)) -> a__isNat(N),
                   a__isNat(length(L)) -> a__isNatList(L),
                            a__zeros() -> zeros(),
                            a__zeros() -> cons(0(), zeros()),
                          a__uTake1(X) -> uTake1(X),
                       a__uTake1(tt()) -> nil(),
                       a__take(X1, X2) -> take(X1, X2),
                      a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
            a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
             a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
             a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                    a__uLength(X1, X2) -> uLength(X1, X2),
                   a__uLength(tt(), L) -> s(a__length(mark(L))),
                          a__length(X) -> length(X),
                 a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
         POLY:
          Argument Filtering:
           pi(uLength) = [0,1], pi(uTake2) = [2,3], pi(uTake1) = 0, pi(isNat) = [], pi(isNatList) = [], pi(isNatIList) = [], pi(and) = [0,1], pi(a__length#) = 0, pi(a__length) = [0], pi(a__uLength#) = 1, pi(a__uLength) = [0,1], pi(a__uTake2) = [2,3], pi(a__take) = 1, pi(a__uTake1) = 0, pi(a__zeros) = [], pi(take) = 1, pi(nil) = [], pi(cons) = [0,1], pi(zeros) = [], pi(length) = [0], pi(s) = 0, pi(0) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__isNatIList#) = [], pi(a__isNatIList) = [], pi(a__isNatList#) = [], pi(a__isNatList) = [], pi(tt) = [], pi(a__and#) = 1, pi(a__and) = [0,1], pi(mark#) = 0, pi(mark) = 0
          Usable Rules:
           {}
          Interpretation:
           [a__isNat#] = 0,
           [a__isNatIList#] = 0,
           [a__isNatList#] = 0,
           [uLength](x0, x1) = x0 + x1 + 1,
           [and](x0, x1) = x0 + x1,
           [cons](x0, x1) = x0 + x1,
           [isNat] = 0,
           [isNatList] = 0,
           [isNatIList] = 0,
           [length](x0) = x0 + 1,
           [a__isNatIList] = 0,
           [a__isNatList] = 0
          Strict:
           {                mark#(s(X)) -> mark#(X),
                    mark#(cons(X1, X2)) -> mark#(X1),
                     mark#(and(X1, X2)) -> mark#(X1),
                     mark#(and(X1, X2)) -> mark#(X2),
                     mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                   mark#(isNatIList(X)) -> a__isNatIList#(X),
                    mark#(isNatList(X)) -> a__isNatList#(X),
                        mark#(isNat(X)) -> a__isNat#(X),
                       mark#(uTake1(X)) -> mark#(X),
                       a__and#(tt(), T) -> mark#(T),
              a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
              a__isNatList#(cons(N, L)) -> a__isNatList#(L),
              a__isNatList#(cons(N, L)) -> a__isNat#(N),
             a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
             a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
             a__isNatList#(take(N, IL)) -> a__isNat#(N),
                     a__isNatIList#(IL) -> a__isNatList#(IL),
            a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
            a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
            a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                        a__isNat#(s(N)) -> a__isNat#(N),
                   a__isNat#(length(L)) -> a__isNatList#(L),
                   a__uLength#(tt(), L) -> mark#(L),
                   a__uLength#(tt(), L) -> a__length#(mark(L)),
                 a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                 a__length#(cons(N, L)) -> a__isNatList#(L),
                 a__length#(cons(N, L)) -> a__isNat#(N),
                 a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L)}
          Weak:
           {                  mark(tt()) -> tt(),
                               mark(0()) -> 0(),
                              mark(s(X)) -> s(mark(X)),
                         mark(length(X)) -> a__length(mark(X)),
                           mark(zeros()) -> a__zeros(),
                      mark(cons(X1, X2)) -> cons(mark(X1), X2),
                             mark(nil()) -> nil(),
                      mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                       mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                     mark(isNatIList(X)) -> a__isNatIList(X),
                      mark(isNatList(X)) -> a__isNatList(X),
                          mark(isNat(X)) -> a__isNat(X),
                         mark(uTake1(X)) -> a__uTake1(mark(X)),
            mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                   mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                          a__and(X1, X2) -> and(X1, X2),
                         a__and(tt(), T) -> mark(T),
                         a__isNatList(X) -> isNatList(X),
                a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                     a__isNatList(nil()) -> tt(),
               a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                       a__isNatIList(IL) -> a__isNatList(IL),
                        a__isNatIList(X) -> isNatIList(X),
                  a__isNatIList(zeros()) -> tt(),
              a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                             a__isNat(X) -> isNat(X),
                           a__isNat(0()) -> tt(),
                          a__isNat(s(N)) -> a__isNat(N),
                     a__isNat(length(L)) -> a__isNatList(L),
                              a__zeros() -> zeros(),
                              a__zeros() -> cons(0(), zeros()),
                            a__uTake1(X) -> uTake1(X),
                         a__uTake1(tt()) -> nil(),
                         a__take(X1, X2) -> take(X1, X2),
                        a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
              a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
               a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
               a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                      a__uLength(X1, X2) -> uLength(X1, X2),
                     a__uLength(tt(), L) -> s(a__length(mark(L))),
                            a__length(X) -> length(X),
                   a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
          EDG:
           {
            (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
            (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
            (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
            (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
            (a__length#(cons(N, L)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
            (a__length#(cons(N, L)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
            (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
            (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
            (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
            (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
            (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
            (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
            (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
            (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
            (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L))
            (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__isNat#(N))
            (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__isNatList#(L))
            (a__uLength#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
            (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
            (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
            (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
            (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(IL) -> a__isNatList#(IL))
            (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(length(L)) -> a__isNatList#(L))
            (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(N)) -> a__isNat#(N))
            (mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)), a__and#(tt(), T) -> mark#(T))
            (a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
            (a__length#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
            (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
            (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
            (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
            (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
            (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
            (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
            (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
            (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
            (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
            (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
            (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
            (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
            (a__uLength#(tt(), L) -> mark#(L), mark#(s(X)) -> mark#(X))
            (a__uLength#(tt(), L) -> mark#(L), mark#(cons(X1, X2)) -> mark#(X1))
            (a__uLength#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> mark#(X1))
            (a__uLength#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> mark#(X2))
            (a__uLength#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
            (a__uLength#(tt(), L) -> mark#(L), mark#(isNatIList(X)) -> a__isNatIList#(X))
            (a__uLength#(tt(), L) -> mark#(L), mark#(isNatList(X)) -> a__isNatList#(X))
            (a__uLength#(tt(), L) -> mark#(L), mark#(isNat(X)) -> a__isNat#(X))
            (a__uLength#(tt(), L) -> mark#(L), mark#(uTake1(X)) -> mark#(X))
            (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
            (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
            (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
            (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
            (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
            (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
            (a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
            (a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
            (mark#(uTake1(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
            (mark#(uTake1(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
            (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
            (mark#(uTake1(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
            (mark#(uTake1(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
            (mark#(uTake1(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
            (mark#(uTake1(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))
            (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
            (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
            (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNat#(N))
            (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
            (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
            (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNat#(N))
            (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
            (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
            (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
            (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
            (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
            (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
            (mark#(s(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))
            (a__and#(tt(), T) -> mark#(T), mark#(s(X)) -> mark#(X))
            (a__and#(tt(), T) -> mark#(T), mark#(cons(X1, X2)) -> mark#(X1))
            (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X1))
            (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X2))
            (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
            (a__and#(tt(), T) -> mark#(T), mark#(isNatIList(X)) -> a__isNatIList#(X))
            (a__and#(tt(), T) -> mark#(T), mark#(isNatList(X)) -> a__isNatList#(X))
            (a__and#(tt(), T) -> mark#(T), mark#(isNat(X)) -> a__isNat#(X))
            (a__and#(tt(), T) -> mark#(T), mark#(uTake1(X)) -> mark#(X))
            (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
            (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
            (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNat#(N))
            (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
            (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
            (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNat#(N))
            (a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L), a__uLength#(tt(), L) -> mark#(L))
            (a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L), a__uLength#(tt(), L) -> a__length#(mark(L)))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
            (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
            (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
            (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
            (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
            (mark#(and(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
            (mark#(and(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X2))
            (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
            (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X))
            (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X))
            (mark#(and(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
            (mark#(and(X1, X2)) -> mark#(X2), mark#(uTake1(X)) -> mark#(X))
           }
           SCCS:
            Scc:
             {  a__uLength#(tt(), L) -> a__length#(mark(L)),
              a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L)}
            Scc:
             {                mark#(s(X)) -> mark#(X),
                      mark#(cons(X1, X2)) -> mark#(X1),
                       mark#(and(X1, X2)) -> mark#(X1),
                       mark#(and(X1, X2)) -> mark#(X2),
                       mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                     mark#(isNatIList(X)) -> a__isNatIList#(X),
                      mark#(isNatList(X)) -> a__isNatList#(X),
                          mark#(isNat(X)) -> a__isNat#(X),
                         mark#(uTake1(X)) -> mark#(X),
                         a__and#(tt(), T) -> mark#(T),
                a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                a__isNatList#(cons(N, L)) -> a__isNat#(N),
               a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
               a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
               a__isNatList#(take(N, IL)) -> a__isNat#(N),
                       a__isNatIList#(IL) -> a__isNatList#(IL),
              a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
              a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
              a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                          a__isNat#(s(N)) -> a__isNat#(N),
                     a__isNat#(length(L)) -> a__isNatList#(L)}
            SCC:
             Strict:
              {  a__uLength#(tt(), L) -> a__length#(mark(L)),
               a__length#(cons(N, L)) -> a__uLength#(a__and(a__isNat(N), a__isNatList(L)), L)}
             Weak:
             {                  mark(tt()) -> tt(),
                                 mark(0()) -> 0(),
                                mark(s(X)) -> s(mark(X)),
                           mark(length(X)) -> a__length(mark(X)),
                             mark(zeros()) -> a__zeros(),
                        mark(cons(X1, X2)) -> cons(mark(X1), X2),
                               mark(nil()) -> nil(),
                        mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                         mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                       mark(isNatIList(X)) -> a__isNatIList(X),
                        mark(isNatList(X)) -> a__isNatList(X),
                            mark(isNat(X)) -> a__isNat(X),
                           mark(uTake1(X)) -> a__uTake1(mark(X)),
              mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                     mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                            a__and(X1, X2) -> and(X1, X2),
                           a__and(tt(), T) -> mark(T),
                           a__isNatList(X) -> isNatList(X),
                  a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                       a__isNatList(nil()) -> tt(),
                 a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                         a__isNatIList(IL) -> a__isNatList(IL),
                          a__isNatIList(X) -> isNatIList(X),
                    a__isNatIList(zeros()) -> tt(),
                a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                               a__isNat(X) -> isNat(X),
                             a__isNat(0()) -> tt(),
                            a__isNat(s(N)) -> a__isNat(N),
                       a__isNat(length(L)) -> a__isNatList(L),
                                a__zeros() -> zeros(),
                                a__zeros() -> cons(0(), zeros()),
                              a__uTake1(X) -> uTake1(X),
                           a__uTake1(tt()) -> nil(),
                           a__take(X1, X2) -> take(X1, X2),
                          a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                 a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                 a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                        a__uLength(X1, X2) -> uLength(X1, X2),
                       a__uLength(tt(), L) -> s(a__length(mark(L))),
                              a__length(X) -> length(X),
                     a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
             Fail
            SCC:
             Strict:
              {                mark#(s(X)) -> mark#(X),
                       mark#(cons(X1, X2)) -> mark#(X1),
                        mark#(and(X1, X2)) -> mark#(X1),
                        mark#(and(X1, X2)) -> mark#(X2),
                        mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                      mark#(isNatIList(X)) -> a__isNatIList#(X),
                       mark#(isNatList(X)) -> a__isNatList#(X),
                           mark#(isNat(X)) -> a__isNat#(X),
                          mark#(uTake1(X)) -> mark#(X),
                          a__and#(tt(), T) -> mark#(T),
                 a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                 a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                 a__isNatList#(cons(N, L)) -> a__isNat#(N),
                a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                a__isNatList#(take(N, IL)) -> a__isNat#(N),
                        a__isNatIList#(IL) -> a__isNatList#(IL),
               a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
               a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
               a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                           a__isNat#(s(N)) -> a__isNat#(N),
                      a__isNat#(length(L)) -> a__isNatList#(L)}
             Weak:
             {                  mark(tt()) -> tt(),
                                 mark(0()) -> 0(),
                                mark(s(X)) -> s(mark(X)),
                           mark(length(X)) -> a__length(mark(X)),
                             mark(zeros()) -> a__zeros(),
                        mark(cons(X1, X2)) -> cons(mark(X1), X2),
                               mark(nil()) -> nil(),
                        mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                         mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                       mark(isNatIList(X)) -> a__isNatIList(X),
                        mark(isNatList(X)) -> a__isNatList(X),
                            mark(isNat(X)) -> a__isNat(X),
                           mark(uTake1(X)) -> a__uTake1(mark(X)),
              mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                     mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                            a__and(X1, X2) -> and(X1, X2),
                           a__and(tt(), T) -> mark(T),
                           a__isNatList(X) -> isNatList(X),
                  a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                       a__isNatList(nil()) -> tt(),
                 a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                         a__isNatIList(IL) -> a__isNatList(IL),
                          a__isNatIList(X) -> isNatIList(X),
                    a__isNatIList(zeros()) -> tt(),
                a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                               a__isNat(X) -> isNat(X),
                             a__isNat(0()) -> tt(),
                            a__isNat(s(N)) -> a__isNat(N),
                       a__isNat(length(L)) -> a__isNatList(L),
                                a__zeros() -> zeros(),
                                a__zeros() -> cons(0(), zeros()),
                              a__uTake1(X) -> uTake1(X),
                           a__uTake1(tt()) -> nil(),
                           a__take(X1, X2) -> take(X1, X2),
                          a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                 a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                 a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                        a__uLength(X1, X2) -> uLength(X1, X2),
                       a__uLength(tt(), L) -> s(a__length(mark(L))),
                              a__length(X) -> length(X),
                     a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
             POLY:
              Argument Filtering:
               pi(uLength) = [], pi(uTake2) = [2], pi(uTake1) = 0, pi(isNat) = [], pi(isNatList) = [], pi(isNatIList) = [], pi(and) = [0,1], pi(a__length) = [], pi(a__uLength) = [], pi(a__uTake2) = [2], pi(a__take) = 1, pi(a__uTake1) = 0, pi(a__zeros) = [], pi(take) = 1, pi(nil) = [], pi(cons) = [0], pi(zeros) = [], pi(length) = [], pi(s) = 0, pi(0) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__isNatIList#) = [], pi(a__isNatIList) = [], pi(a__isNatList#) = [], pi(a__isNatList) = [], pi(tt) = [], pi(a__and#) = 1, pi(a__and) = [0,1], pi(mark#) = 0, pi(mark) = 0
              Usable Rules:
               {}
              Interpretation:
               [a__isNat#] = 0,
               [a__isNatIList#] = 0,
               [a__isNatList#] = 0,
               [and](x0, x1) = x0 + x1,
               [cons](x0) = x0 + 1,
               [isNat] = 0,
               [isNatList] = 0,
               [isNatIList] = 0,
               [a__isNatIList] = 0,
               [a__isNatList] = 0
              Strict:
               {                mark#(s(X)) -> mark#(X),
                         mark#(and(X1, X2)) -> mark#(X1),
                         mark#(and(X1, X2)) -> mark#(X2),
                         mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                       mark#(isNatIList(X)) -> a__isNatIList#(X),
                        mark#(isNatList(X)) -> a__isNatList#(X),
                            mark#(isNat(X)) -> a__isNat#(X),
                           mark#(uTake1(X)) -> mark#(X),
                           a__and#(tt(), T) -> mark#(T),
                  a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                  a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                  a__isNatList#(cons(N, L)) -> a__isNat#(N),
                 a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                 a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                 a__isNatList#(take(N, IL)) -> a__isNat#(N),
                         a__isNatIList#(IL) -> a__isNatList#(IL),
                a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
                a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                            a__isNat#(s(N)) -> a__isNat#(N),
                       a__isNat#(length(L)) -> a__isNatList#(L)}
              Weak:
               {                  mark(tt()) -> tt(),
                                   mark(0()) -> 0(),
                                  mark(s(X)) -> s(mark(X)),
                             mark(length(X)) -> a__length(mark(X)),
                               mark(zeros()) -> a__zeros(),
                          mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                 mark(nil()) -> nil(),
                          mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                           mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                         mark(isNatIList(X)) -> a__isNatIList(X),
                          mark(isNatList(X)) -> a__isNatList(X),
                              mark(isNat(X)) -> a__isNat(X),
                             mark(uTake1(X)) -> a__uTake1(mark(X)),
                mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                       mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                              a__and(X1, X2) -> and(X1, X2),
                             a__and(tt(), T) -> mark(T),
                             a__isNatList(X) -> isNatList(X),
                    a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                         a__isNatList(nil()) -> tt(),
                   a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                           a__isNatIList(IL) -> a__isNatList(IL),
                            a__isNatIList(X) -> isNatIList(X),
                      a__isNatIList(zeros()) -> tt(),
                  a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                 a__isNat(X) -> isNat(X),
                               a__isNat(0()) -> tt(),
                              a__isNat(s(N)) -> a__isNat(N),
                         a__isNat(length(L)) -> a__isNatList(L),
                                  a__zeros() -> zeros(),
                                  a__zeros() -> cons(0(), zeros()),
                                a__uTake1(X) -> uTake1(X),
                             a__uTake1(tt()) -> nil(),
                             a__take(X1, X2) -> take(X1, X2),
                            a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                  a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                   a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                   a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                          a__uLength(X1, X2) -> uLength(X1, X2),
                         a__uLength(tt(), L) -> s(a__length(mark(L))),
                                a__length(X) -> length(X),
                       a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
              EDG:
               {(mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
                (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(IL) -> a__isNatList#(IL))
                (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(length(L)) -> a__isNatList#(L))
                (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(N)) -> a__isNat#(N))
                (mark#(and(X1, X2)) -> mark#(X2), mark#(uTake1(X)) -> mark#(X))
                (mark#(and(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
                (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X))
                (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X))
                (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X2))
                (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
                (mark#(and(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
                (mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)), a__and#(tt(), T) -> mark#(T))
                (a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
                (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
                (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
                (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
                (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
                (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
                (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
                (a__and#(tt(), T) -> mark#(T), mark#(s(X)) -> mark#(X))
                (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X1))
                (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X2))
                (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                (a__and#(tt(), T) -> mark#(T), mark#(isNatIList(X)) -> a__isNatIList#(X))
                (a__and#(tt(), T) -> mark#(T), mark#(isNatList(X)) -> a__isNatList#(X))
                (a__and#(tt(), T) -> mark#(T), mark#(isNat(X)) -> a__isNat#(X))
                (a__and#(tt(), T) -> mark#(T), mark#(uTake1(X)) -> mark#(X))
                (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
                (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
                (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                (a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
                (a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(uTake1(X)) -> mark#(X))
                (mark#(uTake1(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
                (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
                (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
                (mark#(uTake1(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                (mark#(uTake1(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
                (mark#(uTake1(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
                (mark#(uTake1(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
                (mark#(uTake1(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))
                (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
                (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
                (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
                (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
                (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
                (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
                (mark#(s(X)) -> mark#(X), mark#(uTake1(X)) -> mark#(X))}
               SCCS:
                Scc:
                 {                mark#(s(X)) -> mark#(X),
                           mark#(and(X1, X2)) -> mark#(X1),
                           mark#(and(X1, X2)) -> mark#(X2),
                           mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                         mark#(isNatIList(X)) -> a__isNatIList#(X),
                          mark#(isNatList(X)) -> a__isNatList#(X),
                              mark#(isNat(X)) -> a__isNat#(X),
                             mark#(uTake1(X)) -> mark#(X),
                             a__and#(tt(), T) -> mark#(T),
                    a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                    a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                    a__isNatList#(cons(N, L)) -> a__isNat#(N),
                   a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                   a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                   a__isNatList#(take(N, IL)) -> a__isNat#(N),
                           a__isNatIList#(IL) -> a__isNatList#(IL),
                  a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                  a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
                  a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                              a__isNat#(s(N)) -> a__isNat#(N),
                         a__isNat#(length(L)) -> a__isNatList#(L)}
                SCC:
                 Strict:
                  {                mark#(s(X)) -> mark#(X),
                            mark#(and(X1, X2)) -> mark#(X1),
                            mark#(and(X1, X2)) -> mark#(X2),
                            mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                          mark#(isNatIList(X)) -> a__isNatIList#(X),
                           mark#(isNatList(X)) -> a__isNatList#(X),
                               mark#(isNat(X)) -> a__isNat#(X),
                              mark#(uTake1(X)) -> mark#(X),
                              a__and#(tt(), T) -> mark#(T),
                     a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                     a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                     a__isNatList#(cons(N, L)) -> a__isNat#(N),
                    a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                    a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                    a__isNatList#(take(N, IL)) -> a__isNat#(N),
                            a__isNatIList#(IL) -> a__isNatList#(IL),
                   a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                   a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
                   a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                               a__isNat#(s(N)) -> a__isNat#(N),
                          a__isNat#(length(L)) -> a__isNatList#(L)}
                 Weak:
                 {                  mark(tt()) -> tt(),
                                     mark(0()) -> 0(),
                                    mark(s(X)) -> s(mark(X)),
                               mark(length(X)) -> a__length(mark(X)),
                                 mark(zeros()) -> a__zeros(),
                            mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                   mark(nil()) -> nil(),
                            mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                             mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                           mark(isNatIList(X)) -> a__isNatIList(X),
                            mark(isNatList(X)) -> a__isNatList(X),
                                mark(isNat(X)) -> a__isNat(X),
                               mark(uTake1(X)) -> a__uTake1(mark(X)),
                  mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                         mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                a__and(X1, X2) -> and(X1, X2),
                               a__and(tt(), T) -> mark(T),
                               a__isNatList(X) -> isNatList(X),
                      a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                           a__isNatList(nil()) -> tt(),
                     a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                             a__isNatIList(IL) -> a__isNatList(IL),
                              a__isNatIList(X) -> isNatIList(X),
                        a__isNatIList(zeros()) -> tt(),
                    a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                   a__isNat(X) -> isNat(X),
                                 a__isNat(0()) -> tt(),
                                a__isNat(s(N)) -> a__isNat(N),
                           a__isNat(length(L)) -> a__isNatList(L),
                                    a__zeros() -> zeros(),
                                    a__zeros() -> cons(0(), zeros()),
                                  a__uTake1(X) -> uTake1(X),
                               a__uTake1(tt()) -> nil(),
                               a__take(X1, X2) -> take(X1, X2),
                              a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                    a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                     a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                     a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                            a__uLength(X1, X2) -> uLength(X1, X2),
                           a__uLength(tt(), L) -> s(a__length(mark(L))),
                                  a__length(X) -> length(X),
                         a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                 POLY:
                  Argument Filtering:
                   pi(uLength) = [], pi(uTake2) = [], pi(uTake1) = [0], pi(isNat) = [], pi(isNatList) = [], pi(isNatIList) = [], pi(and) = [0,1], pi(a__length) = [], pi(a__uLength) = [], pi(a__uTake2) = [], pi(a__take) = [0], pi(a__uTake1) = [0], pi(a__zeros) = [], pi(take) = [0], pi(nil) = [], pi(cons) = [], pi(zeros) = [], pi(length) = [], pi(s) = 0, pi(0) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__isNatIList#) = [], pi(a__isNatIList) = [], pi(a__isNatList#) = [], pi(a__isNatList) = [], pi(tt) = [], pi(a__and#) = [1], pi(a__and) = [0,1], pi(mark#) = [0], pi(mark) = 0
                  Usable Rules:
                   {}
                  Interpretation:
                   [a__and#](x0) = x0 + 1,
                   [a__isNat#] = 1,
                   [a__isNatIList#] = 1,
                   [a__isNatList#] = 1,
                   [mark#](x0) = x0 + 1,
                   [and](x0, x1) = x0 + x1,
                   [uTake1](x0) = x0 + 1,
                   [isNat] = 0,
                   [isNatList] = 0,
                   [isNatIList] = 0,
                   [a__isNatIList] = 0,
                   [a__isNatList] = 0
                  Strict:
                   {                mark#(s(X)) -> mark#(X),
                             mark#(and(X1, X2)) -> mark#(X1),
                             mark#(and(X1, X2)) -> mark#(X2),
                             mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                           mark#(isNatIList(X)) -> a__isNatIList#(X),
                            mark#(isNatList(X)) -> a__isNatList#(X),
                                mark#(isNat(X)) -> a__isNat#(X),
                               a__and#(tt(), T) -> mark#(T),
                      a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                      a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                      a__isNatList#(cons(N, L)) -> a__isNat#(N),
                     a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                     a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                     a__isNatList#(take(N, IL)) -> a__isNat#(N),
                             a__isNatIList#(IL) -> a__isNatList#(IL),
                    a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                    a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
                    a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                                a__isNat#(s(N)) -> a__isNat#(N),
                           a__isNat#(length(L)) -> a__isNatList#(L)}
                  Weak:
                   {                  mark(tt()) -> tt(),
                                       mark(0()) -> 0(),
                                      mark(s(X)) -> s(mark(X)),
                                 mark(length(X)) -> a__length(mark(X)),
                                   mark(zeros()) -> a__zeros(),
                              mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                     mark(nil()) -> nil(),
                              mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                               mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                             mark(isNatIList(X)) -> a__isNatIList(X),
                              mark(isNatList(X)) -> a__isNatList(X),
                                  mark(isNat(X)) -> a__isNat(X),
                                 mark(uTake1(X)) -> a__uTake1(mark(X)),
                    mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                           mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                  a__and(X1, X2) -> and(X1, X2),
                                 a__and(tt(), T) -> mark(T),
                                 a__isNatList(X) -> isNatList(X),
                        a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                             a__isNatList(nil()) -> tt(),
                       a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                               a__isNatIList(IL) -> a__isNatList(IL),
                                a__isNatIList(X) -> isNatIList(X),
                          a__isNatIList(zeros()) -> tt(),
                      a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                     a__isNat(X) -> isNat(X),
                                   a__isNat(0()) -> tt(),
                                  a__isNat(s(N)) -> a__isNat(N),
                             a__isNat(length(L)) -> a__isNatList(L),
                                      a__zeros() -> zeros(),
                                      a__zeros() -> cons(0(), zeros()),
                                    a__uTake1(X) -> uTake1(X),
                                 a__uTake1(tt()) -> nil(),
                                 a__take(X1, X2) -> take(X1, X2),
                                a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                      a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                       a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                       a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                              a__uLength(X1, X2) -> uLength(X1, X2),
                             a__uLength(tt(), L) -> s(a__length(mark(L))),
                                    a__length(X) -> length(X),
                           a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                  EDG:
                   {(a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
                    (a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
                    (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
                    (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                    (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                    (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
                    (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
                    (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                    (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                    (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
                    (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
                    (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                    (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
                    (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                    (a__isNat#(length(L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                    (mark#(and(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
                    (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X))
                    (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X))
                    (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                    (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X2))
                    (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
                    (mark#(and(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
                    (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
                    (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                    (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                    (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(IL) -> a__isNatList#(IL))
                    (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(length(L)) -> a__isNatList#(L))
                    (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(N)) -> a__isNat#(N))
                    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                    (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
                    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
                    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
                    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                    (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
                    (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
                    (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
                    (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
                    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
                    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
                    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                    (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
                    (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
                    (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
                    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                    (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                    (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                    (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
                    (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                    (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(length(L)) -> a__isNatList#(L))
                    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                    (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                    (a__and#(tt(), T) -> mark#(T), mark#(s(X)) -> mark#(X))
                    (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X1))
                    (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X2))
                    (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                    (a__and#(tt(), T) -> mark#(T), mark#(isNatIList(X)) -> a__isNatIList#(X))
                    (a__and#(tt(), T) -> mark#(T), mark#(isNatList(X)) -> a__isNatList#(X))
                    (a__and#(tt(), T) -> mark#(T), mark#(isNat(X)) -> a__isNat#(X))
                    (a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
                    (mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)), a__and#(tt(), T) -> mark#(T))}
                   SCCS:
                    Scc:
                     {                mark#(s(X)) -> mark#(X),
                               mark#(and(X1, X2)) -> mark#(X1),
                               mark#(and(X1, X2)) -> mark#(X2),
                               mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                             mark#(isNatIList(X)) -> a__isNatIList#(X),
                              mark#(isNatList(X)) -> a__isNatList#(X),
                                  mark#(isNat(X)) -> a__isNat#(X),
                                 a__and#(tt(), T) -> mark#(T),
                        a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                        a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                        a__isNatList#(cons(N, L)) -> a__isNat#(N),
                       a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                       a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                       a__isNatList#(take(N, IL)) -> a__isNat#(N),
                               a__isNatIList#(IL) -> a__isNatList#(IL),
                      a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                      a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
                      a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                                  a__isNat#(s(N)) -> a__isNat#(N),
                             a__isNat#(length(L)) -> a__isNatList#(L)}
                    SCC:
                     Strict:
                      {                mark#(s(X)) -> mark#(X),
                                mark#(and(X1, X2)) -> mark#(X1),
                                mark#(and(X1, X2)) -> mark#(X2),
                                mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                              mark#(isNatIList(X)) -> a__isNatIList#(X),
                               mark#(isNatList(X)) -> a__isNatList#(X),
                                   mark#(isNat(X)) -> a__isNat#(X),
                                  a__and#(tt(), T) -> mark#(T),
                         a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                         a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                         a__isNatList#(cons(N, L)) -> a__isNat#(N),
                        a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                        a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                        a__isNatList#(take(N, IL)) -> a__isNat#(N),
                                a__isNatIList#(IL) -> a__isNatList#(IL),
                       a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                       a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
                       a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                                   a__isNat#(s(N)) -> a__isNat#(N),
                              a__isNat#(length(L)) -> a__isNatList#(L)}
                     Weak:
                     {                  mark(tt()) -> tt(),
                                         mark(0()) -> 0(),
                                        mark(s(X)) -> s(mark(X)),
                                   mark(length(X)) -> a__length(mark(X)),
                                     mark(zeros()) -> a__zeros(),
                                mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                       mark(nil()) -> nil(),
                                mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                                 mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                               mark(isNatIList(X)) -> a__isNatIList(X),
                                mark(isNatList(X)) -> a__isNatList(X),
                                    mark(isNat(X)) -> a__isNat(X),
                                   mark(uTake1(X)) -> a__uTake1(mark(X)),
                      mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                             mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                    a__and(X1, X2) -> and(X1, X2),
                                   a__and(tt(), T) -> mark(T),
                                   a__isNatList(X) -> isNatList(X),
                          a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                               a__isNatList(nil()) -> tt(),
                         a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                 a__isNatIList(IL) -> a__isNatList(IL),
                                  a__isNatIList(X) -> isNatIList(X),
                            a__isNatIList(zeros()) -> tt(),
                        a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                       a__isNat(X) -> isNat(X),
                                     a__isNat(0()) -> tt(),
                                    a__isNat(s(N)) -> a__isNat(N),
                               a__isNat(length(L)) -> a__isNatList(L),
                                        a__zeros() -> zeros(),
                                        a__zeros() -> cons(0(), zeros()),
                                      a__uTake1(X) -> uTake1(X),
                                   a__uTake1(tt()) -> nil(),
                                   a__take(X1, X2) -> take(X1, X2),
                                  a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                        a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                         a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                         a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                                a__uLength(X1, X2) -> uLength(X1, X2),
                               a__uLength(tt(), L) -> s(a__length(mark(L))),
                                      a__length(X) -> length(X),
                             a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                     POLY:
                      Argument Filtering:
                       pi(uLength) = [1], pi(uTake2) = [1,2,3], pi(uTake1) = 0, pi(isNat) = 0, pi(isNatList) = 0, pi(isNatIList) = 0, pi(and) = [0,1], pi(a__length) = [0], pi(a__uLength) = [1], pi(a__uTake2) = [1,2,3], pi(a__take) = [0,1], pi(a__uTake1) = 0, pi(a__zeros) = [], pi(take) = [0,1], pi(nil) = [], pi(cons) = [0,1], pi(zeros) = [], pi(length) = [0], pi(s) = 0, pi(0) = [], pi(a__isNat#) = 0, pi(a__isNat) = 0, pi(a__isNatIList#) = 0, pi(a__isNatIList) = 0, pi(a__isNatList#) = 0, pi(a__isNatList) = 0, pi(tt) = [], pi(a__and#) = 1, pi(a__and) = [0,1], pi(mark#) = 0, pi(mark) = 0
                      Usable Rules:
                       {}
                      Interpretation:
                       [and](x0, x1) = x0 + x1,
                       [take](x0, x1) = x0 + x1,
                       [cons](x0, x1) = x0 + x1,
                       [length](x0) = x0 + 1
                      Strict:
                       {                mark#(s(X)) -> mark#(X),
                                 mark#(and(X1, X2)) -> mark#(X1),
                                 mark#(and(X1, X2)) -> mark#(X2),
                                 mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                               mark#(isNatIList(X)) -> a__isNatIList#(X),
                                mark#(isNatList(X)) -> a__isNatList#(X),
                                    mark#(isNat(X)) -> a__isNat#(X),
                                   a__and#(tt(), T) -> mark#(T),
                          a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                          a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                          a__isNatList#(cons(N, L)) -> a__isNat#(N),
                         a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                         a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                         a__isNatList#(take(N, IL)) -> a__isNat#(N),
                                 a__isNatIList#(IL) -> a__isNatList#(IL),
                        a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                        a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL),
                        a__isNatIList#(cons(N, IL)) -> a__isNat#(N),
                                    a__isNat#(s(N)) -> a__isNat#(N)}
                      Weak:
                       {                  mark(tt()) -> tt(),
                                           mark(0()) -> 0(),
                                          mark(s(X)) -> s(mark(X)),
                                     mark(length(X)) -> a__length(mark(X)),
                                       mark(zeros()) -> a__zeros(),
                                  mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                         mark(nil()) -> nil(),
                                  mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                                   mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                                 mark(isNatIList(X)) -> a__isNatIList(X),
                                  mark(isNatList(X)) -> a__isNatList(X),
                                      mark(isNat(X)) -> a__isNat(X),
                                     mark(uTake1(X)) -> a__uTake1(mark(X)),
                        mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                               mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                      a__and(X1, X2) -> and(X1, X2),
                                     a__and(tt(), T) -> mark(T),
                                     a__isNatList(X) -> isNatList(X),
                            a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                                 a__isNatList(nil()) -> tt(),
                           a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                   a__isNatIList(IL) -> a__isNatList(IL),
                                    a__isNatIList(X) -> isNatIList(X),
                              a__isNatIList(zeros()) -> tt(),
                          a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                         a__isNat(X) -> isNat(X),
                                       a__isNat(0()) -> tt(),
                                      a__isNat(s(N)) -> a__isNat(N),
                                 a__isNat(length(L)) -> a__isNatList(L),
                                          a__zeros() -> zeros(),
                                          a__zeros() -> cons(0(), zeros()),
                                        a__uTake1(X) -> uTake1(X),
                                     a__uTake1(tt()) -> nil(),
                                     a__take(X1, X2) -> take(X1, X2),
                                    a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                          a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                           a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                           a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                                  a__uLength(X1, X2) -> uLength(X1, X2),
                                 a__uLength(tt(), L) -> s(a__length(mark(L))),
                                        a__length(X) -> length(X),
                               a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                      EDG:
                       {(a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
                        (a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
                        (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
                        (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
                        (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
                        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
                        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
                        (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
                        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                        (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                        (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNat#(N))
                        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__isNatIList#(IL))
                        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNat#(N))
                        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                        (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                        (mark#(and(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
                        (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X))
                        (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X))
                        (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                        (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X2))
                        (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
                        (mark#(and(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
                        (a__isNatList#(cons(N, L)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                        (a__isNatIList#(cons(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                        (a__isNat#(s(N)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                        (a__isNatList#(take(N, IL)) -> a__isNat#(N), a__isNat#(s(N)) -> a__isNat#(N))
                        (a__and#(tt(), T) -> mark#(T), mark#(s(X)) -> mark#(X))
                        (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X1))
                        (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X2))
                        (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                        (a__and#(tt(), T) -> mark#(T), mark#(isNatIList(X)) -> a__isNatIList#(X))
                        (a__and#(tt(), T) -> mark#(T), mark#(isNatList(X)) -> a__isNatList#(X))
                        (a__and#(tt(), T) -> mark#(T), mark#(isNat(X)) -> a__isNat#(X))
                        (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
                        (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                        (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                        (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
                        (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
                        (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                        (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                        (a__isNatList#(take(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
                        (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(N)) -> a__isNat#(N))
                        (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(IL) -> a__isNatList#(IL))
                        (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                        (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                        (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNat#(N))
                        (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
                        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
                        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
                        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                        (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
                        (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
                        (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
                        (a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
                        (mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)), a__and#(tt(), T) -> mark#(T))}
                       SCCS:
                        Scc:
                         {a__isNat#(s(N)) -> a__isNat#(N)}
                        Scc:
                         {                mark#(s(X)) -> mark#(X),
                                   mark#(and(X1, X2)) -> mark#(X1),
                                   mark#(and(X1, X2)) -> mark#(X2),
                                   mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                                 mark#(isNatIList(X)) -> a__isNatIList#(X),
                                  mark#(isNatList(X)) -> a__isNatList#(X),
                                     a__and#(tt(), T) -> mark#(T),
                            a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                            a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                           a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                           a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                                   a__isNatIList#(IL) -> a__isNatList#(IL),
                          a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                          a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL)}
                        SCC:
                         Strict:
                          {a__isNat#(s(N)) -> a__isNat#(N)}
                         Weak:
                         {                  mark(tt()) -> tt(),
                                             mark(0()) -> 0(),
                                            mark(s(X)) -> s(mark(X)),
                                       mark(length(X)) -> a__length(mark(X)),
                                         mark(zeros()) -> a__zeros(),
                                    mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                           mark(nil()) -> nil(),
                                    mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                                     mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                                   mark(isNatIList(X)) -> a__isNatIList(X),
                                    mark(isNatList(X)) -> a__isNatList(X),
                                        mark(isNat(X)) -> a__isNat(X),
                                       mark(uTake1(X)) -> a__uTake1(mark(X)),
                          mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                                 mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                        a__and(X1, X2) -> and(X1, X2),
                                       a__and(tt(), T) -> mark(T),
                                       a__isNatList(X) -> isNatList(X),
                              a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                                   a__isNatList(nil()) -> tt(),
                             a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                     a__isNatIList(IL) -> a__isNatList(IL),
                                      a__isNatIList(X) -> isNatIList(X),
                                a__isNatIList(zeros()) -> tt(),
                            a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                           a__isNat(X) -> isNat(X),
                                         a__isNat(0()) -> tt(),
                                        a__isNat(s(N)) -> a__isNat(N),
                                   a__isNat(length(L)) -> a__isNatList(L),
                                            a__zeros() -> zeros(),
                                            a__zeros() -> cons(0(), zeros()),
                                          a__uTake1(X) -> uTake1(X),
                                       a__uTake1(tt()) -> nil(),
                                       a__take(X1, X2) -> take(X1, X2),
                                      a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                            a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                             a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                             a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                                    a__uLength(X1, X2) -> uLength(X1, X2),
                                   a__uLength(tt(), L) -> s(a__length(mark(L))),
                                          a__length(X) -> length(X),
                                 a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                         SPSC:
                          Simple Projection:
                           pi(a__isNat#) = 0
                          Strict:
                           {}
                          Qed
                        SCC:
                         Strict:
                          {                mark#(s(X)) -> mark#(X),
                                    mark#(and(X1, X2)) -> mark#(X1),
                                    mark#(and(X1, X2)) -> mark#(X2),
                                    mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                                  mark#(isNatIList(X)) -> a__isNatIList#(X),
                                   mark#(isNatList(X)) -> a__isNatList#(X),
                                      a__and#(tt(), T) -> mark#(T),
                             a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                             a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                            a__isNatList#(take(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                            a__isNatList#(take(N, IL)) -> a__isNatIList#(IL),
                                    a__isNatIList#(IL) -> a__isNatList#(IL),
                           a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                           a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL)}
                         Weak:
                         {                  mark(tt()) -> tt(),
                                             mark(0()) -> 0(),
                                            mark(s(X)) -> s(mark(X)),
                                       mark(length(X)) -> a__length(mark(X)),
                                         mark(zeros()) -> a__zeros(),
                                    mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                           mark(nil()) -> nil(),
                                    mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                                     mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                                   mark(isNatIList(X)) -> a__isNatIList(X),
                                    mark(isNatList(X)) -> a__isNatList(X),
                                        mark(isNat(X)) -> a__isNat(X),
                                       mark(uTake1(X)) -> a__uTake1(mark(X)),
                          mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                                 mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                        a__and(X1, X2) -> and(X1, X2),
                                       a__and(tt(), T) -> mark(T),
                                       a__isNatList(X) -> isNatList(X),
                              a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                                   a__isNatList(nil()) -> tt(),
                             a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                     a__isNatIList(IL) -> a__isNatList(IL),
                                      a__isNatIList(X) -> isNatIList(X),
                                a__isNatIList(zeros()) -> tt(),
                            a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                           a__isNat(X) -> isNat(X),
                                         a__isNat(0()) -> tt(),
                                        a__isNat(s(N)) -> a__isNat(N),
                                   a__isNat(length(L)) -> a__isNatList(L),
                                            a__zeros() -> zeros(),
                                            a__zeros() -> cons(0(), zeros()),
                                          a__uTake1(X) -> uTake1(X),
                                       a__uTake1(tt()) -> nil(),
                                       a__take(X1, X2) -> take(X1, X2),
                                      a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                            a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                             a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                             a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                                    a__uLength(X1, X2) -> uLength(X1, X2),
                                   a__uLength(tt(), L) -> s(a__length(mark(L))),
                                          a__length(X) -> length(X),
                                 a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                         POLY:
                          Argument Filtering:
                           pi(uLength) = [1], pi(uTake2) = [1,2,3], pi(uTake1) = [], pi(isNat) = 0, pi(isNatList) = [0], pi(isNatIList) = [0], pi(and) = [0,1], pi(a__length) = [0], pi(a__uLength) = [1], pi(a__uTake2) = [1,2,3], pi(a__take) = [0,1], pi(a__uTake1) = [], pi(a__zeros) = [], pi(take) = [0,1], pi(nil) = [], pi(cons) = [0,1], pi(zeros) = [], pi(length) = [0], pi(s) = 0, pi(0) = [], pi(a__isNat) = 0, pi(a__isNatIList#) = [0], pi(a__isNatIList) = [0], pi(a__isNatList#) = [0], pi(a__isNatList) = [0], pi(tt) = [], pi(a__and#) = 1, pi(a__and) = [0,1], pi(mark#) = 0, pi(mark) = 0
                          Usable Rules:
                           {}
                          Interpretation:
                           [a__isNatIList#](x0) = x0 + 1,
                           [a__isNatList#](x0) = x0 + 1,
                           [and](x0, x1) = x0 + x1,
                           [take](x0, x1) = x0 + x1 + 1,
                           [cons](x0, x1) = x0 + x1,
                           [isNatList](x0) = x0 + 1,
                           [isNatIList](x0) = x0 + 1,
                           [a__isNatIList](x0) = x0 + 1,
                           [a__isNatList](x0) = x0 + 1
                          Strict:
                           {                mark#(s(X)) -> mark#(X),
                                     mark#(and(X1, X2)) -> mark#(X1),
                                     mark#(and(X1, X2)) -> mark#(X2),
                                     mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                                   mark#(isNatIList(X)) -> a__isNatIList#(X),
                                    mark#(isNatList(X)) -> a__isNatList#(X),
                                       a__and#(tt(), T) -> mark#(T),
                              a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                              a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                                     a__isNatIList#(IL) -> a__isNatList#(IL),
                            a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                            a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL)}
                          Weak:
                           {                  mark(tt()) -> tt(),
                                               mark(0()) -> 0(),
                                              mark(s(X)) -> s(mark(X)),
                                         mark(length(X)) -> a__length(mark(X)),
                                           mark(zeros()) -> a__zeros(),
                                      mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                             mark(nil()) -> nil(),
                                      mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                                       mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                                     mark(isNatIList(X)) -> a__isNatIList(X),
                                      mark(isNatList(X)) -> a__isNatList(X),
                                          mark(isNat(X)) -> a__isNat(X),
                                         mark(uTake1(X)) -> a__uTake1(mark(X)),
                            mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                                   mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                          a__and(X1, X2) -> and(X1, X2),
                                         a__and(tt(), T) -> mark(T),
                                         a__isNatList(X) -> isNatList(X),
                                a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                                     a__isNatList(nil()) -> tt(),
                               a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                       a__isNatIList(IL) -> a__isNatList(IL),
                                        a__isNatIList(X) -> isNatIList(X),
                                  a__isNatIList(zeros()) -> tt(),
                              a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                             a__isNat(X) -> isNat(X),
                                           a__isNat(0()) -> tt(),
                                          a__isNat(s(N)) -> a__isNat(N),
                                     a__isNat(length(L)) -> a__isNatList(L),
                                              a__zeros() -> zeros(),
                                              a__zeros() -> cons(0(), zeros()),
                                            a__uTake1(X) -> uTake1(X),
                                         a__uTake1(tt()) -> nil(),
                                         a__take(X1, X2) -> take(X1, X2),
                                        a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                              a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                               a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                               a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                                      a__uLength(X1, X2) -> uLength(X1, X2),
                                     a__uLength(tt(), L) -> s(a__length(mark(L))),
                                            a__length(X) -> length(X),
                                   a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                          EDG:
                           {(mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                            (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                            (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(IL) -> a__isNatList#(IL))
                            (a__and#(tt(), T) -> mark#(T), mark#(isNatList(X)) -> a__isNatList#(X))
                            (a__and#(tt(), T) -> mark#(T), mark#(isNatIList(X)) -> a__isNatIList#(X))
                            (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                            (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X2))
                            (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X1))
                            (a__and#(tt(), T) -> mark#(T), mark#(s(X)) -> mark#(X))
                            (a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
                            (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                            (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                            (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
                            (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
                            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
                            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
                            (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
                            (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                            (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                            (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(IL) -> a__isNatList#(IL))
                            (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                            (a__isNatIList#(IL) -> a__isNatList#(IL), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                            (mark#(and(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
                            (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
                            (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X2))
                            (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                            (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X))
                            (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X))
                            (a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
                            (mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)), a__and#(tt(), T) -> mark#(T))
                            (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                            (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                            (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
                            (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
                            (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
                            (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                            (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
                            (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))}
                           SCCS:
                            Scc:
                             {                mark#(s(X)) -> mark#(X),
                                       mark#(and(X1, X2)) -> mark#(X1),
                                       mark#(and(X1, X2)) -> mark#(X2),
                                       mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                                     mark#(isNatIList(X)) -> a__isNatIList#(X),
                                      mark#(isNatList(X)) -> a__isNatList#(X),
                                         a__and#(tt(), T) -> mark#(T),
                                a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                                a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                                       a__isNatIList#(IL) -> a__isNatList#(IL),
                              a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                              a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL)}
                            SCC:
                             Strict:
                              {                mark#(s(X)) -> mark#(X),
                                        mark#(and(X1, X2)) -> mark#(X1),
                                        mark#(and(X1, X2)) -> mark#(X2),
                                        mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                                      mark#(isNatIList(X)) -> a__isNatIList#(X),
                                       mark#(isNatList(X)) -> a__isNatList#(X),
                                          a__and#(tt(), T) -> mark#(T),
                                 a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                                 a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                                        a__isNatIList#(IL) -> a__isNatList#(IL),
                               a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                               a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL)}
                             Weak:
                             {                  mark(tt()) -> tt(),
                                                 mark(0()) -> 0(),
                                                mark(s(X)) -> s(mark(X)),
                                           mark(length(X)) -> a__length(mark(X)),
                                             mark(zeros()) -> a__zeros(),
                                        mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                               mark(nil()) -> nil(),
                                        mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                                         mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                                       mark(isNatIList(X)) -> a__isNatIList(X),
                                        mark(isNatList(X)) -> a__isNatList(X),
                                            mark(isNat(X)) -> a__isNat(X),
                                           mark(uTake1(X)) -> a__uTake1(mark(X)),
                              mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                                     mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                            a__and(X1, X2) -> and(X1, X2),
                                           a__and(tt(), T) -> mark(T),
                                           a__isNatList(X) -> isNatList(X),
                                  a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                                       a__isNatList(nil()) -> tt(),
                                 a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                         a__isNatIList(IL) -> a__isNatList(IL),
                                          a__isNatIList(X) -> isNatIList(X),
                                    a__isNatIList(zeros()) -> tt(),
                                a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                               a__isNat(X) -> isNat(X),
                                             a__isNat(0()) -> tt(),
                                            a__isNat(s(N)) -> a__isNat(N),
                                       a__isNat(length(L)) -> a__isNatList(L),
                                                a__zeros() -> zeros(),
                                                a__zeros() -> cons(0(), zeros()),
                                              a__uTake1(X) -> uTake1(X),
                                           a__uTake1(tt()) -> nil(),
                                           a__take(X1, X2) -> take(X1, X2),
                                          a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                                a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                                 a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                                 a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                                        a__uLength(X1, X2) -> uLength(X1, X2),
                                       a__uLength(tt(), L) -> s(a__length(mark(L))),
                                              a__length(X) -> length(X),
                                     a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                             POLY:
                              Argument Filtering:
                               pi(uLength) = 1, pi(uTake2) = [1,2,3], pi(uTake1) = [], pi(isNat) = 0, pi(isNatList) = 0, pi(isNatIList) = [0], pi(and) = [0,1], pi(a__length) = 0, pi(a__uLength) = 1, pi(a__uTake2) = [1,2,3], pi(a__take) = [0,1], pi(a__uTake1) = [], pi(a__zeros) = [], pi(take) = [0,1], pi(nil) = [], pi(cons) = [0,1], pi(zeros) = [], pi(length) = 0, pi(s) = 0, pi(0) = [], pi(a__isNat) = 0, pi(a__isNatIList#) = [0], pi(a__isNatIList) = [0], pi(a__isNatList#) = 0, pi(a__isNatList) = 0, pi(tt) = [], pi(a__and#) = 1, pi(a__and) = [0,1], pi(mark#) = 0, pi(mark) = 0
                              Usable Rules:
                               {}
                              Interpretation:
                               [a__isNatIList#](x0) = x0 + 1,
                               [and](x0, x1) = x0 + x1,
                               [cons](x0, x1) = x0 + x1,
                               [isNatIList](x0) = x0 + 1,
                               [a__isNatIList](x0) = x0 + 1
                              Strict:
                               {                mark#(s(X)) -> mark#(X),
                                         mark#(and(X1, X2)) -> mark#(X1),
                                         mark#(and(X1, X2)) -> mark#(X2),
                                         mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                                       mark#(isNatIList(X)) -> a__isNatIList#(X),
                                        mark#(isNatList(X)) -> a__isNatList#(X),
                                           a__and#(tt(), T) -> mark#(T),
                                  a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                                  a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                                a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                                a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL)}
                              Weak:
                               {                  mark(tt()) -> tt(),
                                                   mark(0()) -> 0(),
                                                  mark(s(X)) -> s(mark(X)),
                                             mark(length(X)) -> a__length(mark(X)),
                                               mark(zeros()) -> a__zeros(),
                                          mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                                 mark(nil()) -> nil(),
                                          mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                                           mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                                         mark(isNatIList(X)) -> a__isNatIList(X),
                                          mark(isNatList(X)) -> a__isNatList(X),
                                              mark(isNat(X)) -> a__isNat(X),
                                             mark(uTake1(X)) -> a__uTake1(mark(X)),
                                mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                                       mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                              a__and(X1, X2) -> and(X1, X2),
                                             a__and(tt(), T) -> mark(T),
                                             a__isNatList(X) -> isNatList(X),
                                    a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                                         a__isNatList(nil()) -> tt(),
                                   a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                           a__isNatIList(IL) -> a__isNatList(IL),
                                            a__isNatIList(X) -> isNatIList(X),
                                      a__isNatIList(zeros()) -> tt(),
                                  a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                                 a__isNat(X) -> isNat(X),
                                               a__isNat(0()) -> tt(),
                                              a__isNat(s(N)) -> a__isNat(N),
                                         a__isNat(length(L)) -> a__isNatList(L),
                                                  a__zeros() -> zeros(),
                                                  a__zeros() -> cons(0(), zeros()),
                                                a__uTake1(X) -> uTake1(X),
                                             a__uTake1(tt()) -> nil(),
                                             a__take(X1, X2) -> take(X1, X2),
                                            a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                                  a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                                   a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                                   a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                                          a__uLength(X1, X2) -> uLength(X1, X2),
                                         a__uLength(tt(), L) -> s(a__length(mark(L))),
                                                a__length(X) -> length(X),
                                       a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                              EDG:
                               {(a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)), a__and#(tt(), T) -> mark#(T))
                                (a__and#(tt(), T) -> mark#(T), mark#(isNatList(X)) -> a__isNatList#(X))
                                (a__and#(tt(), T) -> mark#(T), mark#(isNatIList(X)) -> a__isNatIList#(X))
                                (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                                (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X2))
                                (a__and#(tt(), T) -> mark#(T), mark#(and(X1, X2)) -> mark#(X1))
                                (a__and#(tt(), T) -> mark#(T), mark#(s(X)) -> mark#(X))
                                (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                                (a__isNatList#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                                (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X))
                                (mark#(and(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X))
                                (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                                (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X2))
                                (mark#(and(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
                                (mark#(and(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
                                (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                                (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                                (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)))
                                (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(N, L)) -> a__isNatList#(L))
                                (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
                                (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
                                (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X2))
                                (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                                (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X))
                                (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X))
                                (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
                                (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
                                (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X2))
                                (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)))
                                (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X))
                                (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))
                                (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)))
                                (a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL))
                                (a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)), a__and#(tt(), T) -> mark#(T))
                                (mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)), a__and#(tt(), T) -> mark#(T))}
                               SCCS:
                                Scc:
                                 {                mark#(s(X)) -> mark#(X),
                                           mark#(and(X1, X2)) -> mark#(X1),
                                           mark#(and(X1, X2)) -> mark#(X2),
                                           mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                                         mark#(isNatIList(X)) -> a__isNatIList#(X),
                                          mark#(isNatList(X)) -> a__isNatList#(X),
                                             a__and#(tt(), T) -> mark#(T),
                                    a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                                    a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                                  a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                                  a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL)}
                                SCC:
                                 Strict:
                                  {                mark#(s(X)) -> mark#(X),
                                            mark#(and(X1, X2)) -> mark#(X1),
                                            mark#(and(X1, X2)) -> mark#(X2),
                                            mark#(and(X1, X2)) -> a__and#(mark(X1), mark(X2)),
                                          mark#(isNatIList(X)) -> a__isNatIList#(X),
                                           mark#(isNatList(X)) -> a__isNatList#(X),
                                              a__and#(tt(), T) -> mark#(T),
                                     a__isNatList#(cons(N, L)) -> a__and#(a__isNat(N), a__isNatList(L)),
                                     a__isNatList#(cons(N, L)) -> a__isNatList#(L),
                                   a__isNatIList#(cons(N, IL)) -> a__and#(a__isNat(N), a__isNatIList(IL)),
                                   a__isNatIList#(cons(N, IL)) -> a__isNatIList#(IL)}
                                 Weak:
                                 {                  mark(tt()) -> tt(),
                                                     mark(0()) -> 0(),
                                                    mark(s(X)) -> s(mark(X)),
                                               mark(length(X)) -> a__length(mark(X)),
                                                 mark(zeros()) -> a__zeros(),
                                            mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                                   mark(nil()) -> nil(),
                                            mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)),
                                             mark(and(X1, X2)) -> a__and(mark(X1), mark(X2)),
                                           mark(isNatIList(X)) -> a__isNatIList(X),
                                            mark(isNatList(X)) -> a__isNatList(X),
                                                mark(isNat(X)) -> a__isNat(X),
                                               mark(uTake1(X)) -> a__uTake1(mark(X)),
                                  mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4),
                                         mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2),
                                                a__and(X1, X2) -> and(X1, X2),
                                               a__and(tt(), T) -> mark(T),
                                               a__isNatList(X) -> isNatList(X),
                                      a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L)),
                                           a__isNatList(nil()) -> tt(),
                                     a__isNatList(take(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                             a__isNatIList(IL) -> a__isNatList(IL),
                                              a__isNatIList(X) -> isNatIList(X),
                                        a__isNatIList(zeros()) -> tt(),
                                    a__isNatIList(cons(N, IL)) -> a__and(a__isNat(N), a__isNatIList(IL)),
                                                   a__isNat(X) -> isNat(X),
                                                 a__isNat(0()) -> tt(),
                                                a__isNat(s(N)) -> a__isNat(N),
                                           a__isNat(length(L)) -> a__isNatList(L),
                                                    a__zeros() -> zeros(),
                                                    a__zeros() -> cons(0(), zeros()),
                                                  a__uTake1(X) -> uTake1(X),
                                               a__uTake1(tt()) -> nil(),
                                               a__take(X1, X2) -> take(X1, X2),
                                              a__take(0(), IL) -> a__uTake1(a__isNatIList(IL)),
                                    a__take(s(M), cons(N, IL)) -> a__uTake2(a__and(a__isNat(M), a__and(a__isNat(N), a__isNatIList(IL))), M, N, IL),
                                     a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4),
                                     a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL)),
                                            a__uLength(X1, X2) -> uLength(X1, X2),
                                           a__uLength(tt(), L) -> s(a__length(mark(L))),
                                                  a__length(X) -> length(X),
                                         a__length(cons(N, L)) -> a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)}
                                 Fail