Input TRS:
    1: dbl(0()) -> 0()
    2: dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
    3: dbls(nil()) -> nil()
    4: dbls(cons(X,Y)) -> cons(n__dbl(activate(X)),n__dbls(activate(Y)))
    5: sel(0(),cons(X,Y)) -> activate(X)
    6: sel(s(X),cons(Y,Z)) -> sel(activate(X),activate(Z))
    7: indx(nil(),X) -> nil()
    8: indx(cons(X,Y),Z) -> cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
    9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
    10: s(X) -> n__s(X)
    11: dbl(X) -> n__dbl(X)
    12: dbls(X) -> n__dbls(X)
    13: sel(X1,X2) -> n__sel(X1,X2)
    14: indx(X1,X2) -> n__indx(X1,X2)
    15: from(X) -> n__from(X)
    16: activate(n__s(X)) -> s(X)
    17: activate(n__dbl(X)) -> dbl(activate(X))
    18: activate(n__dbls(X)) -> dbls(activate(X))
    19: activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2))
    20: activate(n__indx(X1,X2)) -> indx(activate(X1),X2)
    21: activate(n__from(X)) -> from(X)
    22: activate(X) -> X
Number of strict rules: 22
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #dbl(s(X)) -> #s(n__s(n__dbl(activate(X))))
   #2: #dbl(s(X)) -> #activate(X)
   #3: #sel(s(X),cons(Y,Z)) -> #sel(activate(X),activate(Z))
   #4: #sel(s(X),cons(Y,Z)) -> #activate(X)
   #5: #sel(s(X),cons(Y,Z)) -> #activate(Z)
   #6: #from(X) -> #activate(X)
   #7: #from(X) -> #activate(X)
   #8: #activate(n__indx(X1,X2)) -> #indx(activate(X1),X2)
   #9: #activate(n__indx(X1,X2)) -> #activate(X1)
   #10: #sel(0(),cons(X,Y)) -> #activate(X)
   #11: #activate(n__dbl(X)) -> #dbl(activate(X))
   #12: #activate(n__dbl(X)) -> #activate(X)
   #13: #activate(n__sel(X1,X2)) -> #sel(activate(X1),activate(X2))
   #14: #activate(n__sel(X1,X2)) -> #activate(X1)
   #15: #activate(n__sel(X1,X2)) -> #activate(X2)
   #16: #activate(n__from(X)) -> #from(X)
   #17: #activate(n__s(X)) -> #s(X)
   #18: #indx(cons(X,Y),Z) -> #activate(X)
   #19: #indx(cons(X,Y),Z) -> #activate(Z)
   #20: #indx(cons(X,Y),Z) -> #activate(Y)
   #21: #indx(cons(X,Y),Z) -> #activate(Z)
   #22: #dbls(cons(X,Y)) -> #activate(X)
   #23: #dbls(cons(X,Y)) -> #activate(Y)
   #24: #activate(n__dbls(X)) -> #dbls(activate(X))
   #25: #activate(n__dbls(X)) -> #activate(X)
Number of SCCs: 1, DPs: 23, edges: 187
	SCC { #2..16 #18..25 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
     s(x1)	weight: x1
  dbls(x1)	weight: (/ 1 4) + x1
activate(x1)	weight: x1
   dbl(x1)	weight: (/ 1 4) + x1
  indx(x1,x2)	weight: max{(/ 3 4) + x2, (/ 7 8) + x1}
n__indx(x1,x2)	weight: max{(/ 3 4) + x2, (/ 7 8) + x1}
n__from(x1)	weight: (/ 1 4) + x1
 #dbl(x1)	weight: (/ 1 8) + x1
#activate(x1)	weight: x1
#dbls(x1)	weight: (/ 1 8) + x1
n__dbls(x1)	weight: (/ 1 4) + x1
  n__s(x1)	weight: x1
n__dbl(x1)	weight: (/ 1 4) + x1
     0()	weight: (/ 1 8)
 #sel(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 4) + x1}
#indx(x1,x2)	weight: max{(/ 1 8) + x2, (/ 1 8) + x1}
   sel(x1,x2)	weight: max{(/ 1 2) + x2, (/ 3 8) + x1}
  from(x1)	weight: (/ 1 4) + x1
   #s(x1)	weight: 0
   nil()	weight: (/ 7 8)
n__sel(x1,x2)	weight: max{(/ 1 2) + x2, (/ 3 8) + x1}
#from(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: max{x2, (/ 1 4) + x1}
    Usable rules: { 1..22 }
    Removed DPs: #2 #4..16 #18..25
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #3 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded.
     s(x1)	weight: x1	status: [x1]	precedence above: n__s #sel
  dbls(x1)	weight: (/ 3 8) + x1	status: []	precedence above: n__dbls nil cons
activate(x1)	weight: x1	status: x1
   dbl(x1)	weight: (/ 3 16) + x1	status: [x1]	precedence above: s n__s n__dbl 0 #sel
  indx(x1,x2)	weight: (/ 1 4) + x2 + x1	status: [x2]	precedence above: n__indx nil cons
n__indx(x1,x2)	weight: (/ 1 4) + x2 + x1	status: [x2]	precedence above: indx nil cons
n__from(x1)	weight: (/ 3 16) + x1	status: []	precedence above: s n__s #sel from cons
 #dbl(x1)	weight: (/ 1 16)	status: []	precedence above:
#activate(x1)	weight: (/ 1 16)	status: []	precedence above:
#dbls(x1)	weight: (/ 1 16)	status: []	precedence above:
n__dbls(x1)	weight: (/ 3 8) + x1	status: []	precedence above: dbls nil cons
  n__s(x1)	weight: x1	status: [x1]	precedence above: s #sel
n__dbl(x1)	weight: (/ 3 16) + x1	status: [x1]	precedence above: s dbl n__s 0 #sel
     0()	weight: (/ 1 16)	status: []	precedence above: s dbl n__s n__dbl #sel
 #sel(x1,x2)	weight: x1	status: [x1]	precedence above:
#indx(x1,x2)	weight: x2	status: []	precedence above:
   sel(x1,x2)	weight: (/ 1 16) + x2	status: []	precedence above: n__sel cons
  from(x1)	weight: (/ 3 16) + x1	status: []	precedence above: s n__from n__s #sel cons
   #s(x1)	weight: x1	status: []	precedence above:
   nil()	weight: (/ 1 16)	status: []	precedence above:
n__sel(x1,x2)	weight: (/ 1 16) + x2	status: []	precedence above: sel cons
#from(x1)	weight: x1	status: []	precedence above:
  cons(x1,x2)	weight: max{x2, (/ 1 8) + x1}	status: []	precedence above:
    Usable rules: { 1..22 }
    Removed DPs: #3
Number of SCCs: 0, DPs: 0, edges: 0
YES