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: active(dbl(X)) -> dbl(active(X))
    19: active(dbls(X)) -> dbls(active(X))
    20: active(sel(X1,X2)) -> sel(active(X1),X2)
    21: active(sel(X1,X2)) -> sel(X1,active(X2))
    22: active(indx(X1,X2)) -> indx(active(X1),X2)
    23: active(dbl1(X)) -> dbl1(active(X))
    24: active(s1(X)) -> s1(active(X))
    25: active(sel1(X1,X2)) -> sel1(active(X1),X2)
    26: active(sel1(X1,X2)) -> sel1(X1,active(X2))
    27: active(quote(X)) -> quote(active(X))
    28: dbl(mark(X)) -> mark(dbl(X))
    29: dbls(mark(X)) -> mark(dbls(X))
    30: sel(mark(X1),X2) -> mark(sel(X1,X2))
    31: sel(X1,mark(X2)) -> mark(sel(X1,X2))
    32: indx(mark(X1),X2) -> mark(indx(X1,X2))
    33: dbl1(mark(X)) -> mark(dbl1(X))
    34: s1(mark(X)) -> mark(s1(X))
    35: sel1(mark(X1),X2) -> mark(sel1(X1,X2))
    36: sel1(X1,mark(X2)) -> mark(sel1(X1,X2))
    37: quote(mark(X)) -> mark(quote(X))
    38: proper(dbl(X)) -> dbl(proper(X))
    39: proper(0()) -> ok(0())
    40: proper(s(X)) -> s(proper(X))
    41: proper(dbls(X)) -> dbls(proper(X))
    42: proper(nil()) -> ok(nil())
    43: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    44: proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
    45: proper(indx(X1,X2)) -> indx(proper(X1),proper(X2))
    46: proper(from(X)) -> from(proper(X))
    47: proper(dbl1(X)) -> dbl1(proper(X))
    48: proper(01()) -> ok(01())
    49: proper(s1(X)) -> s1(proper(X))
    50: proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2))
    51: proper(quote(X)) -> quote(proper(X))
    52: dbl(ok(X)) -> ok(dbl(X))
    53: s(ok(X)) -> ok(s(X))
    54: dbls(ok(X)) -> ok(dbls(X))
    55: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    56: sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
    57: indx(ok(X1),ok(X2)) -> ok(indx(X1,X2))
    58: from(ok(X)) -> ok(from(X))
    59: dbl1(ok(X)) -> ok(dbl1(X))
    60: s1(ok(X)) -> ok(s1(X))
    61: sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2))
    62: quote(ok(X)) -> ok(quote(X))
    63: top(mark(X)) -> top(proper(X))
    64: top(ok(X)) -> top(active(X))
Number of strict rules: 64
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(dbl(s(X))) -> #s(s(dbl(X)))
   #2: #active(dbl(s(X))) -> #s(dbl(X))
   #3: #active(dbl(s(X))) -> #dbl(X)
   #4: #proper(cons(X1,X2)) -> #cons(proper(X1),proper(X2))
   #5: #proper(cons(X1,X2)) -> #proper(X1)
   #6: #proper(cons(X1,X2)) -> #proper(X2)
   #7: #dbls(mark(X)) -> #dbls(X)
   #8: #sel1(mark(X1),X2) -> #sel1(X1,X2)
   #9: #proper(from(X)) -> #from(proper(X))
   #10: #proper(from(X)) -> #proper(X)
   #11: #proper(dbls(X)) -> #dbls(proper(X))
   #12: #proper(dbls(X)) -> #proper(X)
   #13: #quote(mark(X)) -> #quote(X)
   #14: #proper(dbl1(X)) -> #dbl1(proper(X))
   #15: #proper(dbl1(X)) -> #proper(X)
   #16: #s(ok(X)) -> #s(X)
   #17: #from(ok(X)) -> #from(X)
   #18: #sel1(ok(X1),ok(X2)) -> #sel1(X1,X2)
   #19: #proper(dbl(X)) -> #dbl(proper(X))
   #20: #proper(dbl(X)) -> #proper(X)
   #21: #active(sel(s(X),cons(Y,Z))) -> #sel(X,Z)
   #22: #dbl1(ok(X)) -> #dbl1(X)
   #23: #cons(ok(X1),ok(X2)) -> #cons(X1,X2)
   #24: #proper(s(X)) -> #s(proper(X))
   #25: #proper(s(X)) -> #proper(X)
   #26: #proper(quote(X)) -> #quote(proper(X))
   #27: #proper(quote(X)) -> #proper(X)
   #28: #active(sel1(s(X),cons(Y,Z))) -> #sel1(X,Z)
   #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))) -> #s1(s1(dbl1(X)))
   #33: #active(dbl1(s(X))) -> #s1(dbl1(X))
   #34: #active(dbl1(s(X))) -> #dbl1(X)
   #35: #indx(ok(X1),ok(X2)) -> #indx(X1,X2)
   #36: #active(s1(X)) -> #s1(active(X))
   #37: #active(s1(X)) -> #active(X)
   #38: #active(dbl1(X)) -> #dbl1(active(X))
   #39: #active(dbl1(X)) -> #active(X)
   #40: #proper(indx(X1,X2)) -> #indx(proper(X1),proper(X2))
   #41: #proper(indx(X1,X2)) -> #proper(X1)
   #42: #proper(indx(X1,X2)) -> #proper(X2)
   #43: #sel(X1,mark(X2)) -> #sel(X1,X2)
   #44: #sel(ok(X1),ok(X2)) -> #sel(X1,X2)
   #45: #quote(ok(X)) -> #quote(X)
   #46: #sel(mark(X1),X2) -> #sel(X1,X2)
   #47: #dbl(ok(X)) -> #dbl(X)
   #48: #proper(s1(X)) -> #s1(proper(X))
   #49: #proper(s1(X)) -> #proper(X)
   #50: #active(sel1(X1,X2)) -> #sel1(active(X1),X2)
   #51: #active(sel1(X1,X2)) -> #active(X1)
   #52: #active(sel(X1,X2)) -> #sel(active(X1),X2)
   #53: #active(sel(X1,X2)) -> #active(X1)
   #54: #top(ok(X)) -> #top(active(X))
   #55: #top(ok(X)) -> #active(X)
   #56: #dbl1(mark(X)) -> #dbl1(X)
   #57: #proper(sel(X1,X2)) -> #sel(proper(X1),proper(X2))
   #58: #proper(sel(X1,X2)) -> #proper(X1)
   #59: #proper(sel(X1,X2)) -> #proper(X2)
   #60: #dbl(mark(X)) -> #dbl(X)
   #61: #active(indx(X1,X2)) -> #indx(active(X1),X2)
   #62: #active(indx(X1,X2)) -> #active(X1)
   #63: #s1(mark(X)) -> #s1(X)
   #64: #active(quote(X)) -> #quote(active(X))
   #65: #active(quote(X)) -> #active(X)
   #66: #s1(ok(X)) -> #s1(X)
   #67: #active(quote(sel(X,Y))) -> #sel1(X,Y)
   #68: #indx(mark(X1),X2) -> #indx(X1,X2)
   #69: #active(dbls(X)) -> #dbls(active(X))
   #70: #active(dbls(X)) -> #active(X)
   #71: #top(mark(X)) -> #top(proper(X))
   #72: #top(mark(X)) -> #proper(X)
   #73: #active(sel1(X1,X2)) -> #sel1(X1,active(X2))
   #74: #active(sel1(X1,X2)) -> #active(X2)
   #75: #sel1(X1,mark(X2)) -> #sel1(X1,X2)
   #76: #active(sel(X1,X2)) -> #sel(X1,active(X2))
   #77: #active(sel(X1,X2)) -> #active(X2)
   #78: #active(quote(dbl(X))) -> #dbl1(X)
   #79: #dbls(ok(X)) -> #dbls(X)
   #80: #active(indx(cons(X,Y),Z)) -> #cons(sel(X,Z),indx(Y,Z))
   #81: #active(indx(cons(X,Y),Z)) -> #sel(X,Z)
   #82: #active(indx(cons(X,Y),Z)) -> #indx(Y,Z)
   #83: #active(quote(s(X))) -> #s1(quote(X))
   #84: #active(quote(s(X))) -> #quote(X)
   #85: #active(dbls(cons(X,Y))) -> #cons(dbl(X),dbls(Y))
   #86: #active(dbls(cons(X,Y))) -> #dbl(X)
   #87: #active(dbls(cons(X,Y))) -> #dbls(Y)
   #88: #proper(sel1(X1,X2)) -> #sel1(proper(X1),proper(X2))
   #89: #proper(sel1(X1,X2)) -> #proper(X1)
   #90: #proper(sel1(X1,X2)) -> #proper(X2)
   #91: #active(dbl(X)) -> #dbl(active(X))
   #92: #active(dbl(X)) -> #active(X)
Number of SCCs: 14, DPs: 48, edges: 374
	SCC { #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
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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: 0
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
 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: #16
Number of SCCs: 13, DPs: 47, edges: 373
	SCC { #17 }
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
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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: 0
#proper(x1)	weight: 0
#from(x1)	weight: x1
active(x1)	weight: 0
 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
Number of SCCs: 12, DPs: 46, edges: 372
	SCC { #23 }
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
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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: 0
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
 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: #23
Number of SCCs: 11, DPs: 45, edges: 371
	SCC { #63 #66 }
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
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
 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: #63 #66
Number of SCCs: 10, DPs: 43, edges: 367
	SCC { #13 #45 }
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
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
 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: #13 #45
Number of SCCs: 9, DPs: 41, edges: 363
	SCC { #47 #60 }
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
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: x1
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
 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: #47 #60
Number of SCCs: 8, DPs: 39, edges: 359
	SCC { #22 #56 }
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
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
 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 #56
Number of SCCs: 7, DPs: 37, edges: 355
	SCC { #7 #79 }
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
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: x1
 #top(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     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
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: 0
 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: #7 #79
Number of SCCs: 6, DPs: 35, edges: 351
	SCC { #54 #71 }
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 16)	status: []	precedence above:
#cons(x1,x2)	weight: x1	status: []	precedence above:
     s(x1)	weight: x1	status: [x1]	precedence above: mark s1
  dbls(x1)	weight: (/ 1 4) + x1	status: [x1]	precedence above: 01 s dbl ok 0 nil dbl1 mark active quote cons s1
   dbl(x1)	weight: (/ 1 8) + x1	status: [x1]	precedence above: 01 s ok 0 mark s1
   top(x1)	weight: (/ 1 16)	status: []	precedence above:
  indx(x1,x2)	weight: (/ 9 16) + x2 + x1	status: [x2,x1]	precedence above: ok sel nil mark cons
 #dbl(x1)	weight: x1	status: []	precedence above:
#dbls(x1)	weight: x1	status: []	precedence above:
 #top(x1)	weight: (/ 1 16) + x1	status: [x1]	precedence above:
proper(x1)	weight: x1	status: x1
    ok(x1)	weight: x1	status: x1
     0()	weight: (/ 1 16)	status: []	precedence above: 01 mark
 #sel(x1,x2)	weight: (/ 1 16) + x2	status: [x2]	precedence above:
#indx(x1,x2)	weight: x1	status: [x1]	precedence above:
   sel(x1,x2)	weight: (/ 5 16) + x2 + x1	status: [x1,x2]	precedence above: mark
  from(x1)	weight: (/ 1 4) + x1	status: [x1]	precedence above: ok mark cons
   #s(x1)	weight: (/ 1 16)	status: []	precedence above:
   nil()	weight: (/ 1 16)	status: []	precedence above:
  dbl1(x1)	weight: x1	status: x1
#sel1(x1,x2)	weight: (/ 1 16) + x2 + x1	status: [x2,x1]	precedence above:
  mark(x1)	weight: x1	status: [x1]	precedence above:
#proper(x1)	weight: (/ 1 16)	status: []	precedence above:
#from(x1)	weight: (/ 1 16)	status: []	precedence above:
active(x1)	weight: x1	status: x1
 quote(x1)	weight: x1	status: [x1]	precedence above: nil dbl1 mark active
  cons(x1,x2)	weight: max{x2, (/ 3 16) + x1}	status: []	precedence above: ok
#active(x1)	weight: x1	status: []	precedence above:
#quote(x1)	weight: (/ 1 16)	status: []	precedence above:
  #s1(x1)	weight: (/ 1 16)	status: []	precedence above:
  sel1(x1,x2)	weight: (/ 1 4) + x2 + x1	status: [x1,x2]	precedence above: ok sel mark
    s1(x1)	weight: x1	status: x1
    Usable rules: { 1..62 }
    Removed DPs: #71
Number of SCCs: 6, DPs: 34, edges: 348
	SCC { #54 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
  dbls(x1)	weight: (/ 1 4) + x1
   dbl(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
  indx(x1,x2)	weight: (/ 1 4) + x2
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: x1
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x1
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: (/ 1 4) + x1
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4)
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
 quote(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: (/ 1 4) + x2
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: (/ 1 4) + x2
    s1(x1)	weight: (/ 1 4) + x1
    Usable rules: { 1..37 52..62 }
    Removed DPs: #54
Number of SCCs: 5, DPs: 33, edges: 347
	SCC { #35 #68 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
  dbls(x1)	weight: (/ 1 4) + x1
   dbl(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
  indx(x1,x2)	weight: (/ 1 4) + x2
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: x1
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: x2
   sel(x1,x2)	weight: (/ 1 4) + x1
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: (/ 1 4) + x1
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4)
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
 quote(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: (/ 1 4) + x2
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: (/ 1 4) + x2
    s1(x1)	weight: (/ 1 4) + x1
    Usable rules: { }
    Removed DPs: #35
Number of SCCs: 6, DPs: 32, edges: 344
	SCC { #68 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
  dbls(x1)	weight: (/ 1 4) + x1
   dbl(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: (/ 1 2) + x1
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: x1
   sel(x1,x2)	weight: (/ 1 4) + x1
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x2
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: x2
    s1(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #68
Number of SCCs: 5, DPs: 31, edges: 343
	SCC { #8 #18 #75 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
  dbls(x1)	weight: (/ 1 4) + x1
   dbl(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x1
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: x1 + x2
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x2
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: x2
    s1(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #8 #18 #75
Number of SCCs: 5, DPs: 28, edges: 334
	SCC { #43 #44 #46 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
  dbls(x1)	weight: (/ 1 4) + x1
   dbl(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: x2
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x1
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x2
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: x2
    s1(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #43 #44
Number of SCCs: 5, DPs: 26, edges: 326
	SCC { #46 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
  dbls(x1)	weight: (/ 1 4) + x1
   dbl(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
  indx(x1,x2)	weight: 0
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: x1
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x1
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: 0
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
 quote(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x2
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: x2
    s1(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #46
Number of SCCs: 4, DPs: 25, edges: 325
	SCC { #37 #39 #51 #53 #62 #65 #70 #74 #77 #92 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
  dbls(x1)	weight: (/ 1 4) + x1
   dbl(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
  indx(x1,x2)	weight: (/ 1 4) + x1
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: (/ 1 4)
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x1 + x2
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: (/ 1 4) + x1
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4)
#proper(x1)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
 quote(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: (/ 1 4) + x2
#active(x1)	weight: x1
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: (/ 1 4) + x1 + x2
    s1(x1)	weight: (/ 1 4) + x1
    Usable rules: { }
    Removed DPs: #37 #39 #51 #53 #62 #65 #70 #74 #77 #92
Number of SCCs: 4, DPs: 15, edges: 225
	SCC { #5 #6 #10 #12 #15 #20 #25 #27 #41 #42 #49 #58 #59 #89 #90 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#dbl1(x1)	weight: 0
    01()	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
  dbls(x1)	weight: (/ 1 4) + x1
   dbl(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: 0
  indx(x1,x2)	weight: (/ 1 4) + x1 + x2
 #dbl(x1)	weight: 0
#dbls(x1)	weight: 0
 #top(x1)	weight: 0
proper(x1)	weight: (/ 1 4)
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
 #sel(x1,x2)	weight: 0
#indx(x1,x2)	weight: 0
   sel(x1,x2)	weight: (/ 1 4) + x1 + x2
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
   nil()	weight: 0
  dbl1(x1)	weight: (/ 1 4) + x1
#sel1(x1,x2)	weight: 0
  mark(x1)	weight: (/ 1 4)
#proper(x1)	weight: x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 4) + x1
 quote(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: (/ 1 4) + x1 + x2
#active(x1)	weight: 0
#quote(x1)	weight: 0
  #s1(x1)	weight: 0
  sel1(x1,x2)	weight: (/ 1 4) + x1 + x2
    s1(x1)	weight: (/ 1 4) + x1
    Usable rules: { }
    Removed DPs: #5 #6 #10 #12 #15 #20 #25 #27 #41 #42 #49 #58 #59 #89 #90
Number of SCCs: 3, DPs: 0, edges: 0
YES