Input TRS:
    1: nats() -> adx(zeros())
    2: zeros() -> cons(n__0(),n__zeros())
    3: incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y)))
    4: adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y))))
    5: hd(cons(X,Y)) -> activate(X)
    6: tl(cons(X,Y)) -> activate(Y)
    7: 0() -> n__0()
    8: zeros() -> n__zeros()
    9: s(X) -> n__s(X)
    10: incr(X) -> n__incr(X)
    11: adx(X) -> n__adx(X)
    12: activate(n__0()) -> 0()
    13: activate(n__zeros()) -> zeros()
    14: activate(n__s(X)) -> s(X)
    15: activate(n__incr(X)) -> incr(activate(X))
    16: activate(n__adx(X)) -> adx(activate(X))
    17: activate(X) -> X
Number of strict rules: 17
Direct Order(PosReal,>,Poly) ... removes: 5 6
  incr(x1)	weight: x1
    hd(x1)	weight: (/ 1 2) + x1
     s(x1)	weight: x1
n__adx(x1)	weight: x1
activate(x1)	weight: x1
n__zeros()	weight: 0
   adx(x1)	weight: x1
 zeros()	weight: 0
  n__s(x1)	weight: x1
     0()	weight: 0
    tl(x1)	weight: (/ 1 2) + x1
  n__0()	weight: 0
  nats()	weight: 0
  cons(x1,x2)	weight: x1 + x2
n__incr(x1)	weight: x1
Number of strict rules: 15
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #activate(n__zeros()) -> #zeros()
   #2: #activate(n__0()) -> #0()
   #3: #activate(n__s(X)) -> #s(X)
   #4: #activate(n__adx(X)) -> #adx(activate(X))
   #5: #activate(n__adx(X)) -> #activate(X)
   #6: #incr(cons(X,Y)) -> #activate(X)
   #7: #incr(cons(X,Y)) -> #activate(Y)
   #8: #nats() -> #adx(zeros())
   #9: #nats() -> #zeros()
   #10: #activate(n__incr(X)) -> #incr(activate(X))
   #11: #activate(n__incr(X)) -> #activate(X)
   #12: #adx(cons(X,Y)) -> #incr(cons(activate(X),n__adx(activate(Y))))
   #13: #adx(cons(X,Y)) -> #activate(X)
   #14: #adx(cons(X,Y)) -> #activate(Y)
Number of SCCs: 1, DPs: 9, edges: 31
	SCC { #4..7 #10..14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #adx(x1)	weight: (/ 1 2) + x1
   #0()	weight: 0
  incr(x1)	weight: x1
    hd(x1)	weight: 0
#nats()	weight: 0
     s(x1)	weight: 0
n__adx(x1)	weight: (/ 1 2) + x1
activate(x1)	weight: x1
n__zeros()	weight: 0
#activate(x1)	weight: x1
   adx(x1)	weight: (/ 1 2) + x1
 zeros()	weight: 0
  n__s(x1)	weight: 0
     0()	weight: 0
#zeros()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: 0
#incr(x1)	weight: x1
  n__0()	weight: 0
  nats()	weight: 0
  cons(x1,x2)	weight: x1 + x2
n__incr(x1)	weight: x1
    Usable rules: { 2..4 7..17 }
    Removed DPs: #5 #13 #14
Number of SCCs: 1, DPs: 6, edges: 14
	SCC { #4 #6 #7 #10..12 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
 #adx(x1)	weight: (/ 1 4) + x1
   #0()	weight: 0
  incr(x1)	weight: x1
    hd(x1)	weight: 0
#nats()	weight: 0
     s(x1)	weight: 0
n__adx(x1)	weight: (/ 1 4) + x1
activate(x1)	weight: x1
n__zeros()	weight: (/ 1 2)
#activate(x1)	weight: x1
   adx(x1)	weight: (/ 1 4) + x1
 zeros()	weight: (/ 1 2)
  n__s(x1)	weight: 0
     0()	weight: 0
#zeros()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: 0
#incr(x1)	weight: x1
  n__0()	weight: 0
  nats()	weight: 0
  cons(x1,x2)	weight: max{x2, (/ 1 2) + x1}
n__incr(x1)	weight: x1
    Usable rules: { 2..4 7..17 }
    Removed DPs: #6
Number of SCCs: 1, DPs: 5, edges: 9
	SCC { #4 #7 #10..12 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
 #adx(x1)	weight: (max (/ 1 2) 0)
   #0()	weight: 0
  incr(x1)	weight: max{0, (/ 1 4) + x1}
    hd(x1)	weight: 0
#nats()	weight: 0
     s(x1)	weight: (max (- (/ 1 2)) 0)
n__adx(x1)	weight: (max (/ 1 4) 0)
activate(x1)	weight: max{0, x1}
n__zeros()	weight: (/ 1 4)
#activate(x1)	weight: max{0, (/ 1 4) + x1}
   adx(x1)	weight: (max (/ 1 4) 0)
 zeros()	weight: (/ 1 4)
  n__s(x1)	weight: (max (- (/ 1 4)) 0)
     0()	weight: (/ 1 4)
#zeros()	weight: 0
   #s(x1)	weight: 0
    tl(x1)	weight: 0
#incr(x1)	weight: max{0, (/ 1 2) + x1}
  n__0()	weight: (/ 1 4)
  nats()	weight: 0
  cons(x1,x2)	weight: max{0, (- (/ 1 4)) + x2}
n__incr(x1)	weight: max{0, (/ 1 4) + x1}
    Usable rules: { 2..4 7..17 }
    Removed DPs: #11
Number of SCCs: 1, DPs: 4, edges: 5
	SCC { #4 #7 #10 #12 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  found.
  #adx(cons(X,n__zeros()))	-#12->
  #incr(cons(activate(X),n__adx(activate(n__zeros()))))	--->*
  #incr(cons(activate(X),n__adx(activate(n__zeros()))))	-#7->
  #activate(n__adx(activate(n__zeros())))	--->*
  #activate(n__adx(activate(n__zeros())))	-#4->
  #adx(activate(activate(n__zeros())))	--->*
  #adx(cons(n__0(),n__zeros()))
  Looping with: [ X := n__0(); ]
NO