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.
  conv(x1)	weight: (/ 3 8)	status: []	precedence above: 0 nil half❆1_0
     s(x1)	weight: x1	status: [x1]	precedence above: half lastbit half❆1_s lastbit❆1_s
#conv(x1)	weight: x1	status: [x1]	precedence above:
#half❆1_s(x1)	weight: x1	status: []	precedence above:
#half(x1)	weight: (/ 1 8)	status: []	precedence above:
#lastbit(x1)	weight: x1	status: []	precedence above:
#lastbit❆1_0()	weight: 0	status: []	precedence above:
lastbit❆1_0()	weight: (/ 1 4)	status: []	precedence above:
  rand(x1)	weight: (/ 1 8) + x1	status: []	precedence above:
#half❆1_0()	weight: 0	status: []	precedence above:
  half(x1)	weight: x1	status: x1
lastbit(x1)	weight: (/ 1 2)	status: []	precedence above: s half half❆1_s lastbit❆1_s
half❆1_s(x1)	weight: x1	status: [x1]	precedence above: half
#lastbit❆1_s(x1)	weight: (/ 1 8)	status: []	precedence above:
     0()	weight: (/ 1 8)	status: []	precedence above: half❆1_0
   nil()	weight: (/ 1 4)	status: []	precedence above:
  cons(x1,x2)	weight: 0	status: []	precedence above: conv 0 nil half❆1_0
lastbit❆1_s(x1)	weight: (/ 1 2)	status: []	precedence above: s half lastbit half❆1_s
half❆1_0()	weight: (/ 1 8)	status: []	precedence above: 0
    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.
  conv(x1)	weight: (/ 3 8)	status: []	precedence above: 0 nil half❆1_0
     s(x1)	weight: x1	status: [x1]	precedence above: #lastbit half lastbit half❆1_s #lastbit❆1_s lastbit❆1_s
#conv(x1)	weight: x1	status: [x1]	precedence above:
#half❆1_s(x1)	weight: x1	status: []	precedence above:
#half(x1)	weight: (/ 1 8)	status: []	precedence above:
#lastbit(x1)	weight: x1	status: [x1]	precedence above: #lastbit❆1_s
#lastbit❆1_0()	weight: 0	status: []	precedence above:
lastbit❆1_0()	weight: (/ 1 4)	status: []	precedence above:
  rand(x1)	weight: (/ 1 8) + x1	status: []	precedence above:
#half❆1_0()	weight: 0	status: []	precedence above:
  half(x1)	weight: x1	status: x1
lastbit(x1)	weight: (/ 1 2)	status: []	precedence above: s #lastbit half half❆1_s #lastbit❆1_s lastbit❆1_s
half❆1_s(x1)	weight: x1	status: [x1]	precedence above: half
#lastbit❆1_s(x1)	weight: x1	status: [x1]	precedence above: #lastbit
     0()	weight: (/ 1 8)	status: []	precedence above: half❆1_0
   nil()	weight: (/ 1 4)	status: []	precedence above:
  cons(x1,x2)	weight: 0	status: []	precedence above: conv 0 nil half❆1_0
lastbit❆1_s(x1)	weight: (/ 1 2)	status: []	precedence above: s #lastbit half lastbit half❆1_s #lastbit❆1_s
half❆1_0()	weight: (/ 1 8)	status: []	precedence above: 0
    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.
  conv(x1)	weight: (/ 3 8)	status: []	precedence above: 0 nil half❆1_0
     s(x1)	weight: x1	status: [x1]	precedence above: #half❆1_s #half half half❆1_s
#conv(x1)	weight: x1	status: [x1]	precedence above:
#half❆1_s(x1)	weight: x1	status: x1
#half(x1)	weight: x1	status: [x1]	precedence above: s #half❆1_s half half❆1_s
#lastbit(x1)	weight: x1	status: [x1]	precedence above: #lastbit❆1_s
#lastbit❆1_0()	weight: 0	status: []	precedence above:
lastbit❆1_0()	weight: (/ 1 4)	status: []	precedence above:
  rand(x1)	weight: (/ 1 8) + x1	status: []	precedence above:
#half❆1_0()	weight: 0	status: []	precedence above:
  half(x1)	weight: x1	status: x1
lastbit(x1)	weight: (/ 1 2)	status: []	precedence above: s #half❆1_s #half #lastbit half half❆1_s #lastbit❆1_s lastbit❆1_s
half❆1_s(x1)	weight: x1	status: [x1]	precedence above: half
#lastbit❆1_s(x1)	weight: x1	status: [x1]	precedence above: #lastbit
     0()	weight: (/ 1 8)	status: []	precedence above: half❆1_0
   nil()	weight: (/ 1 4)	status: []	precedence above:
  cons(x1,x2)	weight: 0	status: []	precedence above: conv 0 nil half❆1_0
lastbit❆1_s(x1)	weight: (/ 1 2)	status: []	precedence above: s #half❆1_s #half #lastbit half lastbit half❆1_s #lastbit❆1_s
half❆1_0()	weight: (/ 1 8)	status: []	precedence above: 0
    Removed DPs: #4
Number of SCCs: 0, DPs: 0, edges: 0
YES