Input TRS:
    1: active(nats()) -> mark(adx(zeros()))
    2: active(zeros()) -> mark(cons(0(),zeros()))
    3: active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
    4: active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
    5: active(hd(cons(X,Y))) -> mark(X)
    6: active(tl(cons(X,Y))) -> mark(Y)
    7: active(adx(X)) -> adx(active(X))
    8: active(incr(X)) -> incr(active(X))
    9: active(hd(X)) -> hd(active(X))
    10: active(tl(X)) -> tl(active(X))
    11: adx(mark(X)) -> mark(adx(X))
    12: incr(mark(X)) -> mark(incr(X))
    13: hd(mark(X)) -> mark(hd(X))
    14: tl(mark(X)) -> mark(tl(X))
    15: proper(nats()) -> ok(nats())
    16: proper(adx(X)) -> adx(proper(X))
    17: proper(zeros()) -> ok(zeros())
    18: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    19: proper(0()) -> ok(0())
    20: proper(incr(X)) -> incr(proper(X))
    21: proper(s(X)) -> s(proper(X))
    22: proper(hd(X)) -> hd(proper(X))
    23: proper(tl(X)) -> tl(proper(X))
    24: adx(ok(X)) -> ok(adx(X))
    25: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    26: incr(ok(X)) -> ok(incr(X))
    27: s(ok(X)) -> ok(s(X))
    28: hd(ok(X)) -> ok(hd(X))
    29: tl(ok(X)) -> ok(tl(X))
    30: top(mark(X)) -> top(proper(X))
    31: top(ok(X)) -> top(active(X))
Number of strict rules: 31
Direct Order(PosReal,>,Poly) ... removes: 5 6
  incr(x1)	weight: x1
    hd(x1)	weight: (/ 1 4) + 2 * x1
     s(x1)	weight: x1
   top(x1)	weight: x1
   adx(x1)	weight: x1
 zeros()	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
    tl(x1)	weight: (/ 1 4) + x1
  mark(x1)	weight: x1
  nats()	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: x1 + x2
Number of strict rules: 29
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(zeros()) -> #cons(0(),zeros())
   #2: #tl(ok(X)) -> #tl(X)
   #3: #hd(mark(X)) -> #hd(X)
   #4: #active(hd(X)) -> #hd(active(X))
   #5: #active(hd(X)) -> #active(X)
   #6: #adx(mark(X)) -> #adx(X)
   #7: #adx(ok(X)) -> #adx(X)
   #8: #proper(tl(X)) -> #tl(proper(X))
   #9: #proper(tl(X)) -> #proper(X)
   #10: #incr(mark(X)) -> #incr(X)
   #11: #top(ok(X)) -> #top(active(X))
   #12: #top(ok(X)) -> #active(X)
   #13: #tl(mark(X)) -> #tl(X)
   #14: #top(mark(X)) -> #top(proper(X))
   #15: #top(mark(X)) -> #proper(X)
   #16: #cons(ok(X1),ok(X2)) -> #cons(X1,X2)
   #17: #proper(incr(X)) -> #incr(proper(X))
   #18: #proper(incr(X)) -> #proper(X)
   #19: #active(adx(X)) -> #adx(active(X))
   #20: #active(adx(X)) -> #active(X)
   #21: #active(tl(X)) -> #tl(active(X))
   #22: #active(tl(X)) -> #active(X)
   #23: #hd(ok(X)) -> #hd(X)
   #24: #proper(hd(X)) -> #hd(proper(X))
   #25: #proper(hd(X)) -> #proper(X)
   #26: #s(ok(X)) -> #s(X)
   #27: #incr(ok(X)) -> #incr(X)
   #28: #proper(s(X)) -> #s(proper(X))
   #29: #proper(s(X)) -> #proper(X)
   #30: #proper(adx(X)) -> #adx(proper(X))
   #31: #proper(adx(X)) -> #proper(X)
   #32: #active(incr(cons(X,Y))) -> #cons(s(X),incr(Y))
   #33: #active(incr(cons(X,Y))) -> #s(X)
   #34: #active(incr(cons(X,Y))) -> #incr(Y)
   #35: #active(nats()) -> #adx(zeros())
   #36: #active(incr(X)) -> #incr(active(X))
   #37: #active(incr(X)) -> #active(X)
   #38: #active(adx(cons(X,Y))) -> #incr(cons(X,adx(Y)))
   #39: #active(adx(cons(X,Y))) -> #cons(X,adx(Y))
   #40: #active(adx(cons(X,Y))) -> #adx(Y)
   #41: #proper(cons(X1,X2)) -> #cons(proper(X1),proper(X2))
   #42: #proper(cons(X1,X2)) -> #proper(X1)
   #43: #proper(cons(X1,X2)) -> #proper(X2)
Number of SCCs: 9, DPs: 23, edges: 87
	SCC { #26 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #adx(x1)	weight: 0
  incr(x1)	weight: 0
    hd(x1)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
   adx(x1)	weight: 0
 zeros()	weight: 0
  #tl(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: x1
    tl(x1)	weight: 0
  mark(x1)	weight: 0
#incr(x1)	weight: 0
#proper(x1)	weight: 0
  #hd(x1)	weight: 0
  nats()	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #26
Number of SCCs: 8, DPs: 22, edges: 86
	SCC { #16 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #adx(x1)	weight: 0
  incr(x1)	weight: 0
    hd(x1)	weight: 0
#cons(x1,x2)	weight: x2
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
   adx(x1)	weight: 0
 zeros()	weight: 0
  #tl(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: 0
  mark(x1)	weight: 0
#incr(x1)	weight: 0
#proper(x1)	weight: 0
  #hd(x1)	weight: 0
  nats()	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #16
Number of SCCs: 7, DPs: 21, edges: 85
	SCC { #6 #7 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #adx(x1)	weight: x1
  incr(x1)	weight: 0
    hd(x1)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
   adx(x1)	weight: 0
 zeros()	weight: 0
  #tl(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#incr(x1)	weight: 0
#proper(x1)	weight: 0
  #hd(x1)	weight: 0
  nats()	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #6 #7
Number of SCCs: 6, DPs: 19, edges: 81
	SCC { #10 #27 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #adx(x1)	weight: 0
  incr(x1)	weight: 0
    hd(x1)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
   adx(x1)	weight: 0
 zeros()	weight: 0
  #tl(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#incr(x1)	weight: x1
#proper(x1)	weight: 0
  #hd(x1)	weight: 0
  nats()	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #10 #27
Number of SCCs: 5, DPs: 17, edges: 77
	SCC { #2 #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #adx(x1)	weight: 0
  incr(x1)	weight: 0
    hd(x1)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
   adx(x1)	weight: 0
 zeros()	weight: 0
  #tl(x1)	weight: x1
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#incr(x1)	weight: 0
#proper(x1)	weight: 0
  #hd(x1)	weight: 0
  nats()	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #2 #13
Number of SCCs: 4, DPs: 15, edges: 73
	SCC { #3 #23 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #adx(x1)	weight: 0
  incr(x1)	weight: 0
    hd(x1)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
   top(x1)	weight: 0
 #top(x1)	weight: 0
   adx(x1)	weight: 0
 zeros()	weight: 0
  #tl(x1)	weight: 0
proper(x1)	weight: 0
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
#incr(x1)	weight: 0
#proper(x1)	weight: 0
  #hd(x1)	weight: x1
  nats()	weight: 0
active(x1)	weight: 0
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #3 #23
Number of SCCs: 3, DPs: 13, edges: 69
	SCC { #11 #14 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
 #adx(x1)	weight: 0
  incr(x1)	weight: (/ 3 8) + x1
    hd(x1)	weight: (/ 1 8) + x1
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
 #top(x1)	weight: x1
   adx(x1)	weight: (/ 5 8) + x1
 zeros()	weight: (/ 1 2)
  #tl(x1)	weight: 0
proper(x1)	weight: (/ 1 4) + x1
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: (/ 1 8)
   #s(x1)	weight: 0
    tl(x1)	weight: x1
  mark(x1)	weight: (/ 3 8) + x1
#incr(x1)	weight: 0
#proper(x1)	weight: 0
  #hd(x1)	weight: 0
  nats()	weight: (/ 11 8)
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: max{0, (/ 1 8) + x1}
#active(x1)	weight: 0
    Usable rules: { 1..4 7..29 }
    Removed DPs: #11 #14
Number of SCCs: 2, DPs: 11, edges: 65
	SCC { #5 #20 #22 #37 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #adx(x1)	weight: 0
  incr(x1)	weight: (/ 1 4) + x1
    hd(x1)	weight: (/ 1 4) + x1
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2)
   top(x1)	weight: 0
 #top(x1)	weight: 0
   adx(x1)	weight: (/ 1 4) + x1
 zeros()	weight: 0
  #tl(x1)	weight: 0
proper(x1)	weight: (/ 1 4)
    ok(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: (/ 1 4) + x1
  mark(x1)	weight: (/ 5 4)
#incr(x1)	weight: 0
#proper(x1)	weight: 0
  #hd(x1)	weight: 0
  nats()	weight: 0
active(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: (/ 1 2)
#active(x1)	weight: x1
    Usable rules: { }
    Removed DPs: #5 #20 #22 #37
Number of SCCs: 1, DPs: 7, edges: 49
	SCC { #9 #18 #25 #29 #31 #42 #43 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #adx(x1)	weight: 0
  incr(x1)	weight: (/ 1 8) + x1
    hd(x1)	weight: (/ 1 8) + x1
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: 0
 #top(x1)	weight: 0
   adx(x1)	weight: (/ 1 8) + x1
 zeros()	weight: 0
  #tl(x1)	weight: 0
proper(x1)	weight: (/ 1 8)
    ok(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: (/ 1 8) + x1
  mark(x1)	weight: (/ 1 2)
#incr(x1)	weight: 0
#proper(x1)	weight: x1
  #hd(x1)	weight: 0
  nats()	weight: 0
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: (/ 1 8) + x1 + x2
#active(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #9 #18 #25 #29 #31 #42 #43
Number of SCCs: 0, DPs: 0, edges: 0
YES