Input TRS:
    1: half(|0|()) -> |0|()
    2: half(s(|0|())) -> |0|()
    3: half(s(s(x))) -> s(half(x))
    4: lastbit(|0|()) -> |0|()
    5: lastbit(s(|0|())) -> s(|0|())
    6: lastbit(s(s(x))) -> lastbit(x)
    7: conv(|0|()) -> cons(nil(),|0|())
    8: conv(s(x)) -> cons(conv(half(s(x))),lastbit(s(x)))
    9: rand(x) ->= x
    10: rand(x) ->= rand(s(x))
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... failed.
Freezing lastbit half
1: half❆1_|0|() -> |0|()
2: half❆1_s(|0|()) -> |0|()
3: half❆1_s(s(x)) -> s(half(x))
4: lastbit❆1_|0|() -> |0|()
5: lastbit❆1_s(|0|()) -> s(|0|())
6: lastbit❆1_s(s(x)) -> lastbit(x)
7: conv(|0|()) -> cons(nil(),|0|())
8: conv(s(x)) -> cons(conv(half❆1_s(x)),lastbit❆1_s(x))
9: rand(x) ->= x
10: rand(x) ->= rand(s(x))
11: half(|0|()) ->= half❆1_|0|()
12: half(s(_1)) ->= half❆1_s(_1)
13: lastbit(|0|()) ->= lastbit❆1_|0|()
14: lastbit(s(_1)) ->= lastbit❆1_s(_1)
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #lastbit❆1_s(s(x)) -> #lastbit(x)
   #2: #lastbit(|0|()) ->? #lastbit❆1_|0|()
   #3: #half(|0|()) ->? #half❆1_|0|()
   #4: #half(s(_1)) ->? #half❆1_s(_1)
   #5: #lastbit(s(_1)) ->? #lastbit❆1_s(_1)
   #6: #half❆1_s(s(x)) -> #half(x)
   #7: #conv(s(x)) -> #conv(half❆1_s(x))
   #8: #conv(s(x)) -> #half❆1_s(x)
   #9: #conv(s(x)) -> #lastbit❆1_s(x)
Number of SCCs: 3, DPs: 5, edges: 5
	SCC { #7 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded.
   |0|()	weight: (/ 1 8)	status: []	precedence above: half❆1_|0| cons
  conv(x1)	weight: (/ 5 8)	status: []	precedence above: |0| s half lastbit half❆1_s half❆1_|0| nil cons lastbit❆1_s
     s(x1)	weight: x1	status: [x1]	precedence above: half lastbit half❆1_s lastbit❆1_s
#conv(x1)	weight: (/ 1 8) + x1	status: [x1]	precedence above:
#half❆1_s(x1)	weight: x1	status: []	precedence above:
#lastbit❆1_|0|()	weight: 0	status: []	precedence above:
#half(x1)	weight: x1	status: []	precedence above:
#lastbit(x1)	weight: x1	status: []	precedence above:
  rand(x1)	weight: (/ 1 8) + x1	status: []	precedence above:
  half(x1)	weight: x1	status: x1
lastbit(x1)	weight: (/ 3 8)	status: []	precedence above: s half half❆1_s lastbit❆1_s
#half❆1_|0|()	weight: 0	status: []	precedence above:
half❆1_s(x1)	weight: x1	status: x1
#lastbit❆1_s(x1)	weight: (/ 1 8)	status: []	precedence above:
half❆1_|0|()	weight: (/ 1 8)	status: []	precedence above: |0| cons
   nil()	weight: (/ 1 4)	status: []	precedence above:
  cons(x1,x2)	weight: max{(/ 1 8) + x2, x1}	status: []	precedence above:
lastbit❆1_s(x1)	weight: (/ 3 8)	status: []	precedence above: s half lastbit half❆1_s
lastbit❆1_|0|()	weight: (/ 1 4)	status: []	precedence above:
    Removed DPs: #7
Number of SCCs: 2, DPs: 4, edges: 4
	SCC { #1 #5 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded.
   |0|()	weight: (/ 1 8)	status: []	precedence above: half❆1_|0| cons
  conv(x1)	weight: (/ 5 8)	status: []	precedence above: |0| s half lastbit half❆1_s #lastbit❆1_s half❆1_|0| nil cons lastbit❆1_s
     s(x1)	weight: x1	status: [x1]	precedence above: half half❆1_s #lastbit❆1_s
#conv(x1)	weight: (/ 1 8) + x1	status: [x1]	precedence above:
#half❆1_s(x1)	weight: x1	status: []	precedence above:
#lastbit❆1_|0|()	weight: 0	status: []	precedence above:
#half(x1)	weight: x1	status: []	precedence above:
#lastbit(x1)	weight: x1	status: x1
  rand(x1)	weight: (/ 1 8) + x1	status: []	precedence above:
  half(x1)	weight: x1	status: x1
lastbit(x1)	weight: (/ 3 8)	status: []	precedence above: s half half❆1_s #lastbit❆1_s lastbit❆1_s
#half❆1_|0|()	weight: 0	status: []	precedence above:
half❆1_s(x1)	weight: x1	status: x1
#lastbit❆1_s(x1)	weight: x1	status: [x1]	precedence above:
half❆1_|0|()	weight: (/ 1 8)	status: []	precedence above: |0| cons
   nil()	weight: (/ 1 4)	status: []	precedence above:
  cons(x1,x2)	weight: max{(/ 1 8) + x2, x1}	status: []	precedence above:
lastbit❆1_s(x1)	weight: (/ 3 8)	status: []	precedence above: s half lastbit half❆1_s #lastbit❆1_s
lastbit❆1_|0|()	weight: (/ 1 4)	status: []	precedence above:
    Removed DPs: #1 #5
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #4 #6 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... succeeded.
   |0|()	weight: (/ 1 8)	status: []	precedence above: half❆1_|0| cons
  conv(x1)	weight: (/ 5 8)	status: []	precedence above: |0| s half lastbit half❆1_s #lastbit❆1_s half❆1_|0| nil cons lastbit❆1_s
     s(x1)	weight: x1	status: [x1]	precedence above: half half❆1_s #lastbit❆1_s
#conv(x1)	weight: (/ 1 8) + x1	status: [x1]	precedence above:
#half❆1_s(x1)	weight: x1	status: x1
#lastbit❆1_|0|()	weight: 0	status: []	precedence above:
#half(x1)	weight: x1	status: x1
#lastbit(x1)	weight: x1	status: x1
  rand(x1)	weight: (/ 1 8) + x1	status: []	precedence above:
  half(x1)	weight: x1	status: x1
lastbit(x1)	weight: (/ 3 8)	status: []	precedence above: s half half❆1_s #lastbit❆1_s lastbit❆1_s
#half❆1_|0|()	weight: 0	status: []	precedence above:
half❆1_s(x1)	weight: x1	status: x1
#lastbit❆1_s(x1)	weight: x1	status: [x1]	precedence above:
half❆1_|0|()	weight: (/ 1 8)	status: []	precedence above: |0| cons
   nil()	weight: (/ 1 4)	status: []	precedence above:
  cons(x1,x2)	weight: max{(/ 1 8) + x2, x1}	status: []	precedence above:
lastbit❆1_s(x1)	weight: (/ 3 8)	status: []	precedence above: s half lastbit half❆1_s #lastbit❆1_s
lastbit❆1_|0|()	weight: (/ 1 4)	status: []	precedence above:
    Removed DPs: #4 #6
Number of SCCs: 0, DPs: 0, edges: 0
YES