MAYBE
Time: 0.045038
TRS:
 {              cons(X1, X2) -> n__cons(X1, X2),
                         0() -> n__0(),
                     zeros() -> cons(0(), n__zeros()),
                     zeros() -> n__zeros(),
                         s X -> n__s X,
                    length X -> n__length X,
           length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L),
                length nil() -> 0(),
                  activate X -> X,
         activate n__zeros() -> zeros(),
    activate n__take(X1, X2) -> take(X1, X2),
             activate n__0() -> 0(),
        activate n__length X -> length X,
             activate n__s X -> s X,
    activate n__isNatIList X -> isNatIList X,
    activate n__cons(X1, X2) -> cons(X1, X2),
           activate n__nil() -> nil(),
     activate n__isNatList X -> isNatList X,
         activate n__isNat X -> isNat X,
     activate n__and(X1, X2) -> and(X1, X2),
                U11(tt(), L) -> s length activate L,
                       nil() -> n__nil(),
                    U21 tt() -> nil(),
         U31(tt(), IL, M, N) -> cons(activate N, n__take(activate M, activate IL)),
                 and(X1, X2) -> n__and(X1, X2),
                and(tt(), X) -> activate X,
                     isNat X -> n__isNat X,
                isNat n__0() -> tt(),
          isNat n__length V1 -> isNatList activate V1,
               isNat n__s V1 -> isNat activate V1,
                 isNatList X -> n__isNatList X,
   isNatList n__take(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2),
   isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2),
          isNatList n__nil() -> tt(),
                isNatIList X -> n__isNatIList X,
                isNatIList V -> isNatList activate V,
       isNatIList n__zeros() -> tt(),
  isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2),
                take(X1, X2) -> n__take(X1, X2),
               take(0(), IL) -> U21 isNatIList IL,
      take(s M, cons(N, IL)) -> U31(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N)}
 DP:
  DP:
   {                   zeros#() -> cons#(0(), n__zeros()),
                       zeros#() -> 0#(),
             length# cons(N, L) -> activate# L,
             length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L),
             length# cons(N, L) -> and#(isNatList activate L, n__isNat N),
             length# cons(N, L) -> isNatList# activate L,
                  length# nil() -> 0#(),
           activate# n__zeros() -> zeros#(),
      activate# n__take(X1, X2) -> take#(X1, X2),
               activate# n__0() -> 0#(),
          activate# n__length X -> length# X,
               activate# n__s X -> s# X,
      activate# n__isNatIList X -> isNatIList# X,
      activate# n__cons(X1, X2) -> cons#(X1, X2),
             activate# n__nil() -> nil#(),
       activate# n__isNatList X -> isNatList# X,
           activate# n__isNat X -> isNat# X,
       activate# n__and(X1, X2) -> and#(X1, X2),
                  U11#(tt(), L) -> s# length activate L,
                  U11#(tt(), L) -> length# activate L,
                  U11#(tt(), L) -> activate# L,
                      U21# tt() -> nil#(),
           U31#(tt(), IL, M, N) -> cons#(activate N, n__take(activate M, activate IL)),
           U31#(tt(), IL, M, N) -> activate# N,
           U31#(tt(), IL, M, N) -> activate# M,
           U31#(tt(), IL, M, N) -> activate# IL,
                  and#(tt(), X) -> activate# X,
            isNat# n__length V1 -> activate# V1,
            isNat# n__length V1 -> isNatList# activate V1,
                 isNat# n__s V1 -> activate# V1,
                 isNat# n__s V1 -> isNat# activate V1,
     isNatList# n__take(V1, V2) -> activate# V1,
     isNatList# n__take(V1, V2) -> activate# V2,
     isNatList# n__take(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2),
     isNatList# n__take(V1, V2) -> isNat# activate V1,
     isNatList# n__cons(V1, V2) -> activate# V1,
     isNatList# n__cons(V1, V2) -> activate# V2,
     isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2),
     isNatList# n__cons(V1, V2) -> isNat# activate V1,
                  isNatIList# V -> activate# V,
                  isNatIList# V -> isNatList# activate V,
    isNatIList# n__cons(V1, V2) -> activate# V1,
    isNatIList# n__cons(V1, V2) -> activate# V2,
    isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2),
    isNatIList# n__cons(V1, V2) -> isNat# activate V1,
                 take#(0(), IL) -> U21# isNatIList IL,
                 take#(0(), IL) -> isNatIList# IL,
        take#(s M, cons(N, IL)) -> activate# IL,
        take#(s M, cons(N, IL)) -> U31#(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N),
        take#(s M, cons(N, IL)) -> and#(isNatIList activate IL, n__and(isNat M, n__isNat N)),
        take#(s M, cons(N, IL)) -> isNat# M,
        take#(s M, cons(N, IL)) -> isNatIList# activate IL}
  TRS:
  {              cons(X1, X2) -> n__cons(X1, X2),
                          0() -> n__0(),
                      zeros() -> cons(0(), n__zeros()),
                      zeros() -> n__zeros(),
                          s X -> n__s X,
                     length X -> n__length X,
            length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L),
                 length nil() -> 0(),
                   activate X -> X,
          activate n__zeros() -> zeros(),
     activate n__take(X1, X2) -> take(X1, X2),
              activate n__0() -> 0(),
         activate n__length X -> length X,
              activate n__s X -> s X,
     activate n__isNatIList X -> isNatIList X,
     activate n__cons(X1, X2) -> cons(X1, X2),
            activate n__nil() -> nil(),
      activate n__isNatList X -> isNatList X,
          activate n__isNat X -> isNat X,
      activate n__and(X1, X2) -> and(X1, X2),
                 U11(tt(), L) -> s length activate L,
                        nil() -> n__nil(),
                     U21 tt() -> nil(),
          U31(tt(), IL, M, N) -> cons(activate N, n__take(activate M, activate IL)),
                  and(X1, X2) -> n__and(X1, X2),
                 and(tt(), X) -> activate X,
                      isNat X -> n__isNat X,
                 isNat n__0() -> tt(),
           isNat n__length V1 -> isNatList activate V1,
                isNat n__s V1 -> isNat activate V1,
                  isNatList X -> n__isNatList X,
    isNatList n__take(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2),
    isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2),
           isNatList n__nil() -> tt(),
                 isNatIList X -> n__isNatIList X,
                 isNatIList V -> isNatList activate V,
        isNatIList n__zeros() -> tt(),
   isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2),
                 take(X1, X2) -> n__take(X1, X2),
                take(0(), IL) -> U21 isNatIList IL,
       take(s M, cons(N, IL)) -> U31(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N)}
  EDG:
   {
    (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
    (isNat# n__s V1 -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNat# n__s V1 -> activate# V1, activate# n__isNatList X -> isNatList# X)
    (isNat# n__s V1 -> activate# V1, activate# n__nil() -> nil#())
    (isNat# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (isNat# n__s V1 -> activate# V1, activate# n__isNatIList X -> isNatIList# X)
    (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X)
    (isNat# n__s V1 -> activate# V1, activate# n__length X -> length# X)
    (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#())
    (isNat# n__s V1 -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2))
    (isNat# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#())
    (isNatList# n__take(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), and#(tt(), X) -> activate# X)
    (isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), and#(tt(), X) -> activate# X)
    (isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), and#(tt(), X) -> activate# X)
    (U11#(tt(), L) -> activate# L, activate# n__and(X1, X2) -> and#(X1, X2))
    (U11#(tt(), L) -> activate# L, activate# n__isNat X -> isNat# X)
    (U11#(tt(), L) -> activate# L, activate# n__isNatList X -> isNatList# X)
    (U11#(tt(), L) -> activate# L, activate# n__nil() -> nil#())
    (U11#(tt(), L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (U11#(tt(), L) -> activate# L, activate# n__isNatIList X -> isNatIList# X)
    (U11#(tt(), L) -> activate# L, activate# n__s X -> s# X)
    (U11#(tt(), L) -> activate# L, activate# n__length X -> length# X)
    (U11#(tt(), L) -> activate# L, activate# n__0() -> 0#())
    (U11#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
    (U11#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#())
    (activate# n__zeros() -> zeros#(), zeros#() -> 0#())
    (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros()))
    (activate# n__length X -> length# X, length# nil() -> 0#())
    (activate# n__length X -> length# X, length# cons(N, L) -> isNatList# activate L)
    (activate# n__length X -> length# X, length# cons(N, L) -> and#(isNatList activate L, n__isNat N))
    (activate# n__length X -> length# X, length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L))
    (activate# n__length X -> length# X, length# cons(N, L) -> activate# L)
    (activate# n__isNatIList X -> isNatIList# X, isNatIList# n__cons(V1, V2) -> isNat# activate V1)
    (activate# n__isNatIList X -> isNatIList# X, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2))
    (activate# n__isNatIList X -> isNatIList# X, isNatIList# n__cons(V1, V2) -> activate# V2)
    (activate# n__isNatIList X -> isNatIList# X, isNatIList# n__cons(V1, V2) -> activate# V1)
    (activate# n__isNatIList X -> isNatIList# X, isNatIList# V -> isNatList# activate V)
    (activate# n__isNatIList X -> isNatIList# X, isNatIList# V -> activate# V)
    (activate# n__isNatList X -> isNatList# X, isNatList# n__cons(V1, V2) -> isNat# activate V1)
    (activate# n__isNatList X -> isNatList# X, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2))
    (activate# n__isNatList X -> isNatList# X, isNatList# n__cons(V1, V2) -> activate# V2)
    (activate# n__isNatList X -> isNatList# X, isNatList# n__cons(V1, V2) -> activate# V1)
    (activate# n__isNatList X -> isNatList# X, isNatList# n__take(V1, V2) -> isNat# activate V1)
    (activate# n__isNatList X -> isNatList# X, isNatList# n__take(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2))
    (activate# n__isNatList X -> isNatList# X, isNatList# n__take(V1, V2) -> activate# V2)
    (activate# n__isNatList X -> isNatList# X, isNatList# n__take(V1, V2) -> activate# V1)
    (length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), U11#(tt(), L) -> activate# L)
    (length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), U11#(tt(), L) -> length# activate L)
    (length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), U11#(tt(), L) -> s# length activate L)
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__and(X1, X2) -> and#(X1, X2))
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__isNat X -> isNat# X)
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__isNatList X -> isNatList# X)
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__nil() -> nil#())
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__isNatIList X -> isNatIList# X)
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__s X -> s# X)
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__length X -> length# X)
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__0() -> 0#())
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__take(X1, X2) -> take#(X1, X2))
    (U31#(tt(), IL, M, N) -> activate# IL, activate# n__zeros() -> zeros#())
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__and(X1, X2) -> and#(X1, X2))
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__isNat X -> isNat# X)
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__isNatList X -> isNatList# X)
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__nil() -> nil#())
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__isNatIList X -> isNatIList# X)
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__s X -> s# X)
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__length X -> length# X)
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__0() -> 0#())
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__take(X1, X2) -> take#(X1, X2))
    (take#(s M, cons(N, IL)) -> activate# IL, activate# n__zeros() -> zeros#())
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2))
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__isNatList X -> isNatList# X)
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__isNatIList X -> isNatIList# X)
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2))
    (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
    (take#(s M, cons(N, IL)) -> isNat# M, isNat# n__s V1 -> isNat# activate V1)
    (take#(s M, cons(N, IL)) -> isNat# M, isNat# n__s V1 -> activate# V1)
    (take#(s M, cons(N, IL)) -> isNat# M, isNat# n__length V1 -> isNatList# activate V1)
    (take#(s M, cons(N, IL)) -> isNat# M, isNat# n__length V1 -> activate# V1)
    (isNatIList# V -> activate# V, activate# n__and(X1, X2) -> and#(X1, X2))
    (isNatIList# V -> activate# V, activate# n__isNat X -> isNat# X)
    (isNatIList# V -> activate# V, activate# n__isNatList X -> isNatList# X)
    (isNatIList# V -> activate# V, activate# n__nil() -> nil#())
    (isNatIList# V -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (isNatIList# V -> activate# V, activate# n__isNatIList X -> isNatIList# X)
    (isNatIList# V -> activate# V, activate# n__s X -> s# X)
    (isNatIList# V -> activate# V, activate# n__length X -> length# X)
    (isNatIList# V -> activate# V, activate# n__0() -> 0#())
    (isNatIList# V -> activate# V, activate# n__take(X1, X2) -> take#(X1, X2))
    (isNatIList# V -> activate# V, activate# n__zeros() -> zeros#())
    (take#(s M, cons(N, IL)) -> and#(isNatIList activate IL, n__and(isNat M, n__isNat N)), and#(tt(), X) -> activate# X)
    (isNatIList# V -> isNatList# activate V, isNatList# n__cons(V1, V2) -> isNat# activate V1)
    (isNatIList# V -> isNatList# activate V, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2))
    (isNatIList# V -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V2)
    (isNatIList# V -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V1)
    (isNatIList# V -> isNatList# activate V, isNatList# n__take(V1, V2) -> isNat# activate V1)
    (isNatIList# V -> isNatList# activate V, isNatList# n__take(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2))
    (isNatIList# V -> isNatList# activate V, isNatList# n__take(V1, V2) -> activate# V2)
    (isNatIList# V -> isNatList# activate V, isNatList# n__take(V1, V2) -> activate# V1)
    (isNat# n__s V1 -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1)
    (isNat# n__s V1 -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
    (isNat# n__s V1 -> isNat# activate V1, isNat# n__length V1 -> isNatList# activate V1)
    (isNat# n__s V1 -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
    (isNatList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1)
    (isNatList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
    (isNatList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatList# activate V1)
    (isNatList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
    (take#(0(), IL) -> U21# isNatIList IL, U21# tt() -> nil#())
    (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> isNat# activate V1)
    (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2))
    (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> activate# V2)
    (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> activate# V1)
    (length# cons(N, L) -> isNatList# activate L, isNatList# n__take(V1, V2) -> isNat# activate V1)
    (length# cons(N, L) -> isNatList# activate L, isNatList# n__take(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2))
    (length# cons(N, L) -> isNatList# activate L, isNatList# n__take(V1, V2) -> activate# V2)
    (length# cons(N, L) -> isNatList# activate L, isNatList# n__take(V1, V2) -> activate# V1)
    (U11#(tt(), L) -> length# activate L, length# nil() -> 0#())
    (U11#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L)
    (U11#(tt(), L) -> length# activate L, length# cons(N, L) -> and#(isNatList activate L, n__isNat N))
    (U11#(tt(), L) -> length# activate L, length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L))
    (U11#(tt(), L) -> length# activate L, length# cons(N, L) -> activate# L)
    (activate# n__and(X1, X2) -> and#(X1, X2), and#(tt(), X) -> activate# X)
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(0(), IL) -> U21# isNatIList IL)
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(0(), IL) -> isNatIList# IL)
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(s M, cons(N, IL)) -> activate# IL)
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(s M, cons(N, IL)) -> U31#(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N))
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(s M, cons(N, IL)) -> and#(isNatIList activate IL, n__and(isNat M, n__isNat N)))
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(s M, cons(N, IL)) -> isNat# M)
    (activate# n__take(X1, X2) -> take#(X1, X2), take#(s M, cons(N, IL)) -> isNatIList# activate IL)
    (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# V -> activate# V)
    (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# V -> isNatList# activate V)
    (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(V1, V2) -> activate# V1)
    (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(V1, V2) -> activate# V2)
    (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2))
    (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(V1, V2) -> isNat# activate V1)
    (isNatIList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
    (isNatIList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatList# activate V1)
    (isNatIList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
    (isNatIList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1)
    (isNatList# n__take(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
    (isNatList# n__take(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatList# activate V1)
    (isNatList# n__take(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
    (isNatList# n__take(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1)
    (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__take(V1, V2) -> activate# V1)
    (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__take(V1, V2) -> activate# V2)
    (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__take(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2))
    (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__take(V1, V2) -> isNat# activate V1)
    (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V1)
    (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V2)
    (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2))
    (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> isNat# activate V1)
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__zeros() -> zeros#())
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__take(X1, X2) -> take#(X1, X2))
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__0() -> 0#())
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__length X -> length# X)
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__s X -> s# X)
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__isNatIList X -> isNatIList# X)
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__nil() -> nil#())
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__isNatList X -> isNatList# X)
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__isNat X -> isNat# X)
    (U31#(tt(), IL, M, N) -> activate# N, activate# n__and(X1, X2) -> and#(X1, X2))
    (take#(s M, cons(N, IL)) -> U31#(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N), U31#(tt(), IL, M, N) -> cons#(activate N, n__take(activate M, activate IL)))
    (take#(s M, cons(N, IL)) -> U31#(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N), U31#(tt(), IL, M, N) -> activate# N)
    (take#(s M, cons(N, IL)) -> U31#(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N), U31#(tt(), IL, M, N) -> activate# M)
    (take#(s M, cons(N, IL)) -> U31#(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N), U31#(tt(), IL, M, N) -> activate# IL)
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#())
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2))
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#())
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X)
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X)
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__isNatIList X -> isNatIList# X)
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#())
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__isNatList X -> isNatList# X)
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__isNat X -> isNat# X)
    (U31#(tt(), IL, M, N) -> activate# M, activate# n__and(X1, X2) -> and#(X1, X2))
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2))
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__isNatIList X -> isNatIList# X)
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__isNatList X -> isNatList# X)
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
    (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2))
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2))
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__0() -> 0#())
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__length X -> length# X)
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__s X -> s# X)
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__isNatIList X -> isNatIList# X)
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__isNatList X -> isNatList# X)
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
    (isNatList# n__take(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2))
    (take#(0(), IL) -> isNatIList# IL, isNatIList# V -> activate# V)
    (take#(0(), IL) -> isNatIList# IL, isNatIList# V -> isNatList# activate V)
    (take#(0(), IL) -> isNatIList# IL, isNatIList# n__cons(V1, V2) -> activate# V1)
    (take#(0(), IL) -> isNatIList# IL, isNatIList# n__cons(V1, V2) -> activate# V2)
    (take#(0(), IL) -> isNatIList# IL, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2))
    (take#(0(), IL) -> isNatIList# IL, isNatIList# n__cons(V1, V2) -> isNat# activate V1)
    (length# cons(N, L) -> and#(isNatList activate L, n__isNat N), and#(tt(), X) -> activate# X)
    (and#(tt(), X) -> activate# X, activate# n__zeros() -> zeros#())
    (and#(tt(), X) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
    (and#(tt(), X) -> activate# X, activate# n__0() -> 0#())
    (and#(tt(), X) -> activate# X, activate# n__length X -> length# X)
    (and#(tt(), X) -> activate# X, activate# n__s X -> s# X)
    (and#(tt(), X) -> activate# X, activate# n__isNatIList X -> isNatIList# X)
    (and#(tt(), X) -> activate# X, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (and#(tt(), X) -> activate# X, activate# n__nil() -> nil#())
    (and#(tt(), X) -> activate# X, activate# n__isNatList X -> isNatList# X)
    (and#(tt(), X) -> activate# X, activate# n__isNat X -> isNat# X)
    (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> and#(X1, X2))
    (activate# n__isNat X -> isNat# X, isNat# n__length V1 -> activate# V1)
    (activate# n__isNat X -> isNat# X, isNat# n__length V1 -> isNatList# activate V1)
    (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> activate# V1)
    (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> isNat# activate V1)
    (length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#())
    (length# cons(N, L) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
    (length# cons(N, L) -> activate# L, activate# n__0() -> 0#())
    (length# cons(N, L) -> activate# L, activate# n__length X -> length# X)
    (length# cons(N, L) -> activate# L, activate# n__s X -> s# X)
    (length# cons(N, L) -> activate# L, activate# n__isNatIList X -> isNatIList# X)
    (length# cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (length# cons(N, L) -> activate# L, activate# n__nil() -> nil#())
    (length# cons(N, L) -> activate# L, activate# n__isNatList X -> isNatList# X)
    (length# cons(N, L) -> activate# L, activate# n__isNat X -> isNat# X)
    (length# cons(N, L) -> activate# L, activate# n__and(X1, X2) -> and#(X1, X2))
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2))
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#())
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X)
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X)
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__isNatIList X -> isNatIList# X)
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__isNatList X -> isNatList# X)
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2))
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#())
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X)
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X)
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__isNatIList X -> isNatIList# X)
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__isNatList X -> isNatList# X)
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2))
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__0() -> 0#())
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__length X -> length# X)
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__s X -> s# X)
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__isNatIList X -> isNatIList# X)
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__isNatList X -> isNatList# X)
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNatList# n__take(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
    (isNat# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#())
    (isNat# n__length V1 -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2))
    (isNat# n__length V1 -> activate# V1, activate# n__0() -> 0#())
    (isNat# n__length V1 -> activate# V1, activate# n__length X -> length# X)
    (isNat# n__length V1 -> activate# V1, activate# n__s X -> s# X)
    (isNat# n__length V1 -> activate# V1, activate# n__isNatIList X -> isNatIList# X)
    (isNat# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
    (isNat# n__length V1 -> activate# V1, activate# n__nil() -> nil#())
    (isNat# n__length V1 -> activate# V1, activate# n__isNatList X -> isNatList# X)
    (isNat# n__length V1 -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNat# n__length V1 -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
   }
   STATUS:
    arrows: 0.895340
    SCCS (1):
     Scc:
      {         length# cons(N, L) -> activate# L,
                length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L),
                length# cons(N, L) -> and#(isNatList activate L, n__isNat N),
                length# cons(N, L) -> isNatList# activate L,
         activate# n__take(X1, X2) -> take#(X1, X2),
             activate# n__length X -> length# X,
         activate# n__isNatIList X -> isNatIList# X,
          activate# n__isNatList X -> isNatList# X,
              activate# n__isNat X -> isNat# X,
          activate# n__and(X1, X2) -> and#(X1, X2),
                     U11#(tt(), L) -> length# activate L,
                     U11#(tt(), L) -> activate# L,
              U31#(tt(), IL, M, N) -> activate# N,
              U31#(tt(), IL, M, N) -> activate# M,
              U31#(tt(), IL, M, N) -> activate# IL,
                     and#(tt(), X) -> activate# X,
               isNat# n__length V1 -> activate# V1,
               isNat# n__length V1 -> isNatList# activate V1,
                    isNat# n__s V1 -> activate# V1,
                    isNat# n__s V1 -> isNat# activate V1,
        isNatList# n__take(V1, V2) -> activate# V1,
        isNatList# n__take(V1, V2) -> activate# V2,
        isNatList# n__take(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2),
        isNatList# n__take(V1, V2) -> isNat# activate V1,
        isNatList# n__cons(V1, V2) -> activate# V1,
        isNatList# n__cons(V1, V2) -> activate# V2,
        isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2),
        isNatList# n__cons(V1, V2) -> isNat# activate V1,
                     isNatIList# V -> activate# V,
                     isNatIList# V -> isNatList# activate V,
       isNatIList# n__cons(V1, V2) -> activate# V1,
       isNatIList# n__cons(V1, V2) -> activate# V2,
       isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2),
       isNatIList# n__cons(V1, V2) -> isNat# activate V1,
                    take#(0(), IL) -> isNatIList# IL,
           take#(s M, cons(N, IL)) -> activate# IL,
           take#(s M, cons(N, IL)) -> U31#(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N),
           take#(s M, cons(N, IL)) -> and#(isNatIList activate IL, n__and(isNat M, n__isNat N)),
           take#(s M, cons(N, IL)) -> isNat# M,
           take#(s M, cons(N, IL)) -> isNatIList# activate IL}
     
     SCC (40):
      Strict:
       {         length# cons(N, L) -> activate# L,
                 length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L),
                 length# cons(N, L) -> and#(isNatList activate L, n__isNat N),
                 length# cons(N, L) -> isNatList# activate L,
          activate# n__take(X1, X2) -> take#(X1, X2),
              activate# n__length X -> length# X,
          activate# n__isNatIList X -> isNatIList# X,
           activate# n__isNatList X -> isNatList# X,
               activate# n__isNat X -> isNat# X,
           activate# n__and(X1, X2) -> and#(X1, X2),
                      U11#(tt(), L) -> length# activate L,
                      U11#(tt(), L) -> activate# L,
               U31#(tt(), IL, M, N) -> activate# N,
               U31#(tt(), IL, M, N) -> activate# M,
               U31#(tt(), IL, M, N) -> activate# IL,
                      and#(tt(), X) -> activate# X,
                isNat# n__length V1 -> activate# V1,
                isNat# n__length V1 -> isNatList# activate V1,
                     isNat# n__s V1 -> activate# V1,
                     isNat# n__s V1 -> isNat# activate V1,
         isNatList# n__take(V1, V2) -> activate# V1,
         isNatList# n__take(V1, V2) -> activate# V2,
         isNatList# n__take(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2),
         isNatList# n__take(V1, V2) -> isNat# activate V1,
         isNatList# n__cons(V1, V2) -> activate# V1,
         isNatList# n__cons(V1, V2) -> activate# V2,
         isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2),
         isNatList# n__cons(V1, V2) -> isNat# activate V1,
                      isNatIList# V -> activate# V,
                      isNatIList# V -> isNatList# activate V,
        isNatIList# n__cons(V1, V2) -> activate# V1,
        isNatIList# n__cons(V1, V2) -> activate# V2,
        isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2),
        isNatIList# n__cons(V1, V2) -> isNat# activate V1,
                     take#(0(), IL) -> isNatIList# IL,
            take#(s M, cons(N, IL)) -> activate# IL,
            take#(s M, cons(N, IL)) -> U31#(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N),
            take#(s M, cons(N, IL)) -> and#(isNatIList activate IL, n__and(isNat M, n__isNat N)),
            take#(s M, cons(N, IL)) -> isNat# M,
            take#(s M, cons(N, IL)) -> isNatIList# activate IL}
      Weak:
      {              cons(X1, X2) -> n__cons(X1, X2),
                              0() -> n__0(),
                          zeros() -> cons(0(), n__zeros()),
                          zeros() -> n__zeros(),
                              s X -> n__s X,
                         length X -> n__length X,
                length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L),
                     length nil() -> 0(),
                       activate X -> X,
              activate n__zeros() -> zeros(),
         activate n__take(X1, X2) -> take(X1, X2),
                  activate n__0() -> 0(),
             activate n__length X -> length X,
                  activate n__s X -> s X,
         activate n__isNatIList X -> isNatIList X,
         activate n__cons(X1, X2) -> cons(X1, X2),
                activate n__nil() -> nil(),
          activate n__isNatList X -> isNatList X,
              activate n__isNat X -> isNat X,
          activate n__and(X1, X2) -> and(X1, X2),
                     U11(tt(), L) -> s length activate L,
                            nil() -> n__nil(),
                         U21 tt() -> nil(),
              U31(tt(), IL, M, N) -> cons(activate N, n__take(activate M, activate IL)),
                      and(X1, X2) -> n__and(X1, X2),
                     and(tt(), X) -> activate X,
                          isNat X -> n__isNat X,
                     isNat n__0() -> tt(),
               isNat n__length V1 -> isNatList activate V1,
                    isNat n__s V1 -> isNat activate V1,
                      isNatList X -> n__isNatList X,
        isNatList n__take(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2),
        isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2),
               isNatList n__nil() -> tt(),
                     isNatIList X -> n__isNatIList X,
                     isNatIList V -> isNatList activate V,
            isNatIList n__zeros() -> tt(),
       isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2),
                     take(X1, X2) -> n__take(X1, X2),
                    take(0(), IL) -> U21 isNatIList IL,
           take(s M, cons(N, IL)) -> U31(and(isNatIList activate IL, n__and(isNat M, n__isNat N)), activate IL, M, N)}
      Open