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