Input TRS:
    1: active(natsFrom(N)) -> mark(cons(N,natsFrom(s(N))))
    2: active(fst(pair(XS,YS))) -> mark(XS)
    3: active(snd(pair(XS,YS))) -> mark(YS)
    4: active(splitAt(0(),XS)) -> mark(pair(nil(),XS))
    5: active(splitAt(s(N),cons(X,XS))) -> mark(u(splitAt(N,XS),N,X,XS))
    6: active(u(pair(YS,ZS),N,X,XS)) -> mark(pair(cons(X,YS),ZS))
    7: active(head(cons(N,XS))) -> mark(N)
    8: active(tail(cons(N,XS))) -> mark(XS)
    9: active(sel(N,XS)) -> mark(head(afterNth(N,XS)))
    10: active(take(N,XS)) -> mark(fst(splitAt(N,XS)))
    11: active(afterNth(N,XS)) -> mark(snd(splitAt(N,XS)))
    12: active(natsFrom(X)) -> natsFrom(active(X))
    13: active(cons(X1,X2)) -> cons(active(X1),X2)
    14: active(s(X)) -> s(active(X))
    15: active(fst(X)) -> fst(active(X))
    16: active(pair(X1,X2)) -> pair(active(X1),X2)
    17: active(pair(X1,X2)) -> pair(X1,active(X2))
    18: active(snd(X)) -> snd(active(X))
    19: active(splitAt(X1,X2)) -> splitAt(active(X1),X2)
    20: active(splitAt(X1,X2)) -> splitAt(X1,active(X2))
    21: active(u(X1,X2,X3,X4)) -> u(active(X1),X2,X3,X4)
    22: active(head(X)) -> head(active(X))
    23: active(tail(X)) -> tail(active(X))
    24: active(sel(X1,X2)) -> sel(active(X1),X2)
    25: active(sel(X1,X2)) -> sel(X1,active(X2))
    26: active(afterNth(X1,X2)) -> afterNth(active(X1),X2)
    27: active(afterNth(X1,X2)) -> afterNth(X1,active(X2))
    28: active(take(X1,X2)) -> take(active(X1),X2)
    29: active(take(X1,X2)) -> take(X1,active(X2))
    30: natsFrom(mark(X)) -> mark(natsFrom(X))
    31: cons(mark(X1),X2) -> mark(cons(X1,X2))
    32: s(mark(X)) -> mark(s(X))
    33: fst(mark(X)) -> mark(fst(X))
    34: pair(mark(X1),X2) -> mark(pair(X1,X2))
    35: pair(X1,mark(X2)) -> mark(pair(X1,X2))
    36: snd(mark(X)) -> mark(snd(X))
    37: splitAt(mark(X1),X2) -> mark(splitAt(X1,X2))
    38: splitAt(X1,mark(X2)) -> mark(splitAt(X1,X2))
    39: u(mark(X1),X2,X3,X4) -> mark(u(X1,X2,X3,X4))
    40: head(mark(X)) -> mark(head(X))
    41: tail(mark(X)) -> mark(tail(X))
    42: sel(mark(X1),X2) -> mark(sel(X1,X2))
    43: sel(X1,mark(X2)) -> mark(sel(X1,X2))
    44: afterNth(mark(X1),X2) -> mark(afterNth(X1,X2))
    45: afterNth(X1,mark(X2)) -> mark(afterNth(X1,X2))
    46: take(mark(X1),X2) -> mark(take(X1,X2))
    47: take(X1,mark(X2)) -> mark(take(X1,X2))
    48: proper(natsFrom(X)) -> natsFrom(proper(X))
    49: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    50: proper(s(X)) -> s(proper(X))
    51: proper(fst(X)) -> fst(proper(X))
    52: proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
    53: proper(snd(X)) -> snd(proper(X))
    54: proper(splitAt(X1,X2)) -> splitAt(proper(X1),proper(X2))
    55: proper(0()) -> ok(0())
    56: proper(nil()) -> ok(nil())
    57: proper(u(X1,X2,X3,X4)) -> u(proper(X1),proper(X2),proper(X3),proper(X4))
    58: proper(head(X)) -> head(proper(X))
    59: proper(tail(X)) -> tail(proper(X))
    60: proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
    61: proper(afterNth(X1,X2)) -> afterNth(proper(X1),proper(X2))
    62: proper(take(X1,X2)) -> take(proper(X1),proper(X2))
    63: natsFrom(ok(X)) -> ok(natsFrom(X))
    64: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    65: s(ok(X)) -> ok(s(X))
    66: fst(ok(X)) -> ok(fst(X))
    67: pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
    68: snd(ok(X)) -> ok(snd(X))
    69: splitAt(ok(X1),ok(X2)) -> ok(splitAt(X1,X2))
    70: u(ok(X1),ok(X2),ok(X3),ok(X4)) -> ok(u(X1,X2,X3,X4))
    71: head(ok(X)) -> ok(head(X))
    72: tail(ok(X)) -> ok(tail(X))
    73: sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
    74: afterNth(ok(X1),ok(X2)) -> ok(afterNth(X1,X2))
    75: take(ok(X1),ok(X2)) -> ok(take(X1,X2))
    76: top(mark(X)) -> top(proper(X))
    77: top(ok(X)) -> top(active(X))
Number of strict rules: 77
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #sel(X1,mark(X2)) -> #sel(X1,X2)
   #2: #active(take(X1,X2)) -> #take(X1,active(X2))
   #3: #active(take(X1,X2)) -> #active(X2)
   #4: #pair(X1,mark(X2)) -> #pair(X1,X2)
   #5: #fst(ok(X)) -> #fst(X)
   #6: #take(mark(X1),X2) -> #take(X1,X2)
   #7: #sel(mark(X1),X2) -> #sel(X1,X2)
   #8: #tail(mark(X)) -> #tail(X)
   #9: #splitAt(mark(X1),X2) -> #splitAt(X1,X2)
   #10: #sel(ok(X1),ok(X2)) -> #sel(X1,X2)
   #11: #take(X1,mark(X2)) -> #take(X1,X2)
   #12: #proper(snd(X)) -> #snd(proper(X))
   #13: #proper(snd(X)) -> #proper(X)
   #14: #head(ok(X)) -> #head(X)
   #15: #proper(natsFrom(X)) -> #natsFrom(proper(X))
   #16: #proper(natsFrom(X)) -> #proper(X)
   #17: #take(ok(X1),ok(X2)) -> #take(X1,X2)
   #18: #afterNth(ok(X1),ok(X2)) -> #afterNth(X1,X2)
   #19: #proper(head(X)) -> #head(proper(X))
   #20: #proper(head(X)) -> #proper(X)
   #21: #proper(afterNth(X1,X2)) -> #afterNth(proper(X1),proper(X2))
   #22: #proper(afterNth(X1,X2)) -> #proper(X1)
   #23: #proper(afterNth(X1,X2)) -> #proper(X2)
   #24: #splitAt(X1,mark(X2)) -> #splitAt(X1,X2)
   #25: #active(u(pair(YS,ZS),N,X,XS)) -> #pair(cons(X,YS),ZS)
   #26: #active(u(pair(YS,ZS),N,X,XS)) -> #cons(X,YS)
   #27: #proper(tail(X)) -> #tail(proper(X))
   #28: #proper(tail(X)) -> #proper(X)
   #29: #pair(ok(X1),ok(X2)) -> #pair(X1,X2)
   #30: #head(mark(X)) -> #head(X)
   #31: #proper(fst(X)) -> #fst(proper(X))
   #32: #proper(fst(X)) -> #proper(X)
   #33: #active(cons(X1,X2)) -> #cons(active(X1),X2)
   #34: #active(cons(X1,X2)) -> #active(X1)
   #35: #active(sel(N,XS)) -> #head(afterNth(N,XS))
   #36: #active(sel(N,XS)) -> #afterNth(N,XS)
   #37: #active(afterNth(N,XS)) -> #snd(splitAt(N,XS))
   #38: #active(afterNth(N,XS)) -> #splitAt(N,XS)
   #39: #proper(u(X1,X2,X3,X4)) -> #u(proper(X1),proper(X2),proper(X3),proper(X4))
   #40: #proper(u(X1,X2,X3,X4)) -> #proper(X1)
   #41: #proper(u(X1,X2,X3,X4)) -> #proper(X2)
   #42: #proper(u(X1,X2,X3,X4)) -> #proper(X3)
   #43: #proper(u(X1,X2,X3,X4)) -> #proper(X4)
   #44: #top(mark(X)) -> #top(proper(X))
   #45: #top(mark(X)) -> #proper(X)
   #46: #active(sel(X1,X2)) -> #sel(active(X1),X2)
   #47: #active(sel(X1,X2)) -> #active(X1)
   #48: #u(ok(X1),ok(X2),ok(X3),ok(X4)) -> #u(X1,X2,X3,X4)
   #49: #active(tail(X)) -> #tail(active(X))
   #50: #active(tail(X)) -> #active(X)
   #51: #afterNth(X1,mark(X2)) -> #afterNth(X1,X2)
   #52: #splitAt(ok(X1),ok(X2)) -> #splitAt(X1,X2)
   #53: #active(natsFrom(X)) -> #natsFrom(active(X))
   #54: #active(natsFrom(X)) -> #active(X)
   #55: #cons(mark(X1),X2) -> #cons(X1,X2)
   #56: #active(s(X)) -> #s(active(X))
   #57: #active(s(X)) -> #active(X)
   #58: #proper(take(X1,X2)) -> #take(proper(X1),proper(X2))
   #59: #proper(take(X1,X2)) -> #proper(X1)
   #60: #proper(take(X1,X2)) -> #proper(X2)
   #61: #natsFrom(mark(X)) -> #natsFrom(X)
   #62: #proper(pair(X1,X2)) -> #pair(proper(X1),proper(X2))
   #63: #proper(pair(X1,X2)) -> #proper(X1)
   #64: #proper(pair(X1,X2)) -> #proper(X2)
   #65: #proper(cons(X1,X2)) -> #cons(proper(X1),proper(X2))
   #66: #proper(cons(X1,X2)) -> #proper(X1)
   #67: #proper(cons(X1,X2)) -> #proper(X2)
   #68: #active(sel(X1,X2)) -> #sel(X1,active(X2))
   #69: #active(sel(X1,X2)) -> #active(X2)
   #70: #active(splitAt(X1,X2)) -> #splitAt(X1,active(X2))
   #71: #active(splitAt(X1,X2)) -> #active(X2)
   #72: #u(mark(X1),X2,X3,X4) -> #u(X1,X2,X3,X4)
   #73: #active(take(N,XS)) -> #fst(splitAt(N,XS))
   #74: #active(take(N,XS)) -> #splitAt(N,XS)
   #75: #cons(ok(X1),ok(X2)) -> #cons(X1,X2)
   #76: #fst(mark(X)) -> #fst(X)
   #77: #tail(ok(X)) -> #tail(X)
   #78: #active(splitAt(s(N),cons(X,XS))) -> #u(splitAt(N,XS),N,X,XS)
   #79: #active(splitAt(s(N),cons(X,XS))) -> #splitAt(N,XS)
   #80: #afterNth(mark(X1),X2) -> #afterNth(X1,X2)
   #81: #s(ok(X)) -> #s(X)
   #82: #active(take(X1,X2)) -> #take(active(X1),X2)
   #83: #active(take(X1,X2)) -> #active(X1)
   #84: #active(head(X)) -> #head(active(X))
   #85: #active(head(X)) -> #active(X)
   #86: #pair(mark(X1),X2) -> #pair(X1,X2)
   #87: #active(afterNth(X1,X2)) -> #afterNth(X1,active(X2))
   #88: #active(afterNth(X1,X2)) -> #active(X2)
   #89: #proper(sel(X1,X2)) -> #sel(proper(X1),proper(X2))
   #90: #proper(sel(X1,X2)) -> #proper(X1)
   #91: #proper(sel(X1,X2)) -> #proper(X2)
   #92: #active(pair(X1,X2)) -> #pair(X1,active(X2))
   #93: #active(pair(X1,X2)) -> #active(X2)
   #94: #s(mark(X)) -> #s(X)
   #95: #active(splitAt(X1,X2)) -> #splitAt(active(X1),X2)
   #96: #active(splitAt(X1,X2)) -> #active(X1)
   #97: #natsFrom(ok(X)) -> #natsFrom(X)
   #98: #active(afterNth(X1,X2)) -> #afterNth(active(X1),X2)
   #99: #active(afterNth(X1,X2)) -> #active(X1)
   #100: #snd(ok(X)) -> #snd(X)
   #101: #snd(mark(X)) -> #snd(X)
   #102: #active(u(X1,X2,X3,X4)) -> #u(active(X1),X2,X3,X4)
   #103: #active(u(X1,X2,X3,X4)) -> #active(X1)
   #104: #active(pair(X1,X2)) -> #pair(active(X1),X2)
   #105: #active(pair(X1,X2)) -> #active(X1)
   #106: #top(ok(X)) -> #top(active(X))
   #107: #top(ok(X)) -> #active(X)
   #108: #active(natsFrom(N)) -> #cons(N,natsFrom(s(N)))
   #109: #active(natsFrom(N)) -> #natsFrom(s(N))
   #110: #active(natsFrom(N)) -> #s(N)
   #111: #proper(splitAt(X1,X2)) -> #splitAt(proper(X1),proper(X2))
   #112: #proper(splitAt(X1,X2)) -> #proper(X1)
   #113: #proper(splitAt(X1,X2)) -> #proper(X2)
   #114: #active(fst(X)) -> #fst(active(X))
   #115: #active(fst(X)) -> #active(X)
   #116: #active(splitAt(0(),XS)) -> #pair(nil(),XS)
   #117: #proper(s(X)) -> #s(proper(X))
   #118: #proper(s(X)) -> #proper(X)
   #119: #active(snd(X)) -> #snd(active(X))
   #120: #active(snd(X)) -> #active(X)
Number of SCCs: 16, DPs: 73, edges: 889
	SCC { #81 #94 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: 0
 #top(x1)	weight: 0
natsFrom(x1)	weight: 0
#head(x1)	weight: 0
splitAt(x1,x2)	weight: 0
 #fst(x1)	weight: 0
  tail(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
   #s(x1)	weight: x1
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: 0
  head(x1)	weight: 0
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: 0
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #81 #94
Number of SCCs: 15, DPs: 71, edges: 885
	SCC { #5 #76 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: 0
 #top(x1)	weight: 0
natsFrom(x1)	weight: 0
#head(x1)	weight: 0
splitAt(x1,x2)	weight: 0
 #fst(x1)	weight: x1
  tail(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: 0
  head(x1)	weight: 0
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: 0
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #5 #76
Number of SCCs: 14, DPs: 69, edges: 881
	SCC { #8 #77 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: 0
 #top(x1)	weight: 0
natsFrom(x1)	weight: 0
#head(x1)	weight: 0
splitAt(x1,x2)	weight: 0
 #fst(x1)	weight: 0
  tail(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: x1
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: 0
  head(x1)	weight: 0
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: 0
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #8 #77
Number of SCCs: 13, DPs: 67, edges: 877
	SCC { #14 #30 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: 0
 #top(x1)	weight: 0
natsFrom(x1)	weight: 0
#head(x1)	weight: x1
splitAt(x1,x2)	weight: 0
 #fst(x1)	weight: 0
  tail(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: 0
  head(x1)	weight: 0
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: 0
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #14 #30
Number of SCCs: 12, DPs: 65, edges: 873
	SCC { #61 #97 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: 0
 #top(x1)	weight: 0
natsFrom(x1)	weight: 0
#head(x1)	weight: 0
splitAt(x1,x2)	weight: 0
 #fst(x1)	weight: 0
  tail(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: 0
  head(x1)	weight: 0
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: 0
#natsFrom(x1)	weight: x1
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #61 #97
Number of SCCs: 11, DPs: 63, edges: 869
	SCC { #100 #101 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: 0
 #top(x1)	weight: 0
natsFrom(x1)	weight: 0
#head(x1)	weight: 0
splitAt(x1,x2)	weight: 0
 #fst(x1)	weight: 0
  tail(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: 0
  head(x1)	weight: 0
 #snd(x1)	weight: x1
  cons(x1,x2)	weight: 0
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #100 #101
Number of SCCs: 10, DPs: 61, edges: 865
	SCC { #44 #106 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded.
#cons(x1,x2)	weight: (/ 1 16) + x1	status: [x1]	precedence above:
     s(x1)	weight: x1	status: [x1]	precedence above: mark
#take(x1,x2)	weight: (/ 1 16) + x2 + x1	status: [x2,x1]	precedence above:
     u(x1,x2,x3,x4)	weight: max{0, (/ 1 8) + x4, (/ 5 16) + x3, x1}	status: [x1]	precedence above: pair mark cons
  take(x1,x2)	weight: (/ 7 16) + x2 + x1	status: [x1,x2]	precedence above: s u pair splitAt ok mark cons snd
   top(x1)	weight: (/ 1 16)	status: []	precedence above:
   #u(x1,x2,x3,x4)	weight: (/ 1 16) + x4	status: [x4]	precedence above:
  pair(x1,x2)	weight: max{(/ 3 16) + x2, (/ 1 4) + x1}	status: [x1,x2]	precedence above: mark
   fst(x1)	weight: x1	status: x1
 #top(x1)	weight: (/ 1 16) + x1	status: [x1]	precedence above:
natsFrom(x1)	weight: (/ 1 8) + x1	status: [x1]	precedence above: s mark cons
#head(x1)	weight: (/ 1 16)	status: []	precedence above:
splitAt(x1,x2)	weight: (/ 3 8) + x2 + x1	status: [x1,x2]	precedence above: s u pair ok mark cons snd
 #fst(x1)	weight: x1	status: []	precedence above:
  tail(x1)	weight: (/ 1 16) + x1	status: [x1]	precedence above: mark
proper(x1)	weight: x1	status: x1
    ok(x1)	weight: x1	status: x1
     0()	weight: (/ 1 8)	status: []	precedence above:
 #sel(x1,x2)	weight: (/ 1 16) + x2 + x1	status: [x1,x2]	precedence above:
   sel(x1,x2)	weight: (/ 9 16) + x2 + x1	status: [x1,x2]	precedence above: afterNth mark head
   #s(x1)	weight: x1	status: []	precedence above:
afterNth(x1,x2)	weight: (/ 7 16) + x2 + x1	status: [x2,x1]	precedence above: mark
   nil()	weight: (/ 1 16)	status: []	precedence above:
#tail(x1)	weight: x1	status: []	precedence above:
#splitAt(x1,x2)	weight: x2	status: [x2]	precedence above:
  mark(x1)	weight: x1	status: [x1]	precedence above:
#afterNth(x1,x2)	weight: (/ 1 16) + x2	status: [x2]	precedence above:
#proper(x1)	weight: (/ 1 16)	status: []	precedence above:
active(x1)	weight: x1	status: x1
  head(x1)	weight: (/ 1 16) + x1	status: [x1]	precedence above: mark
 #snd(x1)	weight: (/ 1 16)	status: []	precedence above:
  cons(x1,x2)	weight: max{x2, (/ 1 16) + x1}	status: [x1]	precedence above: mark
#natsFrom(x1)	weight: x1	status: []	precedence above:
#active(x1)	weight: x1	status: []	precedence above:
   snd(x1)	weight: x1	status: x1
#pair(x1,x2)	weight: (/ 1 16)	status: []	precedence above:
    Usable rules: { 1..75 }
    Removed DPs: #44
Number of SCCs: 10, DPs: 60, edges: 862
	SCC { #106 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: (/ 1 4) + x4
  take(x1,x2)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: (/ 1 4) + x2
   fst(x1)	weight: (/ 1 4) + x1
 #top(x1)	weight: x1
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: (/ 1 4) + x1
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: (/ 1 4) + x2
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4)
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  head(x1)	weight: (/ 1 4) + x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: (/ 1 4) + x1
#pair(x1,x2)	weight: 0
    Usable rules: { 1..47 63..75 }
    Removed DPs: #106
Number of SCCs: 9, DPs: 59, edges: 861
	SCC { #55 #75 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x2
     s(x1)	weight: (/ 1 4) + x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: (/ 1 4) + x4
  take(x1,x2)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: (/ 1 4) + x2
   fst(x1)	weight: (/ 1 4) + x1
 #top(x1)	weight: x1
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: (/ 1 4) + x1
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: (/ 1 4) + x2
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4)
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  head(x1)	weight: (/ 1 4) + x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: (/ 1 4) + x1
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #75
Number of SCCs: 10, DPs: 58, edges: 858
	SCC { #55 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x1
     s(x1)	weight: x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #55
Number of SCCs: 9, DPs: 57, edges: 857
	SCC { #9 #24 #52 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: x2
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #24 #52
Number of SCCs: 10, DPs: 55, edges: 849
	SCC { #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: x1
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #9
Number of SCCs: 9, DPs: 54, edges: 848
	SCC { #1 #7 #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: x1
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #7 #10
Number of SCCs: 10, DPs: 52, edges: 840
	SCC { #1 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: x2
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #1
Number of SCCs: 9, DPs: 51, edges: 839
	SCC { #4 #29 #86 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: x1 + x2
    Usable rules: { }
    Removed DPs: #4 #29 #86
Number of SCCs: 9, DPs: 48, edges: 830
	SCC { #6 #11 #17 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: x2
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #11 #17
Number of SCCs: 9, DPs: 46, edges: 822
	SCC { #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: x1
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #6
Number of SCCs: 8, DPs: 45, edges: 821
	SCC { #18 #51 #80 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: x1 + x2
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #18 #51 #80
Number of SCCs: 8, DPs: 42, edges: 812
	SCC { #48 #72 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: x3
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #48
Number of SCCs: 8, DPs: 41, edges: 809
	SCC { #72 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: 0
  take(x1,x2)	weight: 0
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: x1
  pair(x1,x2)	weight: 0
   fst(x1)	weight: (/ 1 4)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 4) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 4) + x1
 #fst(x1)	weight: 0
  tail(x1)	weight: x1
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: 0
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #72
Number of SCCs: 7, DPs: 40, edges: 808
	SCC { #3 #34 #47 #50 #54 #57 #69 #71 #83 #85 #88 #93 #96 #99 #103 #105 #115 #120 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: (/ 1 8) + x1 + x3
  take(x1,x2)	weight: (/ 1 8) + x1 + x2
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: x1 + x2
   fst(x1)	weight: (/ 1 8) + x1
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 8) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 8) + x1 + x2
 #fst(x1)	weight: 0
  tail(x1)	weight: (/ 1 8) + x1
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 8) + x1 + x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: (/ 1 8) + x1 + x2
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 3 8) + x1
  head(x1)	weight: (/ 1 8) + x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 8) + x1 + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: x1
   snd(x1)	weight: (/ 1 8) + x1
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #3 #34 #47 #50 #54 #57 #69 #71 #83 #85 #88 #96 #99 #103 #115 #120
Number of SCCs: 8, DPs: 24, edges: 488
	SCC { #93 #105 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: (/ 1 8) + x1 + x3
  take(x1,x2)	weight: (/ 1 8) + x1 + x2
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: (/ 1 8) + x1 + x2
   fst(x1)	weight: (/ 1 8)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 8) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 8) + x1 + x2
 #fst(x1)	weight: 0
  tail(x1)	weight: (/ 1 8) + x1
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 8) + x1 + x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: (/ 1 8) + x1 + x2
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: 0
active(x1)	weight: (/ 3 8) + x1
  head(x1)	weight: (/ 1 8) + x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 8) + x1 + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: x1
   snd(x1)	weight: (/ 1 8) + x1
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #93 #105
Number of SCCs: 7, DPs: 22, edges: 484
	SCC { #13 #16 #20 #22 #23 #28 #32 #40..43 #59 #60 #63 #64 #66 #67 #90 #91 #112 #113 #118 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: (/ 1 8) + x1 + x2 + x3 + x4
  take(x1,x2)	weight: (/ 1 8) + x1 + x2
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: x1 + x2
   fst(x1)	weight: (/ 1 8) + x1
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 8) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 8) + x1 + x2
 #fst(x1)	weight: 0
  tail(x1)	weight: (/ 1 8) + x1
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 8) + x1 + x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: (/ 1 8) + x1 + x2
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: x1
active(x1)	weight: (/ 3 8) + x1
  head(x1)	weight: (/ 1 8) + x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 8) + x1 + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: (/ 1 8) + x1
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #13 #16 #20 #22 #23 #28 #32 #40..43 #59 #60 #66 #67 #90 #91 #112 #113 #118
Number of SCCs: 8, DPs: 2, edges: 4
	SCC { #63 #64 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
#take(x1,x2)	weight: 0
     u(x1,x2,x3,x4)	weight: (/ 1 8) + x1 + x2 + x3 + x4
  take(x1,x2)	weight: (/ 1 8) + x1 + x2
   top(x1)	weight: 0
   #u(x1,x2,x3,x4)	weight: 0
  pair(x1,x2)	weight: (/ 1 8) + x1 + x2
   fst(x1)	weight: (/ 1 8)
 #top(x1)	weight: 0
natsFrom(x1)	weight: (/ 1 8) + x1
#head(x1)	weight: 0
splitAt(x1,x2)	weight: (/ 1 8) + x1 + x2
 #fst(x1)	weight: 0
  tail(x1)	weight: (/ 1 8) + x1
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 8) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 8) + x1 + x2
   #s(x1)	weight: 0
afterNth(x1,x2)	weight: (/ 1 8) + x1 + x2
   nil()	weight: 0
#tail(x1)	weight: 0
#splitAt(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
#afterNth(x1,x2)	weight: 0
#proper(x1)	weight: x1
active(x1)	weight: (/ 3 8) + x1
  head(x1)	weight: (/ 1 8) + x1
 #snd(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 8) + x1 + x2
#natsFrom(x1)	weight: 0
#active(x1)	weight: 0
   snd(x1)	weight: (/ 1 8) + x1
#pair(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #63 #64
Number of SCCs: 7, DPs: 0, edges: 0
YES