Input TRS:
    1: U101(tt(),V1,V2) -> U102(isNatural(activate(V1)),activate(V2))
    2: U102(tt(),V2) -> U103(isLNat(activate(V2)))
    3: U103(tt()) -> tt()
    4: U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
    5: U111(tt(),V1) -> U112(isLNat(activate(V1)))
    6: U112(tt()) -> tt()
    7: U121(tt(),V1) -> U122(isNatural(activate(V1)))
    8: U122(tt()) -> tt()
    9: U131(tt(),V1,V2) -> U132(isNatural(activate(V1)),activate(V2))
    10: U132(tt(),V2) -> U133(isLNat(activate(V2)))
    11: U133(tt()) -> tt()
    12: U141(tt(),V1,V2) -> U142(isLNat(activate(V1)),activate(V2))
    13: U142(tt(),V2) -> U143(isLNat(activate(V2)))
    14: U143(tt()) -> tt()
    15: U151(tt(),V1,V2) -> U152(isNatural(activate(V1)),activate(V2))
    16: U152(tt(),V2) -> U153(isLNat(activate(V2)))
    17: U153(tt()) -> tt()
    18: U161(tt(),N) -> cons(activate(N),n__natsFrom(s(activate(N))))
    19: U171(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
    20: U181(tt(),Y) -> activate(Y)
    21: U191(tt(),XS) -> pair(nil(),activate(XS))
    22: U201(tt(),N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X))
    23: U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
    24: U21(tt(),X) -> activate(X)
    25: U211(tt(),XS) -> activate(XS)
    26: U221(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
    27: U31(tt(),N) -> activate(N)
    28: U41(tt(),V1,V2) -> U42(isNatural(activate(V1)),activate(V2))
    29: U42(tt(),V2) -> U43(isLNat(activate(V2)))
    30: U43(tt()) -> tt()
    31: U51(tt(),V1,V2) -> U52(isNatural(activate(V1)),activate(V2))
    32: U52(tt(),V2) -> U53(isLNat(activate(V2)))
    33: U53(tt()) -> tt()
    34: U61(tt(),V1) -> U62(isPLNat(activate(V1)))
    35: U62(tt()) -> tt()
    36: U71(tt(),V1) -> U72(isNatural(activate(V1)))
    37: U72(tt()) -> tt()
    38: U81(tt(),V1) -> U82(isPLNat(activate(V1)))
    39: U82(tt()) -> tt()
    40: U91(tt(),V1) -> U92(isLNat(activate(V1)))
    41: U92(tt()) -> tt()
    42: afterNth(N,XS) -> U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
    43: and(tt(),X) -> activate(X)
    44: fst(pair(X,Y)) -> U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X)
    45: head(cons(N,XS)) -> U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS)))),N)
    46: isLNat(n__nil()) -> tt()
    47: isLNat(n__afterNth(V1,V2)) -> U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    48: isLNat(n__cons(V1,V2)) -> U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    49: isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1))
    50: isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1))
    51: isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1))
    52: isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1))
    53: isLNat(n__take(V1,V2)) -> U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    54: isLNatKind(n__nil()) -> tt()
    55: isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    56: isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    57: isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1))
    58: isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1))
    59: isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1))
    60: isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1))
    61: isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    62: isNatural(n__0()) -> tt()
    63: isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1))
    64: isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1))
    65: isNatural(n__sel(V1,V2)) -> U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    66: isNaturalKind(n__0()) -> tt()
    67: isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1))
    68: isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1))
    69: isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    70: isPLNat(n__pair(V1,V2)) -> U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    71: isPLNat(n__splitAt(V1,V2)) -> U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
    72: isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
    73: isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
    74: natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N)
    75: sel(N,XS) -> U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
    76: snd(pair(X,Y)) -> U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y)
    77: splitAt(0(),XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS)
    78: splitAt(s(N),cons(X,XS)) -> U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS))))),N,X,activate(XS))
    79: tail(cons(N,XS)) -> U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS)))),activate(XS))
    80: take(N,XS) -> U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
    81: natsFrom(X) -> n__natsFrom(X)
    82: isNaturalKind(X) -> n__isNaturalKind(X)
    83: and(X1,X2) -> n__and(X1,X2)
    84: isLNatKind(X) -> n__isLNatKind(X)
    85: nil() -> n__nil()
    86: afterNth(X1,X2) -> n__afterNth(X1,X2)
    87: cons(X1,X2) -> n__cons(X1,X2)
    88: fst(X) -> n__fst(X)
    89: snd(X) -> n__snd(X)
    90: tail(X) -> n__tail(X)
    91: take(X1,X2) -> n__take(X1,X2)
    92: 0() -> n__0()
    93: head(X) -> n__head(X)
    94: s(X) -> n__s(X)
    95: sel(X1,X2) -> n__sel(X1,X2)
    96: pair(X1,X2) -> n__pair(X1,X2)
    97: splitAt(X1,X2) -> n__splitAt(X1,X2)
    98: activate(n__natsFrom(X)) -> natsFrom(X)
    99: activate(n__isNaturalKind(X)) -> isNaturalKind(X)
    100: activate(n__and(X1,X2)) -> and(X1,X2)
    101: activate(n__isLNatKind(X)) -> isLNatKind(X)
    102: activate(n__nil()) -> nil()
    103: activate(n__afterNth(X1,X2)) -> afterNth(X1,X2)
    104: activate(n__cons(X1,X2)) -> cons(X1,X2)
    105: activate(n__fst(X)) -> fst(X)
    106: activate(n__snd(X)) -> snd(X)
    107: activate(n__tail(X)) -> tail(X)
    108: activate(n__take(X1,X2)) -> take(X1,X2)
    109: activate(n__0()) -> 0()
    110: activate(n__head(X)) -> head(X)
    111: activate(n__s(X)) -> s(X)
    112: activate(n__sel(X1,X2)) -> sel(X1,X2)
    113: activate(n__pair(X1,X2)) -> pair(X1,X2)
    114: activate(n__splitAt(X1,X2)) -> splitAt(X1,X2)
    115: activate(X) -> X
Number of strict rules: 115
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #U102(tt(),V2) -> #U103(isLNat(activate(V2)))
   #2: #U102(tt(),V2) -> #isLNat(activate(V2))
   #3: #U102(tt(),V2) -> #activate(V2)
   #4: #and(tt(),X) -> #activate(X)
   #5: #U42(tt(),V2) -> #U43(isLNat(activate(V2)))
   #6: #U42(tt(),V2) -> #isLNat(activate(V2))
   #7: #U42(tt(),V2) -> #activate(V2)
   #8: #afterNth(N,XS) -> #U11(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
   #9: #afterNth(N,XS) -> #and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
   #10: #afterNth(N,XS) -> #and(isNatural(N),n__isNaturalKind(N))
   #11: #afterNth(N,XS) -> #isNatural(N)
   #12: #afterNth(N,XS) -> #isLNat(XS)
   #13: #activate(n__splitAt(X1,X2)) -> #splitAt(X1,X2)
   #14: #activate(n__isNaturalKind(X)) -> #isNaturalKind(X)
   #15: #isPLNatKind(n__splitAt(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #16: #isPLNatKind(n__splitAt(V1,V2)) -> #isNaturalKind(activate(V1))
   #17: #isPLNatKind(n__splitAt(V1,V2)) -> #activate(V1)
   #18: #isPLNatKind(n__splitAt(V1,V2)) -> #activate(V2)
   #19: #isLNat(n__afterNth(V1,V2)) -> #U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   #20: #isLNat(n__afterNth(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #21: #isLNat(n__afterNth(V1,V2)) -> #isNaturalKind(activate(V1))
   #22: #isLNat(n__afterNth(V1,V2)) -> #activate(V1)
   #23: #isLNat(n__afterNth(V1,V2)) -> #activate(V2)
   #24: #isLNat(n__afterNth(V1,V2)) -> #activate(V1)
   #25: #isLNat(n__afterNth(V1,V2)) -> #activate(V2)
   #26: #isLNat(n__take(V1,V2)) -> #U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   #27: #isLNat(n__take(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #28: #isLNat(n__take(V1,V2)) -> #isNaturalKind(activate(V1))
   #29: #isLNat(n__take(V1,V2)) -> #activate(V1)
   #30: #isLNat(n__take(V1,V2)) -> #activate(V2)
   #31: #isLNat(n__take(V1,V2)) -> #activate(V1)
   #32: #isLNat(n__take(V1,V2)) -> #activate(V2)
   #33: #isPLNat(n__splitAt(V1,V2)) -> #U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   #34: #isPLNat(n__splitAt(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #35: #isPLNat(n__splitAt(V1,V2)) -> #isNaturalKind(activate(V1))
   #36: #isPLNat(n__splitAt(V1,V2)) -> #activate(V1)
   #37: #isPLNat(n__splitAt(V1,V2)) -> #activate(V2)
   #38: #isPLNat(n__splitAt(V1,V2)) -> #activate(V1)
   #39: #isPLNat(n__splitAt(V1,V2)) -> #activate(V2)
   #40: #isLNat(n__cons(V1,V2)) -> #U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   #41: #isLNat(n__cons(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #42: #isLNat(n__cons(V1,V2)) -> #isNaturalKind(activate(V1))
   #43: #isLNat(n__cons(V1,V2)) -> #activate(V1)
   #44: #isLNat(n__cons(V1,V2)) -> #activate(V2)
   #45: #isLNat(n__cons(V1,V2)) -> #activate(V1)
   #46: #isLNat(n__cons(V1,V2)) -> #activate(V2)
   #47: #sel(N,XS) -> #U171(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
   #48: #sel(N,XS) -> #and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
   #49: #sel(N,XS) -> #and(isNatural(N),n__isNaturalKind(N))
   #50: #sel(N,XS) -> #isNatural(N)
   #51: #sel(N,XS) -> #isLNat(XS)
   #52: #activate(n__sel(X1,X2)) -> #sel(X1,X2)
   #53: #natsFrom(N) -> #U161(and(isNatural(N),n__isNaturalKind(N)),N)
   #54: #natsFrom(N) -> #and(isNatural(N),n__isNaturalKind(N))
   #55: #natsFrom(N) -> #isNatural(N)
   #56: #isLNatKind(n__natsFrom(V1)) -> #isNaturalKind(activate(V1))
   #57: #isLNatKind(n__natsFrom(V1)) -> #activate(V1)
   #58: #activate(n__pair(X1,X2)) -> #pair(X1,X2)
   #59: #isLNatKind(n__take(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #60: #isLNatKind(n__take(V1,V2)) -> #isNaturalKind(activate(V1))
   #61: #isLNatKind(n__take(V1,V2)) -> #activate(V1)
   #62: #isLNatKind(n__take(V1,V2)) -> #activate(V2)
   #63: #U81(tt(),V1) -> #U82(isPLNat(activate(V1)))
   #64: #U81(tt(),V1) -> #isPLNat(activate(V1))
   #65: #U81(tt(),V1) -> #activate(V1)
   #66: #isLNatKind(n__snd(V1)) -> #isPLNatKind(activate(V1))
   #67: #isLNatKind(n__snd(V1)) -> #activate(V1)
   #68: #activate(n__head(X)) -> #head(X)
   #69: #isLNatKind(n__afterNth(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #70: #isLNatKind(n__afterNth(V1,V2)) -> #isNaturalKind(activate(V1))
   #71: #isLNatKind(n__afterNth(V1,V2)) -> #activate(V1)
   #72: #isLNatKind(n__afterNth(V1,V2)) -> #activate(V2)
   #73: #isNaturalKind(n__head(V1)) -> #isLNatKind(activate(V1))
   #74: #isNaturalKind(n__head(V1)) -> #activate(V1)
   #75: #U91(tt(),V1) -> #U92(isLNat(activate(V1)))
   #76: #U91(tt(),V1) -> #isLNat(activate(V1))
   #77: #U91(tt(),V1) -> #activate(V1)
   #78: #activate(n__tail(X)) -> #tail(X)
   #79: #isLNat(n__snd(V1)) -> #U81(isPLNatKind(activate(V1)),activate(V1))
   #80: #isLNat(n__snd(V1)) -> #isPLNatKind(activate(V1))
   #81: #isLNat(n__snd(V1)) -> #activate(V1)
   #82: #isLNat(n__snd(V1)) -> #activate(V1)
   #83: #U142(tt(),V2) -> #U143(isLNat(activate(V2)))
   #84: #U142(tt(),V2) -> #isLNat(activate(V2))
   #85: #U142(tt(),V2) -> #activate(V2)
   #86: #U131(tt(),V1,V2) -> #U132(isNatural(activate(V1)),activate(V2))
   #87: #U131(tt(),V1,V2) -> #isNatural(activate(V1))
   #88: #U131(tt(),V1,V2) -> #activate(V1)
   #89: #U131(tt(),V1,V2) -> #activate(V2)
   #90: #activate(n__natsFrom(X)) -> #natsFrom(X)
   #91: #isLNatKind(n__fst(V1)) -> #isPLNatKind(activate(V1))
   #92: #isLNatKind(n__fst(V1)) -> #activate(V1)
   #93: #snd(pair(X,Y)) -> #U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),Y)
   #94: #snd(pair(X,Y)) -> #and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y)))
   #95: #snd(pair(X,Y)) -> #and(isLNat(X),n__isLNatKind(X))
   #96: #snd(pair(X,Y)) -> #isLNat(X)
   #97: #snd(pair(X,Y)) -> #isLNat(Y)
   #98: #activate(n__0()) -> #0()
   #99: #U21(tt(),X) -> #activate(X)
   #100: #isPLNat(n__pair(V1,V2)) -> #U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   #101: #isPLNat(n__pair(V1,V2)) -> #and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
   #102: #isPLNat(n__pair(V1,V2)) -> #isLNatKind(activate(V1))
   #103: #isPLNat(n__pair(V1,V2)) -> #activate(V1)
   #104: #isPLNat(n__pair(V1,V2)) -> #activate(V2)
   #105: #isPLNat(n__pair(V1,V2)) -> #activate(V1)
   #106: #isPLNat(n__pair(V1,V2)) -> #activate(V2)
   #107: #U202(pair(YS,ZS),X) -> #pair(cons(activate(X),YS),ZS)
   #108: #U202(pair(YS,ZS),X) -> #cons(activate(X),YS)
   #109: #U202(pair(YS,ZS),X) -> #activate(X)
   #110: #splitAt(s(N),cons(X,XS)) -> #U201(and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS))))),N,X,activate(XS))
   #111: #splitAt(s(N),cons(X,XS)) -> #and(and(isNatural(N),n__isNaturalKind(N)),n__and(and(isNatural(X),n__isNaturalKind(X)),n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS)))))
   #112: #splitAt(s(N),cons(X,XS)) -> #and(isNatural(N),n__isNaturalKind(N))
   #113: #splitAt(s(N),cons(X,XS)) -> #isNatural(N)
   #114: #splitAt(s(N),cons(X,XS)) -> #and(isNatural(X),n__isNaturalKind(X))
   #115: #splitAt(s(N),cons(X,XS)) -> #isNatural(X)
   #116: #splitAt(s(N),cons(X,XS)) -> #isLNat(activate(XS))
   #117: #splitAt(s(N),cons(X,XS)) -> #activate(XS)
   #118: #splitAt(s(N),cons(X,XS)) -> #activate(XS)
   #119: #splitAt(s(N),cons(X,XS)) -> #activate(XS)
   #120: #head(cons(N,XS)) -> #U31(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS)))),N)
   #121: #head(cons(N,XS)) -> #and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS))))
   #122: #head(cons(N,XS)) -> #and(isNatural(N),n__isNaturalKind(N))
   #123: #head(cons(N,XS)) -> #isNatural(N)
   #124: #head(cons(N,XS)) -> #isLNat(activate(XS))
   #125: #head(cons(N,XS)) -> #activate(XS)
   #126: #head(cons(N,XS)) -> #activate(XS)
   #127: #isNaturalKind(n__sel(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #128: #isNaturalKind(n__sel(V1,V2)) -> #isNaturalKind(activate(V1))
   #129: #isNaturalKind(n__sel(V1,V2)) -> #activate(V1)
   #130: #isNaturalKind(n__sel(V1,V2)) -> #activate(V2)
   #131: #activate(n__isLNatKind(X)) -> #isLNatKind(X)
   #132: #U141(tt(),V1,V2) -> #U142(isLNat(activate(V1)),activate(V2))
   #133: #U141(tt(),V1,V2) -> #isLNat(activate(V1))
   #134: #U141(tt(),V1,V2) -> #activate(V1)
   #135: #U141(tt(),V1,V2) -> #activate(V2)
   #136: #U51(tt(),V1,V2) -> #U52(isNatural(activate(V1)),activate(V2))
   #137: #U51(tt(),V1,V2) -> #isNatural(activate(V1))
   #138: #U51(tt(),V1,V2) -> #activate(V1)
   #139: #U51(tt(),V1,V2) -> #activate(V2)
   #140: #tail(cons(N,XS)) -> #U211(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS)))),activate(XS))
   #141: #tail(cons(N,XS)) -> #and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS))))
   #142: #tail(cons(N,XS)) -> #and(isNatural(N),n__isNaturalKind(N))
   #143: #tail(cons(N,XS)) -> #isNatural(N)
   #144: #tail(cons(N,XS)) -> #isLNat(activate(XS))
   #145: #tail(cons(N,XS)) -> #activate(XS)
   #146: #tail(cons(N,XS)) -> #activate(XS)
   #147: #tail(cons(N,XS)) -> #activate(XS)
   #148: #isLNatKind(n__cons(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #149: #isLNatKind(n__cons(V1,V2)) -> #isNaturalKind(activate(V1))
   #150: #isLNatKind(n__cons(V1,V2)) -> #activate(V1)
   #151: #isLNatKind(n__cons(V1,V2)) -> #activate(V2)
   #152: #activate(n__s(X)) -> #s(X)
   #153: #activate(n__snd(X)) -> #snd(X)
   #154: #isLNat(n__tail(V1)) -> #U91(isLNatKind(activate(V1)),activate(V1))
   #155: #isLNat(n__tail(V1)) -> #isLNatKind(activate(V1))
   #156: #isLNat(n__tail(V1)) -> #activate(V1)
   #157: #isLNat(n__tail(V1)) -> #activate(V1)
   #158: #isLNat(n__fst(V1)) -> #U61(isPLNatKind(activate(V1)),activate(V1))
   #159: #isLNat(n__fst(V1)) -> #isPLNatKind(activate(V1))
   #160: #isLNat(n__fst(V1)) -> #activate(V1)
   #161: #isLNat(n__fst(V1)) -> #activate(V1)
   #162: #U211(tt(),XS) -> #activate(XS)
   #163: #activate(n__take(X1,X2)) -> #take(X1,X2)
   #164: #U181(tt(),Y) -> #activate(Y)
   #165: #U121(tt(),V1) -> #U122(isNatural(activate(V1)))
   #166: #U121(tt(),V1) -> #isNatural(activate(V1))
   #167: #U121(tt(),V1) -> #activate(V1)
   #168: #U132(tt(),V2) -> #U133(isLNat(activate(V2)))
   #169: #U132(tt(),V2) -> #isLNat(activate(V2))
   #170: #U132(tt(),V2) -> #activate(V2)
   #171: #isNatural(n__s(V1)) -> #U121(isNaturalKind(activate(V1)),activate(V1))
   #172: #isNatural(n__s(V1)) -> #isNaturalKind(activate(V1))
   #173: #isNatural(n__s(V1)) -> #activate(V1)
   #174: #isNatural(n__s(V1)) -> #activate(V1)
   #175: #isPLNatKind(n__pair(V1,V2)) -> #and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2)))
   #176: #isPLNatKind(n__pair(V1,V2)) -> #isLNatKind(activate(V1))
   #177: #isPLNatKind(n__pair(V1,V2)) -> #activate(V1)
   #178: #isPLNatKind(n__pair(V1,V2)) -> #activate(V2)
   #179: #U111(tt(),V1) -> #U112(isLNat(activate(V1)))
   #180: #U111(tt(),V1) -> #isLNat(activate(V1))
   #181: #U111(tt(),V1) -> #activate(V1)
   #182: #fst(pair(X,Y)) -> #U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X)
   #183: #fst(pair(X,Y)) -> #and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y)))
   #184: #fst(pair(X,Y)) -> #and(isLNat(X),n__isLNatKind(X))
   #185: #fst(pair(X,Y)) -> #isLNat(X)
   #186: #fst(pair(X,Y)) -> #isLNat(Y)
   #187: #isNatural(n__sel(V1,V2)) -> #U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1),activate(V2))
   #188: #isNatural(n__sel(V1,V2)) -> #and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2)))
   #189: #isNatural(n__sel(V1,V2)) -> #isNaturalKind(activate(V1))
   #190: #isNatural(n__sel(V1,V2)) -> #activate(V1)
   #191: #isNatural(n__sel(V1,V2)) -> #activate(V2)
   #192: #isNatural(n__sel(V1,V2)) -> #activate(V1)
   #193: #isNatural(n__sel(V1,V2)) -> #activate(V2)
   #194: #U41(tt(),V1,V2) -> #U42(isNatural(activate(V1)),activate(V2))
   #195: #U41(tt(),V1,V2) -> #isNatural(activate(V1))
   #196: #U41(tt(),V1,V2) -> #activate(V1)
   #197: #U41(tt(),V1,V2) -> #activate(V2)
   #198: #U201(tt(),N,X,XS) -> #U202(splitAt(activate(N),activate(XS)),activate(X))
   #199: #U201(tt(),N,X,XS) -> #splitAt(activate(N),activate(XS))
   #200: #U201(tt(),N,X,XS) -> #activate(N)
   #201: #U201(tt(),N,X,XS) -> #activate(XS)
   #202: #U201(tt(),N,X,XS) -> #activate(X)
   #203: #U61(tt(),V1) -> #U62(isPLNat(activate(V1)))
   #204: #U61(tt(),V1) -> #isPLNat(activate(V1))
   #205: #U61(tt(),V1) -> #activate(V1)
   #206: #U31(tt(),N) -> #activate(N)
   #207: #isLNatKind(n__tail(V1)) -> #isLNatKind(activate(V1))
   #208: #isLNatKind(n__tail(V1)) -> #activate(V1)
   #209: #U52(tt(),V2) -> #U53(isLNat(activate(V2)))
   #210: #U52(tt(),V2) -> #isLNat(activate(V2))
   #211: #U52(tt(),V2) -> #activate(V2)
   #212: #U171(tt(),N,XS) -> #head(afterNth(activate(N),activate(XS)))
   #213: #U171(tt(),N,XS) -> #afterNth(activate(N),activate(XS))
   #214: #U171(tt(),N,XS) -> #activate(N)
   #215: #U171(tt(),N,XS) -> #activate(XS)
   #216: #isNatural(n__head(V1)) -> #U111(isLNatKind(activate(V1)),activate(V1))
   #217: #isNatural(n__head(V1)) -> #isLNatKind(activate(V1))
   #218: #isNatural(n__head(V1)) -> #activate(V1)
   #219: #isNatural(n__head(V1)) -> #activate(V1)
   #220: #activate(n__fst(X)) -> #fst(X)
   #221: #U221(tt(),N,XS) -> #fst(splitAt(activate(N),activate(XS)))
   #222: #U221(tt(),N,XS) -> #splitAt(activate(N),activate(XS))
   #223: #U221(tt(),N,XS) -> #activate(N)
   #224: #U221(tt(),N,XS) -> #activate(XS)
   #225: #activate(n__and(X1,X2)) -> #and(X1,X2)
   #226: #isNaturalKind(n__s(V1)) -> #isNaturalKind(activate(V1))
   #227: #isNaturalKind(n__s(V1)) -> #activate(V1)
   #228: #U71(tt(),V1) -> #U72(isNatural(activate(V1)))
   #229: #U71(tt(),V1) -> #isNatural(activate(V1))
   #230: #U71(tt(),V1) -> #activate(V1)
   #231: #U191(tt(),XS) -> #pair(nil(),activate(XS))
   #232: #U191(tt(),XS) -> #nil()
   #233: #U191(tt(),XS) -> #activate(XS)
   #234: #U152(tt(),V2) -> #U153(isLNat(activate(V2)))
   #235: #U152(tt(),V2) -> #isLNat(activate(V2))
   #236: #U152(tt(),V2) -> #activate(V2)
   #237: #splitAt(0(),XS) -> #U191(and(isLNat(XS),n__isLNatKind(XS)),XS)
   #238: #splitAt(0(),XS) -> #and(isLNat(XS),n__isLNatKind(XS))
   #239: #splitAt(0(),XS) -> #isLNat(XS)
   #240: #U101(tt(),V1,V2) -> #U102(isNatural(activate(V1)),activate(V2))
   #241: #U101(tt(),V1,V2) -> #isNatural(activate(V1))
   #242: #U101(tt(),V1,V2) -> #activate(V1)
   #243: #U101(tt(),V1,V2) -> #activate(V2)
   #244: #U151(tt(),V1,V2) -> #U152(isNatural(activate(V1)),activate(V2))
   #245: #U151(tt(),V1,V2) -> #isNatural(activate(V1))
   #246: #U151(tt(),V1,V2) -> #activate(V1)
   #247: #U151(tt(),V1,V2) -> #activate(V2)
   #248: #activate(n__nil()) -> #nil()
   #249: #activate(n__afterNth(X1,X2)) -> #afterNth(X1,X2)
   #250: #U11(tt(),N,XS) -> #snd(splitAt(activate(N),activate(XS)))
   #251: #U11(tt(),N,XS) -> #splitAt(activate(N),activate(XS))
   #252: #U11(tt(),N,XS) -> #activate(N)
   #253: #U11(tt(),N,XS) -> #activate(XS)
   #254: #activate(n__cons(X1,X2)) -> #cons(X1,X2)
   #255: #take(N,XS) -> #U221(and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS))),N,XS)
   #256: #take(N,XS) -> #and(and(isNatural(N),n__isNaturalKind(N)),n__and(isLNat(XS),n__isLNatKind(XS)))
   #257: #take(N,XS) -> #and(isNatural(N),n__isNaturalKind(N))
   #258: #take(N,XS) -> #isNatural(N)
   #259: #take(N,XS) -> #isLNat(XS)
   #260: #isLNat(n__natsFrom(V1)) -> #U71(isNaturalKind(activate(V1)),activate(V1))
   #261: #isLNat(n__natsFrom(V1)) -> #isNaturalKind(activate(V1))
   #262: #isLNat(n__natsFrom(V1)) -> #activate(V1)
   #263: #isLNat(n__natsFrom(V1)) -> #activate(V1)
   #264: #U161(tt(),N) -> #cons(activate(N),n__natsFrom(s(activate(N))))
   #265: #U161(tt(),N) -> #activate(N)
   #266: #U161(tt(),N) -> #s(activate(N))
   #267: #U161(tt(),N) -> #activate(N)
Number of SCCs: 1, DPs: 244, edges: 2755
	SCC { #2..4 #6..57 #59..62 #64..74 #76..82 #84..97 #99..106 #109..151 #153..164 #166 #167 #169..178 #180..202 #204..208 #210..227 #229 #230 #233 #235..247 #249..253 #255..263 #265 #267 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
#U201(x1,x2,x3,x4)	weight: max{(/ 17 64) + x4, (/ 5 16) + x3, (/ 19 64) + x2, (/ 3 16) + x1}
#isLNatKind(x1)	weight: (/ 3 16) + x1
   #0()	weight: 0
 #U72(x1)	weight: 0
   U21(x1,x2)	weight: max{x2, (/ 5 32) + x1}
  U161(x1,x2)	weight: max{0, (/ 13 64) + x2}
n__isLNatKind(x1)	weight: (/ 5 64) + x1
   U11(x1,x2,x3)	weight: max{(/ 1020309 64) + x3, (/ 1 4) + x2, (/ 1020309 64) + x1}
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
n__pair(x1,x2)	weight: max{(/ 7 32) + x2, (/ 1 8) + x1}
  U143(x1)	weight: 0
#U142(x1,x2)	weight: max{0, (/ 7 32) + x2}
#take(x1,x2)	weight: max{(/ 31 64) + x2, (/ 3 8) + x1}
isPLNatKind(x1)	weight: (/ 3 64) + x1
  U142(x1,x2)	weight: 0
#U152(x1,x2)	weight: max{0, (/ 7 32) + x2}
#U181(x1,x2)	weight: max{(/ 1 8) + x2, (/ 13 64) + x1}
isPLNat(x1)	weight: 0
   U42(x1,x2)	weight: max{(/ 1020343 64) + x2, (/ 1020329 64) + x1}
   U91(x1,x2)	weight: max{(/ 15 64) + x2, (/ 5 32) + x1}
  U221(x1,x2,x3)	weight: max{0, (/ 13 32) + x3, (/ 1 4) + x2}
#U101(x1,x2,x3)	weight: max{(/ 15 64) + x3, (/ 15 64) + x2, (/ 1 32) + x1}
activate(x1)	weight: x1
 #U82(x1)	weight: 0
  take(x1,x2)	weight: max{(/ 13 32) + x2, (/ 25 64) + x1}
   U71(x1,x2)	weight: max{0, (/ 1 16) + x1}
 #U81(x1,x2)	weight: max{(/ 9 64) + x2, x1}
   and(x1,x2)	weight: max{0, x2}
 #U92(x1)	weight: 0
#U133(x1)	weight: 0
  U131(x1,x2,x3)	weight: max{0, (/ 1020333 64) + x1}
  U101(x1,x2,x3)	weight: max{0, (/ 7 16) + x3}
  pair(x1,x2)	weight: max{(/ 7 32) + x2, (/ 1 8) + x1}
   fst(x1)	weight: (/ 1 64) + x1
  U111(x1,x2)	weight: max{0, (/ 5 16) + x2}
  U132(x1,x2)	weight: max{(/ 1020347 64) + x2, (/ 510173 32) + x1}
   U43(x1)	weight: (/ 510171 32) + x1
#activate(x1)	weight: (/ 7 64) + x1
  U152(x1,x2)	weight: max{(/ 1 64) + x2, x1}
  U103(x1)	weight: (/ 29 64) + x1
 #U53(x1)	weight: 0
natsFrom(x1)	weight: (/ 13 64) + x1
#head(x1)	weight: (/ 19 64) + x1
 #U43(x1)	weight: 0
#U121(x1,x2)	weight: max{(/ 3 16) + x2, x1}
splitAt(x1,x2)	weight: max{(/ 1 4) + x2, (/ 13 64) + x1}
isNaturalKind(x1)	weight: (/ 11 64) + x1
#U131(x1,x2,x3)	weight: max{(/ 15 64) + x3, (/ 15 64) + x2, (/ 1 32) + x1}
   U72(x1)	weight: 0
n__isNaturalKind(x1)	weight: (/ 11 64) + x1
 #fst(x1)	weight: (/ 3 32) + x1
#U143(x1)	weight: 0
n__nil()	weight: (/ 1 8)
 #U52(x1,x2)	weight: max{0, (/ 13 64) + x2}
#U103(x1)	weight: 0
#isPLNatKind(x1)	weight: (/ 5 64) + x1
#U202(x1,x2)	weight: max{(/ 1 8) + x2, x1}
n__natsFrom(x1)	weight: (/ 13 64) + x1
isNatural(x1)	weight: (/ 1 64) + x1
n__snd(x1)	weight: (/ 1 64) + x1
  U201(x1,x2,x3,x4)	weight: max{0, (/ 1 4) + x4, (/ 3 16) + x3, (/ 13 64) + x2}
  n__s(x1)	weight: x1
n__splitAt(x1,x2)	weight: max{(/ 1 4) + x2, (/ 13 64) + x1}
 #U42(x1,x2)	weight: max{0, (/ 7 32) + x2}
#U141(x1,x2,x3)	weight: max{(/ 17 64) + x3, (/ 15 64) + x2, (/ 1 32) + x1}
  U141(x1,x2,x3)	weight: max{0, (/ 1 64) + x3}
#U171(x1,x2,x3)	weight: max{0, (/ 63771 4) + x3, (/ 510167 32) + x2}
  tail(x1)	weight: (/ 13 64) + x1
 #U62(x1)	weight: 0
     0()	weight: (/ 1 32)
  U191(x1,x2)	weight: max{0, (/ 1 4) + x2}
n__take(x1,x2)	weight: max{(/ 13 32) + x2, (/ 25 64) + x1}
 #sel(x1,x2)	weight: max{(/ 1020337 64) + x2, (/ 1020335 64) + x1}
#U102(x1,x2)	weight: max{0, (/ 7 32) + x2}
  U153(x1)	weight: (/ 13 64) + x1
  U171(x1,x2,x3)	weight: max{0, (/ 255083 16) + x3, (/ 1020331 64) + x2}
#isLNat(x1)	weight: (/ 13 64) + x1
  U202(x1,x2)	weight: max{(/ 3 16) + x2, x1}
   sel(x1,x2)	weight: max{(/ 255083 16) + x2, (/ 1020331 64) + x1}
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: max{(/ 510157 32) + x2, (/ 255077 16) + x1}
n__cons(x1,x2)	weight: max{x2, (/ 1 16) + x1}
#U211(x1,x2)	weight: max{0, (/ 1 8) + x2}
#isPLNat(x1)	weight: (/ 1 8) + x1
   nil()	weight: (/ 1 8)
isLNat(x1)	weight: (/ 1 64) + x1
   U62(x1)	weight: x1
#U153(x1)	weight: 0
n__sel(x1,x2)	weight: max{(/ 255083 16) + x2, (/ 1020331 64) + x1}
#tail(x1)	weight: (/ 19 64) + x1
#isNaturalKind(x1)	weight: (/ 1 8) + x1
#splitAt(x1,x2)	weight: max{(/ 17 64) + x2, (/ 19 64) + x1}
  U151(x1,x2,x3)	weight: max{0, (/ 1 64) + x1}
 #nil()	weight: 0
  U133(x1)	weight: (/ 1020359 64) + x1
n__tail(x1)	weight: (/ 13 64) + x1
#afterNth(x1,x2)	weight: max{(/ 510157 32) + x2, (/ 127539 8) + x1}
#U111(x1,x2)	weight: max{(/ 7 32) + x2, (/ 1 64) + x1}
#U221(x1,x2,x3)	weight: max{(/ 25 64) + x3, (/ 23 64) + x2, (/ 25 64) + x1}
  n__0()	weight: (/ 1 32)
n__afterNth(x1,x2)	weight: max{(/ 510157 32) + x2, (/ 255077 16) + x1}
  U211(x1,x2)	weight: max{0, (/ 13 64) + x2}
isLNatKind(x1)	weight: (/ 5 64) + x1
   U52(x1,x2)	weight: 0
   U61(x1,x2)	weight: max{0, x1}
 #U51(x1,x2,x3)	weight: max{(/ 13 64) + x3, (/ 17 64) + x2, (/ 1 8) + x1}
n__fst(x1)	weight: (/ 1 64) + x1
 #U11(x1,x2,x3)	weight: max{0, (/ 1020313 64) + x3, (/ 1020311 64) + x2}
   U31(x1,x2)	weight: max{0, (/ 19 64) + x2}
   U92(x1)	weight: (/ 3 16)
  head(x1)	weight: (/ 9 32) + x1
  U112(x1)	weight: (/ 3 16)
 #snd(x1)	weight: (/ 3 32) + x1
 #U41(x1,x2,x3)	weight: max{(/ 15 64) + x3, (/ 15 64) + x2, (/ 1 32) + x1}
  cons(x1,x2)	weight: max{x2, (/ 1 16) + x1}
#natsFrom(x1)	weight: (/ 19 64) + x1
  U102(x1,x2)	weight: max{0, (/ 29 64) + x2}
   snd(x1)	weight: (/ 1 64) + x1
#U191(x1,x2)	weight: max{(/ 1 8) + x2, (/ 11 64) + x1}
 #U21(x1,x2)	weight: max{0, (/ 1 8) + x2}
   U81(x1,x2)	weight: max{0, x1}
   U82(x1)	weight: (/ 7 32)
#U112(x1)	weight: 0
    tt()	weight: (/ 13 64)
n__and(x1,x2)	weight: max{0, x2}
 #U71(x1,x2)	weight: max{(/ 13 64) + x2, x1}
#U151(x1,x2,x3)	weight: max{(/ 15 64) + x3, (/ 15 64) + x2, (/ 1 32) + x1}
#isNatural(x1)	weight: (/ 3 16) + x1
#pair(x1,x2)	weight: 0
n__head(x1)	weight: (/ 9 32) + x1
   U51(x1,x2,x3)	weight: max{0, (/ 1 32) + x1}
#U161(x1,x2)	weight: max{(/ 1 8) + x2, (/ 3 64) + x1}
#U122(x1)	weight: 0
   U53(x1)	weight: x1
   U41(x1,x2,x3)	weight: max{(/ 255079 16) + x3, (/ 510165 32) + x2, (/ 255079 16) + x1}
 #U31(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 64) + x1}
 #and(x1,x2)	weight: max{0, (/ 7 64) + x2}
 #U91(x1,x2)	weight: max{(/ 7 32) + x2, (/ 1 64) + x1}
#U132(x1,x2)	weight: max{0, (/ 7 32) + x2}
  U121(x1,x2)	weight: max{0, x1}
 #U61(x1,x2)	weight: max{(/ 9 64) + x2, x1}
  U181(x1,x2)	weight: max{0, x2}
  U122(x1)	weight: (/ 13 64) + x1
    Usable rules: { 4 18..27 42..45 54..61 66..69 72..115 }
    Removed DPs: #2 #3 #6..39 #41..57 #59..62 #64..74 #76..82 #84..97 #99..106 #109 #111..130 #132..135 #137..147 #149..151 #153..164 #167 #169 #170 #172..178 #180..198 #200..202 #204..208 #211..224 #227 #229 #230 #233 #235..247 #249..253 #255..263 #265 #267
Number of SCCs: 5, DPs: 12, edges: 13
	SCC { #226 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)...