Input TRS:
    1: active(dbl(0())) -> mark(0())
    2: active(dbl(s(X))) -> mark(s(s(dbl(X))))
    3: active(dbls(nil())) -> mark(nil())
    4: active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
    5: active(sel(0(),cons(X,Y))) -> mark(X)
    6: active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
    7: active(indx(nil(),X)) -> mark(nil())
    8: active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z)))
    9: active(from(X)) -> mark(cons(X,from(s(X))))
    10: active(dbl1(0())) -> mark(01())
    11: active(dbl1(s(X))) -> mark(s1(s1(dbl1(X))))
    12: active(sel1(0(),cons(X,Y))) -> mark(X)
    13: active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z))
    14: active(quote(0())) -> mark(01())
    15: active(quote(s(X))) -> mark(s1(quote(X)))
    16: active(quote(dbl(X))) -> mark(dbl1(X))
    17: active(quote(sel(X,Y))) -> mark(sel1(X,Y))
    18: mark(dbl(X)) -> active(dbl(mark(X)))
    19: mark(0()) -> active(0())
    20: mark(s(X)) -> active(s(X))
    21: mark(dbls(X)) -> active(dbls(mark(X)))
    22: mark(nil()) -> active(nil())
    23: mark(cons(X1,X2)) -> active(cons(X1,X2))
    24: mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
    25: mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
    26: mark(from(X)) -> active(from(X))
    27: mark(dbl1(X)) -> active(dbl1(mark(X)))
    28: mark(01()) -> active(01())
    29: mark(s1(X)) -> active(s1(mark(X)))
    30: mark(sel1(X1,X2)) -> active(sel1(mark(X1),mark(X2)))
    31: mark(quote(X)) -> active(quote(mark(X)))
    32: dbl(mark(X)) -> dbl(X)
    33: dbl(active(X)) -> dbl(X)
    34: s(mark(X)) -> s(X)
    35: s(active(X)) -> s(X)
    36: dbls(mark(X)) -> dbls(X)
    37: dbls(active(X)) -> dbls(X)
    38: cons(mark(X1),X2) -> cons(X1,X2)
    39: cons(X1,mark(X2)) -> cons(X1,X2)
    40: cons(active(X1),X2) -> cons(X1,X2)
    41: cons(X1,active(X2)) -> cons(X1,X2)
    42: sel(mark(X1),X2) -> sel(X1,X2)
    43: sel(X1,mark(X2)) -> sel(X1,X2)
    44: sel(active(X1),X2) -> sel(X1,X2)
    45: sel(X1,active(X2)) -> sel(X1,X2)
    46: indx(mark(X1),X2) -> indx(X1,X2)
    47: indx(X1,mark(X2)) -> indx(X1,X2)
    48: indx(active(X1),X2) -> indx(X1,X2)
    49: indx(X1,active(X2)) -> indx(X1,X2)
    50: from(mark(X)) -> from(X)
    51: from(active(X)) -> from(X)
    52: dbl1(mark(X)) -> dbl1(X)
    53: dbl1(active(X)) -> dbl1(X)
    54: s1(mark(X)) -> s1(X)
    55: s1(active(X)) -> s1(X)
    56: sel1(mark(X1),X2) -> sel1(X1,X2)
    57: sel1(X1,mark(X2)) -> sel1(X1,X2)
    58: sel1(active(X1),X2) -> sel1(X1,X2)
    59: sel1(X1,active(X2)) -> sel1(X1,X2)
    60: quote(mark(X)) -> quote(X)
    61: quote(active(X)) -> quote(X)
Number of strict rules: 61
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(dbl(s(X))) -> #mark(s(s(dbl(X))))
   #2: #active(dbl(s(X))) -> #s(s(dbl(X)))
   #3: #active(dbl(s(X))) -> #s(dbl(X))
   #4: #active(dbl(s(X))) -> #dbl(X)
   #5: #sel(X1,mark(X2)) -> #sel(X1,X2)
   #6: #mark(s1(X)) -> #active(s1(mark(X)))
   #7: #mark(s1(X)) -> #s1(mark(X))
   #8: #mark(s1(X)) -> #mark(X)
   #9: #s(active(X)) -> #s(X)
   #10: #indx(mark(X1),X2) -> #indx(X1,X2)
   #11: #sel(mark(X1),X2) -> #sel(X1,X2)
   #12: #cons(X1,active(X2)) -> #cons(X1,X2)
   #13: #dbls(active(X)) -> #dbls(X)
   #14: #indx(X1,mark(X2)) -> #indx(X1,X2)
   #15: #dbl1(active(X)) -> #dbl1(X)
   #16: #indx(active(X1),X2) -> #indx(X1,X2)
   #17: #sel1(active(X1),X2) -> #sel1(X1,X2)
   #18: #quote(active(X)) -> #quote(X)
   #19: #cons(mark(X1),X2) -> #cons(X1,X2)
   #20: #active(sel(s(X),cons(Y,Z))) -> #mark(sel(X,Z))
   #21: #active(sel(s(X),cons(Y,Z))) -> #sel(X,Z)
   #22: #sel1(X1,active(X2)) -> #sel1(X1,X2)
   #23: #s1(active(X)) -> #s1(X)
   #24: #cons(active(X1),X2) -> #cons(X1,X2)
   #25: #from(active(X)) -> #from(X)
   #26: #active(sel1(s(X),cons(Y,Z))) -> #mark(sel1(X,Z))
   #27: #active(sel1(s(X),cons(Y,Z))) -> #sel1(X,Z)
   #28: #active(from(X)) -> #mark(cons(X,from(s(X))))
   #29: #active(from(X)) -> #cons(X,from(s(X)))
   #30: #active(from(X)) -> #from(s(X))
   #31: #active(from(X)) -> #s(X)
   #32: #active(dbl1(s(X))) -> #mark(s1(s1(dbl1(X))))
   #33: #active(dbl1(s(X))) -> #s1(s1(dbl1(X)))
   #34: #active(dbl1(s(X))) -> #s1(dbl1(X))
   #35: #active(dbl1(s(X))) -> #dbl1(X)
   #36: #sel1(X1,mark(X2)) -> #sel1(X1,X2)
   #37: #mark(sel(X1,X2)) -> #active(sel(mark(X1),mark(X2)))
   #38: #mark(sel(X1,X2)) -> #sel(mark(X1),mark(X2))
   #39: #mark(sel(X1,X2)) -> #mark(X1)
   #40: #mark(sel(X1,X2)) -> #mark(X2)
   #41: #mark(cons(X1,X2)) -> #active(cons(X1,X2))
   #42: #sel(X1,active(X2)) -> #sel(X1,X2)
   #43: #active(sel1(0(),cons(X,Y))) -> #mark(X)
   #44: #mark(quote(X)) -> #active(quote(mark(X)))
   #45: #mark(quote(X)) -> #quote(mark(X))
   #46: #mark(quote(X)) -> #mark(X)
   #47: #sel1(mark(X1),X2) -> #sel1(X1,X2)
   #48: #active(quote(0())) -> #mark(01())
   #49: #mark(sel1(X1,X2)) -> #active(sel1(mark(X1),mark(X2)))
   #50: #mark(sel1(X1,X2)) -> #sel1(mark(X1),mark(X2))
   #51: #mark(sel1(X1,X2)) -> #mark(X1)
   #52: #mark(sel1(X1,X2)) -> #mark(X2)
   #53: #dbl1(mark(X)) -> #dbl1(X)
   #54: #indx(X1,active(X2)) -> #indx(X1,X2)
   #55: #mark(indx(X1,X2)) -> #active(indx(mark(X1),X2))
   #56: #mark(indx(X1,X2)) -> #indx(mark(X1),X2)
   #57: #mark(indx(X1,X2)) -> #mark(X1)
   #58: #mark(s(X)) -> #active(s(X))
   #59: #active(indx(nil(),X)) -> #mark(nil())
   #60: #cons(X1,mark(X2)) -> #cons(X1,X2)
   #61: #active(dbl1(0())) -> #mark(01())
   #62: #dbl(active(X)) -> #dbl(X)
   #63: #active(sel(0(),cons(X,Y))) -> #mark(X)
   #64: #sel(active(X1),X2) -> #sel(X1,X2)
   #65: #mark(01()) -> #active(01())
   #66: #mark(nil()) -> #active(nil())
   #67: #s(mark(X)) -> #s(X)
   #68: #mark(dbl1(X)) -> #active(dbl1(mark(X)))
   #69: #mark(dbl1(X)) -> #dbl1(mark(X))
   #70: #mark(dbl1(X)) -> #mark(X)
   #71: #quote(mark(X)) -> #quote(X)
   #72: #active(quote(sel(X,Y))) -> #mark(sel1(X,Y))
   #73: #active(quote(sel(X,Y))) -> #sel1(X,Y)
   #74: #dbl(mark(X)) -> #dbl(X)
   #75: #mark(0()) -> #active(0())
   #76: #mark(from(X)) -> #active(from(X))
   #77: #dbls(mark(X)) -> #dbls(X)
   #78: #mark(dbls(X)) -> #active(dbls(mark(X)))
   #79: #mark(dbls(X)) -> #dbls(mark(X))
   #80: #mark(dbls(X)) -> #mark(X)
   #81: #active(quote(dbl(X))) -> #mark(dbl1(X))
   #82: #active(quote(dbl(X))) -> #dbl1(X)
   #83: #active(dbls(nil())) -> #mark(nil())
   #84: #active(dbl(0())) -> #mark(0())
   #85: #s1(mark(X)) -> #s1(X)
   #86: #active(indx(cons(X,Y),Z)) -> #mark(cons(sel(X,Z),indx(Y,Z)))
   #87: #active(indx(cons(X,Y),Z)) -> #cons(sel(X,Z),indx(Y,Z))
   #88: #active(indx(cons(X,Y),Z)) -> #sel(X,Z)
   #89: #active(indx(cons(X,Y),Z)) -> #indx(Y,Z)
   #90: #active(quote(s(X))) -> #mark(s1(quote(X)))
   #91: #active(quote(s(X))) -> #s1(quote(X))
   #92: #active(quote(s(X))) -> #quote(X)
   #93: #active(dbls(cons(X,Y))) -> #mark(cons(dbl(X),dbls(Y)))
   #94: #active(dbls(cons(X,Y))) -> #cons(dbl(X),dbls(Y))
   #95: #active(dbls(cons(X,Y))) -> #dbl(X)
   #96: #active(dbls(cons(X,Y))) -> #dbls(Y)
   #97: #from(mark(X)) -> #from(X)
   #98: #mark(dbl(X)) -> #active(dbl(mark(X)))
   #99: #mark(dbl(X)) -> #dbl(mark(X))
   #100: #mark(dbl(X)) -> #mark(X)
Number of SCCs: 12, DPs: 52, edges: 281
	SCC { #62 #74 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: x1
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #62 #74
Number of SCCs: 11, DPs: 50, edges: 277
	SCC { #13 #77 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: x1
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #13 #77
Number of SCCs: 10, DPs: 48, edges: 273
	SCC { #9 #67 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: x1
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #9 #67
Number of SCCs: 9, DPs: 46, edges: 269
	SCC { #15 #53 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: x1
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #15 #53
Number of SCCs: 8, DPs: 44, edges: 265
	SCC { #18 #71 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: x1
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #18 #71
Number of SCCs: 7, DPs: 42, edges: 261
	SCC { #23 #85 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: x1
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #23 #85
Number of SCCs: 6, DPs: 40, edges: 257
	SCC { #25 #97 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: x1
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #25 #97
Number of SCCs: 5, DPs: 38, edges: 253
	SCC { #12 #19 #24 #60 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: x1
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #19 #24
Number of SCCs: 5, DPs: 36, edges: 241
	SCC { #12 #60 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: x2
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #12 #60
Number of SCCs: 4, DPs: 34, edges: 237
	SCC { #10 #14 #16 #54 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: x2
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #14 #54
Number of SCCs: 5, DPs: 32, edges: 225
	SCC { #10 #16 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: x1
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #10 #16
Number of SCCs: 4, DPs: 30, edges: 221
	SCC { #5 #11 #42 #64 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: x1
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #11 #64
Number of SCCs: 5, DPs: 28, edges: 209
	SCC { #5 #42 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: x2
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #5 #42
Number of SCCs: 4, DPs: 26, edges: 205
	SCC { #17 #22 #36 #47 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: x2
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #22 #36
Number of SCCs: 5, DPs: 24, edges: 193
	SCC { #17 #47 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
  dbls(x1)	weight: 0
   dbl(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: x1
  mark(x1)	weight: (/ 1 2) + x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: 0
    s1(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #17 #47
Number of SCCs: 4, DPs: 22, edges: 189
	SCC { #8 #20 #26 #32 #37 #39 #40 #43 #44 #46 #49 #51 #52 #57 #63 #68 #70 #72 #80 #81 #90 #100 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
  dbls(x1)	weight: (/ 116971 4) + x1
   dbl(x1)	weight: (/ 4569 4) + x1
  indx(x1,x2)	weight: max{56201 + x2, 56201 + x1}
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
#mark(x1)	weight: x1
     0()	weight: (/ 1 4)
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: max{(/ 1 4) + x2, (/ 56201 2) + x1}
  from(x1)	weight: (/ 56201 2) + x1
   #s(x1)	weight: 0
   nil()	weight: (/ 1 4)
  dbl1(x1)	weight: (/ 1 4) + x1
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: x1
#from(x1)	weight: 0
active(x1)	weight: x1
 quote(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: max{x2, (/ 56201 2) + x1}
#active(x1)	weight: x1
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: max{(/ 1 2) + x2, (/ 1 4) + x1}
    s1(x1)	weight: x1
    Usable rules: { 1..61 }
    Removed DPs: #39 #40 #43 #46 #51 #52 #57 #63 #70 #72 #80 #81 #100
Number of SCCs: 7, DPs: 9, edges: 11
	SCC { #26 #49 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded.
#dbl1(x1)	weight: x1	status: []	precedence above:
    01()	weight: (/ 3 8)	status: []	precedence above:
#cons(x1,x2)	weight: x2	status: []	precedence above:
     s(x1)	weight: x1	status: [x1]	precedence above:
  dbls(x1)	weight: x1	status: []	precedence above: 01 s dbl #mark 0 nil mark active cons sel1
   dbl(x1)	weight: x1	status: [x1]	precedence above: 01 s #mark 0 mark active cons sel1
  indx(x1,x2)	weight: (/ 1 4) + x2 + x1	status: [x2]	precedence above: 01 #mark 0 mark active cons sel1
 #dbl(x1)	weight: (/ 1 8)	status: []	precedence above:
#dbls(x1)	weight: (/ 1 8)	status: []	precedence above:
#mark(x1)	weight: x1	status: [x1]	precedence above:
     0()	weight: (/ 3 8)	status: []	precedence above: 01 #mark mark cons sel1
 #sel(x1,x2)	weight: (/ 1 8) + x2 + x1	status: [x1,x2]	precedence above:
#indx(x1,x2)	weight: x1	status: [x1]	precedence above:
   sel(x1,x2)	weight: x2 + x1	status: []	precedence above:
  from(x1)	weight: (/ 1 8) + x1	status: []	precedence above: #mark cons sel1
   #s(x1)	weight: (/ 1 8)	status: []	precedence above:
   nil()	weight: 0	status: []	precedence above:
  dbl1(x1)	weight: (/ 3 8)	status: []	precedence above: 01 s1
#sel1(x1,x2)	weight: (/ 1 8) + x2	status: [x2]	precedence above:
  mark(x1)	weight: x1	status: x1
#from(x1)	weight: x1	status: []	precedence above:
active(x1)	weight: x1	status: x1
 quote(x1)	weight: (/ 3 8) + x1	status: [x1]	precedence above: 01 #mark dbl1 sel1 s1
  cons(x1,x2)	weight: max{x2, (/ 1 8) + x1}	status: []	precedence above: #mark sel1
#active(x1)	weight: x1	status: x1
#quote(x1)	weight: (/ 1 8)	status: []	precedence above:
  #s1(x1)	weight: x1	status: []	precedence above:
  sel1(x1,x2)	weight: (/ 1 4) + x2 + x1	status: [x1]	precedence above: #mark
    s1(x1)	weight: (/ 3 8)	status: []	precedence above: 01 dbl1
    Usable rules: { 1..61 }
    Removed DPs: #26 #49
Number of SCCs: 6, DPs: 7, edges: 9
	SCC { #20 #37 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded.
#dbl1(x1)	weight: x1	status: []	precedence above:
    01()	weight: (/ 3 8)	status: []	precedence above:
#cons(x1,x2)	weight: x2	status: []	precedence above:
     s(x1)	weight: x1	status: [x1]	precedence above:
  dbls(x1)	weight: x1	status: []	precedence above: 01 s dbl #mark 0 nil mark active cons sel1
   dbl(x1)	weight: x1	status: [x1]	precedence above: 01 s #mark 0 mark active cons sel1
  indx(x1,x2)	weight: (/ 1 4) + x2 + x1	status: [x2]	precedence above: 01 #mark 0 mark active cons sel1
 #dbl(x1)	weight: (/ 1 8)	status: []	precedence above:
#dbls(x1)	weight: (/ 1 8)	status: []	precedence above:
#mark(x1)	weight: x1	status: [x1]	precedence above:
     0()	weight: (/ 3 8)	status: []	precedence above: 01 #mark mark cons sel1
 #sel(x1,x2)	weight: (/ 1 8) + x2 + x1	status: [x1,x2]	precedence above:
#indx(x1,x2)	weight: x1	status: [x1]	precedence above:
   sel(x1,x2)	weight: x2 + x1	status: [x1]	precedence above: #mark
  from(x1)	weight: (/ 1 8) + x1	status: []	precedence above: #mark cons sel1
   #s(x1)	weight: (/ 1 8)	status: []	precedence above:
   nil()	weight: 0	status: []	precedence above:
  dbl1(x1)	weight: (/ 3 8)	status: []	precedence above: 01 s1
#sel1(x1,x2)	weight: (/ 1 8) + x2	status: [x2]	precedence above:
  mark(x1)	weight: x1	status: x1
#from(x1)	weight: x1	status: []	precedence above:
active(x1)	weight: x1	status: x1
 quote(x1)	weight: (/ 3 8) + x1	status: [x1]	precedence above: 01 #mark dbl1 sel1 s1
  cons(x1,x2)	weight: max{x2, (/ 1 8) + x1}	status: []	precedence above: #mark sel1
#active(x1)	weight: x1	status: x1
#quote(x1)	weight: (/ 1 8)	status: []	precedence above:
  #s1(x1)	weight: x1	status: []	precedence above:
  sel1(x1,x2)	weight: (/ 1 4) + x2 + x1	status: [x1]	precedence above: #mark
    s1(x1)	weight: (/ 3 8)	status: []	precedence above: 01 dbl1
    Usable rules: { 1..61 }
    Removed DPs: #20 #37
Number of SCCs: 5, DPs: 5, edges: 7
	SCC { #8 #32 #44 #68 #90 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded.
#dbl1(x1)	weight: x1	status: []	precedence above:
    01()	weight: (/ 1 4)	status: []	precedence above:
#cons(x1,x2)	weight: x2	status: []	precedence above:
     s(x1)	weight: x1	status: [x1]	precedence above:
  dbls(x1)	weight: x1	status: []	precedence above: 01 s dbl #mark 0 nil mark active cons sel1
   dbl(x1)	weight: x1	status: [x1]	precedence above: 01 s #mark 0 mark active cons sel1
  indx(x1,x2)	weight: (/ 1 2) + x2 + x1	status: [x2]	precedence above: 01 s #mark 0 mark active cons sel1
 #dbl(x1)	weight: (/ 1 4)	status: []	precedence above:
#dbls(x1)	weight: (/ 1 4)	status: []	precedence above:
#mark(x1)	weight: x1	status: [x1]	precedence above:
     0()	weight: (/ 1 4)	status: []	precedence above: 01 #mark cons sel1
 #sel(x1,x2)	weight: (/ 1 4) + x2 + x1	status: [x1,x2]	precedence above:
#indx(x1,x2)	weight: x1	status: [x1]	precedence above:
   sel(x1,x2)	weight: x2 + x1	status: [x1]	precedence above: #mark
  from(x1)	weight: (/ 1 4) + x1	status: []	precedence above: #mark cons sel1
   #s(x1)	weight: (/ 1 4)	status: []	precedence above:
   nil()	weight: 0	status: []	precedence above:
  dbl1(x1)	weight: (/ 126391 4) + x1	status: [x1]	precedence above: 01 #mark s1
#sel1(x1,x2)	weight: (/ 1 4) + x2	status: [x2]	precedence above:
  mark(x1)	weight: x1	status: x1
#from(x1)	weight: x1	status: []	precedence above:
active(x1)	weight: x1	status: x1
 quote(x1)	weight: (/ 126391 4) + x1	status: [x1]	precedence above: 01 #mark dbl1 sel1 s1
  cons(x1,x2)	weight: max{x2, (/ 1 4) + x1}	status: []	precedence above: #mark sel1
#active(x1)	weight: x1	status: x1
#quote(x1)	weight: (/ 1 4)	status: []	precedence above:
  #s1(x1)	weight: x1	status: []	precedence above:
  sel1(x1,x2)	weight: (/ 63195 2) + x2 + x1	status: [x1]	precedence above: #mark
    s1(x1)	weight: x1	status: [x1]	precedence above: 01
    Usable rules: { 1..61 }
    Removed DPs: #8 #32 #44 #68 #90
Number of SCCs: 4, DPs: 0, edges: 0
YES