Input TRS:
    1: U101(tt(),V1,V2) -> U102(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    2: U102(tt(),V1,V2) -> U103(isLNatKind(activate(V2)),activate(V1),activate(V2))
    3: U103(tt(),V1,V2) -> U104(isLNatKind(activate(V2)),activate(V1),activate(V2))
    4: U104(tt(),V1,V2) -> U105(isNatural(activate(V1)),activate(V2))
    5: U105(tt(),V2) -> U106(isLNat(activate(V2)))
    6: U106(tt()) -> tt()
    7: U11(tt(),N,XS) -> U12(isNaturalKind(activate(N)),activate(N),activate(XS))
    8: U111(tt(),V2) -> U112(isLNatKind(activate(V2)))
    9: U112(tt()) -> tt()
    10: U12(tt(),N,XS) -> U13(isLNat(activate(XS)),activate(N),activate(XS))
    11: U121(tt(),V2) -> U122(isLNatKind(activate(V2)))
    12: U122(tt()) -> tt()
    13: U13(tt(),N,XS) -> U14(isLNatKind(activate(XS)),activate(N),activate(XS))
    14: U131(tt()) -> tt()
    15: U14(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
    16: U141(tt()) -> tt()
    17: U151(tt()) -> tt()
    18: U161(tt()) -> tt()
    19: U171(tt(),V2) -> U172(isLNatKind(activate(V2)))
    20: U172(tt()) -> tt()
    21: U181(tt(),V1) -> U182(isLNatKind(activate(V1)),activate(V1))
    22: U182(tt(),V1) -> U183(isLNat(activate(V1)))
    23: U183(tt()) -> tt()
    24: U191(tt(),V1) -> U192(isNaturalKind(activate(V1)),activate(V1))
    25: U192(tt(),V1) -> U193(isNatural(activate(V1)))
    26: U193(tt()) -> tt()
    27: U201(tt(),V1,V2) -> U202(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    28: U202(tt(),V1,V2) -> U203(isLNatKind(activate(V2)),activate(V1),activate(V2))
    29: U203(tt(),V1,V2) -> U204(isLNatKind(activate(V2)),activate(V1),activate(V2))
    30: U204(tt(),V1,V2) -> U205(isNatural(activate(V1)),activate(V2))
    31: U205(tt(),V2) -> U206(isLNat(activate(V2)))
    32: U206(tt()) -> tt()
    33: U21(tt(),X,Y) -> U22(isLNatKind(activate(X)),activate(X),activate(Y))
    34: U211(tt()) -> tt()
    35: U22(tt(),X,Y) -> U23(isLNat(activate(Y)),activate(X),activate(Y))
    36: U221(tt()) -> tt()
    37: U23(tt(),X,Y) -> U24(isLNatKind(activate(Y)),activate(X))
    38: U231(tt(),V2) -> U232(isLNatKind(activate(V2)))
    39: U232(tt()) -> tt()
    40: U24(tt(),X) -> activate(X)
    41: U241(tt(),V1,V2) -> U242(isLNatKind(activate(V1)),activate(V1),activate(V2))
    42: U242(tt(),V1,V2) -> U243(isLNatKind(activate(V2)),activate(V1),activate(V2))
    43: U243(tt(),V1,V2) -> U244(isLNatKind(activate(V2)),activate(V1),activate(V2))
    44: U244(tt(),V1,V2) -> U245(isLNat(activate(V1)),activate(V2))
    45: U245(tt(),V2) -> U246(isLNat(activate(V2)))
    46: U246(tt()) -> tt()
    47: U251(tt(),V1,V2) -> U252(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    48: U252(tt(),V1,V2) -> U253(isLNatKind(activate(V2)),activate(V1),activate(V2))
    49: U253(tt(),V1,V2) -> U254(isLNatKind(activate(V2)),activate(V1),activate(V2))
    50: U254(tt(),V1,V2) -> U255(isNatural(activate(V1)),activate(V2))
    51: U255(tt(),V2) -> U256(isLNat(activate(V2)))
    52: U256(tt()) -> tt()
    53: U261(tt(),V2) -> U262(isLNatKind(activate(V2)))
    54: U262(tt()) -> tt()
    55: U271(tt(),V2) -> U272(isLNatKind(activate(V2)))
    56: U272(tt()) -> tt()
    57: U281(tt(),N) -> U282(isNaturalKind(activate(N)),activate(N))
    58: U282(tt(),N) -> cons(activate(N),n__natsFrom(n__s(activate(N))))
    59: U291(tt(),N,XS) -> U292(isNaturalKind(activate(N)),activate(N),activate(XS))
    60: U292(tt(),N,XS) -> U293(isLNat(activate(XS)),activate(N),activate(XS))
    61: U293(tt(),N,XS) -> U294(isLNatKind(activate(XS)),activate(N),activate(XS))
    62: U294(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
    63: U301(tt(),X,Y) -> U302(isLNatKind(activate(X)),activate(Y))
    64: U302(tt(),Y) -> U303(isLNat(activate(Y)),activate(Y))
    65: U303(tt(),Y) -> U304(isLNatKind(activate(Y)),activate(Y))
    66: U304(tt(),Y) -> activate(Y)
    67: U31(tt(),N,XS) -> U32(isNaturalKind(activate(N)),activate(N),activate(XS))
    68: U311(tt(),XS) -> U312(isLNatKind(activate(XS)),activate(XS))
    69: U312(tt(),XS) -> pair(nil(),activate(XS))
    70: U32(tt(),N,XS) -> U33(isLNat(activate(XS)),activate(N),activate(XS))
    71: U321(tt(),N,X,XS) -> U322(isNaturalKind(activate(N)),activate(N),activate(X),activate(XS))
    72: U322(tt(),N,X,XS) -> U323(isNatural(activate(X)),activate(N),activate(X),activate(XS))
    73: U323(tt(),N,X,XS) -> U324(isNaturalKind(activate(X)),activate(N),activate(X),activate(XS))
    74: U324(tt(),N,X,XS) -> U325(isLNat(activate(XS)),activate(N),activate(X),activate(XS))
    75: U325(tt(),N,X,XS) -> U326(isLNatKind(activate(XS)),activate(N),activate(X),activate(XS))
    76: U326(tt(),N,X,XS) -> U327(splitAt(activate(N),activate(XS)),activate(X))
    77: U327(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
    78: U33(tt(),N,XS) -> U34(isLNatKind(activate(XS)),activate(N))
    79: U331(tt(),N,XS) -> U332(isNaturalKind(activate(N)),activate(XS))
    80: U332(tt(),XS) -> U333(isLNat(activate(XS)),activate(XS))
    81: U333(tt(),XS) -> U334(isLNatKind(activate(XS)),activate(XS))
    82: U334(tt(),XS) -> activate(XS)
    83: U34(tt(),N) -> activate(N)
    84: U341(tt(),N,XS) -> U342(isNaturalKind(activate(N)),activate(N),activate(XS))
    85: U342(tt(),N,XS) -> U343(isLNat(activate(XS)),activate(N),activate(XS))
    86: U343(tt(),N,XS) -> U344(isLNatKind(activate(XS)),activate(N),activate(XS))
    87: U344(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
    88: U41(tt(),V1,V2) -> U42(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    89: U42(tt(),V1,V2) -> U43(isLNatKind(activate(V2)),activate(V1),activate(V2))
    90: U43(tt(),V1,V2) -> U44(isLNatKind(activate(V2)),activate(V1),activate(V2))
    91: U44(tt(),V1,V2) -> U45(isNatural(activate(V1)),activate(V2))
    92: U45(tt(),V2) -> U46(isLNat(activate(V2)))
    93: U46(tt()) -> tt()
    94: U51(tt(),V1,V2) -> U52(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    95: U52(tt(),V1,V2) -> U53(isLNatKind(activate(V2)),activate(V1),activate(V2))
    96: U53(tt(),V1,V2) -> U54(isLNatKind(activate(V2)),activate(V1),activate(V2))
    97: U54(tt(),V1,V2) -> U55(isNatural(activate(V1)),activate(V2))
    98: U55(tt(),V2) -> U56(isLNat(activate(V2)))
    99: U56(tt()) -> tt()
    100: U61(tt(),V1) -> U62(isPLNatKind(activate(V1)),activate(V1))
    101: U62(tt(),V1) -> U63(isPLNat(activate(V1)))
    102: U63(tt()) -> tt()
    103: U71(tt(),V1) -> U72(isNaturalKind(activate(V1)),activate(V1))
    104: U72(tt(),V1) -> U73(isNatural(activate(V1)))
    105: U73(tt()) -> tt()
    106: U81(tt(),V1) -> U82(isPLNatKind(activate(V1)),activate(V1))
    107: U82(tt(),V1) -> U83(isPLNat(activate(V1)))
    108: U83(tt()) -> tt()
    109: U91(tt(),V1) -> U92(isLNatKind(activate(V1)),activate(V1))
    110: U92(tt(),V1) -> U93(isLNat(activate(V1)))
    111: U93(tt()) -> tt()
    112: afterNth(N,XS) -> U11(isNatural(N),N,XS)
    113: fst(pair(X,Y)) -> U21(isLNat(X),X,Y)
    114: head(cons(N,XS)) -> U31(isNatural(N),N,activate(XS))
    115: isLNat(n__nil()) -> tt()
    116: isLNat(n__afterNth(V1,V2)) -> U41(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    117: isLNat(n__cons(V1,V2)) -> U51(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    118: isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1))
    119: isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1))
    120: isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1))
    121: isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1))
    122: isLNat(n__take(V1,V2)) -> U101(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    123: isLNatKind(n__nil()) -> tt()
    124: isLNatKind(n__afterNth(V1,V2)) -> U111(isNaturalKind(activate(V1)),activate(V2))
    125: isLNatKind(n__cons(V1,V2)) -> U121(isNaturalKind(activate(V1)),activate(V2))
    126: isLNatKind(n__fst(V1)) -> U131(isPLNatKind(activate(V1)))
    127: isLNatKind(n__natsFrom(V1)) -> U141(isNaturalKind(activate(V1)))
    128: isLNatKind(n__snd(V1)) -> U151(isPLNatKind(activate(V1)))
    129: isLNatKind(n__tail(V1)) -> U161(isLNatKind(activate(V1)))
    130: isLNatKind(n__take(V1,V2)) -> U171(isNaturalKind(activate(V1)),activate(V2))
    131: isNatural(n__0()) -> tt()
    132: isNatural(n__head(V1)) -> U181(isLNatKind(activate(V1)),activate(V1))
    133: isNatural(n__s(V1)) -> U191(isNaturalKind(activate(V1)),activate(V1))
    134: isNatural(n__sel(V1,V2)) -> U201(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    135: isNaturalKind(n__0()) -> tt()
    136: isNaturalKind(n__head(V1)) -> U211(isLNatKind(activate(V1)))
    137: isNaturalKind(n__s(V1)) -> U221(isNaturalKind(activate(V1)))
    138: isNaturalKind(n__sel(V1,V2)) -> U231(isNaturalKind(activate(V1)),activate(V2))
    139: isPLNat(n__pair(V1,V2)) -> U241(isLNatKind(activate(V1)),activate(V1),activate(V2))
    140: isPLNat(n__splitAt(V1,V2)) -> U251(isNaturalKind(activate(V1)),activate(V1),activate(V2))
    141: isPLNatKind(n__pair(V1,V2)) -> U261(isLNatKind(activate(V1)),activate(V2))
    142: isPLNatKind(n__splitAt(V1,V2)) -> U271(isNaturalKind(activate(V1)),activate(V2))
    143: natsFrom(N) -> U281(isNatural(N),N)
    144: sel(N,XS) -> U291(isNatural(N),N,XS)
    145: snd(pair(X,Y)) -> U301(isLNat(X),X,Y)
    146: splitAt(0(),XS) -> U311(isLNat(XS),XS)
    147: splitAt(s(N),cons(X,XS)) -> U321(isNatural(N),N,X,activate(XS))
    148: tail(cons(N,XS)) -> U331(isNatural(N),N,activate(XS))
    149: take(N,XS) -> U341(isNatural(N),N,XS)
    150: natsFrom(X) -> n__natsFrom(X)
    151: s(X) -> n__s(X)
    152: nil() -> n__nil()
    153: afterNth(X1,X2) -> n__afterNth(X1,X2)
    154: cons(X1,X2) -> n__cons(X1,X2)
    155: fst(X) -> n__fst(X)
    156: snd(X) -> n__snd(X)
    157: tail(X) -> n__tail(X)
    158: take(X1,X2) -> n__take(X1,X2)
    159: 0() -> n__0()
    160: head(X) -> n__head(X)
    161: sel(X1,X2) -> n__sel(X1,X2)
    162: pair(X1,X2) -> n__pair(X1,X2)
    163: splitAt(X1,X2) -> n__splitAt(X1,X2)
    164: activate(n__natsFrom(X)) -> natsFrom(activate(X))
    165: activate(n__s(X)) -> s(activate(X))
    166: activate(n__nil()) -> nil()
    167: activate(n__afterNth(X1,X2)) -> afterNth(activate(X1),activate(X2))
    168: activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
    169: activate(n__fst(X)) -> fst(activate(X))
    170: activate(n__snd(X)) -> snd(activate(X))
    171: activate(n__tail(X)) -> tail(activate(X))
    172: activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
    173: activate(n__0()) -> 0()
    174: activate(n__head(X)) -> head(activate(X))
    175: activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2))
    176: activate(n__pair(X1,X2)) -> pair(activate(X1),activate(X2))
    177: activate(n__splitAt(X1,X2)) -> splitAt(activate(X1),activate(X2))
    178: activate(X) -> X
Number of strict rules: 178
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #U102(tt(),V1,V2) -> #U103(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #2: #U102(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #3: #U102(tt(),V1,V2) -> #activate(V2)
   #4: #U102(tt(),V1,V2) -> #activate(V1)
   #5: #U102(tt(),V1,V2) -> #activate(V2)
   #6: #U343(tt(),N,XS) -> #U344(isLNatKind(activate(XS)),activate(N),activate(XS))
   #7: #U343(tt(),N,XS) -> #isLNatKind(activate(XS))
   #8: #U343(tt(),N,XS) -> #activate(XS)
   #9: #U343(tt(),N,XS) -> #activate(N)
   #10: #U343(tt(),N,XS) -> #activate(XS)
   #11: #U243(tt(),V1,V2) -> #U244(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #12: #U243(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #13: #U243(tt(),V1,V2) -> #activate(V2)
   #14: #U243(tt(),V1,V2) -> #activate(V1)
   #15: #U243(tt(),V1,V2) -> #activate(V2)
   #16: #U203(tt(),V1,V2) -> #U204(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #17: #U203(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #18: #U203(tt(),V1,V2) -> #activate(V2)
   #19: #U203(tt(),V1,V2) -> #activate(V1)
   #20: #U203(tt(),V1,V2) -> #activate(V2)
   #21: #U22(tt(),X,Y) -> #U23(isLNat(activate(Y)),activate(X),activate(Y))
   #22: #U22(tt(),X,Y) -> #isLNat(activate(Y))
   #23: #U22(tt(),X,Y) -> #activate(Y)
   #24: #U22(tt(),X,Y) -> #activate(X)
   #25: #U22(tt(),X,Y) -> #activate(Y)
   #26: #U34(tt(),N) -> #activate(N)
   #27: #U304(tt(),Y) -> #activate(Y)
   #28: #activate(n__splitAt(X1,X2)) -> #splitAt(activate(X1),activate(X2))
   #29: #activate(n__splitAt(X1,X2)) -> #activate(X1)
   #30: #activate(n__splitAt(X1,X2)) -> #activate(X2)
   #31: #U242(tt(),V1,V2) -> #U243(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #32: #U242(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #33: #U242(tt(),V1,V2) -> #activate(V2)
   #34: #U242(tt(),V1,V2) -> #activate(V1)
   #35: #U242(tt(),V1,V2) -> #activate(V2)
   #36: #take(N,XS) -> #U341(isNatural(N),N,XS)
   #37: #take(N,XS) -> #isNatural(N)
   #38: #U52(tt(),V1,V2) -> #U53(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #39: #U52(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #40: #U52(tt(),V1,V2) -> #activate(V2)
   #41: #U52(tt(),V1,V2) -> #activate(V1)
   #42: #U52(tt(),V1,V2) -> #activate(V2)
   #43: #U241(tt(),V1,V2) -> #U242(isLNatKind(activate(V1)),activate(V1),activate(V2))
   #44: #U241(tt(),V1,V2) -> #isLNatKind(activate(V1))
   #45: #U241(tt(),V1,V2) -> #activate(V1)
   #46: #U241(tt(),V1,V2) -> #activate(V1)
   #47: #U241(tt(),V1,V2) -> #activate(V2)
   #48: #U23(tt(),X,Y) -> #U24(isLNatKind(activate(Y)),activate(X))
   #49: #U23(tt(),X,Y) -> #isLNatKind(activate(Y))
   #50: #U23(tt(),X,Y) -> #activate(Y)
   #51: #U23(tt(),X,Y) -> #activate(X)
   #52: #head(cons(N,XS)) -> #U31(isNatural(N),N,activate(XS))
   #53: #head(cons(N,XS)) -> #isNatural(N)
   #54: #head(cons(N,XS)) -> #activate(XS)
   #55: #U54(tt(),V1,V2) -> #U55(isNatural(activate(V1)),activate(V2))
   #56: #U54(tt(),V1,V2) -> #isNatural(activate(V1))
   #57: #U54(tt(),V1,V2) -> #activate(V1)
   #58: #U54(tt(),V1,V2) -> #activate(V2)
   #59: #U44(tt(),V1,V2) -> #U45(isNatural(activate(V1)),activate(V2))
   #60: #U44(tt(),V1,V2) -> #isNatural(activate(V1))
   #61: #U44(tt(),V1,V2) -> #activate(V1)
   #62: #U44(tt(),V1,V2) -> #activate(V2)
   #63: #U323(tt(),N,X,XS) -> #U324(isNaturalKind(activate(X)),activate(N),activate(X),activate(XS))
   #64: #U323(tt(),N,X,XS) -> #isNaturalKind(activate(X))
   #65: #U323(tt(),N,X,XS) -> #activate(X)
   #66: #U323(tt(),N,X,XS) -> #activate(N)
   #67: #U323(tt(),N,X,XS) -> #activate(X)
   #68: #U323(tt(),N,X,XS) -> #activate(XS)
   #69: #U251(tt(),V1,V2) -> #U252(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #70: #U251(tt(),V1,V2) -> #isNaturalKind(activate(V1))
   #71: #U251(tt(),V1,V2) -> #activate(V1)
   #72: #U251(tt(),V1,V2) -> #activate(V1)
   #73: #U251(tt(),V1,V2) -> #activate(V2)
   #74: #U261(tt(),V2) -> #U262(isLNatKind(activate(V2)))
   #75: #U261(tt(),V2) -> #isLNatKind(activate(V2))
   #76: #U261(tt(),V2) -> #activate(V2)
   #77: #activate(n__0()) -> #0()
   #78: #U321(tt(),N,X,XS) -> #U322(isNaturalKind(activate(N)),activate(N),activate(X),activate(XS))
   #79: #U321(tt(),N,X,XS) -> #isNaturalKind(activate(N))
   #80: #U321(tt(),N,X,XS) -> #activate(N)
   #81: #U321(tt(),N,X,XS) -> #activate(N)
   #82: #U321(tt(),N,X,XS) -> #activate(X)
   #83: #U321(tt(),N,X,XS) -> #activate(XS)
   #84: #splitAt(s(N),cons(X,XS)) -> #U321(isNatural(N),N,X,activate(XS))
   #85: #splitAt(s(N),cons(X,XS)) -> #isNatural(N)
   #86: #splitAt(s(N),cons(X,XS)) -> #activate(XS)
   #87: #isPLNat(n__pair(V1,V2)) -> #U241(isLNatKind(activate(V1)),activate(V1),activate(V2))
   #88: #isPLNat(n__pair(V1,V2)) -> #isLNatKind(activate(V1))
   #89: #isPLNat(n__pair(V1,V2)) -> #activate(V1)
   #90: #isPLNat(n__pair(V1,V2)) -> #activate(V1)
   #91: #isPLNat(n__pair(V1,V2)) -> #activate(V2)
   #92: #U252(tt(),V1,V2) -> #U253(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #93: #U252(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #94: #U252(tt(),V1,V2) -> #activate(V2)
   #95: #U252(tt(),V1,V2) -> #activate(V1)
   #96: #U252(tt(),V1,V2) -> #activate(V2)
   #97: #U325(tt(),N,X,XS) -> #U326(isLNatKind(activate(XS)),activate(N),activate(X),activate(XS))
   #98: #U325(tt(),N,X,XS) -> #isLNatKind(activate(XS))
   #99: #U325(tt(),N,X,XS) -> #activate(XS)
   #100: #U325(tt(),N,X,XS) -> #activate(N)
   #101: #U325(tt(),N,X,XS) -> #activate(X)
   #102: #U325(tt(),N,X,XS) -> #activate(XS)
   #103: #afterNth(N,XS) -> #U11(isNatural(N),N,XS)
   #104: #afterNth(N,XS) -> #isNatural(N)
   #105: #U324(tt(),N,X,XS) -> #U325(isLNat(activate(XS)),activate(N),activate(X),activate(XS))
   #106: #U324(tt(),N,X,XS) -> #isLNat(activate(XS))
   #107: #U324(tt(),N,X,XS) -> #activate(XS)
   #108: #U324(tt(),N,X,XS) -> #activate(N)
   #109: #U324(tt(),N,X,XS) -> #activate(X)
   #110: #U324(tt(),N,X,XS) -> #activate(XS)
   #111: #activate(n__snd(X)) -> #snd(activate(X))
   #112: #activate(n__snd(X)) -> #activate(X)
   #113: #U282(tt(),N) -> #cons(activate(N),n__natsFrom(n__s(activate(N))))
   #114: #U282(tt(),N) -> #activate(N)
   #115: #U282(tt(),N) -> #activate(N)
   #116: #isNaturalKind(n__sel(V1,V2)) -> #U231(isNaturalKind(activate(V1)),activate(V2))
   #117: #isNaturalKind(n__sel(V1,V2)) -> #isNaturalKind(activate(V1))
   #118: #isNaturalKind(n__sel(V1,V2)) -> #activate(V1)
   #119: #isNaturalKind(n__sel(V1,V2)) -> #activate(V2)
   #120: #fst(pair(X,Y)) -> #U21(isLNat(X),X,Y)
   #121: #fst(pair(X,Y)) -> #isLNat(X)
   #122: #U293(tt(),N,XS) -> #U294(isLNatKind(activate(XS)),activate(N),activate(XS))
   #123: #U293(tt(),N,XS) -> #isLNatKind(activate(XS))
   #124: #U293(tt(),N,XS) -> #activate(XS)
   #125: #U293(tt(),N,XS) -> #activate(N)
   #126: #U293(tt(),N,XS) -> #activate(XS)
   #127: #U231(tt(),V2) -> #U232(isLNatKind(activate(V2)))
   #128: #U231(tt(),V2) -> #isLNatKind(activate(V2))
   #129: #U231(tt(),V2) -> #activate(V2)
   #130: #isLNat(n__afterNth(V1,V2)) -> #U41(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #131: #isLNat(n__afterNth(V1,V2)) -> #isNaturalKind(activate(V1))
   #132: #isLNat(n__afterNth(V1,V2)) -> #activate(V1)
   #133: #isLNat(n__afterNth(V1,V2)) -> #activate(V1)
   #134: #isLNat(n__afterNth(V1,V2)) -> #activate(V2)
   #135: #activate(n__s(X)) -> #s(activate(X))
   #136: #activate(n__s(X)) -> #activate(X)
   #137: #U291(tt(),N,XS) -> #U292(isNaturalKind(activate(N)),activate(N),activate(XS))
   #138: #U291(tt(),N,XS) -> #isNaturalKind(activate(N))
   #139: #U291(tt(),N,XS) -> #activate(N)
   #140: #U291(tt(),N,XS) -> #activate(N)
   #141: #U291(tt(),N,XS) -> #activate(XS)
   #142: #U92(tt(),V1) -> #U93(isLNat(activate(V1)))
   #143: #U92(tt(),V1) -> #isLNat(activate(V1))
   #144: #U92(tt(),V1) -> #activate(V1)
   #145: #isNatural(n__head(V1)) -> #U181(isLNatKind(activate(V1)),activate(V1))
   #146: #isNatural(n__head(V1)) -> #isLNatKind(activate(V1))
   #147: #isNatural(n__head(V1)) -> #activate(V1)
   #148: #isNatural(n__head(V1)) -> #activate(V1)
   #149: #U271(tt(),V2) -> #U272(isLNatKind(activate(V2)))
   #150: #U271(tt(),V2) -> #isLNatKind(activate(V2))
   #151: #U271(tt(),V2) -> #activate(V2)
   #152: #U31(tt(),N,XS) -> #U32(isNaturalKind(activate(N)),activate(N),activate(XS))
   #153: #U31(tt(),N,XS) -> #isNaturalKind(activate(N))
   #154: #U31(tt(),N,XS) -> #activate(N)
   #155: #U31(tt(),N,XS) -> #activate(N)
   #156: #U31(tt(),N,XS) -> #activate(XS)
   #157: #U24(tt(),X) -> #activate(X)
   #158: #U43(tt(),V1,V2) -> #U44(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #159: #U43(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #160: #U43(tt(),V1,V2) -> #activate(V2)
   #161: #U43(tt(),V1,V2) -> #activate(V1)
   #162: #U43(tt(),V1,V2) -> #activate(V2)
   #163: #splitAt(0(),XS) -> #U311(isLNat(XS),XS)
   #164: #splitAt(0(),XS) -> #isLNat(XS)
   #165: #U82(tt(),V1) -> #U83(isPLNat(activate(V1)))
   #166: #U82(tt(),V1) -> #isPLNat(activate(V1))
   #167: #U82(tt(),V1) -> #activate(V1)
   #168: #U255(tt(),V2) -> #U256(isLNat(activate(V2)))
   #169: #U255(tt(),V2) -> #isLNat(activate(V2))
   #170: #U255(tt(),V2) -> #activate(V2)
   #171: #U13(tt(),N,XS) -> #U14(isLNatKind(activate(XS)),activate(N),activate(XS))
   #172: #U13(tt(),N,XS) -> #isLNatKind(activate(XS))
   #173: #U13(tt(),N,XS) -> #activate(XS)
   #174: #U13(tt(),N,XS) -> #activate(N)
   #175: #U13(tt(),N,XS) -> #activate(XS)
   #176: #U121(tt(),V2) -> #U122(isLNatKind(activate(V2)))
   #177: #U121(tt(),V2) -> #isLNatKind(activate(V2))
   #178: #U121(tt(),V2) -> #activate(V2)
   #179: #U55(tt(),V2) -> #U56(isLNat(activate(V2)))
   #180: #U55(tt(),V2) -> #isLNat(activate(V2))
   #181: #U55(tt(),V2) -> #activate(V2)
   #182: #U281(tt(),N) -> #U282(isNaturalKind(activate(N)),activate(N))
   #183: #U281(tt(),N) -> #isNaturalKind(activate(N))
   #184: #U281(tt(),N) -> #activate(N)
   #185: #U281(tt(),N) -> #activate(N)
   #186: #U326(tt(),N,X,XS) -> #U327(splitAt(activate(N),activate(XS)),activate(X))
   #187: #U326(tt(),N,X,XS) -> #splitAt(activate(N),activate(XS))
   #188: #U326(tt(),N,X,XS) -> #activate(N)
   #189: #U326(tt(),N,X,XS) -> #activate(XS)
   #190: #U326(tt(),N,X,XS) -> #activate(X)
   #191: #activate(n__afterNth(X1,X2)) -> #afterNth(activate(X1),activate(X2))
   #192: #activate(n__afterNth(X1,X2)) -> #activate(X1)
   #193: #activate(n__afterNth(X1,X2)) -> #activate(X2)
   #194: #U91(tt(),V1) -> #U92(isLNatKind(activate(V1)),activate(V1))
   #195: #U91(tt(),V1) -> #isLNatKind(activate(V1))
   #196: #U91(tt(),V1) -> #activate(V1)
   #197: #U91(tt(),V1) -> #activate(V1)
   #198: #U51(tt(),V1,V2) -> #U52(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #199: #U51(tt(),V1,V2) -> #isNaturalKind(activate(V1))
   #200: #U51(tt(),V1,V2) -> #activate(V1)
   #201: #U51(tt(),V1,V2) -> #activate(V1)
   #202: #U51(tt(),V1,V2) -> #activate(V2)
   #203: #U191(tt(),V1) -> #U192(isNaturalKind(activate(V1)),activate(V1))
   #204: #U191(tt(),V1) -> #isNaturalKind(activate(V1))
   #205: #U191(tt(),V1) -> #activate(V1)
   #206: #U191(tt(),V1) -> #activate(V1)
   #207: #isNatural(n__sel(V1,V2)) -> #U201(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #208: #isNatural(n__sel(V1,V2)) -> #isNaturalKind(activate(V1))
   #209: #isNatural(n__sel(V1,V2)) -> #activate(V1)
   #210: #isNatural(n__sel(V1,V2)) -> #activate(V1)
   #211: #isNatural(n__sel(V1,V2)) -> #activate(V2)
   #212: #U32(tt(),N,XS) -> #U33(isLNat(activate(XS)),activate(N),activate(XS))
   #213: #U32(tt(),N,XS) -> #isLNat(activate(XS))
   #214: #U32(tt(),N,XS) -> #activate(XS)
   #215: #U32(tt(),N,XS) -> #activate(N)
   #216: #U32(tt(),N,XS) -> #activate(XS)
   #217: #isLNatKind(n__snd(V1)) -> #U151(isPLNatKind(activate(V1)))
   #218: #isLNatKind(n__snd(V1)) -> #isPLNatKind(activate(V1))
   #219: #isLNatKind(n__snd(V1)) -> #activate(V1)
   #220: #U333(tt(),XS) -> #U334(isLNatKind(activate(XS)),activate(XS))
   #221: #U333(tt(),XS) -> #isLNatKind(activate(XS))
   #222: #U333(tt(),XS) -> #activate(XS)
   #223: #U333(tt(),XS) -> #activate(XS)
   #224: #isLNat(n__fst(V1)) -> #U61(isPLNatKind(activate(V1)),activate(V1))
   #225: #isLNat(n__fst(V1)) -> #isPLNatKind(activate(V1))
   #226: #isLNat(n__fst(V1)) -> #activate(V1)
   #227: #isLNat(n__fst(V1)) -> #activate(V1)
   #228: #U33(tt(),N,XS) -> #U34(isLNatKind(activate(XS)),activate(N))
   #229: #U33(tt(),N,XS) -> #isLNatKind(activate(XS))
   #230: #U33(tt(),N,XS) -> #activate(XS)
   #231: #U33(tt(),N,XS) -> #activate(N)
   #232: #U245(tt(),V2) -> #U246(isLNat(activate(V2)))
   #233: #U245(tt(),V2) -> #isLNat(activate(V2))
   #234: #U245(tt(),V2) -> #activate(V2)
   #235: #U53(tt(),V1,V2) -> #U54(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #236: #U53(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #237: #U53(tt(),V1,V2) -> #activate(V2)
   #238: #U53(tt(),V1,V2) -> #activate(V1)
   #239: #U53(tt(),V1,V2) -> #activate(V2)
   #240: #U312(tt(),XS) -> #pair(nil(),activate(XS))
   #241: #U312(tt(),XS) -> #nil()
   #242: #U312(tt(),XS) -> #activate(XS)
   #243: #U62(tt(),V1) -> #U63(isPLNat(activate(V1)))
   #244: #U62(tt(),V1) -> #isPLNat(activate(V1))
   #245: #U62(tt(),V1) -> #activate(V1)
   #246: #U205(tt(),V2) -> #U206(isLNat(activate(V2)))
   #247: #U205(tt(),V2) -> #isLNat(activate(V2))
   #248: #U205(tt(),V2) -> #activate(V2)
   #249: #activate(n__natsFrom(X)) -> #natsFrom(activate(X))
   #250: #activate(n__natsFrom(X)) -> #activate(X)
   #251: #U331(tt(),N,XS) -> #U332(isNaturalKind(activate(N)),activate(XS))
   #252: #U331(tt(),N,XS) -> #isNaturalKind(activate(N))
   #253: #U331(tt(),N,XS) -> #activate(N)
   #254: #U331(tt(),N,XS) -> #activate(XS)
   #255: #U42(tt(),V1,V2) -> #U43(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #256: #U42(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #257: #U42(tt(),V1,V2) -> #activate(V2)
   #258: #U42(tt(),V1,V2) -> #activate(V1)
   #259: #U42(tt(),V1,V2) -> #activate(V2)
   #260: #isNatural(n__s(V1)) -> #U191(isNaturalKind(activate(V1)),activate(V1))
   #261: #isNatural(n__s(V1)) -> #isNaturalKind(activate(V1))
   #262: #isNatural(n__s(V1)) -> #activate(V1)
   #263: #isNatural(n__s(V1)) -> #activate(V1)
   #264: #U334(tt(),XS) -> #activate(XS)
   #265: #U81(tt(),V1) -> #U82(isPLNatKind(activate(V1)),activate(V1))
   #266: #U81(tt(),V1) -> #isPLNatKind(activate(V1))
   #267: #U81(tt(),V1) -> #activate(V1)
   #268: #U81(tt(),V1) -> #activate(V1)
   #269: #U294(tt(),N,XS) -> #head(afterNth(activate(N),activate(XS)))
   #270: #U294(tt(),N,XS) -> #afterNth(activate(N),activate(XS))
   #271: #U294(tt(),N,XS) -> #activate(N)
   #272: #U294(tt(),N,XS) -> #activate(XS)
   #273: #U204(tt(),V1,V2) -> #U205(isNatural(activate(V1)),activate(V2))
   #274: #U204(tt(),V1,V2) -> #isNatural(activate(V1))
   #275: #U204(tt(),V1,V2) -> #activate(V1)
   #276: #U204(tt(),V1,V2) -> #activate(V2)
   #277: #U253(tt(),V1,V2) -> #U254(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #278: #U253(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #279: #U253(tt(),V1,V2) -> #activate(V2)
   #280: #U253(tt(),V1,V2) -> #activate(V1)
   #281: #U253(tt(),V1,V2) -> #activate(V2)
   #282: #U192(tt(),V1) -> #U193(isNatural(activate(V1)))
   #283: #U192(tt(),V1) -> #isNatural(activate(V1))
   #284: #U192(tt(),V1) -> #activate(V1)
   #285: #isLNatKind(n__take(V1,V2)) -> #U171(isNaturalKind(activate(V1)),activate(V2))
   #286: #isLNatKind(n__take(V1,V2)) -> #isNaturalKind(activate(V1))
   #287: #isLNatKind(n__take(V1,V2)) -> #activate(V1)
   #288: #isLNatKind(n__take(V1,V2)) -> #activate(V2)
   #289: #activate(n__nil()) -> #nil()
   #290: #isLNatKind(n__tail(V1)) -> #U161(isLNatKind(activate(V1)))
   #291: #isLNatKind(n__tail(V1)) -> #isLNatKind(activate(V1))
   #292: #isLNatKind(n__tail(V1)) -> #activate(V1)
   #293: #isLNatKind(n__fst(V1)) -> #U131(isPLNatKind(activate(V1)))
   #294: #isLNatKind(n__fst(V1)) -> #isPLNatKind(activate(V1))
   #295: #isLNatKind(n__fst(V1)) -> #activate(V1)
   #296: #activate(n__head(X)) -> #head(activate(X))
   #297: #activate(n__head(X)) -> #activate(X)
   #298: #U41(tt(),V1,V2) -> #U42(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #299: #U41(tt(),V1,V2) -> #isNaturalKind(activate(V1))
   #300: #U41(tt(),V1,V2) -> #activate(V1)
   #301: #U41(tt(),V1,V2) -> #activate(V1)
   #302: #U41(tt(),V1,V2) -> #activate(V2)
   #303: #U11(tt(),N,XS) -> #U12(isNaturalKind(activate(N)),activate(N),activate(XS))
   #304: #U11(tt(),N,XS) -> #isNaturalKind(activate(N))
   #305: #U11(tt(),N,XS) -> #activate(N)
   #306: #U11(tt(),N,XS) -> #activate(N)
   #307: #U11(tt(),N,XS) -> #activate(XS)
   #308: #isNaturalKind(n__head(V1)) -> #U211(isLNatKind(activate(V1)))
   #309: #isNaturalKind(n__head(V1)) -> #isLNatKind(activate(V1))
   #310: #isNaturalKind(n__head(V1)) -> #activate(V1)
   #311: #U12(tt(),N,XS) -> #U13(isLNat(activate(XS)),activate(N),activate(XS))
   #312: #U12(tt(),N,XS) -> #isLNat(activate(XS))
   #313: #U12(tt(),N,XS) -> #activate(XS)
   #314: #U12(tt(),N,XS) -> #activate(N)
   #315: #U12(tt(),N,XS) -> #activate(XS)
   #316: #U45(tt(),V2) -> #U46(isLNat(activate(V2)))
   #317: #U45(tt(),V2) -> #isLNat(activate(V2))
   #318: #U45(tt(),V2) -> #activate(V2)
   #319: #activate(n__sel(X1,X2)) -> #sel(activate(X1),activate(X2))
   #320: #activate(n__sel(X1,X2)) -> #activate(X1)
   #321: #activate(n__sel(X1,X2)) -> #activate(X2)
   #322: #isLNat(n__natsFrom(V1)) -> #U71(isNaturalKind(activate(V1)),activate(V1))
   #323: #isLNat(n__natsFrom(V1)) -> #isNaturalKind(activate(V1))
   #324: #isLNat(n__natsFrom(V1)) -> #activate(V1)
   #325: #isLNat(n__natsFrom(V1)) -> #activate(V1)
   #326: #U302(tt(),Y) -> #U303(isLNat(activate(Y)),activate(Y))
   #327: #U302(tt(),Y) -> #isLNat(activate(Y))
   #328: #U302(tt(),Y) -> #activate(Y)
   #329: #U302(tt(),Y) -> #activate(Y)
   #330: #U21(tt(),X,Y) -> #U22(isLNatKind(activate(X)),activate(X),activate(Y))
   #331: #U21(tt(),X,Y) -> #isLNatKind(activate(X))
   #332: #U21(tt(),X,Y) -> #activate(X)
   #333: #U21(tt(),X,Y) -> #activate(X)
   #334: #U21(tt(),X,Y) -> #activate(Y)
   #335: #U322(tt(),N,X,XS) -> #U323(isNatural(activate(X)),activate(N),activate(X),activate(XS))
   #336: #U322(tt(),N,X,XS) -> #isNatural(activate(X))
   #337: #U322(tt(),N,X,XS) -> #activate(X)
   #338: #U322(tt(),N,X,XS) -> #activate(N)
   #339: #U322(tt(),N,X,XS) -> #activate(X)
   #340: #U322(tt(),N,X,XS) -> #activate(XS)
   #341: #isLNat(n__snd(V1)) -> #U81(isPLNatKind(activate(V1)),activate(V1))
   #342: #isLNat(n__snd(V1)) -> #isPLNatKind(activate(V1))
   #343: #isLNat(n__snd(V1)) -> #activate(V1)
   #344: #isLNat(n__snd(V1)) -> #activate(V1)
   #345: #U105(tt(),V2) -> #U106(isLNat(activate(V2)))
   #346: #U105(tt(),V2) -> #isLNat(activate(V2))
   #347: #U105(tt(),V2) -> #activate(V2)
   #348: #U244(tt(),V1,V2) -> #U245(isLNat(activate(V1)),activate(V2))
   #349: #U244(tt(),V1,V2) -> #isLNat(activate(V1))
   #350: #U244(tt(),V1,V2) -> #activate(V1)
   #351: #U244(tt(),V1,V2) -> #activate(V2)
   #352: #U303(tt(),Y) -> #U304(isLNatKind(activate(Y)),activate(Y))
   #353: #U303(tt(),Y) -> #isLNatKind(activate(Y))
   #354: #U303(tt(),Y) -> #activate(Y)
   #355: #U303(tt(),Y) -> #activate(Y)
   #356: #tail(cons(N,XS)) -> #U331(isNatural(N),N,activate(XS))
   #357: #tail(cons(N,XS)) -> #isNatural(N)
   #358: #tail(cons(N,XS)) -> #activate(XS)
   #359: #U202(tt(),V1,V2) -> #U203(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #360: #U202(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #361: #U202(tt(),V1,V2) -> #activate(V2)
   #362: #U202(tt(),V1,V2) -> #activate(V1)
   #363: #U202(tt(),V1,V2) -> #activate(V2)
   #364: #U182(tt(),V1) -> #U183(isLNat(activate(V1)))
   #365: #U182(tt(),V1) -> #isLNat(activate(V1))
   #366: #U182(tt(),V1) -> #activate(V1)
   #367: #isLNatKind(n__natsFrom(V1)) -> #U141(isNaturalKind(activate(V1)))
   #368: #isLNatKind(n__natsFrom(V1)) -> #isNaturalKind(activate(V1))
   #369: #isLNatKind(n__natsFrom(V1)) -> #activate(V1)
   #370: #activate(n__fst(X)) -> #fst(activate(X))
   #371: #activate(n__fst(X)) -> #activate(X)
   #372: #activate(n__tail(X)) -> #tail(activate(X))
   #373: #activate(n__tail(X)) -> #activate(X)
   #374: #U341(tt(),N,XS) -> #U342(isNaturalKind(activate(N)),activate(N),activate(XS))
   #375: #U341(tt(),N,XS) -> #isNaturalKind(activate(N))
   #376: #U341(tt(),N,XS) -> #activate(N)
   #377: #U341(tt(),N,XS) -> #activate(N)
   #378: #U341(tt(),N,XS) -> #activate(XS)
   #379: #U344(tt(),N,XS) -> #fst(splitAt(activate(N),activate(XS)))
   #380: #U344(tt(),N,XS) -> #splitAt(activate(N),activate(XS))
   #381: #U344(tt(),N,XS) -> #activate(N)
   #382: #U344(tt(),N,XS) -> #activate(XS)
   #383: #U201(tt(),V1,V2) -> #U202(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #384: #U201(tt(),V1,V2) -> #isNaturalKind(activate(V1))
   #385: #U201(tt(),V1,V2) -> #activate(V1)
   #386: #U201(tt(),V1,V2) -> #activate(V1)
   #387: #U201(tt(),V1,V2) -> #activate(V2)
   #388: #isNaturalKind(n__s(V1)) -> #U221(isNaturalKind(activate(V1)))
   #389: #isNaturalKind(n__s(V1)) -> #isNaturalKind(activate(V1))
   #390: #isNaturalKind(n__s(V1)) -> #activate(V1)
   #391: #sel(N,XS) -> #U291(isNatural(N),N,XS)
   #392: #sel(N,XS) -> #isNatural(N)
   #393: #isPLNatKind(n__splitAt(V1,V2)) -> #U271(isNaturalKind(activate(V1)),activate(V2))
   #394: #isPLNatKind(n__splitAt(V1,V2)) -> #isNaturalKind(activate(V1))
   #395: #isPLNatKind(n__splitAt(V1,V2)) -> #activate(V1)
   #396: #isPLNatKind(n__splitAt(V1,V2)) -> #activate(V2)
   #397: #U292(tt(),N,XS) -> #U293(isLNat(activate(XS)),activate(N),activate(XS))
   #398: #U292(tt(),N,XS) -> #isLNat(activate(XS))
   #399: #U292(tt(),N,XS) -> #activate(XS)
   #400: #U292(tt(),N,XS) -> #activate(N)
   #401: #U292(tt(),N,XS) -> #activate(XS)
   #402: #isLNat(n__cons(V1,V2)) -> #U51(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #403: #isLNat(n__cons(V1,V2)) -> #isNaturalKind(activate(V1))
   #404: #isLNat(n__cons(V1,V2)) -> #activate(V1)
   #405: #isLNat(n__cons(V1,V2)) -> #activate(V1)
   #406: #isLNat(n__cons(V1,V2)) -> #activate(V2)
   #407: #activate(n__take(X1,X2)) -> #take(activate(X1),activate(X2))
   #408: #activate(n__take(X1,X2)) -> #activate(X1)
   #409: #activate(n__take(X1,X2)) -> #activate(X2)
   #410: #U171(tt(),V2) -> #U172(isLNatKind(activate(V2)))
   #411: #U171(tt(),V2) -> #isLNatKind(activate(V2))
   #412: #U171(tt(),V2) -> #activate(V2)
   #413: #natsFrom(N) -> #U281(isNatural(N),N)
   #414: #natsFrom(N) -> #isNatural(N)
   #415: #isLNatKind(n__cons(V1,V2)) -> #U121(isNaturalKind(activate(V1)),activate(V2))
   #416: #isLNatKind(n__cons(V1,V2)) -> #isNaturalKind(activate(V1))
   #417: #isLNatKind(n__cons(V1,V2)) -> #activate(V1)
   #418: #isLNatKind(n__cons(V1,V2)) -> #activate(V2)
   #419: #activate(n__pair(X1,X2)) -> #pair(activate(X1),activate(X2))
   #420: #activate(n__pair(X1,X2)) -> #activate(X1)
   #421: #activate(n__pair(X1,X2)) -> #activate(X2)
   #422: #U301(tt(),X,Y) -> #U302(isLNatKind(activate(X)),activate(Y))
   #423: #U301(tt(),X,Y) -> #isLNatKind(activate(X))
   #424: #U301(tt(),X,Y) -> #activate(X)
   #425: #U301(tt(),X,Y) -> #activate(Y)
   #426: #U61(tt(),V1) -> #U62(isPLNatKind(activate(V1)),activate(V1))
   #427: #U61(tt(),V1) -> #isPLNatKind(activate(V1))
   #428: #U61(tt(),V1) -> #activate(V1)
   #429: #U61(tt(),V1) -> #activate(V1)
   #430: #U342(tt(),N,XS) -> #U343(isLNat(activate(XS)),activate(N),activate(XS))
   #431: #U342(tt(),N,XS) -> #isLNat(activate(XS))
   #432: #U342(tt(),N,XS) -> #activate(XS)
   #433: #U342(tt(),N,XS) -> #activate(N)
   #434: #U342(tt(),N,XS) -> #activate(XS)
   #435: #isLNat(n__take(V1,V2)) -> #U101(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #436: #isLNat(n__take(V1,V2)) -> #isNaturalKind(activate(V1))
   #437: #isLNat(n__take(V1,V2)) -> #activate(V1)
   #438: #isLNat(n__take(V1,V2)) -> #activate(V1)
   #439: #isLNat(n__take(V1,V2)) -> #activate(V2)
   #440: #U311(tt(),XS) -> #U312(isLNatKind(activate(XS)),activate(XS))
   #441: #U311(tt(),XS) -> #isLNatKind(activate(XS))
   #442: #U311(tt(),XS) -> #activate(XS)
   #443: #U311(tt(),XS) -> #activate(XS)
   #444: #U181(tt(),V1) -> #U182(isLNatKind(activate(V1)),activate(V1))
   #445: #U181(tt(),V1) -> #isLNatKind(activate(V1))
   #446: #U181(tt(),V1) -> #activate(V1)
   #447: #U181(tt(),V1) -> #activate(V1)
   #448: #U103(tt(),V1,V2) -> #U104(isLNatKind(activate(V2)),activate(V1),activate(V2))
   #449: #U103(tt(),V1,V2) -> #isLNatKind(activate(V2))
   #450: #U103(tt(),V1,V2) -> #activate(V2)
   #451: #U103(tt(),V1,V2) -> #activate(V1)
   #452: #U103(tt(),V1,V2) -> #activate(V2)
   #453: #U327(pair(YS,ZS),X) -> #pair(cons(activate(X),YS),ZS)
   #454: #U327(pair(YS,ZS),X) -> #cons(activate(X),YS)
   #455: #U327(pair(YS,ZS),X) -> #activate(X)
   #456: #U101(tt(),V1,V2) -> #U102(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #457: #U101(tt(),V1,V2) -> #isNaturalKind(activate(V1))
   #458: #U101(tt(),V1,V2) -> #activate(V1)
   #459: #U101(tt(),V1,V2) -> #activate(V1)
   #460: #U101(tt(),V1,V2) -> #activate(V2)
   #461: #isPLNat(n__splitAt(V1,V2)) -> #U251(isNaturalKind(activate(V1)),activate(V1),activate(V2))
   #462: #isPLNat(n__splitAt(V1,V2)) -> #isNaturalKind(activate(V1))
   #463: #isPLNat(n__splitAt(V1,V2)) -> #activate(V1)
   #464: #isPLNat(n__splitAt(V1,V2)) -> #activate(V1)
   #465: #isPLNat(n__splitAt(V1,V2)) -> #activate(V2)
   #466: #isLNatKind(n__afterNth(V1,V2)) -> #U111(isNaturalKind(activate(V1)),activate(V2))
   #467: #isLNatKind(n__afterNth(V1,V2)) -> #isNaturalKind(activate(V1))
   #468: #isLNatKind(n__afterNth(V1,V2)) -> #activate(V1)
   #469: #isLNatKind(n__afterNth(V1,V2)) -> #activate(V2)
   #470: #U111(tt(),V2) -> #U112(isLNatKind(activate(V2)))
   #471: #U111(tt(),V2) -> #isLNatKind(activate(V2))
   #472: #U111(tt(),V2) -> #activate(V2)
   #473: #activate(n__cons(X1,X2)) -> #cons(activate(X1),X2)
   #474: #activate(n__cons(X1,X2)) -> #activate(X1)
   #475: #isPLNatKind(n__pair(V1,V2)) -> #U261(isLNatKind(activate(V1)),activate(V2))
   #476: #isPLNatKind(n__pair(V1,V2)) -> #isLNatKind(activate(V1))
   #477: #isPLNatKind(n__pair(V1,V2)) -> #activate(V1)
   #478: #isPLNatKind(n__pair(V1,V2)) -> #activate(V2)
   #479: #isLNat(n__tail(V1)) -> #U91(isLNatKind(activate(V1)),activate(V1))
   #480: #isLNat(n__tail(V1)) -> #isLNatKind(activate(V1))
   #481: #isLNat(n__tail(V1)) -> #activate(V1)
   #482: #isLNat(n__tail(V1)) -> #activate(V1)
   #483: #U14(tt(),N,XS) -> #snd(splitAt(activate(N),activate(XS)))
   #484: #U14(tt(),N,XS) -> #splitAt(activate(N),activate(XS))
   #485: #U14(tt(),N,XS) -> #activate(N)
   #486: #U14(tt(),N,XS) -> #activate(XS)
   #487: #snd(pair(X,Y)) -> #U301(isLNat(X),X,Y)
   #488: #snd(pair(X,Y)) -> #isLNat(X)
   #489: #U71(tt(),V1) -> #U72(isNaturalKind(activate(V1)),activate(V1))
   #490: #U71(tt(),V1) -> #isNaturalKind(activate(V1))
   #491: #U71(tt(),V1) -> #activate(V1)
   #492: #U71(tt(),V1) -> #activate(V1)
   #493: #U104(tt(),V1,V2) -> #U105(isNatural(activate(V1)),activate(V2))
   #494: #U104(tt(),V1,V2) -> #isNatural(activate(V1))
   #495: #U104(tt(),V1,V2) -> #activate(V1)
   #496: #U104(tt(),V1,V2) -> #activate(V2)
   #497: #U72(tt(),V1) -> #U73(isNatural(activate(V1)))
   #498: #U72(tt(),V1) -> #isNatural(activate(V1))
   #499: #U72(tt(),V1) -> #activate(V1)
   #500: #U332(tt(),XS) -> #U333(isLNat(activate(XS)),activate(XS))
   #501: #U332(tt(),XS) -> #isLNat(activate(XS))
   #502: #U332(tt(),XS) -> #activate(XS)
   #503: #U332(tt(),XS) -> #activate(XS)
   #504: #U254(tt(),V1,V2) -> #U255(isNatural(activate(V1)),activate(V2))
   #505: #U254(tt(),V1,V2) -> #isNatural(activate(V1))
   #506: #U254(tt(),V1,V2) -> #activate(V1)
   #507: #U254(tt(),V1,V2) -> #activate(V2)
Number of SCCs: 1, DPs: 473, edges: 9016
	SCC { #1..73 #75 #76 #78..112 #114..126 #128..134 #136..141 #143..148 #150..164 #166 #167 #169..175 #177 #178 #180..216 #218..231 #233..239 #242 #244 #245 #247..281 #283..288 #291 #292 #294..307 #309..315 #317..344 #346..363 #365 #366 #368..387 #389..409 #411..418 #420..452 #455..469 #471 #472 #474..496 #498..507 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  U291(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
#U201(x1,x2,x3)	weight: max{0, x3, x2}
  U231(x1,x2)	weight: max{0, x1}
  U301(x1,x2,x3)	weight: max{0, x3}
#isLNatKind(x1)	weight: x1
  U204(x1,x2,x3)	weight: max{0, (/ 97991 4) + x3}
   #0()	weight: 0
 #U72(x1,x2)	weight: max{0, x2}
 #U32(x1,x2,x3)	weight: max{0, x3, x2}
   U21(x1,x2,x3)	weight: max{0, x2}
  U261(x1,x2)	weight: max{(/ 97989 4) + x2, x1}
 #U83(x1)	weight: 0
  U254(x1,x2,x3)	weight: 0
  U333(x1,x2)	weight: max{0, x2}
  U193(x1)	weight: (/ 1 4)
#U256(x1)	weight: 0
  U161(x1)	weight: (/ 97991 4)
  U182(x1,x2)	weight: max{(/ 97993 4) + x2, (/ 1 2) + x1}
   U11(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
#U272(x1)	weight: 0
  U243(x1,x2,x3)	weight: max{0, 24498 + x3, x1}
#cons(x1,x2)	weight: 0
#U324(x1,x2,x3,x4)	weight: max{0, x4, x3, x2}
     s(x1)	weight: x1
#U255(x1,x2)	weight: max{0, x2}
  U105(x1,x2)	weight: max{(/ 1 4) + x2, x1}
  U303(x1,x2)	weight: max{0, x2}
n__pair(x1,x2)	weight: max{x2, x1}
#U246(x1)	weight: 0
  U192(x1,x2)	weight: 0
   U24(x1,x2)	weight: max{0, x2}
  U106(x1)	weight: (/ 48995 2)
#take(x1,x2)	weight: max{x2, 24498 + x1}
isPLNatKind(x1)	weight: (/ 97991 4)
 #U24(x1,x2)	weight: max{0, x2}
#U244(x1,x2,x3)	weight: max{0, x3, x2}
  U242(x1,x2,x3)	weight: max{0, (/ 97991 4) + x2}
#U181(x1,x2)	weight: max{0, x2}
  U262(x1)	weight: (/ 48995 2)
  U244(x1,x2,x3)	weight: 0
  U272(x1)	weight: 0
   U56(x1)	weight: (/ 1 4)
isPLNat(x1)	weight: (/ 97991 4)
   U42(x1,x2,x3)	weight: max{0, (/ 97993 4) + x3, (/ 1 2) + x1}
   U91(x1,x2)	weight: max{0, x1}
  U221(x1)	weight: (/ 97991 4)
  U293(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
#U101(x1,x2,x3)	weight: max{0, x3, x2}
activate(x1)	weight: x1
  U325(x1,x2,x3,x4)	weight: max{0, x4, x3, 24498 + x2}
 #U82(x1,x2)	weight: max{0, x2}
#U254(x1,x2,x3)	weight: max{0, x3, x2}
  take(x1,x2)	weight: max{x2, 24498 + x1}
#U183(x1)	weight: 0
#U104(x1,x2,x3)	weight: max{0, x3, x2}
   U71(x1,x2)	weight: 0
 #U81(x1,x2)	weight: max{0, x2}
#U322(x1,x2,x3,x4)	weight: max{0, x4, x3, x2}
 #U92(x1,x2)	weight: max{0, x2}
#U323(x1,x2,x3,x4)	weight: max{0, x4, x3, x2}
  U131(x1)	weight: (/ 97991 4)
  U206(x1)	weight: (/ 48995 2)
#U243(x1,x2,x3)	weight: max{0, x3, x2}
#U334(x1,x2)	weight: max{0, x2}
#U321(x1,x2,x3,x4)	weight: max{0, x4, x3, x2}
  U101(x1,x2,x3)	weight: max{0, 24498 + x2, x1}
  U255(x1,x2)	weight: max{0, (/ 97991 4) + x2}
  pair(x1,x2)	weight: max{x2, x1}
#U231(x1,x2)	weight: max{0, x2}
   fst(x1)	weight: x1
  U111(x1,x2)	weight: max{(/ 97991 4) + x2, (/ 1 4) + x1}
   U43(x1,x2,x3)	weight: max{0, (/ 48997 2) + x3}
 #U93(x1)	weight: 0
#activate(x1)	weight: x1
#U342(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
#U245(x1,x2)	weight: max{0, x2}
  U103(x1,x2,x3)	weight: max{0, (/ 1 2) + x2}
 #U23(x1,x2,x3)	weight: max{0, x3, x2}
 #U53(x1,x2,x3)	weight: max{0, x3, x2}
  U281(x1,x2)	weight: max{0, x2}
natsFrom(x1)	weight: x1
#head(x1)	weight: x1
#U331(x1,x2,x3)	weight: max{0, x3, x2}
   U44(x1,x2,x3)	weight: 0
   U55(x1,x2)	weight: 0
#U106(x1)	weight: 0
 #U43(x1,x2,x3)	weight: max{0, x3, x2}
#U121(x1,x2)	weight: max{0, x2}
  U253(x1,x2,x3)	weight: 0
  U312(x1,x2)	weight: max{0, x2}
  U341(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
   U23(x1,x2,x3)	weight: max{0, x2}
  U292(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
  U342(x1,x2,x3)	weight: max{x3, 24498 + x2, x1}
   U63(x1)	weight: 0
  U172(x1)	weight: (/ 97991 4)
   U93(x1)	weight: (/ 97991 4)
#U344(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
#U241(x1,x2,x3)	weight: max{0, x3, x2}
isNaturalKind(x1)	weight: (/ 97991 4)
splitAt(x1,x2)	weight: max{x2, 24498 + x1}
  U326(x1,x2,x3,x4)	weight: max{0, x4, x3, 24498 + x2}
#U131(x1)	weight: 0
#U311(x1,x2)	weight: max{0, x2}
   U72(x1,x2)	weight: max{0, x1}
 #U13(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
 #fst(x1)	weight: x1
  U241(x1,x2,x3)	weight: 0
   U34(x1,x2)	weight: max{0, x2}
#U271(x1,x2)	weight: max{0, x2}
n__nil()	weight: 0
 #U52(x1,x2,x3)	weight: max{0, x3, x2}
#U103(x1,x2,x3)	weight: max{0, x3, x2}
   U12(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
  U271(x1,x2)	weight: max{0, (/ 1 4) + x1}
#isPLNatKind(x1)	weight: x1
#U282(x1,x2)	weight: max{0, x2}
 #U33(x1,x2,x3)	weight: max{0, x3, x2}
#U253(x1,x2,x3)	weight: max{0, x3, x2}
#U202(x1,x2,x3)	weight: max{0, x3, x2}
#U205(x1,x2)	weight: max{0, x2}
n__natsFrom(x1)	weight: x1
isNatural(x1)	weight: (/ 97991 4)
  U302(x1,x2)	weight: max{0, x2}
   U54(x1,x2,x3)	weight: 0
  U232(x1)	weight: (/ 97991 4)
n__snd(x1)	weight: x1
  U205(x1,x2)	weight: max{24498 + x2, x1}
#U252(x1,x2,x3)	weight: max{x3, x2, (/ 1 4) + x1}
 #U44(x1,x2,x3)	weight: max{0, x3, x2}
  U201(x1,x2,x3)	weight: max{0, 24498 + x3, (/ 1 4) + x1}
  n__s(x1)	weight: x1
 #U54(x1,x2,x3)	weight: max{0, x3, x2}
  U104(x1,x2,x3)	weight: 0
n__splitAt(x1,x2)	weight: max{x2, 24498 + x1}
#U242(x1,x2,x3)	weight: max{0, x3, x2}
 #U42(x1,x2,x3)	weight: max{0, x3, x2}
#U141(x1)	weight: 0
  U252(x1,x2,x3)	weight: max{0, (/ 1 4) + x1}
 #U12(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
  U141(x1)	weight: (/ 97991 4)
#U171(x1,x2)	weight: max{0, x2}
  tail(x1)	weight: x1
 #U62(x1,x2)	weight: max{0, x2}
   U83(x1)	weight: (/ 48995 2)
#U327(x1,x2)	weight: max{0, x2}
#U301(x1,x2,x3)	weight: max{0, x3, x2}
     0()	weight: 0
  U294(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
  U191(x1,x2)	weight: 0
 #U14(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
  U343(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
n__take(x1,x2)	weight: max{x2, 24498 + x1}
 #sel(x1,x2)	weight: max{x2, (/ 48997 2) + x1}
   U73(x1)	weight: 0
  U332(x1,x2)	weight: max{0, x2}
#U102(x1,x2,x3)	weight: max{0, x3, x2}
  U171(x1,x2)	weight: max{(/ 48995 2) + x2, x1}
#isLNat(x1)	weight: x1
  U202(x1,x2,x3)	weight: max{0, (/ 1 2) + x1}
   sel(x1,x2)	weight: max{x2, (/ 48997 2) + x1}
 #U73(x1)	weight: 0
   #s(x1)	weight: 0
#U105(x1,x2)	weight: max{0, x2}
afterNth(x1,x2)	weight: max{x2, 24498 + x1}
n__cons(x1,x2)	weight: max{x2, x1}
#U211(x1)	weight: 0
#isPLNat(x1)	weight: x1
   nil()	weight: 0
isLNat(x1)	weight: (/ 97991 4)
#U304(x1,x2)	weight: max{0, x2}
  U246(x1)	weight: 0
   U62(x1,x2)	weight: 0
n__sel(x1,x2)	weight: max{x2, (/ 48997 2) + x1}
#tail(x1)	weight: x1
 #U63(x1)	weight: 0
#isNaturalKind(x1)	weight: x1
  U304(x1,x2)	weight: max{0, x2}
   U45(x1,x2)	weight: 0
#U182(x1,x2)	weight: max{0, x2}
#splitAt(x1,x2)	weight: max{x2, x1}
  U151(x1)	weight: (/ 97991 4)
 #nil()	weight: 0
n__tail(x1)	weight: x1
#U292(x1,x2,x3)	weight: max{0, x3, (/ 97993 4) + x2}
  U334(x1,x2)	weight: max{0, x2}
#U341(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
#afterNth(x1,x2)	weight: max{x2, 24498 + x1}
#U262(x1)	weight: 0
#U192(x1,x2)	weight: max{0, x2}
#U111(x1,x2)	weight: max{0, x2}
#U326(x1,x2,x3,x4)	weight: max{0, x4, x3, x2}
   U32(x1,x2,x3)	weight: max{0, x2}
#U221(x1)	weight: 0
#U206(x1)	weight: 0
   U33(x1,x2,x3)	weight: max{0, x2}
#U302(x1,x2)	weight: max{0, x2}
#U232(x1)	weight: 0
  n__0()	weight: 0
 #U46(x1)	weight: 0
#U251(x1,x2,x3)	weight: max{x3, x2, (/ 1 4) + x1}
n__afterNth(x1,x2)	weight: max{x2, 24498 + x1}
 #U34(x1,x2)	weight: max{0, x2}
isLNatKind(x1)	weight: (/ 97991 4) + x1
   U14(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
  U211(x1)	weight: (/ 97991 4)
 #U56(x1)	weight: 0
#U281(x1,x2)	weight: max{0, x2}
#U343(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
  U203(x1,x2,x3)	weight: 0
  U327(x1,x2)	weight: max{x2, x1}
   U46(x1)	weight: 0
  U251(x1,x2,x3)	weight: max{0, x1}
#U291(x1,x2,x3)	weight: max{0, x3, (/ 48997 2) + x2}
   U52(x1,x2,x3)	weight: 0
   U61(x1,x2)	weight: 0
 #U51(x1,x2,x3)	weight: max{0, x3, x2}
n__fst(x1)	weight: x1
 #U11(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
   U31(x1,x2,x3)	weight: max{0, x2}
  U183(x1)	weight: (/ 3 4) + x1
  U245(x1,x2)	weight: max{(/ 1 4) + x2, x1}
   U92(x1,x2)	weight: 0
  head(x1)	weight: x1
  U112(x1)	weight: 24498
#U193(x1)	weight: 0
 #snd(x1)	weight: x1
 #U41(x1,x2,x3)	weight: max{0, x3, x2}
  cons(x1,x2)	weight: max{x2, x1}
  U323(x1,x2,x3,x4)	weight: max{0, x4, x3, 24498 + x2}
#U294(x1,x2,x3)	weight: max{0, x3, (/ 97993 4) + x2}
#U325(x1,x2,x3,x4)	weight: max{0, x4, x3, x2}
#natsFrom(x1)	weight: x1
  U102(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 1 2) + x1}
   snd(x1)	weight: x1
#U191(x1,x2)	weight: max{0, x2}
  U256(x1)	weight: (/ 97991 4)
#U293(x1,x2,x3)	weight: max{0, x3, (/ 97993 4) + x2}
 #U21(x1,x2,x3)	weight: max{0, x3, x2}
   U81(x1,x2)	weight: 0
   U82(x1,x2)	weight: max{(/ 1 4) + x2, x1}
 #U22(x1,x2,x3)	weight: max{0, x3, x2}
#U112(x1)	weight: 0
    tt()	weight: (/ 97991 4)
#U303(x1,x2)	weight: max{0, x2}
 #U71(x1,x2)	weight: max{0, x2}
   U13(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
#U151(x1)	weight: 0
#isNatural(x1)	weight: x1
  U321(x1,x2,x3,x4)	weight: max{0, x4, x3, 24498 + x2}
#pair(x1,x2)	weight: 0
   U22(x1,x2,x3)	weight: max{0, x2}
n__head(x1)	weight: x1
 #U45(x1,x2)	weight: max{0, x2}
   U51(x1,x2,x3)	weight: max{0, (/ 1 4) + x1}
#U161(x1)	weight: 0
#U312(x1,x2)	weight: max{0, x2}
#U172(x1)	weight: 0
  U311(x1,x2)	weight: max{0, x2}
  U322(x1,x2,x3,x4)	weight: max{x4, x3, 24498 + x2, (/ 1 4) + x1}
  U344(x1,x2,x3)	weight: max{0, x3, 24498 + x2}
#U261(x1,x2)	weight: max{0, x2}
#U203(x1,x2,x3)	weight: max{0, x3, x2}
#U122(x1)	weight: 0
   U53(x1,x2,x3)	weight: max{0, x1}
   U41(x1,x2,x3)	weight: max{0, (/ 1 4) + x1}
 #U31(x1,x2,x3)	weight: max{0, x3, x2}
#U332(x1,x2)	weight: max{0, x2}
 #U91(x1,x2)	weight: max{0, x2}
 #U55(x1,x2)	weight: max{0, x2}
  U282(x1,x2)	weight: max{0, x2}
  U121(x1,x2)	weight: max{(/ 48995 2) + x2, x1}
#U204(x1,x2,x3)	weight: max{0, x3, x2}
 #U61(x1,x2)	weight: max{0, x2}
  U181(x1,x2)	weight: max{0, (/ 1 4) + x1}
  U324(x1,x2,x3,x4)	weight: max{x4, x3, 24498 + x2, (/ 1 4) + x1}
  U331(x1,x2,x3)	weight: max{0, x3}
  U122(x1)	weight: (/ 97991 4)
#U333(x1,x2)	weight: max{0, x2}
    Usable rules: { 7..20 33..40 57..87 112..114 123..130 135..138 143..178 }
    Removed DPs: #9 #29 #37 #104 #117 #118 #125 #131..133 #138..140 #174 #192 #208..210 #271 #286 #287 #304..306 #314 #320 #375..377 #381 #392 #394 #395 #400 #408 #433 #436..438 #462..464 #467 #468 #485
Number of SCCs: 1, DPs: 428, edges: 6783
	SCC { #1..8 #10..28 #30..36 #38..73 #75 #76 #78..103 #105..112 #114..116 #119..124 #126 #128..130 #134 #136 #137 #141 #143..148 #150..164 #166 #167 #169..173 #175 #177 #178 #180..191 #193..207 #211..216 #218..231 #233..239 #242 #244 #245 #247..270 #272..281 #283..285 #288 #291 #292 #294..303 #307 #309..313 #315 #317..319 #321..344 #346..363 #365 #366 #368..374 #378..380 #382..387 #389..391 #393 #396..399 #401..407 #409 #411..418 #420..432 #434 #435 #439..452 #455..461 #465 #466 #469 #471 #472 #474..484 #486..496 #498..507 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  U291(x1,x2,x3)	weight: max{(/ 69 128) + x3, (/ 69 128) + x2, (/ 11 32) + x1}
#U201(x1,x2,x3)	weight: max{(/ 35 128) + x3, (/ 33 128) + x2, (/ 19 32) + x1}
  U231(x1,x2)	weight: max{0, x1}
  U301(x1,x2,x3)	weight: max{0, (/ 1 128) + x3}
#isLNatKind(x1)	weight: (/ 17 128) + x1
  U204(x1,x2,x3)	weight: max{(/ 13 64) + x3, (/ 27 128) + x2, (/ 11 128) + x1}
   #0()	weight: 0
 #U72(x1,x2)	weight: max{(/ 13 64) + x2, (/ 197665 32) + x1}
 #U32(x1,x2,x3)	weight: max{(/ 27 128) + x3, (/ 27 128) + x2, (/ 5 128) + x1}
   U21(x1,x2,x3)	weight: max{0, (/ 1 128) + x3, (/ 1 128) + x2}
  U261(x1,x2)	weight: max{(/ 1 128) + x2, x1}
 #U83(x1)	weight: 0
  U254(x1,x2,x3)	weight: max{0, (/ 1 64) + x3}
  U333(x1,x2)	weight: max{0, x2}
  U193(x1)	weight: (/ 3 16)
#U256(x1)	weight: 0
  U161(x1)	weight: (/ 3 16)
  U182(x1,x2)	weight: max{(/ 1 128) + x2, (/ 1 16) + x1}
   U11(x1,x2,x3)	weight: max{0, (/ 41 128) + x3, (/ 41 128) + x2}
#U272(x1)	weight: 0
  U243(x1,x2,x3)	weight: max{(/ 5 32) + x3, (/ 5 32) + x2, (/ 1 32) + x1}
#cons(x1,x2)	weight: 0
#U324(x1,x2,x3,x4)	weight: max{0, (/ 17 64) + x4, (/ 37 128) + x3, (/ 39 128) + x2}
     s(x1)	weight: x1
#U255(x1,x2)	weight: max{0, (/ 27 128) + x2}
  U105(x1,x2)	weight: max{(/ 25 128) + x2, x1}
  U303(x1,x2)	weight: max{0, (/ 1 128) + x2}
n__pair(x1,x2)	weight: max{(/ 25 128) + x2, (/ 1 8) + x1}
#U246(x1)	weight: 0
  U192(x1,x2)	weight: max{(/ 1 128) + x2, (/ 1 128) + x1}
   U24(x1,x2)	weight: max{0, x2}
  U106(x1)	weight: (/ 25 128)
#take(x1,x2)	weight: max{(/ 1009207 128) + x2, (/ 51 128) + x1}
isPLNatKind(x1)	weight: (/ 17 128)
 #U24(x1,x2)	weight: max{0, (/ 1 8) + x2}
#U244(x1,x2,x3)	weight: max{(/ 7 32) + x3, (/ 15 64) + x2, (/ 1 32) + x1}
  U242(x1,x2,x3)	weight: max{0, (/ 5 32) + x3, (/ 19 128) + x2}
#U181(x1,x2)	weight: max{(/ 7 32) + x2, (/ 1 32) + x1}
  U262(x1)	weight: (/ 1 64)
  U244(x1,x2,x3)	weight: max{0, (/ 21 128) + x2, (/ 1 32) + x1}
  U272(x1)	weight: 0
   U56(x1)	weight: (/ 1 64)
isPLNat(x1)	weight: (/ 1 128) + x1
   U42(x1,x2,x3)	weight: 0
   U91(x1,x2)	weight: max{(/ 1 128) + x2, x1}
  U221(x1)	weight: (/ 3 16)
  U293(x1,x2,x3)	weight: max{0, (/ 69 128) + x3, (/ 17 32) + x2}
#U101(x1,x2,x3)	weight: max{(/ 31 128) + x3, (/ 33 128) + x2, (/ 11 128) + x1}
activate(x1)	weight: x1
  U325(x1,x2,x3,x4)	weight: max{0, (/ 25 128) + x4, (/ 3 16) + x3, (/ 17 64) + x2}
 #U82(x1,x2)	weight: max{0, (/ 31 128) + x2}
#U254(x1,x2,x3)	weight: max{(/ 7 32) + x3, (/ 15 64) + x2, (/ 1 32) + x1}
  take(x1,x2)	weight: max{(/ 1009195 128) + x2, (/ 1009193 128) + x1}
#U183(x1)	weight: 0
#U104(x1,x2,x3)	weight: max{(/ 7 32) + x3, (/ 7 32) + x2, (/ 1 32) + x1}
   U71(x1,x2)	weight: max{0, (/ 1 128) + x2}
 #U81(x1,x2)	weight: max{0, (/ 1 4) + x2}
#U322(x1,x2,x3,x4)	weight: max{(/ 17 64) + x4, (/ 19 64) + x3, (/ 39 128) + x2, (/ 1 8) + x1}
 #U92(x1,x2)	weight: max{(/ 27 128) + x2, (/ 3 128) + x1}
#U323(x1,x2,x3,x4)	weight: max{0, (/ 17 64) + x4, (/ 19 64) + x3, (/ 39 128) + x2}
  U131(x1)	weight: (/ 3 16)
  U206(x1)	weight: (/ 25 128)
#U243(x1,x2,x3)	weight: max{(/ 29 128) + x3, (/ 31 128) + x2, (/ 5 128) + x1}
#U334(x1,x2)	weight: max{(/ 1 8) + x2, x1}
#U321(x1,x2,x3,x4)	weight: max{(/ 17 64) + x4, (/ 41 128) + x3, (/ 39 128) + x2, (/ 11 128) + x1}
  U101(x1,x2,x3)	weight: max{0, (/ 3 16) + x3}
  U255(x1,x2)	weight: max{(/ 3 128) + x2, x1}
  pair(x1,x2)	weight: max{(/ 25 128) + x2, (/ 1 8) + x1}
#U231(x1,x2)	weight: max{(/ 9 64) + x2, (/ 67 128) + x1}
   fst(x1)	weight: (/ 1009159 128) + x1
  U111(x1,x2)	weight: max{0, (/ 41 128) + x1}
   U43(x1,x2,x3)	weight: max{0, (/ 17 128) + x3}
 #U93(x1)	weight: 0
#activate(x1)	weight: (/ 15 128) + x1
#U342(x1,x2,x3)	weight: max{(/ 47 128) + x3, (/ 49 128) + x2, (/ 17 128) + x1}
#U245(x1,x2)	weight: max{0, (/ 27 128) + x2}
  U103(x1,x2,x3)	weight: max{0, (/ 13 64) + x2, x1}
 #U23(x1,x2,x3)	weight: max{0, (/ 9 64) + x3, (/ 9 64) + x2}
 #U53(x1,x2,x3)	weight: max{0, (/ 13 64) + x3, (/ 27 128) + x2}
  U281(x1,x2)	weight: max{0, (/ 1602703 128) + x2}
natsFrom(x1)	weight: (/ 1602703 128) + x1
#head(x1)	weight: (/ 15 64) + x1
#U331(x1,x2,x3)	weight: max{(/ 7 32) + x3, (/ 7 32) + x2, (/ 1 32) + x1}
   U44(x1,x2,x3)	weight: max{0, (/ 1 128) + x3, x1}
   U55(x1,x2)	weight: max{0, (/ 1 128) + x2}
#U106(x1)	weight: 0
 #U43(x1,x2,x3)	weight: max{(/ 5 16) + x3, (/ 29 128) + x2, (/ 7 64) + x1}
#U121(x1,x2)	weight: max{0, (/ 17 128) + x2}
  U253(x1,x2,x3)	weight: max{0, (/ 3 128) + x3, (/ 1 128) + x2}
  U312(x1,x2)	weight: max{(/ 25 128) + x2, (/ 1 16) + x1}
  U341(x1,x2,x3)	weight: max{(/ 504593 64) + x3, (/ 1009193 128) + x2, (/ 504581 64) + x1}
   U23(x1,x2,x3)	weight: max{0, x2}
  U292(x1,x2,x3)	weight: max{0, (/ 69 128) + x3, (/ 17 32) + x2}
  U342(x1,x2,x3)	weight: max{0, (/ 504593 64) + x3, (/ 1009193 128) + x2}
   U63(x1)	weight: 0
  U172(x1)	weight: (/ 1009195 128) + x1
   U93(x1)	weight: (/ 1 64)
#U344(x1,x2,x3)	weight: max{(/ 19 64) + x3, (/ 47 128) + x2, (/ 11 64) + x1}
#U241(x1,x2,x3)	weight: max{(/ 31 128) + x3, (/ 45 128) + x2, (/ 7 128) + x1}
isNaturalKind(x1)	weight: (/ 3 16)
splitAt(x1,x2)	weight: max{(/ 25 128) + x2, (/ 17 64) + x1}
  U326(x1,x2,x3,x4)	weight: max{0, (/ 25 128) + x4, (/ 3 16) + x3, (/ 17 64) + x2}
#U131(x1)	weight: 0
#U311(x1,x2)	weight: max{0, (/ 33 128) + x2}
   U72(x1,x2)	weight: max{(/ 1 64) + x2, x1}
 #U13(x1,x2,x3)	weight: max{0, (/ 53 128) + x3, (/ 51 128) + x2}
 #fst(x1)	weight: (/ 3 32) + x1
  U241(x1,x2,x3)	weight: max{0, (/ 9 64) + x2, x1}
   U34(x1,x2)	weight: max{0, x2}
#U271(x1,x2)	weight: max{(/ 9 64) + x2, (/ 5 128) + x1}
n__nil()	weight: (/ 1 8)
 #U52(x1,x2,x3)	weight: max{(/ 13 64) + x3, (/ 33 128) + x2, (/ 3 128) + x1}
#U103(x1,x2,x3)	weight: max{0, (/ 29 128) + x3, (/ 29 128) + x2}
   U12(x1,x2,x3)	weight: max{(/ 41 128) + x3, (/ 41 128) + x2, (/ 17 128) + x1}
  U271(x1,x2)	weight: max{0, x1}
#isPLNatKind(x1)	weight: (/ 3 128) + x1
#U282(x1,x2)	weight: max{(/ 1 8) + x2, 12521 + x1}
 #U33(x1,x2,x3)	weight: max{0, (/ 9 64) + x3, (/ 13 64) + x2}
#U253(x1,x2,x3)	weight: max{0, (/ 29 128) + x3, (/ 31 128) + x2}
#U202(x1,x2,x3)	weight: max{0, (/ 17 64) + x3, (/ 1 4) + x2}
#U205(x1,x2)	weight: max{0, (/ 27 128) + x2}
n__natsFrom(x1)	weight: (/ 1602703 128) + x1
isNatural(x1)	weight: (/ 27 128) + x1
  U302(x1,x2)	weight: max{0, (/ 1 128) + x2}
   U54(x1,x2,x3)	weight: max{0, (/ 33 128) + x3, (/ 1 128) + x2}
  U232(x1)	weight: (/ 3 16)
n__snd(x1)	weight: (/ 7 128) + x1
  U205(x1,x2)	weight: max{(/ 13 64) + x2, x1}
#U252(x1,x2,x3)	weight: max{(/ 15 64) + x3, (/ 1 4) + x2, (/ 5 64) + x1}
 #U44(x1,x2,x3)	weight: max{(/ 7 32) + x3, (/ 7 32) + x2, (/ 11 64) + x1}
  U201(x1,x2,x3)	weight: max{(/ 51 64) + x3, (/ 27 128) + x2, (/ 39 64) + x1}
  n__s(x1)	weight: x1
 #U54(x1,x2,x3)	weight: max{(/ 13 64) + x3, (/ 27 128) + x2, (/ 3 128) + x1}
  U104(x1,x2,x3)	weight: max{0, (/ 5 64) + x1}
n__splitAt(x1,x2)	weight: max{(/ 25 128) + x2, (/ 17 64) + x1}
#U242(x1,x2,x3)	weight: max{(/ 15 64) + x3, (/ 11 32) + x2, (/ 3 64) + x1}
 #U42(x1,x2,x3)	weight: max{(/ 41 128) + x3, (/ 43 128) + x2, (/ 3 64) + x1}
#U141(x1)	weight: 0
  U252(x1,x2,x3)	weight: max{0, (/ 7 32) + x3, (/ 1 64) + x2}
 #U12(x1,x2,x3)	weight: max{(/ 55 128) + x3, (/ 27 64) + x2, (/ 1 4) + x1}
  U141(x1)	weight: x1
#U171(x1,x2)	weight: max{0, (/ 9 64) + x2}
  tail(x1)	weight: (/ 15 128) + x1
 #U62(x1,x2)	weight: max{0, (/ 1009183 128) + x2}
   U83(x1)	weight: (/ 25 128)
#U327(x1,x2)	weight: max{(/ 1 8) + x2, x1}
#U301(x1,x2,x3)	weight: max{0, (/ 7 32) + x3, (/ 15 64) + x2}
     0()	weight: (/ 1 128)
  U294(x1,x2,x3)	weight: max{(/ 17 32) + x3, (/ 17 32) + x2, (/ 13 32) + x1}
  U191(x1,x2)	weight: max{(/ 25 128) + x2, x1}
 #U14(x1,x2,x3)	weight: max{(/ 25 64) + x3, (/ 25 64) + x2, (/ 35 128) + x1}
  U343(x1,x2,x3)	weight: max{0, (/ 504593 64) + x3, (/ 1009193 128) + x2}
n__take(x1,x2)	weight: max{(/ 1009195 128) + x2, (/ 1009193 128) + x1}
 #sel(x1,x2)	weight: max{(/ 21 32) + x2, (/ 11 16) + x1}
   U73(x1)	weight: (/ 1 64)
  U332(x1,x2)	weight: max{0, x2}
#U102(x1,x2,x3)	weight: max{(/ 15 64) + x3, (/ 1 4) + x2, (/ 5 64) + x1}
  U171(x1,x2)	weight: max{(/ 252303 32) + x2, (/ 1009187 128) + x1}
#isLNat(x1)	weight: (/ 13 64) + x1
  U202(x1,x2,x3)	weight: max{(/ 7 32) + x3, (/ 27 128) + x2, x1}
   sel(x1,x2)	weight: max{(/ 19 32) + x2, (/ 37 64) + x1}
 #U73(x1)	weight: 0
   #s(x1)	weight: 0
#U105(x1,x2)	weight: max{0, (/ 27 128) + x2}
afterNth(x1,x2)	weight: max{(/ 49 128) + x2, (/ 47 128) + x1}
n__cons(x1,x2)	weight: max{x2, (/ 1 16) + x1}
#U211(x1)	weight: 0
#isPLNat(x1)	weight: (/ 15 64) + x1
   nil()	weight: (/ 1 8)
isLNat(x1)	weight: x1
#U304(x1,x2)	weight: max{0, (/ 1 8) + x2}
  U246(x1)	weight: (/ 23 128)
   U62(x1,x2)	weight: 0
n__sel(x1,x2)	weight: max{(/ 19 32) + x2, (/ 37 64) + x1}
#tail(x1)	weight: (/ 29 128) + x1
 #U63(x1)	weight: 0
#isNaturalKind(x1)	weight: (/ 1 8) + x1
  U304(x1,x2)	weight: max{0, x2}
   U45(x1,x2)	weight: max{(/ 25 128) + x2, x1}
#U182(x1,x2)	weight: max{0, (/ 27 128) + x2}
#splitAt(x1,x2)	weight: max{(/ 17 64) + x2, (/ 39 128) + x1}
  U151(x1)	weight: (/ 3 16)
 #nil()	weight: 0
n__tail(x1)	weight: (/ 15 128) + x1
#U292(x1,x2,x3)	weight: max{(/ 41 64) + x3, (/ 43 64) + x2, (/ 15 32) + x1}
  U334(x1,x2)	weight: max{0, x2}
#U341(x1,x2,x3)	weight: max{(/ 3 8) + x3, (/ 25 64) + x2, (/ 9 64) + x1}
#afterNth(x1,x2)	weight: max{(/ 57 128) + x2, (/ 61 128) + x1}
#U262(x1)	weight: 0
#U192(x1,x2)	weight: max{(/ 25 128) + x2, (/ 1 128) + x1}
#U111(x1,x2)	weight: max{(/ 9 64) + x2, (/ 41 128) + x1}
#U326(x1,x2,x3,x4)	weight: max{(/ 17 64) + x4, (/ 35 128) + x3, (/ 39 128) + x2, (/ 1 8) + x1}
   U32(x1,x2,x3)	weight: max{0, x2}
#U221(x1)	weight: 0
#U206(x1)	weight: 0
   U33(x1,x2,x3)	weight: max{0, x2}
#U302(x1,x2)	weight: max{(/ 27 128) + x2, (/ 3 32) + x1}
#U232(x1)	weight: 0
  n__0()	weight: (/ 1 128)
 #U46(x1)	weight: 0
#U251(x1,x2,x3)	weight: max{0, (/ 33 128) + x3, (/ 35 128) + x2}
n__afterNth(x1,x2)	weight: max{(/ 49 128) + x2, (/ 47 128) + x1}
 #U34(x1,x2)	weight: max{0, (/ 1 8) + x2}
isLNatKind(x1)	weight: (/ 17 128) + x1
   U14(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 41 128) + x2}
  U211(x1)	weight: (/ 3 16)
 #U56(x1)	weight: 0
#U281(x1,x2)	weight: max{(/ 17 128) + x2, (/ 1602689 128) + x1}
#U343(x1,x2,x3)	weight: max{0, (/ 5 16) + x3, (/ 3 8) + x2}
  U203(x1,x2,x3)	weight: max{(/ 7 32) + x3, (/ 27 128) + x2, (/ 1 32) + x1}
  U327(x1,x2)	weight: max{(/ 3 16) + x2, x1}
   U46(x1)	weight: x1
  U251(x1,x2,x3)	weight: max{0, (/ 27 128) + x3, (/ 1 128) + x2}
#U291(x1,x2,x3)	weight: max{0, (/ 83 128) + x3, (/ 87 128) + x2}
   U52(x1,x2,x3)	weight: max{0, x1}
   U61(x1,x2)	weight: 0
 #U51(x1,x2,x3)	weight: max{(/ 13 64) + x3, (/ 17 64) + x2, (/ 5 64) + x1}
n__fst(x1)	weight: (/ 1009159 128) + x1
 #U11(x1,x2,x3)	weight: max{(/ 7 16) + x3, (/ 55 128) + x2, (/ 33 128) + x1}
   U31(x1,x2,x3)	weight: max{0, x2, x1}
  U183(x1)	weight: (/ 3 16)
  U245(x1,x2)	weight: max{(/ 11 64) + x2, (/ 11 64) + x1}
   U92(x1,x2)	weight: max{0, (/ 1 128) + x2}
  head(x1)	weight: (/ 19 128) + x1
  U112(x1)	weight: (/ 3 16)
#U193(x1)	weight: 0
 #snd(x1)	weight: (/ 15 128) + x1
 #U41(x1,x2,x3)	weight: max{(/ 21 64) + x3, (/ 11 32) + x2, (/ 9 64) + x1}
  cons(x1,x2)	weight: max{x2, (/ 1 16) + x1}
  U323(x1,x2,x3,x4)	weight: max{0, (/ 25 128) + x4, (/ 3 16) + x3, (/ 17 64) + x2}
#U294(x1,x2,x3)	weight: max{0, (/ 5 8) + x3, (/ 41 64) + x2}
#U325(x1,x2,x3,x4)	weight: max{0, (/ 17 64) + x4, (/ 9 32) + x3, (/ 39 128) + x2}
#natsFrom(x1)	weight: (/ 1602717 128) + x1
  U102(x1,x2,x3)	weight: max{0, (/ 25 128) + x2, x1}
   snd(x1)	weight: (/ 7 128) + x1
#U191(x1,x2)	weight: max{(/ 25 128) + x2, x1}
  U256(x1)	weight: (/ 3 128)
#U293(x1,x2,x3)	weight: max{0, (/ 81 128) + x3, (/ 85 128) + x2}
 #U21(x1,x2,x3)	weight: max{0, (/ 7 32) + x3, (/ 27 128) + x2}
   U81(x1,x2)	weight: 0
   U82(x1,x2)	weight: max{0, x1}
 #U22(x1,x2,x3)	weight: max{0, (/ 27 128) + x3, (/ 19 128) + x2}
#U112(x1)	weight: 0
    tt()	weight: (/ 3 16)
#U303(x1,x2)	weight: max{0, (/ 9 64) + x2}
 #U71(x1,x2)	weight: max{(/ 790683 128) + x2, (/ 790661 128) + x1}
   U13(x1,x2,x3)	weight: max{0, (/ 1 4) + x3, (/ 41 128) + x2}
#U151(x1)	weight: 0
#isNatural(x1)	weight: (/ 25 128) + x1
  U321(x1,x2,x3,x4)	weight: max{(/ 25 128) + x4, (/ 13 64) + x3, (/ 17 64) + x2, (/ 7 128) + x1}
#pair(x1,x2)	weight: 0
   U22(x1,x2,x3)	weight: max{0, (/ 1 128) + x3, (/ 1 128) + x2}
n__head(x1)	weight: (/ 19 128) + x1
 #U45(x1,x2)	weight: max{0, (/ 27 128) + x2}
   U51(x1,x2,x3)	weight: max{0, (/ 9 128) + x3}
#U161(x1)	weight: 0
#U312(x1,x2)	weight: max{(/ 1 8) + x2, x1}
#U172(x1)	weight: 0
  U311(x1,x2)	weight: max{0, (/ 25 128) + x2}
  U322(x1,x2,x3,x4)	weight: max{0, (/ 25 128) + x4, (/ 3 16) + x3, (/ 17 64) + x2}
  U344(x1,x2,x3)	weight: max{(/ 31537 4) + x3, (/ 1009193 128) + x2, (/ 1009169 128) + x1}
#U261(x1,x2)	weight: max{0, (/ 9 64) + x2}
#U203(x1,x2,x3)	weight: max{(/ 29 128) + x3, (/ 31 128) + x2, (/ 1 8) + x1}
#U122(x1)	weight: 0
   U53(x1,x2,x3)	weight: max{0, (/ 33 128) + x3, (/ 1 16) + x1}
   U41(x1,x2,x3)	weight: max{0, (/ 13 64) + x1}
 #U31(x1,x2,x3)	weight: max{(/ 29 128) + x3, (/ 37 128) + x2, (/ 1 32) + x1}
#U332(x1,x2)	weight: max{(/ 27 128) + x2, (/ 3 128) + x1}
 #U91(x1,x2)	weight: max{0, (/ 7 32) + x2}
 #U55(x1,x2)	weight: max{0, (/ 13 64) + x2}
  U282(x1,x2)	weight: max{0, (/ 1602703 128) + x2}
  U121(x1,x2)	weight: max{0, x1}
#U204(x1,x2,x3)	weight: max{(/ 7 32) + x3, (/ 15 64) + x2, (/ 1 32) + x1}
 #U61(x1,x2)	weight: max{0, (/ 31537 4) + x2}
  U181(x1,x2)	weight: max{(/ 25 128) + x2, x1}
  U324(x1,x2,x3,x4)	weight: max{0, (/ 25 128) + x4, (/ 3 16) + x3, (/ 17 64) + x2}
  U331(x1,x2,x3)	weight: max{0, x3}
  U122(x1)	weight: (/ 3 16)
#U333(x1,x2)	weight: max{0, (/ 9 64) + x2}
    Usable rules: { 7..40 57..87 112..114 123..138 143..178 }
    Removed DPs: #1..8 #10..28 #30..36 #39..54 #56..62 #64..73 #75 #76 #79..83 #85..96 #98..103 #106..112 #114..116 #119..124 #126 #128..130 #134 #137 #141 #143..148 #150..164 #166 #167 #169..173 #175 #178 #181..186 #188..191 #193..197 #199..202 #204..207 #211..216 #218..231 #233 #234 #236..239 #242 #244 #245 #247..259 #261..270 #272..281 #284 #285 #288 #291 #292 #294..303 #307 #309..313 #315 #317..319 #321..334 #336..344 #346..363 #365 #366 #368..374 #378..380 #382..387 #390 #391 #393 #396..399 #401 #403..407 #409 #411..414 #416..418 #420..432 #434 #435 #439..452 #455..461 #465 #466 #469 #471 #472 #474..484 #486..496 #498..507
Number of SCCs: 6, DPs: 20, edges: 20
	SCC { #136 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
  U291(x1,x2,x3)	weight: (/ 1 16) + x3
#U201(x1,x2,x3)	weight: 0
  U231(x1,x2)	weight: (/ 1 32)
  U301(x1,x2,x3)	weight: x1 + x2 + x3
#isLNatKind(x1)	weight: 0
  U204(x1,x2,x3)	weight: (/ 5 32)
   #0()	weight: 0
 #U72(x1,x2)	weight: 0
 #U32(x1,x2,x3)	weight: 0
   U21(x1,x2,x3)	weight: (/ 3 16) + x2
  U261(x1,x2)	weight: 0
 #U83(x1)	weight: 0
  U254(x1,x2,x3)	weight: (/ 1 32)
  U333(x1,x2)	weight: x2
  U193(x1)	weight: (/ 3 32) + x1
#U256(x1)	weight: 0
  U161(x1)	weight: x1
  U182(x1,x2)	weight: x2
   U11(x1,x2,x3)	weight: (/ 1 16) + x3
#U272(x1)	weight: 0
  U243(x1,x2,x3)	weight: x1 + x2
#cons(x1,x2)	weight: 0
#U324(x1,x2,x3,x4)	weight: 0
     s(x1)	weight: (/ 5 32)
#U255(x1,x2)	weight: 0
  U105(x1,x2)	weight: x1
  U303(x1,x2)	weight: (/ 1 16)
n__pair(x1,x2)	weight: (/ 3 16) + x1
#U246(x1)	weight: 0
  U192(x1,x2)	weight: (/ 3 32)
   U24(x1,x2)	weight: (/ 1 32)
  U106(x1)	weight: x1
#take(x1,x2)	weight: 0
isPLNatKind(x1)	weight: (/ 1 32)
 #U24(x1,x2)	weight: 0
#U244(x1,x2,x3)	weight: 0
  U242(x1,x2,x3)	weight: x1 + x2 + x3
#U181(x1,x2)	weight: 0
  U262(x1)	weight: 0
  U244(x1,x2,x3)	weight: x1 + x2 + x3
  U272(x1)	weight: 0
   U56(x1)	weight: (/ 1 4)
isPLNat(x1)	weight: x1
   U42(x1,x2,x3)	weight: (/ 1 8) + x3
   U91(x1,x2)	weight: (/ 7 32)
  U221(x1)	weight: (/ 1 32) + x1
  U293(x1,x2,x3)	weight: x1
#U101(x1,x2,x3)	weight: 0
activate(x1)	weight: (/ 1 8)
  U325(x1,x2,x3,x4)	weight: x4
 #U82(x1,x2)	weight: 0
#U254(x1,x2,x3)	weight: 0
  take(x1,x2)	weight: (/ 1 32) + x1
#U183(x1)	weight: 0
#U104(x1,x2,x3)	weight: 0
   U71(x1,x2)	weight: (/ 7 32)
 #U81(x1,x2)	weight: 0
#U322(x1,x2,x3,x4)	weight: 0
 #U92(x1,x2)	weight: 0
#U323(x1,x2,x3,x4)	weight: 0
  U131(x1)	weight: x1
  U206(x1)	weight: (/ 3 16)
#U243(x1,x2,x3)	weight: 0
#U334(x1,x2)	weight: 0
#U321(x1,x2,x3,x4)	weight: 0
  U101(x1,x2,x3)	weight: (/ 3 32) + x1 + x3
  U255(x1,x2)	weight: x1 + x2
  pair(x1,x2)	weight: (/ 5 32)
#U231(x1,x2)	weight: 0
   fst(x1)	weight: (/ 5 32)
  U111(x1,x2)	weight: (/ 1 32)
   U43(x1,x2,x3)	weight: (/ 1 32) + x3
 #U93(x1)	weight: 0
#activate(x1)	weight: x1
#U342(x1,x2,x3)	weight: 0
#U245(x1,x2)	weight: 0
  U103(x1,x2,x3)	weight: (/ 1 32)
 #U23(x1,x2,x3)	weight: 0
 #U53(x1,x2,x3)	weight: 0
  U281(x1,x2)	weight: (/ 1 16) + x2
natsFrom(x1)	weight: (/ 1 32) + x1
#head(x1)	weight: 0
#U331(x1,x2,x3)	weight: 0
   U44(x1,x2,x3)	weight: (/ 1 16)
   U55(x1,x2)	weight: (/ 7 32) + x2
#U106(x1)	weight: 0
 #U43(x1,x2,x3)	weight: 0
#U121(x1,x2)	weight: 0
  U253(x1,x2,x3)	weight: x1 + x2 + x3
  U312(x1,x2)	weight: (/ 3 32)
  U341(x1,x2,x3)	weight: (/ 13 32) + x3
   U23(x1,x2,x3)	weight: x2 + x3
  U292(x1,x2,x3)	weight: (/ 5 32) + x2 + x3
  U342(x1,x2,x3)	weight: (/ 5 16) + x1 + x3
   U63(x1)	weight: (/ 1 8) + x1
  U172(x1)	weight: x1
   U93(x1)	weight: (/ 3 32) + x1
#U344(x1,x2,x3)	weight: 0
#U241(x1,x2,x3)	weight: 0
isNaturalKind(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 32) + x2
  U326(x1,x2,x3,x4)	weight: (/ 5 32) + x3 + x4
#U131(x1)	weight: 0
#U311(x1,x2)	weight: 0
   U72(x1,x2)	weight: (/ 1 4)
 #U13(x1,x2,x3)	weight: 0
 #fst(x1)	weight: 0
  U241(x1,x2,x3)	weight: (/ 1 16) + x1 + x3
   U34(x1,x2)	weight: (/ 3 32)
#U271(x1,x2)	weight: 0
n__nil()	weight: 0
 #U52(x1,x2,x3)	weight: 0
#U103(x1,x2,x3)	weight: 0
   U12(x1,x2,x3)	weight: (/ 1 2) + x2 + x3
  U271(x1,x2)	weight: 0
#isPLNatKind(x1)	weight: 0
#U282(x1,x2)	weight: 0
 #U33(x1,x2,x3)	weight: 0
#U253(x1,x2,x3)	weight: 0
#U202(x1,x2,x3)	weight: 0
#U205(x1,x2)	weight: 0
n__natsFrom(x1)	weight: (/ 1 16) + x1
isNatural(x1)	weight: (/ 1 32)
  U302(x1,x2)	weight: (/ 1 32)
   U54(x1,x2,x3)	weight: (/ 5 16)
  U232(x1)	weight: (/ 1 16)
n__snd(x1)	weight: (/ 3 16)
  U205(x1,x2)	weight: (/ 5 32) + x1
#U252(x1,x2,x3)	weight: 0
 #U44(x1,x2,x3)	weight: 0
  U201(x1,x2,x3)	weight: (/ 1 16)
  n__s(x1)	weight: (/ 3 16) + x1
 #U54(x1,x2,x3)	weight: 0
  U104(x1,x2,x3)	weight: x2
n__splitAt(x1,x2)	weight: (/ 1 16) + x1 + x2
#U242(x1,x2,x3)	weight: 0
 #U42(x1,x2,x3)	weight: 0
#U141(x1)	weight: 0
  U252(x1,x2,x3)	weight: (/ 1 32)
 #U12(x1,x2,x3)	weight: 0
  U141(x1)	weight: 0
#U171(x1,x2)	weight: 0
  tail(x1)	weight: (/ 1 32) + x1
 #U62(x1,x2)	weight: 0
   U83(x1)	weight: (/ 1 4)
#U327(x1,x2)	weight: 0
#U301(x1,x2,x3)	weight: 0
     0()	weight: 0
  U294(x1,x2,x3)	weight: (/ 5 32) + x3
  U191(x1,x2)	weight: (/ 1 16)
 #U14(x1,x2,x3)	weight: x1
  U343(x1,x2,x3)	weight: (/ 7 32) + x3
n__take(x1,x2)	weight: (/ 1 16) + x2
 #sel(x1,x2)	weight: 0
   U73(x1)	weight: (/ 1 4) + x1
  U332(x1,x2)	weight: (/ 3 32) + x2
#U102(x1,x2,x3)	weight: 0
  U171(x1,x2)	weight: (/ 1 32)
#isLNat(x1)	weight: 0
  U202(x1,x2,x3)	weight: (/ 3 32)
   sel(x1,x2)	weight: (/ 1 32) + x2
 #U73(x1)	weight: 0
   #s(x1)	weight: 0
#U105(x1,x2)	weight: 0
afterNth(x1,x2)	weight: (/ 1 32) + x2
n__cons(x1,x2)	weight: (/ 1 16) + x1 + x2
#U211(x1)	weight: 0
#isPLNat(x1)	weight: 0
   nil()	weight: 0
isLNat(x1)	weight: (/ 3 16)
#U304(x1,x2)	weight: 0
  U246(x1)	weight: x1
   U62(x1,x2)	weight: (/ 7 32) + x1
n__sel(x1,x2)	weight: (/ 1 16) + x1 + x2
#tail(x1)	weight: 0
 #U63(x1)	weight: 0
#isNaturalKind(x1)	weight: 0
  U304(x1,x2)	weight: (/ 3 32)
   U45(x1,x2)	weight: (/ 1 16) + x1
#U182(x1,x2)	weight: 0
#splitAt(x1,x2)	weight: 0
  U151(x1)	weight: (/ 1 32)
 #nil()	weight: 0
n__tail(x1)	weight: (/ 1 16) + x1
#U292(x1,x2,x3)	weight: 0
  U334(x1,x2)	weight: (/ 1 32)
#U341(x1,x2,x3)	weight: 0
#afterNth(x1,x2)	weight: 0
#U262(x1)	weight: 0
#U192(x1,x2)	weight: 0
#U111(x1,x2)	weight: 0
#U326(x1,x2,x3,x4)	weight: 0
   U32(x1,x2,x3)	weight: x2
#U221(x1)	weight: 0
#U206(x1)	weight: 0
   U33(x1,x2,x3)	weight: x2 + x3
#U302(x1,x2)	weight: 0
#U232(x1)	weight: 0
  n__0()	weight: 0
 #U46(x1)	weight: 0
#U251(x1,x2,x3)	weight: 0
n__afterNth(x1,x2)	weight: (/ 1 16) + x2
 #U34(x1,x2)	weight: 0
isLNatKind(x1)	weight: (/ 1 32)
   U14(x1,x2,x3)	weight: x2 + x3
  U211(x1)	weight: x1
 #U56(x1)	weight: 0
#U281(x1,x2)	weight: 0
#U343(x1,x2,x3)	weight: 0
  U203(x1,x2,x3)	weight: (/ 1 8)
  U327(x1,x2)	weight: (/ 5 32)
   U46(x1)	weight: (/ 3 32)
  U251(x1,x2,x3)	weight: x1 + x3
#U291(x1,x2,x3)	weight: 0
   U52(x1,x2,x3)	weight: (/ 1 4)
   U61(x1,x2)	weight: (/ 7 32)
 #U51(x1,x2,x3)	weight: 0
n__fst(x1)	weight: (/ 3 16)
 #U11(x1,x2,x3)	weight: 0
   U31(x1,x2,x3)	weight: (/ 3 32) + x2
  U183(x1)	weight: x1
  U245(x1,x2)	weight: x1
   U92(x1,x2)	weight: (/ 1 4)
  head(x1)	weight: (/ 1 32) + x1
  U112(x1)	weight: x1
#U193(x1)	weight: 0
 #snd(x1)	weight: 0
 #U41(x1,x2,x3)	weight: 0
  cons(x1,x2)	weight: (/ 1 32) + x1 + x2
  U323(x1,x2,x3,x4)	weight: x2 + x4
#U294(x1,x2,x3)	weight: 0
#U325(x1,x2,x3,x4)	weight: 0
#natsFrom(x1)	weight: 0
  U102(x1,x2,x3)	weight: x1 + x2
   snd(x1)	weight: (/ 5 32)
#U191(x1,x2)	weight: 0
  U256(x1)	weight: x1
#U293(x1,x2,x3)	weight: 0
 #U21(x1,x2,x3)	weight: 0
   U81(x1,x2)	weight: (/ 7 32)
   U82(x1,x2)	weight: (/ 7 32) + x1
 #U22(x1,x2,x3)	weight: 0
#U112(x1)	weight: 0
    tt()	weight: 0
#U303(x1,x2)	weight: 0
 #U71(x1,x2)	weight: 0
   U13(x1,x2,x3)	weight: (/ 7 32) + x1 + x3
#U151(x1)	weight: 0
#isNatural(x1)	weight: 0
  U321(x1,x2,x3,x4)	weight: x2 + x4
#pair(x1,x2)	weight: 0
   U22(x1,x2,x3)	weight: x2 + x3
n__head(x1)	weight: (/ 1 16) + x1
 #U45(x1,x2)	weight: 0
   U51(x1,x2,x3)	weight: (/ 7 32)
#U161(x1)	weight: 0
#U312(x1,x2)	weight: 0
#U172(x1)	weight: 0
  U311(x1,x2)	weight: (/ 1 16)
  U322(x1,x2,x3,x4)	weight: x1 + x4
  U344(x1,x2,x3)	weight: (/ 1 8) + x3
#U261(x1,x2)	weight: 0
#U203(x1,x2,x3)	weight: 0
#U122(x1)	weight: 0
   U53(x1,x2,x3)	weight: (/ 9 32)
   U41(x1,x2,x3)	weight: (/ 7 32) + x1
 #U31(x1,x2,x3)	weight: 0
#U332(x1,x2)	weight: 0
 #U91(x1,x2)	weight: 0
 #U55(x1,x2)	weight: 0
  U282(x1,x2)	weight: (/ 3 32)
  U121(x1,x2)	weight: 0
#U204(x1,x2,x3)	weight: 0
 #U61(x1,x2)	weight: 0
  U181(x1,x2)	weight: (/ 1 16)
  U324(x1,x2,x3,x4)	weight: x1 + x2 + x4
  U331(x1,x2,x3)	weight: (/ 1 16) + x1
  U122(x1)	weight: 0
#U333(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #136
Number of SCCs: 5, DPs: 19, edges: 19
	SCC { #389 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS.