Input TRS:
    1: a__zeros() -> cons(0(),zeros())
    2: a__U101(tt(),V1,V2) -> a__U102(a__isNatKind(V1),V1,V2)
    3: a__U102(tt(),V1,V2) -> a__U103(a__isNatIListKind(V2),V1,V2)
    4: a__U103(tt(),V1,V2) -> a__U104(a__isNatIListKind(V2),V1,V2)
    5: a__U104(tt(),V1,V2) -> a__U105(a__isNat(V1),V2)
    6: a__U105(tt(),V2) -> a__U106(a__isNatIList(V2))
    7: a__U106(tt()) -> tt()
    8: a__U11(tt(),V1) -> a__U12(a__isNatIListKind(V1),V1)
    9: a__U111(tt(),L,N) -> a__U112(a__isNatIListKind(L),L,N)
    10: a__U112(tt(),L,N) -> a__U113(a__isNat(N),L,N)
    11: a__U113(tt(),L,N) -> a__U114(a__isNatKind(N),L)
    12: a__U114(tt(),L) -> s(a__length(mark(L)))
    13: a__U12(tt(),V1) -> a__U13(a__isNatList(V1))
    14: a__U121(tt(),IL) -> a__U122(a__isNatIListKind(IL))
    15: a__U122(tt()) -> nil()
    16: a__U13(tt()) -> tt()
    17: a__U131(tt(),IL,M,N) -> a__U132(a__isNatIListKind(IL),IL,M,N)
    18: a__U132(tt(),IL,M,N) -> a__U133(a__isNat(M),IL,M,N)
    19: a__U133(tt(),IL,M,N) -> a__U134(a__isNatKind(M),IL,M,N)
    20: a__U134(tt(),IL,M,N) -> a__U135(a__isNat(N),IL,M,N)
    21: a__U135(tt(),IL,M,N) -> a__U136(a__isNatKind(N),IL,M,N)
    22: a__U136(tt(),IL,M,N) -> cons(mark(N),take(M,IL))
    23: a__U21(tt(),V1) -> a__U22(a__isNatKind(V1),V1)
    24: a__U22(tt(),V1) -> a__U23(a__isNat(V1))
    25: a__U23(tt()) -> tt()
    26: a__U31(tt(),V) -> a__U32(a__isNatIListKind(V),V)
    27: a__U32(tt(),V) -> a__U33(a__isNatList(V))
    28: a__U33(tt()) -> tt()
    29: a__U41(tt(),V1,V2) -> a__U42(a__isNatKind(V1),V1,V2)
    30: a__U42(tt(),V1,V2) -> a__U43(a__isNatIListKind(V2),V1,V2)
    31: a__U43(tt(),V1,V2) -> a__U44(a__isNatIListKind(V2),V1,V2)
    32: a__U44(tt(),V1,V2) -> a__U45(a__isNat(V1),V2)
    33: a__U45(tt(),V2) -> a__U46(a__isNatIList(V2))
    34: a__U46(tt()) -> tt()
    35: a__U51(tt(),V2) -> a__U52(a__isNatIListKind(V2))
    36: a__U52(tt()) -> tt()
    37: a__U61(tt(),V2) -> a__U62(a__isNatIListKind(V2))
    38: a__U62(tt()) -> tt()
    39: a__U71(tt()) -> tt()
    40: a__U81(tt()) -> tt()
    41: a__U91(tt(),V1,V2) -> a__U92(a__isNatKind(V1),V1,V2)
    42: a__U92(tt(),V1,V2) -> a__U93(a__isNatIListKind(V2),V1,V2)
    43: a__U93(tt(),V1,V2) -> a__U94(a__isNatIListKind(V2),V1,V2)
    44: a__U94(tt(),V1,V2) -> a__U95(a__isNat(V1),V2)
    45: a__U95(tt(),V2) -> a__U96(a__isNatList(V2))
    46: a__U96(tt()) -> tt()
    47: a__isNat(0()) -> tt()
    48: a__isNat(length(V1)) -> a__U11(a__isNatIListKind(V1),V1)
    49: a__isNat(s(V1)) -> a__U21(a__isNatKind(V1),V1)
    50: a__isNatIList(V) -> a__U31(a__isNatIListKind(V),V)
    51: a__isNatIList(zeros()) -> tt()
    52: a__isNatIList(cons(V1,V2)) -> a__U41(a__isNatKind(V1),V1,V2)
    53: a__isNatIListKind(nil()) -> tt()
    54: a__isNatIListKind(zeros()) -> tt()
    55: a__isNatIListKind(cons(V1,V2)) -> a__U51(a__isNatKind(V1),V2)
    56: a__isNatIListKind(take(V1,V2)) -> a__U61(a__isNatKind(V1),V2)
    57: a__isNatKind(0()) -> tt()
    58: a__isNatKind(length(V1)) -> a__U71(a__isNatIListKind(V1))
    59: a__isNatKind(s(V1)) -> a__U81(a__isNatKind(V1))
    60: a__isNatList(nil()) -> tt()
    61: a__isNatList(cons(V1,V2)) -> a__U91(a__isNatKind(V1),V1,V2)
    62: a__isNatList(take(V1,V2)) -> a__U101(a__isNatKind(V1),V1,V2)
    63: a__length(nil()) -> 0()
    64: a__length(cons(N,L)) -> a__U111(a__isNatList(L),L,N)
    65: a__take(0(),IL) -> a__U121(a__isNatIList(IL),IL)
    66: a__take(s(M),cons(N,IL)) -> a__U131(a__isNatIList(IL),IL,M,N)
    67: mark(zeros()) -> a__zeros()
    68: mark(U101(X1,X2,X3)) -> a__U101(mark(X1),X2,X3)
    69: mark(U102(X1,X2,X3)) -> a__U102(mark(X1),X2,X3)
    70: mark(isNatKind(X)) -> a__isNatKind(X)
    71: mark(U103(X1,X2,X3)) -> a__U103(mark(X1),X2,X3)
    72: mark(isNatIListKind(X)) -> a__isNatIListKind(X)
    73: mark(U104(X1,X2,X3)) -> a__U104(mark(X1),X2,X3)
    74: mark(U105(X1,X2)) -> a__U105(mark(X1),X2)
    75: mark(isNat(X)) -> a__isNat(X)
    76: mark(U106(X)) -> a__U106(mark(X))
    77: mark(isNatIList(X)) -> a__isNatIList(X)
    78: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
    79: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
    80: mark(U111(X1,X2,X3)) -> a__U111(mark(X1),X2,X3)
    81: mark(U112(X1,X2,X3)) -> a__U112(mark(X1),X2,X3)
    82: mark(U113(X1,X2,X3)) -> a__U113(mark(X1),X2,X3)
    83: mark(U114(X1,X2)) -> a__U114(mark(X1),X2)
    84: mark(length(X)) -> a__length(mark(X))
    85: mark(U13(X)) -> a__U13(mark(X))
    86: mark(isNatList(X)) -> a__isNatList(X)
    87: mark(U121(X1,X2)) -> a__U121(mark(X1),X2)
    88: mark(U122(X)) -> a__U122(mark(X))
    89: mark(U131(X1,X2,X3,X4)) -> a__U131(mark(X1),X2,X3,X4)
    90: mark(U132(X1,X2,X3,X4)) -> a__U132(mark(X1),X2,X3,X4)
    91: mark(U133(X1,X2,X3,X4)) -> a__U133(mark(X1),X2,X3,X4)
    92: mark(U134(X1,X2,X3,X4)) -> a__U134(mark(X1),X2,X3,X4)
    93: mark(U135(X1,X2,X3,X4)) -> a__U135(mark(X1),X2,X3,X4)
    94: mark(U136(X1,X2,X3,X4)) -> a__U136(mark(X1),X2,X3,X4)
    95: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
    96: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
    97: mark(U22(X1,X2)) -> a__U22(mark(X1),X2)
    98: mark(U23(X)) -> a__U23(mark(X))
    99: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
    100: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
    101: mark(U33(X)) -> a__U33(mark(X))
    102: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
    103: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
    104: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
    105: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
    106: mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
    107: mark(U46(X)) -> a__U46(mark(X))
    108: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
    109: mark(U52(X)) -> a__U52(mark(X))
    110: mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
    111: mark(U62(X)) -> a__U62(mark(X))
    112: mark(U71(X)) -> a__U71(mark(X))
    113: mark(U81(X)) -> a__U81(mark(X))
    114: mark(U91(X1,X2,X3)) -> a__U91(mark(X1),X2,X3)
    115: mark(U92(X1,X2,X3)) -> a__U92(mark(X1),X2,X3)
    116: mark(U93(X1,X2,X3)) -> a__U93(mark(X1),X2,X3)
    117: mark(U94(X1,X2,X3)) -> a__U94(mark(X1),X2,X3)
    118: mark(U95(X1,X2)) -> a__U95(mark(X1),X2)
    119: mark(U96(X)) -> a__U96(mark(X))
    120: mark(cons(X1,X2)) -> cons(mark(X1),X2)
    121: mark(0()) -> 0()
    122: mark(tt()) -> tt()
    123: mark(s(X)) -> s(mark(X))
    124: mark(nil()) -> nil()
    125: a__zeros() -> zeros()
    126: a__U101(X1,X2,X3) -> U101(X1,X2,X3)
    127: a__U102(X1,X2,X3) -> U102(X1,X2,X3)
    128: a__isNatKind(X) -> isNatKind(X)
    129: a__U103(X1,X2,X3) -> U103(X1,X2,X3)
    130: a__isNatIListKind(X) -> isNatIListKind(X)
    131: a__U104(X1,X2,X3) -> U104(X1,X2,X3)
    132: a__U105(X1,X2) -> U105(X1,X2)
    133: a__isNat(X) -> isNat(X)
    134: a__U106(X) -> U106(X)
    135: a__isNatIList(X) -> isNatIList(X)
    136: a__U11(X1,X2) -> U11(X1,X2)
    137: a__U12(X1,X2) -> U12(X1,X2)
    138: a__U111(X1,X2,X3) -> U111(X1,X2,X3)
    139: a__U112(X1,X2,X3) -> U112(X1,X2,X3)
    140: a__U113(X1,X2,X3) -> U113(X1,X2,X3)
    141: a__U114(X1,X2) -> U114(X1,X2)
    142: a__length(X) -> length(X)
    143: a__U13(X) -> U13(X)
    144: a__isNatList(X) -> isNatList(X)
    145: a__U121(X1,X2) -> U121(X1,X2)
    146: a__U122(X) -> U122(X)
    147: a__U131(X1,X2,X3,X4) -> U131(X1,X2,X3,X4)
    148: a__U132(X1,X2,X3,X4) -> U132(X1,X2,X3,X4)
    149: a__U133(X1,X2,X3,X4) -> U133(X1,X2,X3,X4)
    150: a__U134(X1,X2,X3,X4) -> U134(X1,X2,X3,X4)
    151: a__U135(X1,X2,X3,X4) -> U135(X1,X2,X3,X4)
    152: a__U136(X1,X2,X3,X4) -> U136(X1,X2,X3,X4)
    153: a__take(X1,X2) -> take(X1,X2)
    154: a__U21(X1,X2) -> U21(X1,X2)
    155: a__U22(X1,X2) -> U22(X1,X2)
    156: a__U23(X) -> U23(X)
    157: a__U31(X1,X2) -> U31(X1,X2)
    158: a__U32(X1,X2) -> U32(X1,X2)
    159: a__U33(X) -> U33(X)
    160: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
    161: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
    162: a__U43(X1,X2,X3) -> U43(X1,X2,X3)
    163: a__U44(X1,X2,X3) -> U44(X1,X2,X3)
    164: a__U45(X1,X2) -> U45(X1,X2)
    165: a__U46(X) -> U46(X)
    166: a__U51(X1,X2) -> U51(X1,X2)
    167: a__U52(X) -> U52(X)
    168: a__U61(X1,X2) -> U61(X1,X2)
    169: a__U62(X) -> U62(X)
    170: a__U71(X) -> U71(X)
    171: a__U81(X) -> U81(X)
    172: a__U91(X1,X2,X3) -> U91(X1,X2,X3)
    173: a__U92(X1,X2,X3) -> U92(X1,X2,X3)
    174: a__U93(X1,X2,X3) -> U93(X1,X2,X3)
    175: a__U94(X1,X2,X3) -> U94(X1,X2,X3)
    176: a__U95(X1,X2) -> U95(X1,X2)
    177: a__U96(X) -> U96(X)
Number of strict rules: 177
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #a__U101(tt(),V1,V2) -> #a__U102(a__isNatKind(V1),V1,V2)
   #2: #a__U101(tt(),V1,V2) -> #a__isNatKind(V1)
   #3: #mark(isNatList(X)) -> #a__isNatList(X)
   #4: #a__U93(tt(),V1,V2) -> #a__U94(a__isNatIListKind(V2),V1,V2)
   #5: #a__U93(tt(),V1,V2) -> #a__isNatIListKind(V2)
   #6: #a__U41(tt(),V1,V2) -> #a__U42(a__isNatKind(V1),V1,V2)
   #7: #a__U41(tt(),V1,V2) -> #a__isNatKind(V1)
   #8: #a__U51(tt(),V2) -> #a__U52(a__isNatIListKind(V2))
   #9: #a__U51(tt(),V2) -> #a__isNatIListKind(V2)
   #10: #mark(U114(X1,X2)) -> #a__U114(mark(X1),X2)
   #11: #mark(U114(X1,X2)) -> #mark(X1)
   #12: #a__take(s(M),cons(N,IL)) -> #a__U131(a__isNatIList(IL),IL,M,N)
   #13: #a__take(s(M),cons(N,IL)) -> #a__isNatIList(IL)
   #14: #a__U92(tt(),V1,V2) -> #a__U93(a__isNatIListKind(V2),V1,V2)
   #15: #a__U92(tt(),V1,V2) -> #a__isNatIListKind(V2)
   #16: #mark(U92(X1,X2,X3)) -> #a__U92(mark(X1),X2,X3)
   #17: #mark(U92(X1,X2,X3)) -> #mark(X1)
   #18: #mark(take(X1,X2)) -> #a__take(mark(X1),mark(X2))
   #19: #mark(take(X1,X2)) -> #mark(X1)
   #20: #mark(take(X1,X2)) -> #mark(X2)
   #21: #a__U91(tt(),V1,V2) -> #a__U92(a__isNatKind(V1),V1,V2)
   #22: #a__U91(tt(),V1,V2) -> #a__isNatKind(V1)
   #23: #a__U61(tt(),V2) -> #a__U62(a__isNatIListKind(V2))
   #24: #a__U61(tt(),V2) -> #a__isNatIListKind(V2)
   #25: #mark(U91(X1,X2,X3)) -> #a__U91(mark(X1),X2,X3)
   #26: #mark(U91(X1,X2,X3)) -> #mark(X1)
   #27: #mark(U31(X1,X2)) -> #a__U31(mark(X1),X2)
   #28: #mark(U31(X1,X2)) -> #mark(X1)
   #29: #mark(U22(X1,X2)) -> #a__U22(mark(X1),X2)
   #30: #mark(U22(X1,X2)) -> #mark(X1)
   #31: #mark(U133(X1,X2,X3,X4)) -> #a__U133(mark(X1),X2,X3,X4)
   #32: #mark(U133(X1,X2,X3,X4)) -> #mark(X1)
   #33: #mark(U104(X1,X2,X3)) -> #a__U104(mark(X1),X2,X3)
   #34: #mark(U104(X1,X2,X3)) -> #mark(X1)
   #35: #mark(U103(X1,X2,X3)) -> #a__U103(mark(X1),X2,X3)
   #36: #mark(U103(X1,X2,X3)) -> #mark(X1)
   #37: #a__isNat(length(V1)) -> #a__U11(a__isNatIListKind(V1),V1)
   #38: #a__isNat(length(V1)) -> #a__isNatIListKind(V1)
   #39: #mark(s(X)) -> #mark(X)
   #40: #mark(isNat(X)) -> #a__isNat(X)
   #41: #mark(U71(X)) -> #a__U71(mark(X))
   #42: #mark(U71(X)) -> #mark(X)
   #43: #mark(U105(X1,X2)) -> #a__U105(mark(X1),X2)
   #44: #mark(U105(X1,X2)) -> #mark(X1)
   #45: #a__isNatKind(length(V1)) -> #a__U71(a__isNatIListKind(V1))
   #46: #a__isNatKind(length(V1)) -> #a__isNatIListKind(V1)
   #47: #mark(U81(X)) -> #a__U81(mark(X))
   #48: #mark(U81(X)) -> #mark(X)
   #49: #a__isNatList(cons(V1,V2)) -> #a__U91(a__isNatKind(V1),V1,V2)
   #50: #a__isNatList(cons(V1,V2)) -> #a__isNatKind(V1)
   #51: #mark(U93(X1,X2,X3)) -> #a__U93(mark(X1),X2,X3)
   #52: #mark(U93(X1,X2,X3)) -> #mark(X1)
   #53: #a__U105(tt(),V2) -> #a__U106(a__isNatIList(V2))
   #54: #a__U105(tt(),V2) -> #a__isNatIList(V2)
   #55: #a__isNatKind(s(V1)) -> #a__U81(a__isNatKind(V1))
   #56: #a__isNatKind(s(V1)) -> #a__isNatKind(V1)
   #57: #mark(U61(X1,X2)) -> #a__U61(mark(X1),X2)
   #58: #mark(U61(X1,X2)) -> #mark(X1)
   #59: #a__isNatIListKind(cons(V1,V2)) -> #a__U51(a__isNatKind(V1),V2)
   #60: #a__isNatIListKind(cons(V1,V2)) -> #a__isNatKind(V1)
   #61: #mark(zeros()) -> #a__zeros()
   #62: #mark(U132(X1,X2,X3,X4)) -> #a__U132(mark(X1),X2,X3,X4)
   #63: #mark(U132(X1,X2,X3,X4)) -> #mark(X1)
   #64: #mark(U46(X)) -> #a__U46(mark(X))
   #65: #mark(U46(X)) -> #mark(X)
   #66: #a__U12(tt(),V1) -> #a__U13(a__isNatList(V1))
   #67: #a__U12(tt(),V1) -> #a__isNatList(V1)
   #68: #a__U111(tt(),L,N) -> #a__U112(a__isNatIListKind(L),L,N)
   #69: #a__U111(tt(),L,N) -> #a__isNatIListKind(L)
   #70: #a__U113(tt(),L,N) -> #a__U114(a__isNatKind(N),L)
   #71: #a__U113(tt(),L,N) -> #a__isNatKind(N)
   #72: #mark(U23(X)) -> #a__U23(mark(X))
   #73: #mark(U23(X)) -> #mark(X)
   #74: #mark(U106(X)) -> #a__U106(mark(X))
   #75: #mark(U106(X)) -> #mark(X)
   #76: #mark(U52(X)) -> #a__U52(mark(X))
   #77: #mark(U52(X)) -> #mark(X)
   #78: #mark(U136(X1,X2,X3,X4)) -> #a__U136(mark(X1),X2,X3,X4)
   #79: #mark(U136(X1,X2,X3,X4)) -> #mark(X1)
   #80: #a__U22(tt(),V1) -> #a__U23(a__isNat(V1))
   #81: #a__U22(tt(),V1) -> #a__isNat(V1)
   #82: #mark(isNatKind(X)) -> #a__isNatKind(X)
   #83: #a__U21(tt(),V1) -> #a__U22(a__isNatKind(V1),V1)
   #84: #a__U21(tt(),V1) -> #a__isNatKind(V1)
   #85: #mark(U112(X1,X2,X3)) -> #a__U112(mark(X1),X2,X3)
   #86: #mark(U112(X1,X2,X3)) -> #mark(X1)
   #87: #mark(U95(X1,X2)) -> #a__U95(mark(X1),X2)
   #88: #mark(U95(X1,X2)) -> #mark(X1)
   #89: #mark(U11(X1,X2)) -> #a__U11(mark(X1),X2)
   #90: #mark(U11(X1,X2)) -> #mark(X1)
   #91: #a__U95(tt(),V2) -> #a__U96(a__isNatList(V2))
   #92: #a__U95(tt(),V2) -> #a__isNatList(V2)
   #93: #mark(U21(X1,X2)) -> #a__U21(mark(X1),X2)
   #94: #mark(U21(X1,X2)) -> #mark(X1)
   #95: #mark(U102(X1,X2,X3)) -> #a__U102(mark(X1),X2,X3)
   #96: #mark(U102(X1,X2,X3)) -> #mark(X1)
   #97: #mark(U33(X)) -> #a__U33(mark(X))
   #98: #mark(U33(X)) -> #mark(X)
   #99: #a__U114(tt(),L) -> #a__length(mark(L))
   #100: #a__U114(tt(),L) -> #mark(L)
   #101: #a__U43(tt(),V1,V2) -> #a__U44(a__isNatIListKind(V2),V1,V2)
   #102: #a__U43(tt(),V1,V2) -> #a__isNatIListKind(V2)
   #103: #mark(U12(X1,X2)) -> #a__U12(mark(X1),X2)
   #104: #mark(U12(X1,X2)) -> #mark(X1)
   #105: #a__isNatIListKind(take(V1,V2)) -> #a__U61(a__isNatKind(V1),V2)
   #106: #a__isNatIListKind(take(V1,V2)) -> #a__isNatKind(V1)
   #107: #mark(U131(X1,X2,X3,X4)) -> #a__U131(mark(X1),X2,X3,X4)
   #108: #mark(U131(X1,X2,X3,X4)) -> #mark(X1)
   #109: #mark(U113(X1,X2,X3)) -> #a__U113(mark(X1),X2,X3)
   #110: #mark(U113(X1,X2,X3)) -> #mark(X1)
   #111: #mark(U62(X)) -> #a__U62(mark(X))
   #112: #mark(U62(X)) -> #mark(X)
   #113: #a__U121(tt(),IL) -> #a__U122(a__isNatIListKind(IL))
   #114: #a__U121(tt(),IL) -> #a__isNatIListKind(IL)
   #115: #mark(U45(X1,X2)) -> #a__U45(mark(X1),X2)
   #116: #mark(U45(X1,X2)) -> #mark(X1)
   #117: #a__isNatList(take(V1,V2)) -> #a__U101(a__isNatKind(V1),V1,V2)
   #118: #a__isNatList(take(V1,V2)) -> #a__isNatKind(V1)
   #119: #a__U42(tt(),V1,V2) -> #a__U43(a__isNatIListKind(V2),V1,V2)
   #120: #a__U42(tt(),V1,V2) -> #a__isNatIListKind(V2)
   #121: #a__isNatIList(cons(V1,V2)) -> #a__U41(a__isNatKind(V1),V1,V2)
   #122: #a__isNatIList(cons(V1,V2)) -> #a__isNatKind(V1)
   #123: #a__isNat(s(V1)) -> #a__U21(a__isNatKind(V1),V1)
   #124: #a__isNat(s(V1)) -> #a__isNatKind(V1)
   #125: #mark(U51(X1,X2)) -> #a__U51(mark(X1),X2)
   #126: #mark(U51(X1,X2)) -> #mark(X1)
   #127: #a__U134(tt(),IL,M,N) -> #a__U135(a__isNat(N),IL,M,N)
   #128: #a__U134(tt(),IL,M,N) -> #a__isNat(N)
   #129: #mark(U122(X)) -> #a__U122(mark(X))
   #130: #mark(U122(X)) -> #mark(X)
   #131: #a__U112(tt(),L,N) -> #a__U113(a__isNat(N),L,N)
   #132: #a__U112(tt(),L,N) -> #a__isNat(N)
   #133: #mark(U134(X1,X2,X3,X4)) -> #a__U134(mark(X1),X2,X3,X4)
   #134: #mark(U134(X1,X2,X3,X4)) -> #mark(X1)
   #135: #mark(U96(X)) -> #a__U96(mark(X))
   #136: #mark(U96(X)) -> #mark(X)
   #137: #mark(U135(X1,X2,X3,X4)) -> #a__U135(mark(X1),X2,X3,X4)
   #138: #mark(U135(X1,X2,X3,X4)) -> #mark(X1)
   #139: #a__length(cons(N,L)) -> #a__U111(a__isNatList(L),L,N)
   #140: #a__length(cons(N,L)) -> #a__isNatList(L)
   #141: #a__U45(tt(),V2) -> #a__U46(a__isNatIList(V2))
   #142: #a__U45(tt(),V2) -> #a__isNatIList(V2)
   #143: #mark(isNatIListKind(X)) -> #a__isNatIListKind(X)
   #144: #mark(cons(X1,X2)) -> #mark(X1)
   #145: #a__U104(tt(),V1,V2) -> #a__U105(a__isNat(V1),V2)
   #146: #a__U104(tt(),V1,V2) -> #a__isNat(V1)
   #147: #a__U94(tt(),V1,V2) -> #a__U95(a__isNat(V1),V2)
   #148: #a__U94(tt(),V1,V2) -> #a__isNat(V1)
   #149: #a__take(0(),IL) -> #a__U121(a__isNatIList(IL),IL)
   #150: #a__take(0(),IL) -> #a__isNatIList(IL)
   #151: #a__U136(tt(),IL,M,N) -> #mark(N)
   #152: #mark(length(X)) -> #a__length(mark(X))
   #153: #mark(length(X)) -> #mark(X)
   #154: #mark(U121(X1,X2)) -> #a__U121(mark(X1),X2)
   #155: #mark(U121(X1,X2)) -> #mark(X1)
   #156: #a__U32(tt(),V) -> #a__U33(a__isNatList(V))
   #157: #a__U32(tt(),V) -> #a__isNatList(V)
   #158: #mark(U94(X1,X2,X3)) -> #a__U94(mark(X1),X2,X3)
   #159: #mark(U94(X1,X2,X3)) -> #mark(X1)
   #160: #a__U131(tt(),IL,M,N) -> #a__U132(a__isNatIListKind(IL),IL,M,N)
   #161: #a__U131(tt(),IL,M,N) -> #a__isNatIListKind(IL)
   #162: #a__U44(tt(),V1,V2) -> #a__U45(a__isNat(V1),V2)
   #163: #a__U44(tt(),V1,V2) -> #a__isNat(V1)
   #164: #a__U133(tt(),IL,M,N) -> #a__U134(a__isNatKind(M),IL,M,N)
   #165: #a__U133(tt(),IL,M,N) -> #a__isNatKind(M)
   #166: #mark(U44(X1,X2,X3)) -> #a__U44(mark(X1),X2,X3)
   #167: #mark(U44(X1,X2,X3)) -> #mark(X1)
   #168: #a__U31(tt(),V) -> #a__U32(a__isNatIListKind(V),V)
   #169: #a__U31(tt(),V) -> #a__isNatIListKind(V)
   #170: #mark(U32(X1,X2)) -> #a__U32(mark(X1),X2)
   #171: #mark(U32(X1,X2)) -> #mark(X1)
   #172: #mark(U13(X)) -> #a__U13(mark(X))
   #173: #mark(U13(X)) -> #mark(X)
   #174: #mark(U101(X1,X2,X3)) -> #a__U101(mark(X1),X2,X3)
   #175: #mark(U101(X1,X2,X3)) -> #mark(X1)
   #176: #a__U135(tt(),IL,M,N) -> #a__U136(a__isNatKind(N),IL,M,N)
   #177: #a__U135(tt(),IL,M,N) -> #a__isNatKind(N)
   #178: #a__U102(tt(),V1,V2) -> #a__U103(a__isNatIListKind(V2),V1,V2)
   #179: #a__U102(tt(),V1,V2) -> #a__isNatIListKind(V2)
   #180: #mark(isNatIList(X)) -> #a__isNatIList(X)
   #181: #a__U11(tt(),V1) -> #a__U12(a__isNatIListKind(V1),V1)
   #182: #a__U11(tt(),V1) -> #a__isNatIListKind(V1)
   #183: #mark(U41(X1,X2,X3)) -> #a__U41(mark(X1),X2,X3)
   #184: #mark(U41(X1,X2,X3)) -> #mark(X1)
   #185: #mark(U42(X1,X2,X3)) -> #a__U42(mark(X1),X2,X3)
   #186: #mark(U42(X1,X2,X3)) -> #mark(X1)
   #187: #a__U103(tt(),V1,V2) -> #a__U104(a__isNatIListKind(V2),V1,V2)
   #188: #a__U103(tt(),V1,V2) -> #a__isNatIListKind(V2)
   #189: #mark(U43(X1,X2,X3)) -> #a__U43(mark(X1),X2,X3)
   #190: #mark(U43(X1,X2,X3)) -> #mark(X1)
   #191: #mark(U111(X1,X2,X3)) -> #a__U111(mark(X1),X2,X3)
   #192: #mark(U111(X1,X2,X3)) -> #mark(X1)
   #193: #a__isNatIList(V) -> #a__U31(a__isNatIListKind(V),V)
   #194: #a__isNatIList(V) -> #a__isNatIListKind(V)
   #195: #a__U132(tt(),IL,M,N) -> #a__U133(a__isNat(M),IL,M,N)
   #196: #a__U132(tt(),IL,M,N) -> #a__isNat(M)
Number of SCCs: 3, DPs: 113, edges: 3311
	SCC { #9 #24 #46 #56 #59 #60 #105 #106 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#a__U94(x1,x2,x3)	weight: 0
#a__isNatKind(x1)	weight: x1
isNatKind(x1)	weight: 0
#a__U131(x1,x2,x3,x4)	weight: 0
   U21(x1,x2)	weight: 0
a__U102(x1,x2,x3)	weight: 0
a__U45(x1,x2)	weight: 0
isNatList(x1)	weight: 0
#a__U71(x1)	weight: 0
   U11(x1,x2)	weight: 0
#a__U92(x1,x2,x3)	weight: 0
a__U104(x1,x2,x3)	weight: 0
  U136(x1,x2,x3,x4)	weight: 0
#a__U112(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
#a__U133(x1,x2,x3,x4)	weight: 0
  U105(x1,x2)	weight: 0
#a__U31(x1,x2)	weight: 0
a__U132(x1,x2,x3,x4)	weight: 0
#a__U33(x1)	weight: 0
#a__U93(x1,x2,x3)	weight: 0
a__U114(x1,x2)	weight: 0
a__isNatIList(x1)	weight: 0
a__U33(x1)	weight: 0
  U106(x1)	weight: 0
#a__isNatIListKind(x1)	weight: x1
#a__U23(x1)	weight: 0
a__U95(x1,x2)	weight: 0
   U42(x1,x2,x3)	weight: 0
   U91(x1,x2,x3)	weight: 0
#a__isNat(x1)	weight: 0
#a__U106(x1)	weight: 0
#a__U136(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: (/ 1 4) + x1 + x2
   U71(x1)	weight: 0
a__U62(x1)	weight: (/ 3 8)
a__U44(x1,x2,x3)	weight: 0
  U131(x1,x2,x3,x4)	weight: 0
isNatIList(x1)	weight: 0
  U135(x1,x2,x3,x4)	weight: 0
  U101(x1,x2,x3)	weight: 0
#a__U43(x1,x2,x3)	weight: 0
   U95(x1,x2)	weight: 0
  U111(x1,x2,x3)	weight: 0
  U132(x1,x2,x3,x4)	weight: 0
   U43(x1,x2,x3)	weight: 0
#a__U13(x1)	weight: 0
a__U121(x1,x2)	weight: 0
#a__U135(x1,x2,x3,x4)	weight: 0
#a__U44(x1,x2,x3)	weight: 0
  U103(x1,x2,x3)	weight: 0
a__U111(x1,x2,x3)	weight: 0
#a__U103(x1,x2,x3)	weight: 0
   U44(x1,x2,x3)	weight: 0
#a__U46(x1)	weight: 0
#a__U114(x1,x2)	weight: 0
#a__U51(x1,x2)	weight: (/ 1 8) + x1 + x2
   U23(x1)	weight: 0
a__U22(x1,x2)	weight: 0
   U93(x1,x2,x3)	weight: 0
a__U94(x1,x2,x3)	weight: 0
a__U106(x1)	weight: 0
#a__U11(x1,x2)	weight: 0
   U94(x1,x2,x3)	weight: 0
 zeros()	weight: 0
a__U31(x1,x2)	weight: 0
a__U51(x1,x2)	weight: (/ 1 4) + x2
a__U81(x1)	weight: 0
#a__take(x1,x2)	weight: 0
   U12(x1,x2)	weight: 0
a__isNatList(x1)	weight: 0
a__U43(x1,x2,x3)	weight: 0
#a__U62(x1)	weight: 0
a__U136(x1,x2,x3,x4)	weight: 0
#a__U42(x1,x2,x3)	weight: 0
a__U41(x1,x2,x3)	weight: 0
a__U134(x1,x2,x3,x4)	weight: 0
#a__U122(x1)	weight: 0
#a__U12(x1,x2)	weight: 0
  U104(x1,x2,x3)	weight: 0
a__U122(x1)	weight: 0
#a__U21(x1,x2)	weight: 0
#a__isNatIList(x1)	weight: 0
#a__U81(x1)	weight: 0
#a__U61(x1,x2)	weight: (/ 1 8) + x2
  U113(x1,x2,x3)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
#a__zeros()	weight: 0
#a__U113(x1,x2,x3)	weight: 0
  U134(x1,x2,x3,x4)	weight: 0
a__U21(x1,x2)	weight: 0
a__U32(x1,x2)	weight: 0
a__U91(x1,x2,x3)	weight: 0
#a__U111(x1,x2,x3)	weight: 0
   nil()	weight: 0
isNatIListKind(x1)	weight: (/ 1 4) + x1
  U114(x1,x2)	weight: 0
   U62(x1)	weight: (/ 1 2) + x1
#a__U52(x1)	weight: 0
#a__U102(x1,x2,x3)	weight: 0
   U45(x1,x2)	weight: 0
  mark(x1)	weight: 0
  U133(x1,x2,x3,x4)	weight: 0
#a__U101(x1,x2,x3)	weight: 0
a__U11(x1,x2)	weight: 0
   U32(x1,x2)	weight: 0
a__U42(x1,x2,x3)	weight: 0
a__U93(x1,x2,x3)	weight: 0
   U33(x1)	weight: 0
#a__U45(x1,x2)	weight: 0
a__U52(x1)	weight: (/ 3 8)
#a__U96(x1)	weight: 0
a__U135(x1,x2,x3,x4)	weight: 0
#a__length(x1)	weight: 0
#a__U105(x1,x2)	weight: 0
a__U12(x1,x2)	weight: 0
a__isNatIListKind(x1)	weight: (/ 1 8)
#a__U104(x1,x2,x3)	weight: 0
 isNat(x1)	weight: 0
   U46(x1)	weight: 0
#a__U121(x1,x2)	weight: 0
   U52(x1)	weight: (/ 1 2) + x1
   U61(x1,x2)	weight: (/ 3 8) + x1
a__U46(x1)	weight: 0
#a__U22(x1,x2)	weight: 0
a__U113(x1,x2,x3)	weight: 0
   U96(x1)	weight: 0
a__U13(x1)	weight: 0
   U31(x1,x2)	weight: 0
#a__isNatList(x1)	weight: 0
a__U71(x1)	weight: 0
   U92(x1,x2,x3)	weight: 0
  U112(x1,x2,x3)	weight: 0
  cons(x1,x2)	weight: (/ 3 8) + x1 + x2
a__U92(x1,x2,x3)	weight: 0
a__U61(x1,x2)	weight: (/ 1 4) + x2
  U102(x1,x2,x3)	weight: 0
a__U105(x1,x2)	weight: 0
a__take(x1,x2)	weight: 0
   U81(x1)	weight: 0
#a__U95(x1,x2)	weight: 0
#a__U41(x1,x2,x3)	weight: 0
    tt()	weight: 0
a__U131(x1,x2,x3,x4)	weight: 0
a__isNat(x1)	weight: 0
   U13(x1)	weight: 0
a__U133(x1,x2,x3,x4)	weight: 0
a__U23(x1)	weight: 0
a__U96(x1)	weight: 0
a__isNatKind(x1)	weight: (/ 1 8)
#a__U134(x1,x2,x3,x4)	weight: 0
   U22(x1,x2)	weight: 0
   U51(x1,x2)	weight: (/ 3 8) + x1
#a__U132(x1,x2,x3,x4)	weight: 0
a__U103(x1,x2,x3)	weight: 0
length(x1)	weight: (/ 1 8) + x1
a__U112(x1,x2,x3)	weight: 0
   U41(x1,x2,x3)	weight: 0
#a__U32(x1,x2)	weight: 0
a__zeros()	weight: 0
a__U101(x1,x2,x3)	weight: 0
#a__U91(x1,x2,x3)	weight: 0
  U121(x1,x2)	weight: 0
a__length(x1)	weight: 0
  U122(x1)	weight: 0
    Usable rules: { 39 40 57..59 128 170 171 }
    Removed DPs: #9 #24 #46 #56 #59 #60 #105 #106
Number of SCCs: 2, DPs: 105, edges: 3291
	SCC { #1 #4 #6 #14 #21 #37 #49 #54 #67 #81 #83 #92 #101 #117 #119 #121 #123 #142 #145..148 #157 #162 #163 #168 #178 #181 #187 #193 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#a__U94(x1,x2,x3)	weight: x2 + x3
#a__isNatKind(x1)	weight: 0
isNatKind(x1)	weight: 0
#a__U131(x1,x2,x3,x4)	weight: 0
   U21(x1,x2)	weight: (/ 3 16) + x1 + x2
a__U102(x1,x2,x3)	weight: (/ 3 16) + x2
a__U45(x1,x2)	weight: (/ 3 8)
isNatList(x1)	weight: (/ 1 8) + x1
#a__U71(x1)	weight: 0
   U11(x1,x2)	weight: (/ 1 8) + x2
#a__U92(x1,x2,x3)	weight: x2 + x3
a__U104(x1,x2,x3)	weight: (/ 3 16) + x1
  U136(x1,x2,x3,x4)	weight: 0
#a__U112(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 3 16) + x1
#a__U133(x1,x2,x3,x4)	weight: 0
  U105(x1,x2)	weight: (/ 5 16) + x1
#a__U31(x1,x2)	weight: x2
a__U132(x1,x2,x3,x4)	weight: 0
#a__U33(x1)	weight: 0
#a__U93(x1,x2,x3)	weight: x2 + x3
a__U114(x1,x2)	weight: 0
a__isNatIList(x1)	weight: (/ 1 16) + x1
a__U33(x1)	weight: (/ 1 8)
  U106(x1)	weight: (/ 3 8) + x1
#a__isNatIListKind(x1)	weight: 0
#a__U23(x1)	weight: 0
a__U95(x1,x2)	weight: (/ 3 8) + x2
   U42(x1,x2,x3)	weight: (/ 1 4) + x1
   U91(x1,x2,x3)	weight: (/ 3 16) + x1 + x2
#a__isNat(x1)	weight: x1
#a__U106(x1)	weight: 0
#a__U136(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: x1 + x2
   U71(x1)	weight: 0
a__U62(x1)	weight: (/ 3 16)
a__U44(x1,x2,x3)	weight: (/ 5 16)
  U131(x1,x2,x3,x4)	weight: 0
isNatIList(x1)	weight: (/ 1 8)
  U135(x1,x2,x3,x4)	weight: 0
  U101(x1,x2,x3)	weight: (/ 3 16) + x1 + x2 + x3
#a__U43(x1,x2,x3)	weight: x2 + x3
   U95(x1,x2)	weight: (/ 7 16)
  U111(x1,x2,x3)	weight: 0
  U132(x1,x2,x3,x4)	weight: 0
   U43(x1,x2,x3)	weight: (/ 5 16) + x1 + x3
#a__U13(x1)	weight: 0
a__U121(x1,x2)	weight: 0
#a__U135(x1,x2,x3,x4)	weight: 0
#a__U44(x1,x2,x3)	weight: x2 + x3
  U103(x1,x2,x3)	weight: (/ 1 4) + x2 + x3
a__U111(x1,x2,x3)	weight: 0
#a__U103(x1,x2,x3)	weight: x2 + x3
   U44(x1,x2,x3)	weight: (/ 3 8) + x1 + x2
#a__U46(x1)	weight: 0
#a__U114(x1,x2)	weight: 0
#a__U51(x1,x2)	weight: (/ 1 16) + x1
   U23(x1)	weight: (/ 5 16) + x1
a__U22(x1,x2)	weight: (/ 3 16) + x2
   U93(x1,x2,x3)	weight: (/ 5 16) + x1 + x2 + x3
a__U94(x1,x2,x3)	weight: (/ 5 16) + x3
a__U106(x1)	weight: (/ 5 16)
#a__U11(x1,x2)	weight: x2
   U94(x1,x2,x3)	weight: (/ 3 8) + x2
 zeros()	weight: 0
a__U31(x1,x2)	weight: (/ 1 16) + x1
a__U51(x1,x2)	weight: (/ 1 8)
a__U81(x1)	weight: 0
#a__take(x1,x2)	weight: 0
   U12(x1,x2)	weight: (/ 3 16) + x1
a__isNatList(x1)	weight: (/ 1 16)
a__U43(x1,x2,x3)	weight: (/ 1 4)
#a__U62(x1)	weight: 0
a__U136(x1,x2,x3,x4)	weight: 0
#a__U42(x1,x2,x3)	weight: x2 + x3
a__U41(x1,x2,x3)	weight: (/ 1 8)
a__U134(x1,x2,x3,x4)	weight: 0
#a__U122(x1)	weight: 0
#a__U12(x1,x2)	weight: x2
  U104(x1,x2,x3)	weight: (/ 1 4) + x3
a__U122(x1)	weight: 0
#a__U21(x1,x2)	weight: (/ 1 8) + x2
#a__isNatIList(x1)	weight: x1
#a__U81(x1)	weight: 0
#a__U61(x1,x2)	weight: (/ 1 16)
  U113(x1,x2,x3)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
#a__zeros()	weight: 0
#a__U113(x1,x2,x3)	weight: 0
  U134(x1,x2,x3,x4)	weight: 0
a__U21(x1,x2)	weight: (/ 1 8)
a__U32(x1,x2)	weight: (/ 1 16) + x1
a__U91(x1,x2,x3)	weight: (/ 1 8)
#a__U111(x1,x2,x3)	weight: 0
   nil()	weight: 0
isNatIListKind(x1)	weight: (/ 1 8) + x1
  U114(x1,x2)	weight: 0
   U62(x1)	weight: (/ 1 4)
#a__U52(x1)	weight: 0
#a__U102(x1,x2,x3)	weight: x2 + x3
   U45(x1,x2)	weight: (/ 7 16) + x1 + x2
  mark(x1)	weight: 0
  U133(x1,x2,x3,x4)	weight: 0
#a__U101(x1,x2,x3)	weight: x2 + x3
a__U11(x1,x2)	weight: (/ 1 16) + x1
   U32(x1,x2)	weight: (/ 1 8)
a__U42(x1,x2,x3)	weight: (/ 3 16) + x2 + x3
a__U93(x1,x2,x3)	weight: (/ 1 4)
   U33(x1)	weight: (/ 3 16) + x1
#a__U45(x1,x2)	weight: x2
a__U52(x1)	weight: (/ 3 16)
#a__U96(x1)	weight: 0
a__U135(x1,x2,x3,x4)	weight: 0
#a__length(x1)	weight: 0
#a__U105(x1,x2)	weight: x2
a__U12(x1,x2)	weight: (/ 1 8) + x2
a__isNatIListKind(x1)	weight: (/ 1 16)
#a__U104(x1,x2,x3)	weight: x2 + x3
 isNat(x1)	weight: (/ 1 8) + x1
   U46(x1)	weight: (/ 7 16)
#a__U121(x1,x2)	weight: 0
   U52(x1)	weight: (/ 1 4) + x1
   U61(x1,x2)	weight: (/ 3 16) + x1 + x2
a__U46(x1)	weight: (/ 3 8) + x1
#a__U22(x1,x2)	weight: (/ 1 16) + x2
a__U113(x1,x2,x3)	weight: 0
   U96(x1)	weight: (/ 1 2) + x1
a__U13(x1)	weight: (/ 3 16)
   U31(x1,x2)	weight: (/ 1 8) + x2
#a__isNatList(x1)	weight: x1
a__U71(x1)	weight: 0
   U92(x1,x2,x3)	weight: (/ 1 4) + x1
  U112(x1,x2,x3)	weight: 0
  cons(x1,x2)	weight: x1 + x2
a__U92(x1,x2,x3)	weight: (/ 3 16) + x2
a__U61(x1,x2)	weight: (/ 1 8)
  U102(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
a__U105(x1,x2)	weight: (/ 1 4) + x2
a__take(x1,x2)	weight: 0
   U81(x1)	weight: 0
#a__U95(x1,x2)	weight: x2
#a__U41(x1,x2,x3)	weight: x2 + x3
    tt()	weight: 0
a__U131(x1,x2,x3,x4)	weight: 0
a__isNat(x1)	weight: (/ 1 16)
   U13(x1)	weight: (/ 1 4) + x1
a__U133(x1,x2,x3,x4)	weight: 0
a__U23(x1)	weight: (/ 1 4)
a__U96(x1)	weight: (/ 7 16)
a__isNatKind(x1)	weight: (/ 1 16)
#a__U134(x1,x2,x3,x4)	weight: 0
   U22(x1,x2)	weight: (/ 1 4) + x1
   U51(x1,x2)	weight: (/ 3 16) + x1
#a__U132(x1,x2,x3,x4)	weight: 0
a__U103(x1,x2,x3)	weight: (/ 3 16) + x1
length(x1)	weight: x1
a__U112(x1,x2,x3)	weight: 0
   U41(x1,x2,x3)	weight: (/ 3 16) + x3
#a__U32(x1,x2)	weight: x2
a__zeros()	weight: 0
a__U101(x1,x2,x3)	weight: (/ 1 8)
#a__U91(x1,x2,x3)	weight: x2 + x3
  U121(x1,x2)	weight: 0
a__length(x1)	weight: 0
  U122(x1)	weight: 0
    Usable rules: { 39 40 57..59 128 170 171 }
    Removed DPs: #81 #83 #123
Number of SCCs: 2, DPs: 102, edges: 3284
	SCC { #1 #4 #6 #14 #21 #37 #49 #54 #67 #92 #101 #117 #119 #121 #142 #145..148 #157 #162 #163 #168 #178 #181 #187 #193 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#a__U94(x1,x2,x3)	weight: x1 + x2 + x3
#a__isNatKind(x1)	weight: 0
isNatKind(x1)	weight: 0
#a__U131(x1,x2,x3,x4)	weight: 0
   U21(x1,x2)	weight: (/ 3 16) + x1 + x2
a__U102(x1,x2,x3)	weight: (/ 3 16) + x2
a__U45(x1,x2)	weight: (/ 3 4)
isNatList(x1)	weight: (/ 1 8) + x1
#a__U71(x1)	weight: 0
   U11(x1,x2)	weight: (/ 3 16) + x1 + x2
#a__U92(x1,x2,x3)	weight: (/ 3 8) + x2 + x3
a__U104(x1,x2,x3)	weight: x1
  U136(x1,x2,x3,x4)	weight: 0
#a__U112(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 3 16) + x1
#a__U133(x1,x2,x3,x4)	weight: 0
  U105(x1,x2)	weight: (/ 1 8) + x1
#a__U31(x1,x2)	weight: x2
a__U132(x1,x2,x3,x4)	weight: 0
#a__U33(x1)	weight: 0
#a__U93(x1,x2,x3)	weight: (/ 3 8) + x2 + x3
a__U114(x1,x2)	weight: 0
a__isNatIList(x1)	weight: (/ 1 16) + x1
a__U33(x1)	weight: (/ 1 16)
  U106(x1)	weight: (/ 3 16) + x1
#a__isNatIListKind(x1)	weight: 0
#a__U23(x1)	weight: 0
a__U95(x1,x2)	weight: (/ 5 16) + x1 + x2
   U42(x1,x2,x3)	weight: (/ 5 8) + x1
   U91(x1,x2,x3)	weight: (/ 3 16) + x1 + x2
#a__isNat(x1)	weight: x1
#a__U106(x1)	weight: 0
#a__U136(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: x1 + x2
   U71(x1)	weight: 0
a__U62(x1)	weight: (/ 3 8)
a__U44(x1,x2,x3)	weight: (/ 11 16)
  U131(x1,x2,x3,x4)	weight: 0
isNatIList(x1)	weight: (/ 1 8)
  U135(x1,x2,x3,x4)	weight: 0
  U101(x1,x2,x3)	weight: (/ 3 16) + x1 + x2 + x3
#a__U43(x1,x2,x3)	weight: (/ 3 16) + x2 + x3
   U95(x1,x2)	weight: (/ 3 8)
  U111(x1,x2,x3)	weight: 0
  U132(x1,x2,x3,x4)	weight: 0
   U43(x1,x2,x3)	weight: (/ 11 16) + x1 + x3
#a__U13(x1)	weight: 0
a__U121(x1,x2)	weight: 0
#a__U135(x1,x2,x3,x4)	weight: 0
#a__U44(x1,x2,x3)	weight: (/ 1 8) + x2 + x3
  U103(x1,x2,x3)	weight: (/ 1 16) + x2 + x3
a__U111(x1,x2,x3)	weight: 0
#a__U103(x1,x2,x3)	weight: x2 + x3
   U44(x1,x2,x3)	weight: (/ 3 4) + x1 + x2
#a__U46(x1)	weight: 0
#a__U114(x1,x2)	weight: 0
#a__U51(x1,x2)	weight: (/ 1 16) + x1
   U23(x1)	weight: (/ 5 16) + x1
a__U22(x1,x2)	weight: (/ 3 16)
   U93(x1,x2,x3)	weight: (/ 5 16) + x1 + x2 + x3
a__U94(x1,x2,x3)	weight: (/ 5 16) + x3
a__U106(x1)	weight: (/ 1 8)
#a__U11(x1,x2)	weight: x2
   U94(x1,x2,x3)	weight: (/ 3 8) + x2
 zeros()	weight: 0
a__U31(x1,x2)	weight: x1
a__U51(x1,x2)	weight: (/ 3 8)
a__U81(x1)	weight: 0
#a__take(x1,x2)	weight: 0
   U12(x1,x2)	weight: (/ 1 4)
a__isNatList(x1)	weight: (/ 1 16)
a__U43(x1,x2,x3)	weight: (/ 5 8)
#a__U62(x1)	weight: 0
a__U136(x1,x2,x3,x4)	weight: 0
#a__U42(x1,x2,x3)	weight: (/ 1 4) + x2 + x3
a__U41(x1,x2,x3)	weight: (/ 1 2)
a__U134(x1,x2,x3,x4)	weight: 0
#a__U122(x1)	weight: 0
#a__U12(x1,x2)	weight: x2
  U104(x1,x2,x3)	weight: (/ 1 16) + x3
a__U122(x1)	weight: 0
#a__U21(x1,x2)	weight: (/ 1 8)
#a__isNatIList(x1)	weight: x1
#a__U81(x1)	weight: 0
#a__U61(x1,x2)	weight: (/ 1 16)
  U113(x1,x2,x3)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
#a__zeros()	weight: 0
#a__U113(x1,x2,x3)	weight: 0
  U134(x1,x2,x3,x4)	weight: 0
a__U21(x1,x2)	weight: (/ 1 8)
a__U32(x1,x2)	weight: x1
a__U91(x1,x2,x3)	weight: (/ 1 8)
#a__U111(x1,x2,x3)	weight: 0
   nil()	weight: 0
isNatIListKind(x1)	weight: (/ 3 8)
  U114(x1,x2)	weight: 0
   U62(x1)	weight: (/ 3 8)
#a__U52(x1)	weight: 0
#a__U102(x1,x2,x3)	weight: x2 + x3
   U45(x1,x2)	weight: (/ 13 16) + x1 + x2
  mark(x1)	weight: 0
  U133(x1,x2,x3,x4)	weight: 0
#a__U101(x1,x2,x3)	weight: x2 + x3
a__U11(x1,x2)	weight: (/ 1 8)
   U32(x1,x2)	weight: (/ 1 16)
a__U42(x1,x2,x3)	weight: (/ 9 16) + x2 + x3
a__U93(x1,x2,x3)	weight: (/ 1 4)
   U33(x1)	weight: (/ 1 8) + x1
#a__U45(x1,x2)	weight: (/ 1 16) + x2
a__U52(x1)	weight: (/ 3 8)
#a__U96(x1)	weight: 0
a__U135(x1,x2,x3,x4)	weight: 0
#a__length(x1)	weight: 0
#a__U105(x1,x2)	weight: x2
a__U12(x1,x2)	weight: (/ 3 16) + x2
a__isNatIListKind(x1)	weight: (/ 3 8)
#a__U104(x1,x2,x3)	weight: x2 + x3
 isNat(x1)	weight: (/ 1 8) + x1
   U46(x1)	weight: (/ 13 16)
#a__U121(x1,x2)	weight: 0
   U52(x1)	weight: (/ 3 8)
   U61(x1,x2)	weight: (/ 3 8)
a__U46(x1)	weight: (/ 3 4) + x1
#a__U22(x1,x2)	weight: (/ 1 16)
a__U113(x1,x2,x3)	weight: 0
   U96(x1)	weight: (/ 7 16) + x1
a__U13(x1)	weight: (/ 1 4)
   U31(x1,x2)	weight: (/ 1 16) + x2
#a__isNatList(x1)	weight: x1
a__U71(x1)	weight: 0
   U92(x1,x2,x3)	weight: (/ 1 4) + x1
  U112(x1,x2,x3)	weight: 0
  cons(x1,x2)	weight: (/ 3 8) + x1 + x2
a__U92(x1,x2,x3)	weight: (/ 3 16) + x2
a__U61(x1,x2)	weight: (/ 3 8)
  U102(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
a__U105(x1,x2)	weight: (/ 1 16) + x2
a__take(x1,x2)	weight: 0
   U81(x1)	weight: 0
#a__U95(x1,x2)	weight: x2
#a__U41(x1,x2,x3)	weight: (/ 5 16) + x2 + x3
    tt()	weight: 0
a__U131(x1,x2,x3,x4)	weight: 0
a__isNat(x1)	weight: (/ 1 16)
   U13(x1)	weight: (/ 5 16) + x1
a__U133(x1,x2,x3,x4)	weight: 0
a__U23(x1)	weight: (/ 1 4)
a__U96(x1)	weight: (/ 3 8)
a__isNatKind(x1)	weight: (/ 1 16)
#a__U134(x1,x2,x3,x4)	weight: 0
   U22(x1,x2)	weight: (/ 1 4) + x1 + x2
   U51(x1,x2)	weight: (/ 3 8)
#a__U132(x1,x2,x3,x4)	weight: 0
a__U103(x1,x2,x3)	weight: x1
length(x1)	weight: x1
a__U112(x1,x2,x3)	weight: 0
   U41(x1,x2,x3)	weight: (/ 9 16) + x3
#a__U32(x1,x2)	weight: x2
a__zeros()	weight: 0
a__U101(x1,x2,x3)	weight: (/ 1 8)
#a__U91(x1,x2,x3)	weight: (/ 3 8) + x2 + x3
  U121(x1,x2)	weight: 0
a__length(x1)	weight: 0
  U122(x1)	weight: 0
    Usable rules: { 35..40 53..59 128 130 166..171 }
    Removed DPs: #6 #101 #119 #121 #142 #162 #163
Number of SCCs: 2, DPs: 95, edges: 3274
	SCC { #1 #4 #14 #21 #37 #49 #54 #67 #92 #117 #145..148 #157 #168 #178 #181 #187 #193 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#a__U94(x1,x2,x3)	weight: (/ 1 8) + x1 + x2 + x3
#a__isNatKind(x1)	weight: 0
isNatKind(x1)	weight: 0
#a__U131(x1,x2,x3,x4)	weight: 0
   U21(x1,x2)	weight: (/ 3 32) + x1 + x2
a__U102(x1,x2,x3)	weight: (/ 3 32) + x2
a__U45(x1,x2)	weight: (/ 5 8)
isNatList(x1)	weight: (/ 1 16) + x1
#a__U71(x1)	weight: 0
   U11(x1,x2)	weight: (/ 3 32) + x1 + x2
#a__U92(x1,x2,x3)	weight: (/ 3 8) + x2 + x3
a__U104(x1,x2,x3)	weight: x1
  U136(x1,x2,x3,x4)	weight: 0
#a__U112(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 3 32) + x1
#a__U133(x1,x2,x3,x4)	weight: 0
  U105(x1,x2)	weight: (/ 1 16) + x1
#a__U31(x1,x2)	weight: (/ 1 16) + x2
a__U132(x1,x2,x3,x4)	weight: 0
#a__U33(x1)	weight: 0
#a__U93(x1,x2,x3)	weight: (/ 11 32) + x2 + x3
a__U114(x1,x2)	weight: 0
a__isNatIList(x1)	weight: (/ 1 32) + x1
a__U33(x1)	weight: (/ 1 32)
  U106(x1)	weight: (/ 3 32) + x1
#a__isNatIListKind(x1)	weight: 0
#a__U23(x1)	weight: 0
a__U95(x1,x2)	weight: (/ 5 32) + x1 + x2
   U42(x1,x2,x3)	weight: (/ 9 16) + x1
   U91(x1,x2,x3)	weight: (/ 3 32) + x1 + x2
#a__isNat(x1)	weight: (/ 3 32) + x1
#a__U106(x1)	weight: 0
#a__U136(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: (/ 9 32) + x1 + x2
   U71(x1)	weight: 0
a__U62(x1)	weight: (/ 3 16)
a__U44(x1,x2,x3)	weight: (/ 19 32)
  U131(x1,x2,x3,x4)	weight: 0
isNatIList(x1)	weight: (/ 1 16)
  U135(x1,x2,x3,x4)	weight: 0
  U101(x1,x2,x3)	weight: (/ 3 32) + x1 + x2 + x3
#a__U43(x1,x2,x3)	weight: (/ 3 32)
   U95(x1,x2)	weight: (/ 3 16)
  U111(x1,x2,x3)	weight: 0
  U132(x1,x2,x3,x4)	weight: 0
   U43(x1,x2,x3)	weight: (/ 19 32) + x1 + x3
#a__U13(x1)	weight: 0
a__U121(x1,x2)	weight: 0
#a__U135(x1,x2,x3,x4)	weight: 0
#a__U44(x1,x2,x3)	weight: (/ 1 16)
  U103(x1,x2,x3)	weight: (/ 1 32) + x2 + x3
a__U111(x1,x2,x3)	weight: 0
#a__U103(x1,x2,x3)	weight: (/ 3 16) + x2 + x3
   U44(x1,x2,x3)	weight: (/ 5 8) + x1 + x2
#a__U46(x1)	weight: 0
#a__U114(x1,x2)	weight: 0
#a__U51(x1,x2)	weight: (/ 1 32) + x1
   U23(x1)	weight: (/ 5 32) + x1
a__U22(x1,x2)	weight: (/ 3 32)
   U93(x1,x2,x3)	weight: (/ 5 32) + x1 + x2 + x3
a__U94(x1,x2,x3)	weight: (/ 5 32) + x3
a__U106(x1)	weight: (/ 1 16)
#a__U11(x1,x2)	weight: (/ 1 16) + x2
   U94(x1,x2,x3)	weight: (/ 3 16) + x2
 zeros()	weight: 0
a__U31(x1,x2)	weight: x1
a__U51(x1,x2)	weight: (/ 3 16)
a__U81(x1)	weight: 0
#a__take(x1,x2)	weight: 0
   U12(x1,x2)	weight: (/ 1 8)
a__isNatList(x1)	weight: (/ 1 32)
a__U43(x1,x2,x3)	weight: (/ 9 16)
#a__U62(x1)	weight: 0
a__U136(x1,x2,x3,x4)	weight: 0
#a__U42(x1,x2,x3)	weight: (/ 1 8)
a__U41(x1,x2,x3)	weight: (/ 1 2)
a__U134(x1,x2,x3,x4)	weight: 0
#a__U122(x1)	weight: 0
#a__U12(x1,x2)	weight: (/ 1 32) + x2
  U104(x1,x2,x3)	weight: (/ 1 32) + x3
a__U122(x1)	weight: 0
#a__U21(x1,x2)	weight: (/ 1 16)
#a__isNatIList(x1)	weight: (/ 3 32) + x1
#a__U81(x1)	weight: 0
#a__U61(x1,x2)	weight: (/ 1 32)
  U113(x1,x2,x3)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
#a__zeros()	weight: 0
#a__U113(x1,x2,x3)	weight: 0
  U134(x1,x2,x3,x4)	weight: 0
a__U21(x1,x2)	weight: (/ 1 16)
a__U32(x1,x2)	weight: x1
a__U91(x1,x2,x3)	weight: (/ 1 16)
#a__U111(x1,x2,x3)	weight: 0
   nil()	weight: 0
isNatIListKind(x1)	weight: (/ 3 16)
  U114(x1,x2)	weight: 0
   U62(x1)	weight: (/ 3 16)
#a__U52(x1)	weight: 0
#a__U102(x1,x2,x3)	weight: (/ 7 32) + x2 + x3
   U45(x1,x2)	weight: (/ 21 32) + x1 + x2
  mark(x1)	weight: 0
  U133(x1,x2,x3,x4)	weight: 0
#a__U101(x1,x2,x3)	weight: (/ 1 4) + x2 + x3
a__U11(x1,x2)	weight: (/ 1 16)
   U32(x1,x2)	weight: (/ 1 32)
a__U42(x1,x2,x3)	weight: (/ 17 32) + x2 + x3
a__U93(x1,x2,x3)	weight: (/ 1 8)
   U33(x1)	weight: (/ 1 16) + x1
#a__U45(x1,x2)	weight: (/ 1 32)
a__U52(x1)	weight: (/ 3 16)
#a__U96(x1)	weight: 0
a__U135(x1,x2,x3,x4)	weight: 0
#a__length(x1)	weight: 0
#a__U105(x1,x2)	weight: (/ 1 8) + x2
a__U12(x1,x2)	weight: (/ 3 32) + x2
a__isNatIListKind(x1)	weight: (/ 3 16)
#a__U104(x1,x2,x3)	weight: (/ 5 32) + x2 + x3
 isNat(x1)	weight: (/ 1 16) + x1
   U46(x1)	weight: (/ 21 32)
#a__U121(x1,x2)	weight: 0
   U52(x1)	weight: (/ 3 16)
   U61(x1,x2)	weight: (/ 3 16)
a__U46(x1)	weight: (/ 5 8) + x1
#a__U22(x1,x2)	weight: (/ 1 32)
a__U113(x1,x2,x3)	weight: 0
   U96(x1)	weight: (/ 7 32) + x1
a__U13(x1)	weight: (/ 1 8)
   U31(x1,x2)	weight: (/ 1 32) + x2
#a__isNatList(x1)	weight: x1
a__U71(x1)	weight: 0
   U92(x1,x2,x3)	weight: (/ 1 8) + x1
  U112(x1,x2,x3)	weight: 0
  cons(x1,x2)	weight: (/ 7 16) + x1 + x2
a__U92(x1,x2,x3)	weight: (/ 3 32) + x2
a__U61(x1,x2)	weight: (/ 3 16)
  U102(x1,x2,x3)	weight: (/ 1 8) + x1 + x2 + x3
a__U105(x1,x2)	weight: (/ 1 32) + x2
a__take(x1,x2)	weight: 0
   U81(x1)	weight: 0
#a__U95(x1,x2)	weight: (/ 1 32) + x2
#a__U41(x1,x2,x3)	weight: (/ 5 32)
    tt()	weight: 0
a__U131(x1,x2,x3,x4)	weight: 0
a__isNat(x1)	weight: (/ 1 32)
   U13(x1)	weight: (/ 5 32) + x1
a__U133(x1,x2,x3,x4)	weight: 0
a__U23(x1)	weight: (/ 1 8)
a__U96(x1)	weight: (/ 3 16)
a__isNatKind(x1)	weight: (/ 1 32)
#a__U134(x1,x2,x3,x4)	weight: 0
   U22(x1,x2)	weight: (/ 1 8) + x1 + x2
   U51(x1,x2)	weight: (/ 3 16)
#a__U132(x1,x2,x3,x4)	weight: 0
a__U103(x1,x2,x3)	weight: x1
length(x1)	weight: x1
a__U112(x1,x2,x3)	weight: 0
   U41(x1,x2,x3)	weight: (/ 17 32) + x3
#a__U32(x1,x2)	weight: (/ 1 32) + x2
a__zeros()	weight: 0
a__U101(x1,x2,x3)	weight: (/ 1 16)
#a__U91(x1,x2,x3)	weight: (/ 13 32) + x2 + x3
  U121(x1,x2)	weight: 0
a__length(x1)	weight: 0
  U122(x1)	weight: 0
    Usable rules: { 35..40 53..59 128 130 166..171 }
    Removed DPs: #1 #4 #14 #21 #37 #49 #54 #67 #92 #117 #145..148 #157 #168 #178 #181 #187 #193
Number of SCCs: 1, DPs: 75, edges: 3249
	SCC { #10..12 #17..20 #26 #28 #30..32 #34 #36 #39 #42 #44 #48 #52 #58 #62 #63 #65 #68 #70 #73 #75 #77..79 #85 #86 #88 #90 #94 #96 #98..100 #104 #107..110 #112 #116 #126 #127 #130 #131 #133 #134 #136..139 #144 #151..153 #155 #159 #160 #164 #167 #171 #173 #175 #176 #184 #186 #190..192 #195 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#a__U94(x1,x2,x3)	weight: (/ 1 4)
#a__isNatKind(x1)	weight: 0
isNatKind(x1)	weight: 0
#a__U131(x1,x2,x3,x4)	weight: (/ 3 8) + x4
   U21(x1,x2)	weight: x1
a__U102(x1,x2,x3)	weight: x1
a__U45(x1,x2)	weight: x1
isNatList(x1)	weight: 0
#a__U71(x1)	weight: 0
   U11(x1,x2)	weight: x1
#a__U92(x1,x2,x3)	weight: (/ 3 4)
a__U104(x1,x2,x3)	weight: x1
  U136(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
#a__U112(x1,x2,x3)	weight: (/ 1 16) + x2
     s(x1)	weight: x1
#a__U133(x1,x2,x3,x4)	weight: (/ 1 4) + x4
  U105(x1,x2)	weight: x1
#a__U31(x1,x2)	weight: (/ 1 8)
a__U132(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
#a__U33(x1)	weight: 0
#a__U93(x1,x2,x3)	weight: (/ 11 16)
a__U114(x1,x2)	weight: (/ 1 8) + x1 + x2
a__isNatIList(x1)	weight: 0
a__U33(x1)	weight: x1
  U106(x1)	weight: x1
#a__isNatIListKind(x1)	weight: 0
#a__U23(x1)	weight: 0
a__U95(x1,x2)	weight: x1
   U42(x1,x2,x3)	weight: x1
   U91(x1,x2,x3)	weight: x1
#a__isNat(x1)	weight: (/ 3 16)
#a__U106(x1)	weight: 0
#a__U136(x1,x2,x3,x4)	weight: (/ 1 16) + x4
  take(x1,x2)	weight: (/ 1 2) + x1 + x2
   U71(x1)	weight: x1
a__U62(x1)	weight: x1
a__U44(x1,x2,x3)	weight: x1
  U131(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
isNatIList(x1)	weight: 0
  U135(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
  U101(x1,x2,x3)	weight: x1
#a__U43(x1,x2,x3)	weight: (/ 3 16)
   U95(x1,x2)	weight: x1
  U111(x1,x2,x3)	weight: (/ 1 8) + x1 + x2
  U132(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
   U43(x1,x2,x3)	weight: x1
#a__U13(x1)	weight: 0
a__U121(x1,x2)	weight: (/ 1 16) + x1
#a__U135(x1,x2,x3,x4)	weight: (/ 1 8) + x4
#a__U44(x1,x2,x3)	weight: (/ 1 8)
  U103(x1,x2,x3)	weight: x1
a__U111(x1,x2,x3)	weight: (/ 1 8) + x1 + x2
#a__U103(x1,x2,x3)	weight: (/ 3 8)
   U44(x1,x2,x3)	weight: x1
#a__U46(x1)	weight: 0
#a__U114(x1,x2)	weight: (/ 1 16) + x2
#a__U51(x1,x2)	weight: (/ 1 16) + x1
   U23(x1)	weight: x1
a__U22(x1,x2)	weight: x1
   U93(x1,x2,x3)	weight: x1
a__U94(x1,x2,x3)	weight: x1
a__U106(x1)	weight: x1
#a__U11(x1,x2)	weight: (/ 1 8)
   U94(x1,x2,x3)	weight: x1
 zeros()	weight: 0
a__U31(x1,x2)	weight: x1
a__U51(x1,x2)	weight: x1
a__U81(x1)	weight: x1
#a__take(x1,x2)	weight: (/ 7 16) + x2
   U12(x1,x2)	weight: x1
a__isNatList(x1)	weight: 0
a__U43(x1,x2,x3)	weight: x1
#a__U62(x1)	weight: 0
a__U136(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
#a__U42(x1,x2,x3)	weight: (/ 1 4)
a__U41(x1,x2,x3)	weight: x1
a__U134(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
#a__U122(x1)	weight: 0
#a__U12(x1,x2)	weight: (/ 1 16)
  U104(x1,x2,x3)	weight: x1
a__U122(x1)	weight: (/ 1 16) + x1
#a__U21(x1,x2)	weight: (/ 1 8)
#a__isNatIList(x1)	weight: (/ 3 16)
#a__U81(x1)	weight: 0
#a__U61(x1,x2)	weight: (/ 1 16)
  U113(x1,x2,x3)	weight: (/ 1 8) + x1 + x2
#mark(x1)	weight: x1
     0()	weight: 0
#a__zeros()	weight: 0
#a__U113(x1,x2,x3)	weight: (/ 1 16) + x2
  U134(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
a__U21(x1,x2)	weight: x1
a__U32(x1,x2)	weight: x1
a__U91(x1,x2,x3)	weight: x1
#a__U111(x1,x2,x3)	weight: (/ 1 16) + x2
   nil()	weight: 0
isNatIListKind(x1)	weight: 0
  U114(x1,x2)	weight: (/ 1 8) + x1 + x2
   U62(x1)	weight: x1
#a__U52(x1)	weight: 0
#a__U102(x1,x2,x3)	weight: (/ 7 16)
   U45(x1,x2)	weight: x1
  mark(x1)	weight: x1
  U133(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
#a__U101(x1,x2,x3)	weight: (/ 1 2)
a__U11(x1,x2)	weight: x1
   U32(x1,x2)	weight: x1
a__U42(x1,x2,x3)	weight: x1
a__U93(x1,x2,x3)	weight: x1
   U33(x1)	weight: x1
#a__U45(x1,x2)	weight: (/ 1 16)
a__U52(x1)	weight: x1
#a__U96(x1)	weight: 0
a__U135(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
#a__length(x1)	weight: (/ 1 16) + x1
#a__U105(x1,x2)	weight: (/ 1 4)
a__U12(x1,x2)	weight: x1
a__isNatIListKind(x1)	weight: 0
#a__U104(x1,x2,x3)	weight: (/ 5 16)
 isNat(x1)	weight: 0
   U46(x1)	weight: x1
#a__U121(x1,x2)	weight: 0
   U52(x1)	weight: x1
   U61(x1,x2)	weight: x1
a__U46(x1)	weight: x1
#a__U22(x1,x2)	weight: (/ 1 16)
a__U113(x1,x2,x3)	weight: (/ 1 8) + x1 + x2
   U96(x1)	weight: x1
a__U13(x1)	weight: x1
   U31(x1,x2)	weight: x1
#a__isNatList(x1)	weight: 0
a__U71(x1)	weight: x1
   U92(x1,x2,x3)	weight: x1
  U112(x1,x2,x3)	weight: (/ 1 8) + x1 + x2
  cons(x1,x2)	weight: x1 + x2
a__U92(x1,x2,x3)	weight: x1
a__U61(x1,x2)	weight: x1
  U102(x1,x2,x3)	weight: x1
a__U105(x1,x2)	weight: x1
a__take(x1,x2)	weight: (/ 1 2) + x1 + x2
   U81(x1)	weight: x1
#a__U95(x1,x2)	weight: (/ 1 16)
#a__U41(x1,x2,x3)	weight: (/ 5 16)
    tt()	weight: 0
a__U131(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
a__isNat(x1)	weight: 0
   U13(x1)	weight: x1
a__U133(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x2 + x3 + x4
a__U23(x1)	weight: x1
a__U96(x1)	weight: x1
a__isNatKind(x1)	weight: 0
#a__U134(x1,x2,x3,x4)	weight: (/ 3 16) + x4
   U22(x1,x2)	weight: x1
   U51(x1,x2)	weight: x1
#a__U132(x1,x2,x3,x4)	weight: (/ 5 16) + x4
a__U103(x1,x2,x3)	weight: x1
length(x1)	weight: (/ 1 8) + x1
a__U112(x1,x2,x3)	weight: (/ 1 8) + x1 + x2
   U41(x1,x2,x3)	weight: x1
#a__U32(x1,x2)	weight: (/ 1 16)
a__zeros()	weight: 0
a__U101(x1,x2,x3)	weight: x1
#a__U91(x1,x2,x3)	weight: (/ 13 16)
  U121(x1,x2)	weight: (/ 1 16) + x1
a__length(x1)	weight: (/ 1 8) + x1
  U122(x1)	weight: (/ 1 16) + x1
    Usable rules: { 1..177 }
    Removed DPs: #10..12 #18..20 #31 #32 #62 #63 #78 #79 #85 #86 #100 #107..110 #127 #130 #133 #134 #137 #138 #151..153 #155 #160 #164 #176 #191 #192 #195
Number of SCCs: 3, DPs: 40, edges: 1230
	SCC { #68 #70 #99 #131 #139 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum).