YES

Problem:
 r0(0(x1)) -> 0(r0(x1))
 r0(1(x1)) -> 1(r0(x1))
 r0(m(x1)) -> m(r0(x1))
 r1(0(x1)) -> 0(r1(x1))
 r1(1(x1)) -> 1(r1(x1))
 r1(m(x1)) -> m(r1(x1))
 r0(b(x1)) -> qr(0(b(x1)))
 r1(b(x1)) -> qr(1(b(x1)))
 0(qr(x1)) -> qr(0(x1))
 1(qr(x1)) -> qr(1(x1))
 m(qr(x1)) -> ql(m(x1))
 0(ql(x1)) -> ql(0(x1))
 1(ql(x1)) -> ql(1(x1))
 b(ql(0(x1))) -> 0(b(r0(x1)))
 b(ql(1(x1))) -> 1(b(r1(x1)))

Proof:
 DP Processor:
  DPs:
   r0#(0(x1)) -> r0#(x1)
   r0#(0(x1)) -> 0#(r0(x1))
   r0#(1(x1)) -> r0#(x1)
   r0#(1(x1)) -> 1#(r0(x1))
   r0#(m(x1)) -> r0#(x1)
   r0#(m(x1)) -> m#(r0(x1))
   r1#(0(x1)) -> r1#(x1)
   r1#(0(x1)) -> 0#(r1(x1))
   r1#(1(x1)) -> r1#(x1)
   r1#(1(x1)) -> 1#(r1(x1))
   r1#(m(x1)) -> r1#(x1)
   r1#(m(x1)) -> m#(r1(x1))
   r0#(b(x1)) -> 0#(b(x1))
   r1#(b(x1)) -> 1#(b(x1))
   0#(qr(x1)) -> 0#(x1)
   1#(qr(x1)) -> 1#(x1)
   m#(qr(x1)) -> m#(x1)
   0#(ql(x1)) -> 0#(x1)
   1#(ql(x1)) -> 1#(x1)
   b#(ql(0(x1))) -> r0#(x1)
   b#(ql(0(x1))) -> b#(r0(x1))
   b#(ql(0(x1))) -> 0#(b(r0(x1)))
   b#(ql(1(x1))) -> r1#(x1)
   b#(ql(1(x1))) -> b#(r1(x1))
   b#(ql(1(x1))) -> 1#(b(r1(x1)))
  TRS:
   r0(0(x1)) -> 0(r0(x1))
   r0(1(x1)) -> 1(r0(x1))
   r0(m(x1)) -> m(r0(x1))
   r1(0(x1)) -> 0(r1(x1))
   r1(1(x1)) -> 1(r1(x1))
   r1(m(x1)) -> m(r1(x1))
   r0(b(x1)) -> qr(0(b(x1)))
   r1(b(x1)) -> qr(1(b(x1)))
   0(qr(x1)) -> qr(0(x1))
   1(qr(x1)) -> qr(1(x1))
   m(qr(x1)) -> ql(m(x1))
   0(ql(x1)) -> ql(0(x1))
   1(ql(x1)) -> ql(1(x1))
   b(ql(0(x1))) -> 0(b(r0(x1)))
   b(ql(1(x1))) -> 1(b(r1(x1)))
  TDG Processor:
   DPs:
    r0#(0(x1)) -> r0#(x1)
    r0#(0(x1)) -> 0#(r0(x1))
    r0#(1(x1)) -> r0#(x1)
    r0#(1(x1)) -> 1#(r0(x1))
    r0#(m(x1)) -> r0#(x1)
    r0#(m(x1)) -> m#(r0(x1))
    r1#(0(x1)) -> r1#(x1)
    r1#(0(x1)) -> 0#(r1(x1))
    r1#(1(x1)) -> r1#(x1)
    r1#(1(x1)) -> 1#(r1(x1))
    r1#(m(x1)) -> r1#(x1)
    r1#(m(x1)) -> m#(r1(x1))
    r0#(b(x1)) -> 0#(b(x1))
    r1#(b(x1)) -> 1#(b(x1))
    0#(qr(x1)) -> 0#(x1)
    1#(qr(x1)) -> 1#(x1)
    m#(qr(x1)) -> m#(x1)
    0#(ql(x1)) -> 0#(x1)
    1#(ql(x1)) -> 1#(x1)
    b#(ql(0(x1))) -> r0#(x1)
    b#(ql(0(x1))) -> b#(r0(x1))
    b#(ql(0(x1))) -> 0#(b(r0(x1)))
    b#(ql(1(x1))) -> r1#(x1)
    b#(ql(1(x1))) -> b#(r1(x1))
    b#(ql(1(x1))) -> 1#(b(r1(x1)))
   TRS:
    r0(0(x1)) -> 0(r0(x1))
    r0(1(x1)) -> 1(r0(x1))
    r0(m(x1)) -> m(r0(x1))
    r1(0(x1)) -> 0(r1(x1))
    r1(1(x1)) -> 1(r1(x1))
    r1(m(x1)) -> m(r1(x1))
    r0(b(x1)) -> qr(0(b(x1)))
    r1(b(x1)) -> qr(1(b(x1)))
    0(qr(x1)) -> qr(0(x1))
    1(qr(x1)) -> qr(1(x1))
    m(qr(x1)) -> ql(m(x1))
    0(ql(x1)) -> ql(0(x1))
    1(ql(x1)) -> ql(1(x1))
    b(ql(0(x1))) -> 0(b(r0(x1)))
    b(ql(1(x1))) -> 1(b(r1(x1)))
   graph:
    b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(1(x1))) -> 1#(b(r1(x1)))
    b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(1(x1))) -> b#(r1(x1))
    b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(1(x1))) -> r1#(x1)
    b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(0(x1))) -> 0#(b(r0(x1)))
    b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(0(x1))) -> b#(r0(x1))
    b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(0(x1))) -> r0#(x1)
    b#(ql(1(x1))) -> r1#(x1) -> r1#(b(x1)) -> 1#(b(x1))
    b#(ql(1(x1))) -> r1#(x1) -> r1#(m(x1)) -> m#(r1(x1))
    b#(ql(1(x1))) -> r1#(x1) -> r1#(m(x1)) -> r1#(x1)
    b#(ql(1(x1))) -> r1#(x1) -> r1#(1(x1)) -> 1#(r1(x1))
    b#(ql(1(x1))) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1)
    b#(ql(1(x1))) -> r1#(x1) -> r1#(0(x1)) -> 0#(r1(x1))
    b#(ql(1(x1))) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1)
    b#(ql(1(x1))) -> 1#(b(r1(x1))) -> 1#(ql(x1)) -> 1#(x1)
    b#(ql(1(x1))) -> 1#(b(r1(x1))) -> 1#(qr(x1)) -> 1#(x1)
    b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(1(x1))) -> 1#(b(r1(x1)))
    b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(1(x1))) -> b#(r1(x1))
    b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(1(x1))) -> r1#(x1)
    b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(0(x1))) -> 0#(b(r0(x1)))
    b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(0(x1))) -> b#(r0(x1))
    b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(0(x1))) -> r0#(x1)
    b#(ql(0(x1))) -> 0#(b(r0(x1))) -> 0#(ql(x1)) -> 0#(x1)
    b#(ql(0(x1))) -> 0#(b(r0(x1))) -> 0#(qr(x1)) -> 0#(x1)
    b#(ql(0(x1))) -> r0#(x1) -> r0#(b(x1)) -> 0#(b(x1))
    b#(ql(0(x1))) -> r0#(x1) -> r0#(m(x1)) -> m#(r0(x1))
    b#(ql(0(x1))) -> r0#(x1) -> r0#(m(x1)) -> r0#(x1)
    b#(ql(0(x1))) -> r0#(x1) -> r0#(1(x1)) -> 1#(r0(x1))
    b#(ql(0(x1))) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1)
    b#(ql(0(x1))) -> r0#(x1) -> r0#(0(x1)) -> 0#(r0(x1))
    b#(ql(0(x1))) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1)
    r1#(b(x1)) -> 1#(b(x1)) -> 1#(ql(x1)) -> 1#(x1)
    r1#(b(x1)) -> 1#(b(x1)) -> 1#(qr(x1)) -> 1#(x1)
    r1#(m(x1)) -> r1#(x1) -> r1#(b(x1)) -> 1#(b(x1))
    r1#(m(x1)) -> r1#(x1) -> r1#(m(x1)) -> m#(r1(x1))
    r1#(m(x1)) -> r1#(x1) -> r1#(m(x1)) -> r1#(x1)
    r1#(m(x1)) -> r1#(x1) -> r1#(1(x1)) -> 1#(r1(x1))
    r1#(m(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1)
    r1#(m(x1)) -> r1#(x1) -> r1#(0(x1)) -> 0#(r1(x1))
    r1#(m(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1)
    r1#(m(x1)) -> m#(r1(x1)) -> m#(qr(x1)) -> m#(x1)
    r1#(1(x1)) -> r1#(x1) -> r1#(b(x1)) -> 1#(b(x1))
    r1#(1(x1)) -> r1#(x1) -> r1#(m(x1)) -> m#(r1(x1))
    r1#(1(x1)) -> r1#(x1) -> r1#(m(x1)) -> r1#(x1)
    r1#(1(x1)) -> r1#(x1) -> r1#(1(x1)) -> 1#(r1(x1))
    r1#(1(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1)
    r1#(1(x1)) -> r1#(x1) -> r1#(0(x1)) -> 0#(r1(x1))
    r1#(1(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1)
    r1#(1(x1)) -> 1#(r1(x1)) -> 1#(ql(x1)) -> 1#(x1)
    r1#(1(x1)) -> 1#(r1(x1)) -> 1#(qr(x1)) -> 1#(x1)
    r1#(0(x1)) -> r1#(x1) -> r1#(b(x1)) -> 1#(b(x1))
    r1#(0(x1)) -> r1#(x1) -> r1#(m(x1)) -> m#(r1(x1))
    r1#(0(x1)) -> r1#(x1) -> r1#(m(x1)) -> r1#(x1)
    r1#(0(x1)) -> r1#(x1) -> r1#(1(x1)) -> 1#(r1(x1))
    r1#(0(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1)
    r1#(0(x1)) -> r1#(x1) -> r1#(0(x1)) -> 0#(r1(x1))
    r1#(0(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1)
    r1#(0(x1)) -> 0#(r1(x1)) -> 0#(ql(x1)) -> 0#(x1)
    r1#(0(x1)) -> 0#(r1(x1)) -> 0#(qr(x1)) -> 0#(x1)
    m#(qr(x1)) -> m#(x1) -> m#(qr(x1)) -> m#(x1)
    1#(ql(x1)) -> 1#(x1) -> 1#(ql(x1)) -> 1#(x1)
    1#(ql(x1)) -> 1#(x1) -> 1#(qr(x1)) -> 1#(x1)
    1#(qr(x1)) -> 1#(x1) -> 1#(ql(x1)) -> 1#(x1)
    1#(qr(x1)) -> 1#(x1) -> 1#(qr(x1)) -> 1#(x1)
    0#(ql(x1)) -> 0#(x1) -> 0#(ql(x1)) -> 0#(x1)
    0#(ql(x1)) -> 0#(x1) -> 0#(qr(x1)) -> 0#(x1)
    0#(qr(x1)) -> 0#(x1) -> 0#(ql(x1)) -> 0#(x1)
    0#(qr(x1)) -> 0#(x1) -> 0#(qr(x1)) -> 0#(x1)
    r0#(b(x1)) -> 0#(b(x1)) -> 0#(ql(x1)) -> 0#(x1)
    r0#(b(x1)) -> 0#(b(x1)) -> 0#(qr(x1)) -> 0#(x1)
    r0#(m(x1)) -> m#(r0(x1)) -> m#(qr(x1)) -> m#(x1)
    r0#(m(x1)) -> r0#(x1) -> r0#(b(x1)) -> 0#(b(x1))
    r0#(m(x1)) -> r0#(x1) -> r0#(m(x1)) -> m#(r0(x1))
    r0#(m(x1)) -> r0#(x1) -> r0#(m(x1)) -> r0#(x1)
    r0#(m(x1)) -> r0#(x1) -> r0#(1(x1)) -> 1#(r0(x1))
    r0#(m(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1)
    r0#(m(x1)) -> r0#(x1) -> r0#(0(x1)) -> 0#(r0(x1))
    r0#(m(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1)
    r0#(1(x1)) -> 1#(r0(x1)) -> 1#(ql(x1)) -> 1#(x1)
    r0#(1(x1)) -> 1#(r0(x1)) -> 1#(qr(x1)) -> 1#(x1)
    r0#(1(x1)) -> r0#(x1) -> r0#(b(x1)) -> 0#(b(x1))
    r0#(1(x1)) -> r0#(x1) -> r0#(m(x1)) -> m#(r0(x1))
    r0#(1(x1)) -> r0#(x1) -> r0#(m(x1)) -> r0#(x1)
    r0#(1(x1)) -> r0#(x1) -> r0#(1(x1)) -> 1#(r0(x1))
    r0#(1(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1)
    r0#(1(x1)) -> r0#(x1) -> r0#(0(x1)) -> 0#(r0(x1))
    r0#(1(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1)
    r0#(0(x1)) -> 0#(r0(x1)) -> 0#(ql(x1)) -> 0#(x1)
    r0#(0(x1)) -> 0#(r0(x1)) -> 0#(qr(x1)) -> 0#(x1)
    r0#(0(x1)) -> r0#(x1) -> r0#(b(x1)) -> 0#(b(x1))
    r0#(0(x1)) -> r0#(x1) -> r0#(m(x1)) -> m#(r0(x1))
    r0#(0(x1)) -> r0#(x1) -> r0#(m(x1)) -> r0#(x1)
    r0#(0(x1)) -> r0#(x1) -> r0#(1(x1)) -> 1#(r0(x1))
    r0#(0(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1)
    r0#(0(x1)) -> r0#(x1) -> r0#(0(x1)) -> 0#(r0(x1))
    r0#(0(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1)
   SCC Processor:
    #sccs: 6
    #rules: 13
    #arcs: 95/625
    DPs:
     b#(ql(1(x1))) -> b#(r1(x1))
     b#(ql(0(x1))) -> b#(r0(x1))
    TRS:
     r0(0(x1)) -> 0(r0(x1))
     r0(1(x1)) -> 1(r0(x1))
     r0(m(x1)) -> m(r0(x1))
     r1(0(x1)) -> 0(r1(x1))
     r1(1(x1)) -> 1(r1(x1))
     r1(m(x1)) -> m(r1(x1))
     r0(b(x1)) -> qr(0(b(x1)))
     r1(b(x1)) -> qr(1(b(x1)))
     0(qr(x1)) -> qr(0(x1))
     1(qr(x1)) -> qr(1(x1))
     m(qr(x1)) -> ql(m(x1))
     0(ql(x1)) -> ql(0(x1))
     1(ql(x1)) -> ql(1(x1))
     b(ql(0(x1))) -> 0(b(r0(x1)))
     b(ql(1(x1))) -> 1(b(r1(x1)))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [b#](x0) = x0 + 1,
      
      [ql](x0) = x0,
      
      [qr](x0) = 0,
      
      [b](x0) = x0 + 1,
      
      [r1](x0) = x0,
      
      [m](x0) = 0,
      
      [1](x0) = 1x0 + 4,
      
      [r0](x0) = x0 + 0,
      
      [0](x0) = x0
     orientation:
      b#(ql(1(x1))) = 1x1 + 4 >= x1 + 1 = b#(r1(x1))
      
      b#(ql(0(x1))) = x1 + 1 >= x1 + 1 = b#(r0(x1))
      
      r0(0(x1)) = x1 + 0 >= x1 + 0 = 0(r0(x1))
      
      r0(1(x1)) = 1x1 + 4 >= 1x1 + 4 = 1(r0(x1))
      
      r0(m(x1)) = 0 >= 0 = m(r0(x1))
      
      r1(0(x1)) = x1 >= x1 = 0(r1(x1))
      
      r1(1(x1)) = 1x1 + 4 >= 1x1 + 4 = 1(r1(x1))
      
      r1(m(x1)) = 0 >= 0 = m(r1(x1))
      
      r0(b(x1)) = x1 + 1 >= 0 = qr(0(b(x1)))
      
      r1(b(x1)) = x1 + 1 >= 0 = qr(1(b(x1)))
      
      0(qr(x1)) = 0 >= 0 = qr(0(x1))
      
      1(qr(x1)) = 4 >= 0 = qr(1(x1))
      
      m(qr(x1)) = 0 >= 0 = ql(m(x1))
      
      0(ql(x1)) = x1 >= x1 = ql(0(x1))
      
      1(ql(x1)) = 1x1 + 4 >= 1x1 + 4 = ql(1(x1))
      
      b(ql(0(x1))) = x1 + 1 >= x1 + 1 = 0(b(r0(x1)))
      
      b(ql(1(x1))) = 1x1 + 4 >= 1x1 + 4 = 1(b(r1(x1)))
     problem:
      DPs:
       b#(ql(0(x1))) -> b#(r0(x1))
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
     EDG Processor:
      DPs:
       b#(ql(0(x1))) -> b#(r0(x1))
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
      graph:
       b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(0(x1))) -> b#(r0(x1))
      KBO Processor:
       argument filtering:
        pi(0) = [0]
        pi(r0) = 0
        pi(1) = 0
        pi(m) = []
        pi(r1) = 0
        pi(b) = [0]
        pi(qr) = []
        pi(ql) = 0
        pi(b#) = 0
       weight function:
        w0 = 1
        w(b#) = w(qr) = w(b) = w(m) = w(0) = 1
        w(ql) = w(r1) = w(1) = w(r0) = 0
       precedence:
        b# ~ b > ql ~ qr ~ r1 ~ m ~ 1 ~ r0 ~ 0
       problem:
        DPs:
         
        TRS:
         r0(0(x1)) -> 0(r0(x1))
         r0(1(x1)) -> 1(r0(x1))
         r0(m(x1)) -> m(r0(x1))
         r1(0(x1)) -> 0(r1(x1))
         r1(1(x1)) -> 1(r1(x1))
         r1(m(x1)) -> m(r1(x1))
         r0(b(x1)) -> qr(0(b(x1)))
         r1(b(x1)) -> qr(1(b(x1)))
         0(qr(x1)) -> qr(0(x1))
         1(qr(x1)) -> qr(1(x1))
         m(qr(x1)) -> ql(m(x1))
         0(ql(x1)) -> ql(0(x1))
         1(ql(x1)) -> ql(1(x1))
         b(ql(0(x1))) -> 0(b(r0(x1)))
         b(ql(1(x1))) -> 1(b(r1(x1)))
       Qed
    
    DPs:
     r1#(0(x1)) -> r1#(x1)
     r1#(1(x1)) -> r1#(x1)
     r1#(m(x1)) -> r1#(x1)
    TRS:
     r0(0(x1)) -> 0(r0(x1))
     r0(1(x1)) -> 1(r0(x1))
     r0(m(x1)) -> m(r0(x1))
     r1(0(x1)) -> 0(r1(x1))
     r1(1(x1)) -> 1(r1(x1))
     r1(m(x1)) -> m(r1(x1))
     r0(b(x1)) -> qr(0(b(x1)))
     r1(b(x1)) -> qr(1(b(x1)))
     0(qr(x1)) -> qr(0(x1))
     1(qr(x1)) -> qr(1(x1))
     m(qr(x1)) -> ql(m(x1))
     0(ql(x1)) -> ql(0(x1))
     1(ql(x1)) -> ql(1(x1))
     b(ql(0(x1))) -> 0(b(r0(x1)))
     b(ql(1(x1))) -> 1(b(r1(x1)))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [r1#](x0) = 1x0 + 0,
      
      [ql](x0) = 0,
      
      [qr](x0) = 0,
      
      [b](x0) = 0,
      
      [r1](x0) = 7x0 + 0,
      
      [m](x0) = 8x0 + 1,
      
      [1](x0) = x0,
      
      [r0](x0) = x0,
      
      [0](x0) = x0
     orientation:
      r1#(0(x1)) = 1x1 + 0 >= 1x1 + 0 = r1#(x1)
      
      r1#(1(x1)) = 1x1 + 0 >= 1x1 + 0 = r1#(x1)
      
      r1#(m(x1)) = 9x1 + 2 >= 1x1 + 0 = r1#(x1)
      
      r0(0(x1)) = x1 >= x1 = 0(r0(x1))
      
      r0(1(x1)) = x1 >= x1 = 1(r0(x1))
      
      r0(m(x1)) = 8x1 + 1 >= 8x1 + 1 = m(r0(x1))
      
      r1(0(x1)) = 7x1 + 0 >= 7x1 + 0 = 0(r1(x1))
      
      r1(1(x1)) = 7x1 + 0 >= 7x1 + 0 = 1(r1(x1))
      
      r1(m(x1)) = 15x1 + 8 >= 15x1 + 8 = m(r1(x1))
      
      r0(b(x1)) = 0 >= 0 = qr(0(b(x1)))
      
      r1(b(x1)) = 7 >= 0 = qr(1(b(x1)))
      
      0(qr(x1)) = 0 >= 0 = qr(0(x1))
      
      1(qr(x1)) = 0 >= 0 = qr(1(x1))
      
      m(qr(x1)) = 8 >= 0 = ql(m(x1))
      
      0(ql(x1)) = 0 >= 0 = ql(0(x1))
      
      1(ql(x1)) = 0 >= 0 = ql(1(x1))
      
      b(ql(0(x1))) = 0 >= 0 = 0(b(r0(x1)))
      
      b(ql(1(x1))) = 0 >= 0 = 1(b(r1(x1)))
     problem:
      DPs:
       r1#(0(x1)) -> r1#(x1)
       r1#(1(x1)) -> r1#(x1)
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
     EDG Processor:
      DPs:
       r1#(0(x1)) -> r1#(x1)
       r1#(1(x1)) -> r1#(x1)
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
      graph:
       r1#(1(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1)
       r1#(1(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1)
       r1#(0(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1)
       r1#(0(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1)
      CDG Processor:
       DPs:
        r1#(0(x1)) -> r1#(x1)
        r1#(1(x1)) -> r1#(x1)
       TRS:
        r0(0(x1)) -> 0(r0(x1))
        r0(1(x1)) -> 1(r0(x1))
        r0(m(x1)) -> m(r0(x1))
        r1(0(x1)) -> 0(r1(x1))
        r1(1(x1)) -> 1(r1(x1))
        r1(m(x1)) -> m(r1(x1))
        r0(b(x1)) -> qr(0(b(x1)))
        r1(b(x1)) -> qr(1(b(x1)))
        0(qr(x1)) -> qr(0(x1))
        1(qr(x1)) -> qr(1(x1))
        m(qr(x1)) -> ql(m(x1))
        0(ql(x1)) -> ql(0(x1))
        1(ql(x1)) -> ql(1(x1))
        b(ql(0(x1))) -> 0(b(r0(x1)))
        b(ql(1(x1))) -> 1(b(r1(x1)))
       graph:
        
       Qed
    
    DPs:
     r0#(0(x1)) -> r0#(x1)
     r0#(1(x1)) -> r0#(x1)
     r0#(m(x1)) -> r0#(x1)
    TRS:
     r0(0(x1)) -> 0(r0(x1))
     r0(1(x1)) -> 1(r0(x1))
     r0(m(x1)) -> m(r0(x1))
     r1(0(x1)) -> 0(r1(x1))
     r1(1(x1)) -> 1(r1(x1))
     r1(m(x1)) -> m(r1(x1))
     r0(b(x1)) -> qr(0(b(x1)))
     r1(b(x1)) -> qr(1(b(x1)))
     0(qr(x1)) -> qr(0(x1))
     1(qr(x1)) -> qr(1(x1))
     m(qr(x1)) -> ql(m(x1))
     0(ql(x1)) -> ql(0(x1))
     1(ql(x1)) -> ql(1(x1))
     b(ql(0(x1))) -> 0(b(r0(x1)))
     b(ql(1(x1))) -> 1(b(r1(x1)))
    KBO Processor:
     argument filtering:
      pi(0) = 0
      pi(r0) = 0
      pi(1) = 0
      pi(m) = [0]
      pi(r1) = 0
      pi(b) = []
      pi(qr) = 0
      pi(ql) = 0
      pi(r0#) = 0
     weight function:
      w0 = 1
      w(r0#) = w(ql) = w(qr) = w(b) = w(r1) = w(m) = w(1) = w(r0) = w(0) = 1
     precedence:
      r0# ~ ql ~ qr ~ b ~ r1 ~ m ~ 1 ~ r0 ~ 0
     problem:
      DPs:
       r0#(0(x1)) -> r0#(x1)
       r0#(1(x1)) -> r0#(x1)
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
     EDG Processor:
      DPs:
       r0#(0(x1)) -> r0#(x1)
       r0#(1(x1)) -> r0#(x1)
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
      graph:
       r0#(1(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1)
       r0#(1(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1)
       r0#(0(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1)
       r0#(0(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1)
      CDG Processor:
       DPs:
        r0#(0(x1)) -> r0#(x1)
        r0#(1(x1)) -> r0#(x1)
       TRS:
        r0(0(x1)) -> 0(r0(x1))
        r0(1(x1)) -> 1(r0(x1))
        r0(m(x1)) -> m(r0(x1))
        r1(0(x1)) -> 0(r1(x1))
        r1(1(x1)) -> 1(r1(x1))
        r1(m(x1)) -> m(r1(x1))
        r0(b(x1)) -> qr(0(b(x1)))
        r1(b(x1)) -> qr(1(b(x1)))
        0(qr(x1)) -> qr(0(x1))
        1(qr(x1)) -> qr(1(x1))
        m(qr(x1)) -> ql(m(x1))
        0(ql(x1)) -> ql(0(x1))
        1(ql(x1)) -> ql(1(x1))
        b(ql(0(x1))) -> 0(b(r0(x1)))
        b(ql(1(x1))) -> 1(b(r1(x1)))
       graph:
        
       Qed
    
    DPs:
     m#(qr(x1)) -> m#(x1)
    TRS:
     r0(0(x1)) -> 0(r0(x1))
     r0(1(x1)) -> 1(r0(x1))
     r0(m(x1)) -> m(r0(x1))
     r1(0(x1)) -> 0(r1(x1))
     r1(1(x1)) -> 1(r1(x1))
     r1(m(x1)) -> m(r1(x1))
     r0(b(x1)) -> qr(0(b(x1)))
     r1(b(x1)) -> qr(1(b(x1)))
     0(qr(x1)) -> qr(0(x1))
     1(qr(x1)) -> qr(1(x1))
     m(qr(x1)) -> ql(m(x1))
     0(ql(x1)) -> ql(0(x1))
     1(ql(x1)) -> ql(1(x1))
     b(ql(0(x1))) -> 0(b(r0(x1)))
     b(ql(1(x1))) -> 1(b(r1(x1)))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [m#](x0) = x0,
      
      [ql](x0) = x0,
      
      [qr](x0) = 7x0,
      
      [b](x0) = 0,
      
      [r1](x0) = 7,
      
      [m](x0) = 0,
      
      [1](x0) = x0,
      
      [r0](x0) = 15x0 + 12,
      
      [0](x0) = x0
     orientation:
      m#(qr(x1)) = 7x1 >= x1 = m#(x1)
      
      r0(0(x1)) = 15x1 + 12 >= 15x1 + 12 = 0(r0(x1))
      
      r0(1(x1)) = 15x1 + 12 >= 15x1 + 12 = 1(r0(x1))
      
      r0(m(x1)) = 15 >= 0 = m(r0(x1))
      
      r1(0(x1)) = 7 >= 7 = 0(r1(x1))
      
      r1(1(x1)) = 7 >= 7 = 1(r1(x1))
      
      r1(m(x1)) = 7 >= 0 = m(r1(x1))
      
      r0(b(x1)) = 15 >= 7 = qr(0(b(x1)))
      
      r1(b(x1)) = 7 >= 7 = qr(1(b(x1)))
      
      0(qr(x1)) = 7x1 >= 7x1 = qr(0(x1))
      
      1(qr(x1)) = 7x1 >= 7x1 = qr(1(x1))
      
      m(qr(x1)) = 0 >= 0 = ql(m(x1))
      
      0(ql(x1)) = x1 >= x1 = ql(0(x1))
      
      1(ql(x1)) = x1 >= x1 = ql(1(x1))
      
      b(ql(0(x1))) = 0 >= 0 = 0(b(r0(x1)))
      
      b(ql(1(x1))) = 0 >= 0 = 1(b(r1(x1)))
     problem:
      DPs:
       
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
     Qed
    
    DPs:
     1#(qr(x1)) -> 1#(x1)
     1#(ql(x1)) -> 1#(x1)
    TRS:
     r0(0(x1)) -> 0(r0(x1))
     r0(1(x1)) -> 1(r0(x1))
     r0(m(x1)) -> m(r0(x1))
     r1(0(x1)) -> 0(r1(x1))
     r1(1(x1)) -> 1(r1(x1))
     r1(m(x1)) -> m(r1(x1))
     r0(b(x1)) -> qr(0(b(x1)))
     r1(b(x1)) -> qr(1(b(x1)))
     0(qr(x1)) -> qr(0(x1))
     1(qr(x1)) -> qr(1(x1))
     m(qr(x1)) -> ql(m(x1))
     0(ql(x1)) -> ql(0(x1))
     1(ql(x1)) -> ql(1(x1))
     b(ql(0(x1))) -> 0(b(r0(x1)))
     b(ql(1(x1))) -> 1(b(r1(x1)))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [1#](x0) = x0,
      
      [ql](x0) = 1x0,
      
      [qr](x0) = 1x0,
      
      [b](x0) = x0,
      
      [r1](x0) = 1x0,
      
      [m](x0) = x0,
      
      [1](x0) = x0,
      
      [r0](x0) = 1x0,
      
      [0](x0) = x0
     orientation:
      1#(qr(x1)) = 1x1 >= x1 = 1#(x1)
      
      1#(ql(x1)) = 1x1 >= x1 = 1#(x1)
      
      r0(0(x1)) = 1x1 >= 1x1 = 0(r0(x1))
      
      r0(1(x1)) = 1x1 >= 1x1 = 1(r0(x1))
      
      r0(m(x1)) = 1x1 >= 1x1 = m(r0(x1))
      
      r1(0(x1)) = 1x1 >= 1x1 = 0(r1(x1))
      
      r1(1(x1)) = 1x1 >= 1x1 = 1(r1(x1))
      
      r1(m(x1)) = 1x1 >= 1x1 = m(r1(x1))
      
      r0(b(x1)) = 1x1 >= 1x1 = qr(0(b(x1)))
      
      r1(b(x1)) = 1x1 >= 1x1 = qr(1(b(x1)))
      
      0(qr(x1)) = 1x1 >= 1x1 = qr(0(x1))
      
      1(qr(x1)) = 1x1 >= 1x1 = qr(1(x1))
      
      m(qr(x1)) = 1x1 >= 1x1 = ql(m(x1))
      
      0(ql(x1)) = 1x1 >= 1x1 = ql(0(x1))
      
      1(ql(x1)) = 1x1 >= 1x1 = ql(1(x1))
      
      b(ql(0(x1))) = 1x1 >= 1x1 = 0(b(r0(x1)))
      
      b(ql(1(x1))) = 1x1 >= 1x1 = 1(b(r1(x1)))
     problem:
      DPs:
       
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
     Qed
    
    DPs:
     0#(qr(x1)) -> 0#(x1)
     0#(ql(x1)) -> 0#(x1)
    TRS:
     r0(0(x1)) -> 0(r0(x1))
     r0(1(x1)) -> 1(r0(x1))
     r0(m(x1)) -> m(r0(x1))
     r1(0(x1)) -> 0(r1(x1))
     r1(1(x1)) -> 1(r1(x1))
     r1(m(x1)) -> m(r1(x1))
     r0(b(x1)) -> qr(0(b(x1)))
     r1(b(x1)) -> qr(1(b(x1)))
     0(qr(x1)) -> qr(0(x1))
     1(qr(x1)) -> qr(1(x1))
     m(qr(x1)) -> ql(m(x1))
     0(ql(x1)) -> ql(0(x1))
     1(ql(x1)) -> ql(1(x1))
     b(ql(0(x1))) -> 0(b(r0(x1)))
     b(ql(1(x1))) -> 1(b(r1(x1)))
    KBO Processor:
     argument filtering:
      pi(0) = 0
      pi(r0) = [0]
      pi(1) = 0
      pi(m) = 0
      pi(r1) = [0]
      pi(b) = []
      pi(qr) = [0]
      pi(ql) = 0
      pi(0#) = 0
     weight function:
      w0 = 1
      w(0#) = w(b) = w(r1) = w(r0) = 1
      w(ql) = w(qr) = w(m) = w(1) = w(0) = 0
     precedence:
      1 > 0# ~ ql ~ qr ~ b ~ r1 ~ m ~ r0 ~ 0
     problem:
      DPs:
       0#(ql(x1)) -> 0#(x1)
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
     EDG Processor:
      DPs:
       0#(ql(x1)) -> 0#(x1)
      TRS:
       r0(0(x1)) -> 0(r0(x1))
       r0(1(x1)) -> 1(r0(x1))
       r0(m(x1)) -> m(r0(x1))
       r1(0(x1)) -> 0(r1(x1))
       r1(1(x1)) -> 1(r1(x1))
       r1(m(x1)) -> m(r1(x1))
       r0(b(x1)) -> qr(0(b(x1)))
       r1(b(x1)) -> qr(1(b(x1)))
       0(qr(x1)) -> qr(0(x1))
       1(qr(x1)) -> qr(1(x1))
       m(qr(x1)) -> ql(m(x1))
       0(ql(x1)) -> ql(0(x1))
       1(ql(x1)) -> ql(1(x1))
       b(ql(0(x1))) -> 0(b(r0(x1)))
       b(ql(1(x1))) -> 1(b(r1(x1)))
      graph:
       0#(ql(x1)) -> 0#(x1) -> 0#(ql(x1)) -> 0#(x1)
      CDG Processor:
       DPs:
        0#(ql(x1)) -> 0#(x1)
       TRS:
        r0(0(x1)) -> 0(r0(x1))
        r0(1(x1)) -> 1(r0(x1))
        r0(m(x1)) -> m(r0(x1))
        r1(0(x1)) -> 0(r1(x1))
        r1(1(x1)) -> 1(r1(x1))
        r1(m(x1)) -> m(r1(x1))
        r0(b(x1)) -> qr(0(b(x1)))
        r1(b(x1)) -> qr(1(b(x1)))
        0(qr(x1)) -> qr(0(x1))
        1(qr(x1)) -> qr(1(x1))
        m(qr(x1)) -> ql(m(x1))
        0(ql(x1)) -> ql(0(x1))
        1(ql(x1)) -> ql(1(x1))
        b(ql(0(x1))) -> 0(b(r0(x1)))
        b(ql(1(x1))) -> 1(b(r1(x1)))
       graph:
        
       Qed