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