Input TRS:
    1: zeros() -> cons(0(),n__zeros())
    2: U101(tt(),V1,V2) -> U102(isNatKind(activate(V1)),activate(V1),activate(V2))
    3: U102(tt(),V1,V2) -> U103(isNatIListKind(activate(V2)),activate(V1),activate(V2))
    4: U103(tt(),V1,V2) -> U104(isNatIListKind(activate(V2)),activate(V1),activate(V2))
    5: U104(tt(),V1,V2) -> U105(isNat(activate(V1)),activate(V2))
    6: U105(tt(),V2) -> U106(isNatIList(activate(V2)))
    7: U106(tt()) -> tt()
    8: U11(tt(),V1) -> U12(isNatIListKind(activate(V1)),activate(V1))
    9: U111(tt(),L,N) -> U112(isNatIListKind(activate(L)),activate(L),activate(N))
    10: U112(tt(),L,N) -> U113(isNat(activate(N)),activate(L),activate(N))
    11: U113(tt(),L,N) -> U114(isNatKind(activate(N)),activate(L))
    12: U114(tt(),L) -> s(length(activate(L)))
    13: U12(tt(),V1) -> U13(isNatList(activate(V1)))
    14: U121(tt(),IL) -> U122(isNatIListKind(activate(IL)))
    15: U122(tt()) -> nil()
    16: U13(tt()) -> tt()
    17: U131(tt(),IL,M,N) -> U132(isNatIListKind(activate(IL)),activate(IL),activate(M),activate(N))
    18: U132(tt(),IL,M,N) -> U133(isNat(activate(M)),activate(IL),activate(M),activate(N))
    19: U133(tt(),IL,M,N) -> U134(isNatKind(activate(M)),activate(IL),activate(M),activate(N))
    20: U134(tt(),IL,M,N) -> U135(isNat(activate(N)),activate(IL),activate(M),activate(N))
    21: U135(tt(),IL,M,N) -> U136(isNatKind(activate(N)),activate(IL),activate(M),activate(N))
    22: U136(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
    23: U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
    24: U22(tt(),V1) -> U23(isNat(activate(V1)))
    25: U23(tt()) -> tt()
    26: U31(tt(),V) -> U32(isNatIListKind(activate(V)),activate(V))
    27: U32(tt(),V) -> U33(isNatList(activate(V)))
    28: U33(tt()) -> tt()
    29: U41(tt(),V1,V2) -> U42(isNatKind(activate(V1)),activate(V1),activate(V2))
    30: U42(tt(),V1,V2) -> U43(isNatIListKind(activate(V2)),activate(V1),activate(V2))
    31: U43(tt(),V1,V2) -> U44(isNatIListKind(activate(V2)),activate(V1),activate(V2))
    32: U44(tt(),V1,V2) -> U45(isNat(activate(V1)),activate(V2))
    33: U45(tt(),V2) -> U46(isNatIList(activate(V2)))
    34: U46(tt()) -> tt()
    35: U51(tt(),V2) -> U52(isNatIListKind(activate(V2)))
    36: U52(tt()) -> tt()
    37: U61(tt(),V2) -> U62(isNatIListKind(activate(V2)))
    38: U62(tt()) -> tt()
    39: U71(tt()) -> tt()
    40: U81(tt()) -> tt()
    41: U91(tt(),V1,V2) -> U92(isNatKind(activate(V1)),activate(V1),activate(V2))
    42: U92(tt(),V1,V2) -> U93(isNatIListKind(activate(V2)),activate(V1),activate(V2))
    43: U93(tt(),V1,V2) -> U94(isNatIListKind(activate(V2)),activate(V1),activate(V2))
    44: U94(tt(),V1,V2) -> U95(isNat(activate(V1)),activate(V2))
    45: U95(tt(),V2) -> U96(isNatList(activate(V2)))
    46: U96(tt()) -> tt()
    47: isNat(n__0()) -> tt()
    48: isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1))
    49: isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
    50: isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V))
    51: isNatIList(n__zeros()) -> tt()
    52: isNatIList(n__cons(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V1),activate(V2))
    53: isNatIListKind(n__nil()) -> tt()
    54: isNatIListKind(n__zeros()) -> tt()
    55: isNatIListKind(n__cons(V1,V2)) -> U51(isNatKind(activate(V1)),activate(V2))
    56: isNatIListKind(n__take(V1,V2)) -> U61(isNatKind(activate(V1)),activate(V2))
    57: isNatKind(n__0()) -> tt()
    58: isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1)))
    59: isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1)))
    60: isNatList(n__nil()) -> tt()
    61: isNatList(n__cons(V1,V2)) -> U91(isNatKind(activate(V1)),activate(V1),activate(V2))
    62: isNatList(n__take(V1,V2)) -> U101(isNatKind(activate(V1)),activate(V1),activate(V2))
    63: length(nil()) -> 0()
    64: length(cons(N,L)) -> U111(isNatList(activate(L)),activate(L),N)
    65: take(0(),IL) -> U121(isNatIList(IL),IL)
    66: take(s(M),cons(N,IL)) -> U131(isNatIList(activate(IL)),activate(IL),M,N)
    67: zeros() -> n__zeros()
    68: take(X1,X2) -> n__take(X1,X2)
    69: 0() -> n__0()
    70: length(X) -> n__length(X)
    71: s(X) -> n__s(X)
    72: cons(X1,X2) -> n__cons(X1,X2)
    73: nil() -> n__nil()
    74: activate(n__zeros()) -> zeros()
    75: activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
    76: activate(n__0()) -> 0()
    77: activate(n__length(X)) -> length(activate(X))
    78: activate(n__s(X)) -> s(activate(X))
    79: activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
    80: activate(n__nil()) -> nil()
    81: activate(X) -> X
Number of strict rules: 81
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #U101(tt(),V1,V2) -> #U102(isNatKind(activate(V1)),activate(V1),activate(V2))
   #2: #U101(tt(),V1,V2) -> #isNatKind(activate(V1))
   #3: #U101(tt(),V1,V2) -> #activate(V1)
   #4: #U101(tt(),V1,V2) -> #activate(V1)
   #5: #U101(tt(),V1,V2) -> #activate(V2)
   #6: #U93(tt(),V1,V2) -> #U94(isNatIListKind(activate(V2)),activate(V1),activate(V2))
   #7: #U93(tt(),V1,V2) -> #isNatIListKind(activate(V2))
   #8: #U93(tt(),V1,V2) -> #activate(V2)
   #9: #U93(tt(),V1,V2) -> #activate(V1)
   #10: #U93(tt(),V1,V2) -> #activate(V2)
   #11: #U41(tt(),V1,V2) -> #U42(isNatKind(activate(V1)),activate(V1),activate(V2))
   #12: #U41(tt(),V1,V2) -> #isNatKind(activate(V1))
   #13: #U41(tt(),V1,V2) -> #activate(V1)
   #14: #U41(tt(),V1,V2) -> #activate(V1)
   #15: #U41(tt(),V1,V2) -> #activate(V2)
   #16: #U51(tt(),V2) -> #U52(isNatIListKind(activate(V2)))
   #17: #U51(tt(),V2) -> #isNatIListKind(activate(V2))
   #18: #U51(tt(),V2) -> #activate(V2)
   #19: #take(s(M),cons(N,IL)) -> #U131(isNatIList(activate(IL)),activate(IL),M,N)
   #20: #take(s(M),cons(N,IL)) -> #isNatIList(activate(IL))
   #21: #take(s(M),cons(N,IL)) -> #activate(IL)
   #22: #take(s(M),cons(N,IL)) -> #activate(IL)
   #23: #U92(tt(),V1,V2) -> #U93(isNatIListKind(activate(V2)),activate(V1),activate(V2))
   #24: #U92(tt(),V1,V2) -> #isNatIListKind(activate(V2))
   #25: #U92(tt(),V1,V2) -> #activate(V2)
   #26: #U92(tt(),V1,V2) -> #activate(V1)
   #27: #U92(tt(),V1,V2) -> #activate(V2)
   #28: #U91(tt(),V1,V2) -> #U92(isNatKind(activate(V1)),activate(V1),activate(V2))
   #29: #U91(tt(),V1,V2) -> #isNatKind(activate(V1))
   #30: #U91(tt(),V1,V2) -> #activate(V1)
   #31: #U91(tt(),V1,V2) -> #activate(V1)
   #32: #U91(tt(),V1,V2) -> #activate(V2)
   #33: #U61(tt(),V2) -> #U62(isNatIListKind(activate(V2)))
   #34: #U61(tt(),V2) -> #isNatIListKind(activate(V2))
   #35: #U61(tt(),V2) -> #activate(V2)
   #36: #isNat(n__length(V1)) -> #U11(isNatIListKind(activate(V1)),activate(V1))
   #37: #isNat(n__length(V1)) -> #isNatIListKind(activate(V1))
   #38: #isNat(n__length(V1)) -> #activate(V1)
   #39: #isNat(n__length(V1)) -> #activate(V1)
   #40: #activate(n__take(X1,X2)) -> #take(activate(X1),activate(X2))
   #41: #activate(n__take(X1,X2)) -> #activate(X1)
   #42: #activate(n__take(X1,X2)) -> #activate(X2)
   #43: #activate(n__zeros()) -> #zeros()
   #44: #isNatKind(n__length(V1)) -> #U71(isNatIListKind(activate(V1)))
   #45: #isNatKind(n__length(V1)) -> #isNatIListKind(activate(V1))
   #46: #isNatKind(n__length(V1)) -> #activate(V1)
   #47: #isNatList(n__cons(V1,V2)) -> #U91(isNatKind(activate(V1)),activate(V1),activate(V2))
   #48: #isNatList(n__cons(V1,V2)) -> #isNatKind(activate(V1))
   #49: #isNatList(n__cons(V1,V2)) -> #activate(V1)
   #50: #isNatList(n__cons(V1,V2)) -> #activate(V1)
   #51: #isNatList(n__cons(V1,V2)) -> #activate(V2)
   #52: #U105(tt(),V2) -> #U106(isNatIList(activate(V2)))
   #53: #U105(tt(),V2) -> #isNatIList(activate(V2))
   #54: #U105(tt(),V2) -> #activate(V2)
   #55: #isNatKind(n__s(V1)) -> #U81(isNatKind(activate(V1)))
   #56: #isNatKind(n__s(V1)) -> #isNatKind(activate(V1))
   #57: #isNatKind(n__s(V1)) -> #activate(V1)
   #58: #isNatIListKind(n__cons(V1,V2)) -> #U51(isNatKind(activate(V1)),activate(V2))
   #59: #isNatIListKind(n__cons(V1,V2)) -> #isNatKind(activate(V1))
   #60: #isNatIListKind(n__cons(V1,V2)) -> #activate(V1)
   #61: #isNatIListKind(n__cons(V1,V2)) -> #activate(V2)
   #62: #U12(tt(),V1) -> #U13(isNatList(activate(V1)))
   #63: #U12(tt(),V1) -> #isNatList(activate(V1))
   #64: #U12(tt(),V1) -> #activate(V1)
   #65: #U111(tt(),L,N) -> #U112(isNatIListKind(activate(L)),activate(L),activate(N))
   #66: #U111(tt(),L,N) -> #isNatIListKind(activate(L))
   #67: #U111(tt(),L,N) -> #activate(L)
   #68: #U111(tt(),L,N) -> #activate(L)
   #69: #U111(tt(),L,N) -> #activate(N)
   #70: #U113(tt(),L,N) -> #U114(isNatKind(activate(N)),activate(L))
   #71: #U113(tt(),L,N) -> #isNatKind(activate(N))
   #72: #U113(tt(),L,N) -> #activate(N)
   #73: #U113(tt(),L,N) -> #activate(L)
   #74: #activate(n__0()) -> #0()
   #75: #U22(tt(),V1) -> #U23(isNat(activate(V1)))
   #76: #U22(tt(),V1) -> #isNat(activate(V1))
   #77: #U22(tt(),V1) -> #activate(V1)
   #78: #U21(tt(),V1) -> #U22(isNatKind(activate(V1)),activate(V1))
   #79: #U21(tt(),V1) -> #isNatKind(activate(V1))
   #80: #U21(tt(),V1) -> #activate(V1)
   #81: #U21(tt(),V1) -> #activate(V1)
   #82: #activate(n__s(X)) -> #s(activate(X))
   #83: #activate(n__s(X)) -> #activate(X)
   #84: #U95(tt(),V2) -> #U96(isNatList(activate(V2)))
   #85: #U95(tt(),V2) -> #isNatList(activate(V2))
   #86: #U95(tt(),V2) -> #activate(V2)
   #87: #U114(tt(),L) -> #s(length(activate(L)))
   #88: #U114(tt(),L) -> #length(activate(L))
   #89: #U114(tt(),L) -> #activate(L)
   #90: #U43(tt(),V1,V2) -> #U44(isNatIListKind(activate(V2)),activate(V1),activate(V2))
   #91: #U43(tt(),V1,V2) -> #isNatIListKind(activate(V2))
   #92: #U43(tt(),V1,V2) -> #activate(V2)
   #93: #U43(tt(),V1,V2) -> #activate(V1)
   #94: #U43(tt(),V1,V2) -> #activate(V2)
   #95: #activate(n__cons(X1,X2)) -> #cons(activate(X1),X2)
   #96: #activate(n__cons(X1,X2)) -> #activate(X1)
   #97: #isNatIListKind(n__take(V1,V2)) -> #U61(isNatKind(activate(V1)),activate(V2))
   #98: #isNatIListKind(n__take(V1,V2)) -> #isNatKind(activate(V1))
   #99: #isNatIListKind(n__take(V1,V2)) -> #activate(V1)
   #100: #isNatIListKind(n__take(V1,V2)) -> #activate(V2)
   #101: #U121(tt(),IL) -> #U122(isNatIListKind(activate(IL)))
   #102: #U121(tt(),IL) -> #isNatIListKind(activate(IL))
   #103: #U121(tt(),IL) -> #activate(IL)
   #104: #isNatList(n__take(V1,V2)) -> #U101(isNatKind(activate(V1)),activate(V1),activate(V2))
   #105: #isNatList(n__take(V1,V2)) -> #isNatKind(activate(V1))
   #106: #isNatList(n__take(V1,V2)) -> #activate(V1)
   #107: #isNatList(n__take(V1,V2)) -> #activate(V1)
   #108: #isNatList(n__take(V1,V2)) -> #activate(V2)
   #109: #U42(tt(),V1,V2) -> #U43(isNatIListKind(activate(V2)),activate(V1),activate(V2))
   #110: #U42(tt(),V1,V2) -> #isNatIListKind(activate(V2))
   #111: #U42(tt(),V1,V2) -> #activate(V2)
   #112: #U42(tt(),V1,V2) -> #activate(V1)
   #113: #U42(tt(),V1,V2) -> #activate(V2)
   #114: #isNatIList(n__cons(V1,V2)) -> #U41(isNatKind(activate(V1)),activate(V1),activate(V2))
   #115: #isNatIList(n__cons(V1,V2)) -> #isNatKind(activate(V1))
   #116: #isNatIList(n__cons(V1,V2)) -> #activate(V1)
   #117: #isNatIList(n__cons(V1,V2)) -> #activate(V1)
   #118: #isNatIList(n__cons(V1,V2)) -> #activate(V2)
   #119: #isNat(n__s(V1)) -> #U21(isNatKind(activate(V1)),activate(V1))
   #120: #isNat(n__s(V1)) -> #isNatKind(activate(V1))
   #121: #isNat(n__s(V1)) -> #activate(V1)
   #122: #isNat(n__s(V1)) -> #activate(V1)
   #123: #U134(tt(),IL,M,N) -> #U135(isNat(activate(N)),activate(IL),activate(M),activate(N))
   #124: #U134(tt(),IL,M,N) -> #isNat(activate(N))
   #125: #U134(tt(),IL,M,N) -> #activate(N)
   #126: #U134(tt(),IL,M,N) -> #activate(IL)
   #127: #U134(tt(),IL,M,N) -> #activate(M)
   #128: #U134(tt(),IL,M,N) -> #activate(N)
   #129: #U112(tt(),L,N) -> #U113(isNat(activate(N)),activate(L),activate(N))
   #130: #U112(tt(),L,N) -> #isNat(activate(N))
   #131: #U112(tt(),L,N) -> #activate(N)
   #132: #U112(tt(),L,N) -> #activate(L)
   #133: #U112(tt(),L,N) -> #activate(N)
   #134: #length(cons(N,L)) -> #U111(isNatList(activate(L)),activate(L),N)
   #135: #length(cons(N,L)) -> #isNatList(activate(L))
   #136: #length(cons(N,L)) -> #activate(L)
   #137: #length(cons(N,L)) -> #activate(L)
   #138: #U45(tt(),V2) -> #U46(isNatIList(activate(V2)))
   #139: #U45(tt(),V2) -> #isNatIList(activate(V2))
   #140: #U45(tt(),V2) -> #activate(V2)
   #141: #U104(tt(),V1,V2) -> #U105(isNat(activate(V1)),activate(V2))
   #142: #U104(tt(),V1,V2) -> #isNat(activate(V1))
   #143: #U104(tt(),V1,V2) -> #activate(V1)
   #144: #U104(tt(),V1,V2) -> #activate(V2)
   #145: #U94(tt(),V1,V2) -> #U95(isNat(activate(V1)),activate(V2))
   #146: #U94(tt(),V1,V2) -> #isNat(activate(V1))
   #147: #U94(tt(),V1,V2) -> #activate(V1)
   #148: #U94(tt(),V1,V2) -> #activate(V2)
   #149: #take(0(),IL) -> #U121(isNatIList(IL),IL)
   #150: #take(0(),IL) -> #isNatIList(IL)
   #151: #U136(tt(),IL,M,N) -> #cons(activate(N),n__take(activate(M),activate(IL)))
   #152: #U136(tt(),IL,M,N) -> #activate(N)
   #153: #U136(tt(),IL,M,N) -> #activate(M)
   #154: #U136(tt(),IL,M,N) -> #activate(IL)
   #155: #U32(tt(),V) -> #U33(isNatList(activate(V)))
   #156: #U32(tt(),V) -> #isNatList(activate(V))
   #157: #U32(tt(),V) -> #activate(V)
   #158: #U131(tt(),IL,M,N) -> #U132(isNatIListKind(activate(IL)),activate(IL),activate(M),activate(N))
   #159: #U131(tt(),IL,M,N) -> #isNatIListKind(activate(IL))
   #160: #U131(tt(),IL,M,N) -> #activate(IL)
   #161: #U131(tt(),IL,M,N) -> #activate(IL)
   #162: #U131(tt(),IL,M,N) -> #activate(M)
   #163: #U131(tt(),IL,M,N) -> #activate(N)
   #164: #U44(tt(),V1,V2) -> #U45(isNat(activate(V1)),activate(V2))
   #165: #U44(tt(),V1,V2) -> #isNat(activate(V1))
   #166: #U44(tt(),V1,V2) -> #activate(V1)
   #167: #U44(tt(),V1,V2) -> #activate(V2)
   #168: #U133(tt(),IL,M,N) -> #U134(isNatKind(activate(M)),activate(IL),activate(M),activate(N))
   #169: #U133(tt(),IL,M,N) -> #isNatKind(activate(M))
   #170: #U133(tt(),IL,M,N) -> #activate(M)
   #171: #U133(tt(),IL,M,N) -> #activate(IL)
   #172: #U133(tt(),IL,M,N) -> #activate(M)
   #173: #U133(tt(),IL,M,N) -> #activate(N)
   #174: #length(nil()) -> #0()
   #175: #U31(tt(),V) -> #U32(isNatIListKind(activate(V)),activate(V))
   #176: #U31(tt(),V) -> #isNatIListKind(activate(V))
   #177: #U31(tt(),V) -> #activate(V)
   #178: #U31(tt(),V) -> #activate(V)
   #179: #U135(tt(),IL,M,N) -> #U136(isNatKind(activate(N)),activate(IL),activate(M),activate(N))
   #180: #U135(tt(),IL,M,N) -> #isNatKind(activate(N))
   #181: #U135(tt(),IL,M,N) -> #activate(N)
   #182: #U135(tt(),IL,M,N) -> #activate(IL)
   #183: #U135(tt(),IL,M,N) -> #activate(M)
   #184: #U135(tt(),IL,M,N) -> #activate(N)
   #185: #U102(tt(),V1,V2) -> #U103(isNatIListKind(activate(V2)),activate(V1),activate(V2))
   #186: #U102(tt(),V1,V2) -> #isNatIListKind(activate(V2))
   #187: #U102(tt(),V1,V2) -> #activate(V2)
   #188: #U102(tt(),V1,V2) -> #activate(V1)
   #189: #U102(tt(),V1,V2) -> #activate(V2)
   #190: #activate(n__length(X)) -> #length(activate(X))
   #191: #activate(n__length(X)) -> #activate(X)
   #192: #zeros() -> #cons(0(),n__zeros())
   #193: #zeros() -> #0()
   #194: #U11(tt(),V1) -> #U12(isNatIListKind(activate(V1)),activate(V1))
   #195: #U11(tt(),V1) -> #isNatIListKind(activate(V1))
   #196: #U11(tt(),V1) -> #activate(V1)
   #197: #U11(tt(),V1) -> #activate(V1)
   #198: #U122(tt()) -> #nil()
   #199: #U103(tt(),V1,V2) -> #U104(isNatIListKind(activate(V2)),activate(V1),activate(V2))
   #200: #U103(tt(),V1,V2) -> #isNatIListKind(activate(V2))
   #201: #U103(tt(),V1,V2) -> #activate(V2)
   #202: #U103(tt(),V1,V2) -> #activate(V1)
   #203: #U103(tt(),V1,V2) -> #activate(V2)
   #204: #activate(n__nil()) -> #nil()
   #205: #isNatIList(V) -> #U31(isNatIListKind(activate(V)),activate(V))
   #206: #isNatIList(V) -> #isNatIListKind(activate(V))
   #207: #isNatIList(V) -> #activate(V)
   #208: #isNatIList(V) -> #activate(V)
   #209: #U132(tt(),IL,M,N) -> #U133(isNat(activate(M)),activate(IL),activate(M),activate(N))
   #210: #U132(tt(),IL,M,N) -> #isNat(activate(M))
   #211: #U132(tt(),IL,M,N) -> #activate(M)
   #212: #U132(tt(),IL,M,N) -> #activate(IL)
   #213: #U132(tt(),IL,M,N) -> #activate(M)
   #214: #U132(tt(),IL,M,N) -> #activate(N)
Number of SCCs: 1, DPs: 192, edges: 1236
	SCC { #1..15 #17..32 #34..42 #45..51 #53 #54 #56..61 #63..73 #76..81 #83 #85 #86 #88..94 #96..100 #102..137 #139..150 #152..154 #156..173 #175..191 #194..197 #199..203 #205..214 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   #0()	weight: 0
 #U32(x1,x2)	weight: x2
#isNatIListKind(x1)	weight: x1
isNatKind(x1)	weight: (/ 1 2)
   U21(x1,x2)	weight: 0
 #U96(x1)	weight: 0
isNatList(x1)	weight: (/ 1 2)
   U11(x1,x2)	weight: x2
  U136(x1,x2,x3,x4)	weight: (/ 9 2) + x2 + x3 + x4
 #U94(x1,x2,x3)	weight: x2 + x3
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
  U105(x1,x2)	weight: x2
#isNat(x1)	weight: x1
  U106(x1)	weight: x1
#take(x1,x2)	weight: x1 + x2
   U42(x1,x2,x3)	weight: 0
   U91(x1,x2,x3)	weight: 0
#U101(x1,x2,x3)	weight: 4 + x2 + x3
activate(x1)	weight: x1
  take(x1,x2)	weight: (/ 9 2) + x1 + x2
#U104(x1,x2,x3)	weight: (/ 3 2) + x1 + x2 + x3
   U71(x1)	weight: 0
 #U81(x1)	weight: 0
 #U92(x1,x2,x3)	weight: x2 + x3
#U133(x1,x2,x3,x4)	weight: x2 + x3 + x4
  U131(x1,x2,x3,x4)	weight: (/ 9 2) + x2 + x3 + x4
n__zeros()	weight: 0
isNatIList(x1)	weight: 0
  U135(x1,x2,x3,x4)	weight: (/ 9 2) + x2 + x3 + x4
  U101(x1,x2,x3)	weight: 0
   U95(x1,x2)	weight: x1
#U136(x1,x2,x3,x4)	weight: x2 + x3 + x4
  U111(x1,x2,x3)	weight: x2
  U132(x1,x2,x3,x4)	weight: (/ 9 2) + x2 + x3 + x4
   U43(x1,x2,x3)	weight: 0
 #U93(x1,x2,x3)	weight: x2 + x3
#activate(x1)	weight: x1
  U103(x1,x2,x3)	weight: 0
 #U23(x1)	weight: 0
   U44(x1,x2,x3)	weight: 0
 #U43(x1,x2,x3)	weight: x2 + x3
#U106(x1)	weight: 0
#U121(x1,x2)	weight: x2
   U23(x1)	weight: 0
   U93(x1,x2,x3)	weight: 0
#U114(x1,x2)	weight: x2
#U131(x1,x2,x3,x4)	weight: x2 + x3 + x4
 #U13(x1)	weight: 0
   U94(x1,x2,x3)	weight: x3
 zeros()	weight: 0
 #U95(x1,x2)	weight: x2
n__nil()	weight: 0
 #U52(x1)	weight: 0
#U103(x1,x2,x3)	weight: (/ 5 2) + x1 + x2 + x3
   U12(x1,x2)	weight: x2
 #U33(x1)	weight: 0
#U135(x1,x2,x3,x4)	weight: x2 + x3 + x4
 #U44(x1,x2,x3)	weight: x2 + x3
  n__s(x1)	weight: x1
  U104(x1,x2,x3)	weight: 0
 #U42(x1,x2,x3)	weight: x2 + x3
  U113(x1,x2,x3)	weight: x2
 #U12(x1,x2)	weight: x2
 #U62(x1)	weight: 0
     0()	weight: 0
#zeros()	weight: 0
  U134(x1,x2,x3,x4)	weight: (/ 9 2) + x2 + x3 + x4
n__take(x1,x2)	weight: (/ 9 2) + x1 + x2
#isNatList(x1)	weight: x1
#U102(x1,x2,x3)	weight: (/ 7 2) + x2 + x3
   #s(x1)	weight: 0
#U105(x1,x2)	weight: (/ 1 2) + x1 + x2
n__cons(x1,x2)	weight: x1 + x2
isNatIListKind(x1)	weight: (/ 1 2)
   nil()	weight: 0
  U114(x1,x2)	weight: x2
   U62(x1)	weight: x1
   U45(x1,x2)	weight: x2
 #nil()	weight: 0
  U133(x1,x2,x3,x4)	weight: (/ 9 2) + x2 + x3 + x4
#U111(x1,x2,x3)	weight: x2 + x3
   U32(x1,x2)	weight: 0
   U33(x1)	weight: 0
  n__0()	weight: 0
n__length(x1)	weight: x1
 #U46(x1)	weight: 0
 isNat(x1)	weight: (/ 1 2) + x1
   U46(x1)	weight: 0
   U52(x1)	weight: (/ 1 2)
   U61(x1,x2)	weight: (/ 1 2)
 #U51(x1,x2)	weight: x2
#U134(x1,x2,x3,x4)	weight: x2 + x3 + x4
#U113(x1,x2,x3)	weight: x2 + x3
 #U11(x1,x2)	weight: x2
   U96(x1)	weight: 0
   U31(x1,x2)	weight: 0
   U92(x1,x2,x3)	weight: 0
  U112(x1,x2,x3)	weight: x2
 #U41(x1,x2,x3)	weight: x2 + x3
  cons(x1,x2)	weight: x1 + x2
  U102(x1,x2,x3)	weight: 0
#isNatIList(x1)	weight: x1
 #U21(x1,x2)	weight: x2
   U81(x1)	weight: x1
 #U22(x1,x2)	weight: x2
#U112(x1,x2,x3)	weight: x2 + x3
    tt()	weight: 0
 #U71(x1)	weight: 0
   U13(x1)	weight: 0
   U22(x1,x2)	weight: 0
 #U45(x1,x2)	weight: x2
   U51(x1,x2)	weight: (/ 1 2)
#isNatKind(x1)	weight: x1
#U122(x1)	weight: 0
length(x1)	weight: x1
#length(x1)	weight: x1
   U41(x1,x2,x3)	weight: x3
 #U31(x1,x2)	weight: x2
 #U91(x1,x2,x3)	weight: x2 + x3
#U132(x1,x2,x3,x4)	weight: x2 + x3 + x4
  U121(x1,x2)	weight: 0
 #U61(x1,x2)	weight: (/ 1 2) + x1 + x2
  U122(x1)	weight: 0
    Usable rules: { 1 8..25 35..40 47..49 53..59 63..81 }
    Removed DPs: #1..5 #34 #35 #40..42 #53 #54 #97..100 #104..108 #141..144 #185..189 #199..203
Number of SCCs: 2, DPs: 86, edges: 336
	SCC { #11 #90 #109 #114 #139 #164 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)...