Input TRS:
    1: U11(tt(),N,XS) -> U12(tt(),activate(N),activate(XS))
    2: U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
    3: U21(tt(),X) -> U22(tt(),activate(X))
    4: U22(tt(),X) -> activate(X)
    5: U31(tt(),N) -> U32(tt(),activate(N))
    6: U32(tt(),N) -> activate(N)
    7: U41(tt(),N,XS) -> U42(tt(),activate(N),activate(XS))
    8: U42(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
    9: U51(tt(),Y) -> U52(tt(),activate(Y))
    10: U52(tt(),Y) -> activate(Y)
    11: U61(tt(),N,X,XS) -> U62(tt(),activate(N),activate(X),activate(XS))
    12: U62(tt(),N,X,XS) -> U63(tt(),activate(N),activate(X),activate(XS))
    13: U63(tt(),N,X,XS) -> U64(splitAt(activate(N),activate(XS)),activate(X))
    14: U64(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
    15: U71(tt(),XS) -> U72(tt(),activate(XS))
    16: U72(tt(),XS) -> activate(XS)
    17: U81(tt(),N,XS) -> U82(tt(),activate(N),activate(XS))
    18: U82(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
    19: afterNth(N,XS) -> U11(tt(),N,XS)
    20: fst(pair(X,Y)) -> U21(tt(),X)
    21: head(cons(N,XS)) -> U31(tt(),N)
    22: natsFrom(N) -> cons(N,n__natsFrom(s(N)))
    23: sel(N,XS) -> U41(tt(),N,XS)
    24: snd(pair(X,Y)) -> U51(tt(),Y)
    25: splitAt(0(),XS) -> pair(nil(),XS)
    26: splitAt(s(N),cons(X,XS)) -> U61(tt(),N,X,activate(XS))
    27: tail(cons(N,XS)) -> U71(tt(),activate(XS))
    28: take(N,XS) -> U81(tt(),N,XS)
    29: natsFrom(X) -> n__natsFrom(X)
    30: activate(n__natsFrom(X)) -> natsFrom(X)
    31: activate(X) -> X
Number of strict rules: 31
Direct Order(PosReal,>,Poly) ... failed.
Freezing U71 U41 U42 U32 U12 U51 U22 U62 U72 U63 U82 U81 U11 U21 U31 U61 U52
1: U11❆1_tt(N,XS) -> U12❆1_tt(activate(N),activate(XS))
2: U12❆1_tt(N,XS) -> snd(splitAt(activate(N),activate(XS)))
3: U21❆1_tt(X) -> U22❆1_tt(activate(X))
4: U22❆1_tt(X) -> activate(X)
5: U31❆1_tt(N) -> U32❆1_tt(activate(N))
6: U32❆1_tt(N) -> activate(N)
7: U41❆1_tt(N,XS) -> U42❆1_tt(activate(N),activate(XS))
8: U42❆1_tt(N,XS) -> head(afterNth(activate(N),activate(XS)))
9: U51❆1_tt(Y) -> U52❆1_tt(activate(Y))
10: U52❆1_tt(Y) -> activate(Y)
11: U61❆1_tt(N,X,XS) -> U62❆1_tt(activate(N),activate(X),activate(XS))
12: U62❆1_tt(N,X,XS) -> U63❆1_tt(activate(N),activate(X),activate(XS))
13: U63❆1_tt(N,X,XS) -> U64(splitAt(activate(N),activate(XS)),activate(X))
14: U64(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
15: U71❆1_tt(XS) -> U72❆1_tt(activate(XS))
16: U72❆1_tt(XS) -> activate(XS)
17: U81❆1_tt(N,XS) -> U82❆1_tt(activate(N),activate(XS))
18: U82❆1_tt(N,XS) -> fst(splitAt(activate(N),activate(XS)))
19: afterNth(N,XS) -> U11❆1_tt(N,XS)
20: fst(pair(X,Y)) -> U21❆1_tt(X)
21: head(cons(N,XS)) -> U31❆1_tt(N)
22: natsFrom(N) -> cons(N,n__natsFrom(s(N)))
23: sel(N,XS) -> U41❆1_tt(N,XS)
24: snd(pair(X,Y)) -> U51❆1_tt(Y)
25: splitAt(0(),XS) -> pair(nil(),XS)
26: splitAt(s(N),cons(X,XS)) -> U61❆1_tt(N,X,activate(XS))
27: tail(cons(N,XS)) -> U71❆1_tt(activate(XS))
28: take(N,XS) -> U81❆1_tt(N,XS)
29: natsFrom(X) -> n__natsFrom(X)
30: activate(n__natsFrom(X)) -> natsFrom(X)
31: activate(X) -> X
32: U52(tt(),_1) ->= U52❆1_tt(_1)
33: U61(tt(),_3,_4,_5) ->= U61❆1_tt(_3,_4,_5)
34: U31(tt(),_1) ->= U31❆1_tt(_1)
35: U21(tt(),_1) ->= U21❆1_tt(_1)
36: U11(tt(),_2,_3) ->= U11❆1_tt(_2,_3)
37: U81(tt(),_2,_3) ->= U81❆1_tt(_2,_3)
38: U82(tt(),_2,_3) ->= U82❆1_tt(_2,_3)
39: U63(tt(),_3,_4,_5) ->= U63❆1_tt(_3,_4,_5)
40: U72(tt(),_1) ->= U72❆1_tt(_1)
41: U62(tt(),_3,_4,_5) ->= U62❆1_tt(_3,_4,_5)
42: U22(tt(),_1) ->= U22❆1_tt(_1)
43: U51(tt(),_1) ->= U51❆1_tt(_1)
44: U12(tt(),_2,_3) ->= U12❆1_tt(_2,_3)
45: U32(tt(),_1) ->= U32❆1_tt(_1)
46: U42(tt(),_2,_3) ->= U42❆1_tt(_2,_3)
47: U41(tt(),_2,_3) ->= U41❆1_tt(_2,_3)
48: U71(tt(),_1) ->= U71❆1_tt(_1)
Number of strict rules: 31
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #U12❆1_tt(N,XS) -> #snd(splitAt(activate(N),activate(XS)))
   #2: #U12❆1_tt(N,XS) -> #splitAt(activate(N),activate(XS))
   #3: #U12❆1_tt(N,XS) -> #activate(N)
   #4: #U12❆1_tt(N,XS) -> #activate(XS)
   #5: #U51(tt(),_1) ->? #U51❆1_tt(_1)
   #6: #U21(tt(),_1) ->? #U21❆1_tt(_1)
   #7: #U42(tt(),_2,_3) ->? #U42❆1_tt(_2,_3)
   #8: #U22(tt(),_1) ->? #U22❆1_tt(_1)
   #9: #U62(tt(),_3,_4,_5) ->? #U62❆1_tt(_3,_4,_5)
   #10: #U81(tt(),_2,_3) ->? #U81❆1_tt(_2,_3)
   #11: #U41(tt(),_2,_3) ->? #U41❆1_tt(_2,_3)
   #12: #U71(tt(),_1) ->? #U71❆1_tt(_1)
   #13: #U82(tt(),_2,_3) ->? #U82❆1_tt(_2,_3)
   #14: #U32❆1_tt(N) -> #activate(N)
   #15: #U72(tt(),_1) ->? #U72❆1_tt(_1)
   #16: #U63❆1_tt(N,X,XS) -> #U64(splitAt(activate(N),activate(XS)),activate(X))
   #17: #U63❆1_tt(N,X,XS) -> #splitAt(activate(N),activate(XS))
   #18: #U63❆1_tt(N,X,XS) -> #activate(N)
   #19: #U63❆1_tt(N,X,XS) -> #activate(XS)
   #20: #U63❆1_tt(N,X,XS) -> #activate(X)
   #21: #U51❆1_tt(Y) -> #U52❆1_tt(activate(Y))
   #22: #U51❆1_tt(Y) -> #activate(Y)
   #23: #U61❆1_tt(N,X,XS) -> #U62❆1_tt(activate(N),activate(X),activate(XS))
   #24: #U61❆1_tt(N,X,XS) -> #activate(N)
   #25: #U61❆1_tt(N,X,XS) -> #activate(X)
   #26: #U61❆1_tt(N,X,XS) -> #activate(XS)
   #27: #snd(pair(X,Y)) -> #U51❆1_tt(Y)
   #28: #sel(N,XS) -> #U41❆1_tt(N,XS)
   #29: #U32(tt(),_1) ->? #U32❆1_tt(_1)
   #30: #U62❆1_tt(N,X,XS) -> #U63❆1_tt(activate(N),activate(X),activate(XS))
   #31: #U62❆1_tt(N,X,XS) -> #activate(N)
   #32: #U62❆1_tt(N,X,XS) -> #activate(X)
   #33: #U62❆1_tt(N,X,XS) -> #activate(XS)
   #34: #U64(pair(YS,ZS),X) -> #activate(X)
   #35: #activate(n__natsFrom(X)) -> #natsFrom(X)
   #36: #fst(pair(X,Y)) -> #U21❆1_tt(X)
   #37: #U41❆1_tt(N,XS) -> #U42❆1_tt(activate(N),activate(XS))
   #38: #U41❆1_tt(N,XS) -> #activate(N)
   #39: #U41❆1_tt(N,XS) -> #activate(XS)
   #40: #U63(tt(),_3,_4,_5) ->? #U63❆1_tt(_3,_4,_5)
   #41: #U52❆1_tt(Y) -> #activate(Y)
   #42: #U61(tt(),_3,_4,_5) ->? #U61❆1_tt(_3,_4,_5)
   #43: #U31❆1_tt(N) -> #U32❆1_tt(activate(N))
   #44: #U31❆1_tt(N) -> #activate(N)
   #45: #U12(tt(),_2,_3) ->? #U12❆1_tt(_2,_3)
   #46: #take(N,XS) -> #U81❆1_tt(N,XS)
   #47: #U31(tt(),_1) ->? #U31❆1_tt(_1)
   #48: #tail(cons(N,XS)) -> #U71❆1_tt(activate(XS))
   #49: #tail(cons(N,XS)) -> #activate(XS)
   #50: #U81❆1_tt(N,XS) -> #U82❆1_tt(activate(N),activate(XS))
   #51: #U81❆1_tt(N,XS) -> #activate(N)
   #52: #U81❆1_tt(N,XS) -> #activate(XS)
   #53: #U52(tt(),_1) ->? #U52❆1_tt(_1)
   #54: #afterNth(N,XS) -> #U11❆1_tt(N,XS)
   #55: #splitAt(s(N),cons(X,XS)) -> #U61❆1_tt(N,X,activate(XS))
   #56: #splitAt(s(N),cons(X,XS)) -> #activate(XS)
   #57: #U11(tt(),_2,_3) ->? #U11❆1_tt(_2,_3)
   #58: #head(cons(N,XS)) -> #U31❆1_tt(N)
   #59: #U72❆1_tt(XS) -> #activate(XS)
   #60: #U21❆1_tt(X) -> #U22❆1_tt(activate(X))
   #61: #U21❆1_tt(X) -> #activate(X)
   #62: #U11❆1_tt(N,XS) -> #U12❆1_tt(activate(N),activate(XS))
   #63: #U11❆1_tt(N,XS) -> #activate(N)
   #64: #U11❆1_tt(N,XS) -> #activate(XS)
   #65: #U42❆1_tt(N,XS) -> #head(afterNth(activate(N),activate(XS)))
   #66: #U42❆1_tt(N,XS) -> #afterNth(activate(N),activate(XS))
   #67: #U42❆1_tt(N,XS) -> #activate(N)
   #68: #U42❆1_tt(N,XS) -> #activate(XS)
   #69: #U71❆1_tt(XS) -> #U72❆1_tt(activate(XS))
   #70: #U71❆1_tt(XS) -> #activate(XS)
   #71: #U22❆1_tt(X) -> #activate(X)
   #72: #U82❆1_tt(N,XS) -> #fst(splitAt(activate(N),activate(XS)))
   #73: #U82❆1_tt(N,XS) -> #splitAt(activate(N),activate(XS))
   #74: #U82❆1_tt(N,XS) -> #activate(N)
   #75: #U82❆1_tt(N,XS) -> #activate(XS)
Number of SCCs: 1, DPs: 4, edges: 4
	SCC { #17 #23 #30 #55 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #U72(x1,x2)	weight: 0
 #U32(x1,x2)	weight: 0
   U21(x1,x2)	weight: 0
   U11(x1,x2,x3)	weight: 0
U72❆1_tt(x1)	weight: 0
#U42❆1_tt(x1,x2)	weight: 0
#U61❆1_tt(x1,x2,x3)	weight: (/ 3 4) + x1
   U64(x1,x2)	weight: 0
     s(x1)	weight: (/ 7 8) + x1
#take(x1,x2)	weight: 0
   U42(x1,x2,x3)	weight: 0
U81❆1_tt(x1,x2)	weight: 0
activate(x1)	weight: (/ 1 8) + x1
 #U82(x1,x2,x3)	weight: 0
#U72❆1_tt(x1)	weight: 0
  take(x1,x2)	weight: 0
   U71(x1,x2)	weight: 0
 #U81(x1,x2,x3)	weight: 0
#U12❆1_tt(x1,x2)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: 0
U61❆1_tt(x1,x2,x3)	weight: 0
#activate(x1)	weight: 0
U21❆1_tt(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4)
#head(x1)	weight: 0
#U41❆1_tt(x1,x2)	weight: 0
#U63❆1_tt(x1,x2,x3)	weight: (/ 1 4) + x1
U71❆1_tt(x1)	weight: 0
   U63(x1,x2,x3,x4)	weight: 0
splitAt(x1,x2)	weight: 0
#U51❆1_tt(x1)	weight: 0
   U72(x1,x2)	weight: 0
 #fst(x1)	weight: 0
 #U52(x1,x2)	weight: 0
   U12(x1,x2,x3)	weight: 0
U11❆1_tt(x1,x2)	weight: 0
U63❆1_tt(x1,x2,x3)	weight: 0
n__natsFrom(x1)	weight: (/ 1 8)
U82❆1_tt(x1,x2)	weight: 0
#U62❆1_tt(x1,x2,x3)	weight: (/ 1 2) + x1
U32❆1_tt(x1)	weight: 0
#U81❆1_tt(x1,x2)	weight: 0
 #U42(x1,x2,x3)	weight: 0
 #U12(x1,x2,x3)	weight: 0
  tail(x1)	weight: 0
U22❆1_tt(x1)	weight: 0
 #U62(x1,x2,x3,x4)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
   U62(x1,x2,x3,x4)	weight: 0
#tail(x1)	weight: 0
 #U63(x1,x2,x3,x4)	weight: 0
#splitAt(x1,x2)	weight: x1
#afterNth(x1,x2)	weight: 0
#U11❆1_tt(x1,x2)	weight: 0
   U32(x1,x2)	weight: 0
#U22❆1_tt(x1)	weight: 0
U41❆1_tt(x1,x2)	weight: 0
#U82❆1_tt(x1,x2)	weight: 0
#U71❆1_tt(x1)	weight: 0
   U52(x1,x2)	weight: 0
   U61(x1,x2,x3,x4)	weight: 0
 #U51(x1,x2)	weight: 0
#U21❆1_tt(x1)	weight: 0
 #U11(x1,x2,x3)	weight: 0
 #U64(x1,x2)	weight: 0
   U31(x1,x2)	weight: 0
  head(x1)	weight: 0
U62❆1_tt(x1,x2,x3)	weight: 0
 #snd(x1)	weight: 0
 #U41(x1,x2,x3)	weight: 0
  cons(x1,x2)	weight: (/ 1 4)
#natsFrom(x1)	weight: 0
U31❆1_tt(x1)	weight: 0
   snd(x1)	weight: 0
 #U21(x1,x2)	weight: 0
   U81(x1,x2,x3)	weight: 0
   U82(x1,x2,x3)	weight: 0
 #U22(x1,x2)	weight: 0
#U31❆1_tt(x1)	weight: 0
    tt()	weight: 0
 #U71(x1,x2)	weight: 0
U12❆1_tt(x1,x2)	weight: 0
   U22(x1,x2)	weight: 0
   U51(x1,x2)	weight: 0
U52❆1_tt(x1)	weight: 0
   U41(x1,x2,x3)	weight: 0
U42❆1_tt(x1,x2)	weight: 0
 #U31(x1,x2)	weight: 0
U51❆1_tt(x1)	weight: 0
#U32❆1_tt(x1)	weight: 0
#U52❆1_tt(x1)	weight: 0
 #U61(x1,x2,x3,x4)	weight: 0
    Usable rules: { 22 29..31 }
    Removed DPs: #17 #23 #30 #55
Number of SCCs: 0, DPs: 0, edges: 0
YES