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)))
    Matrix Interpretation Processor: dim=3
     
     interpretation:
      [b#](x0) = [1 0 0]x0,
      
                 [0 0 1]  
      [ql](x0) = [0 0 0]x0
                 [0 0 1]  ,
      
                 [0]
      [qr](x0) = [0]
                 [0],
      
                [1 0 1]     [0]
      [b](x0) = [1 0 1]x0 + [0]
                [1 0 0]     [1],
      
                 [0 0 1]  
      [r1](x0) = [0 0 0]x0
                 [0 0 1]  ,
      
                [0]
      [m](x0) = [0]
                [0],
      
                [0 0 1]     [1]
      [1](x0) = [0 0 0]x0 + [0]
                [0 0 1]     [1],
      
                 [0 0 1]  
      [r0](x0) = [0 0 0]x0
                 [0 0 1]  ,
      
                [0 0 1]     [1]
      [0](x0) = [0 0 0]x0 + [0]
                [0 0 1]     [1]
     orientation:
      b#(ql(1(x1))) = [0 0 1]x1 + [1] >= [0 0 1]x1 = b#(r1(x1))
      
      b#(ql(0(x1))) = [0 0 1]x1 + [1] >= [0 0 1]x1 = b#(r0(x1))
      
                  [0 0 1]     [1]    [0 0 1]     [1]            
      r0(0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(r0(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [1]    [0 0 1]     [1]            
      r0(1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(r0(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0]    [0]            
      r0(m(x1)) = [0] >= [0] = m(r0(x1))
                  [0]    [0]            
      
                  [0 0 1]     [1]    [0 0 1]     [1]            
      r1(0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(r1(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [1]    [0 0 1]     [1]            
      r1(1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(r1(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0]    [0]            
      r1(m(x1)) = [0] >= [0] = m(r1(x1))
                  [0]    [0]            
      
                  [1 0 0]     [1]    [0]               
      r0(b(x1)) = [0 0 0]x1 + [0] >= [0] = qr(0(b(x1)))
                  [1 0 0]     [1]    [0]               
      
                  [1 0 0]     [1]    [0]               
      r1(b(x1)) = [0 0 0]x1 + [0] >= [0] = qr(1(b(x1)))
                  [1 0 0]     [1]    [0]               
      
                  [1]    [0]            
      0(qr(x1)) = [0] >= [0] = qr(0(x1))
                  [1]    [0]            
      
                  [1]    [0]            
      1(qr(x1)) = [0] >= [0] = qr(1(x1))
                  [1]    [0]            
      
                  [0]    [0]            
      m(qr(x1)) = [0] >= [0] = ql(m(x1))
                  [0]    [0]            
      
                  [0 0 1]     [1]    [0 0 1]     [1]            
      0(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(0(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [1]    [0 0 1]     [1]            
      1(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(1(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                     [0 0 2]     [2]    [0 0 1]     [2]               
      b(ql(0(x1))) = [0 0 2]x1 + [2] >= [0 0 0]x1 + [0] = 0(b(r0(x1)))
                     [0 0 1]     [2]    [0 0 1]     [2]               
      
                     [0 0 2]     [2]    [0 0 1]     [2]               
      b(ql(1(x1))) = [0 0 2]x1 + [2] >= [0 0 0]x1 + [0] = 1(b(r1(x1)))
                     [0 0 1]     [2]    [0 0 1]     [2]               
     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)))
    Matrix Interpretation Processor: dim=3
     
     interpretation:
      [r1#](x0) = [1 0 1]x0,
      
                 [1 0 0]     [1]
      [ql](x0) = [0 0 0]x0 + [0]
                 [0 0 0]     [0],
      
                 [0 0 1]     [0]
      [qr](x0) = [0 0 0]x0 + [0]
                 [0 0 1]     [1],
      
                [1 0 0]  
      [b](x0) = [1 0 1]x0
                [0 0 0]  ,
      
                 [1 0 0]     [1]
      [r1](x0) = [0 0 1]x0 + [0]
                 [0 0 1]     [1],
      
                [0 0 1]     [1]
      [m](x0) = [0 0 0]x0 + [0]
                [1 0 0]     [0],
      
                [1 0 0]     [1]
      [1](x0) = [0 0 0]x0 + [0]
                [0 0 1]     [0],
      
                 [1 0 0]     [1]
      [r0](x0) = [0 0 0]x0 + [0]
                 [0 0 1]     [1],
      
                [1 0 0]     [1]
      [0](x0) = [0 0 0]x0 + [0]
                [0 0 1]     [0]
     orientation:
      r1#(0(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 = r1#(x1)
      
      r1#(1(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 = r1#(x1)
      
      r1#(m(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 = r1#(x1)
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      r0(0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(r0(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      r0(1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(r0(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [2]    [0 0 1]     [2]            
      r0(m(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = m(r0(x1))
                  [1 0 0]     [1]    [1 0 0]     [1]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      r1(0(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 0(r1(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      r1(1(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 1(r1(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [2]    [0 0 1]     [2]            
      r1(m(x1)) = [1 0 0]x1 + [0] >= [0 0 0]x1 + [0] = m(r1(x1))
                  [1 0 0]     [1]    [1 0 0]     [1]            
      
                  [1 0 0]     [1]    [0]               
      r0(b(x1)) = [0 0 0]x1 + [0] >= [0] = qr(0(b(x1)))
                  [0 0 0]     [1]    [1]               
      
                  [1 0 0]     [1]    [0]               
      r1(b(x1)) = [0 0 0]x1 + [0] >= [0] = qr(1(b(x1)))
                  [0 0 0]     [1]    [1]               
      
                  [0 0 1]     [1]    [0 0 1]     [0]            
      0(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = qr(0(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [1]    [0 0 1]     [0]            
      1(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = qr(1(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [2]    [0 0 1]     [2]            
      m(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(m(x1))
                  [0 0 1]     [0]    [0 0 0]     [0]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      0(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(0(x1))
                  [0 0 0]     [0]    [0 0 0]     [0]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      1(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(1(x1))
                  [0 0 0]     [0]    [0 0 0]     [0]            
      
                     [1 0 0]     [2]    [1 0 0]     [2]               
      b(ql(0(x1))) = [1 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 0(b(r0(x1)))
                     [0 0 0]     [0]    [0 0 0]     [0]               
      
                     [1 0 0]     [2]    [1 0 0]     [2]               
      b(ql(1(x1))) = [1 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 1(b(r1(x1)))
                     [0 0 0]     [0]    [0 0 0]     [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:
     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)))
    Matrix Interpretation Processor: dim=3
     
     interpretation:
      [r0#](x0) = [1 0 1]x0,
      
                 [1 0 0]     [1]
      [ql](x0) = [0 0 0]x0 + [0]
                 [0 0 0]     [0],
      
                 [0 0 1]     [0]
      [qr](x0) = [0 0 0]x0 + [0]
                 [0 0 1]     [1],
      
                [1 0 0]  
      [b](x0) = [1 0 1]x0
                [0 0 0]  ,
      
                 [1 0 0]     [1]
      [r1](x0) = [0 0 1]x0 + [0]
                 [0 0 1]     [1],
      
                [0 0 1]     [1]
      [m](x0) = [0 0 0]x0 + [0]
                [1 0 0]     [0],
      
                [1 0 0]     [1]
      [1](x0) = [0 0 0]x0 + [0]
                [0 0 1]     [0],
      
                 [1 0 0]     [1]
      [r0](x0) = [0 0 0]x0 + [0]
                 [0 0 1]     [1],
      
                [1 0 0]     [1]
      [0](x0) = [0 0 0]x0 + [0]
                [0 0 1]     [0]
     orientation:
      r0#(0(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 = r0#(x1)
      
      r0#(1(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 = r0#(x1)
      
      r0#(m(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 = r0#(x1)
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      r0(0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0(r0(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      r0(1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(r0(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [2]    [0 0 1]     [2]            
      r0(m(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = m(r0(x1))
                  [1 0 0]     [1]    [1 0 0]     [1]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      r1(0(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 0(r1(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      r1(1(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 1(r1(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [2]    [0 0 1]     [2]            
      r1(m(x1)) = [1 0 0]x1 + [0] >= [0 0 0]x1 + [0] = m(r1(x1))
                  [1 0 0]     [1]    [1 0 0]     [1]            
      
                  [1 0 0]     [1]    [0]               
      r0(b(x1)) = [0 0 0]x1 + [0] >= [0] = qr(0(b(x1)))
                  [0 0 0]     [1]    [1]               
      
                  [1 0 0]     [1]    [0]               
      r1(b(x1)) = [0 0 0]x1 + [0] >= [0] = qr(1(b(x1)))
                  [0 0 0]     [1]    [1]               
      
                  [0 0 1]     [1]    [0 0 1]     [0]            
      0(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = qr(0(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [1]    [0 0 1]     [0]            
      1(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = qr(1(x1))
                  [0 0 1]     [1]    [0 0 1]     [1]            
      
                  [0 0 1]     [2]    [0 0 1]     [2]            
      m(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(m(x1))
                  [0 0 1]     [0]    [0 0 0]     [0]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      0(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(0(x1))
                  [0 0 0]     [0]    [0 0 0]     [0]            
      
                  [1 0 0]     [2]    [1 0 0]     [2]            
      1(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(1(x1))
                  [0 0 0]     [0]    [0 0 0]     [0]            
      
                     [1 0 0]     [2]    [1 0 0]     [2]               
      b(ql(0(x1))) = [1 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 0(b(r0(x1)))
                     [0 0 0]     [0]    [0 0 0]     [0]               
      
                     [1 0 0]     [2]    [1 0 0]     [2]               
      b(ql(1(x1))) = [1 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 1(b(r1(x1)))
                     [0 0 0]     [0]    [0 0 0]     [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:
    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)))
   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) = []
     pi(m#) = 0
    weight function:
     w0 = 1
     w(m#) = w(ql) = w(qr) = w(b) = w(r1) = w(m) = w(1) = w(r0) = w(0) = 1
    precedence:
     m# ~ ql ~ b ~ r0 > r1 > qr ~ m ~ 1 ~ 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:
    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)))
   Matrix Interpretation Processor: dim=3
    
    interpretation:
     [1#](x0) = [0 1 1]x0 + [1],
     
                [0 0 0]     [0]
     [ql](x0) = [0 0 0]x0 + [0]
                [0 1 1]     [1],
     
                [0 0 0]     [0]
     [qr](x0) = [0 1 0]x0 + [0]
                [0 0 1]     [1],
     
               [0 1 0]  
     [b](x0) = [0 1 0]x0
               [0 0 0]  ,
     
                [1 0 0]     [1]
     [r1](x0) = [0 1 1]x0 + [0]
                [0 0 1]     [1],
     
               [0 0 1]  
     [m](x0) = [0 0 0]x0
               [0 0 1]  ,
     
               [0 0 0]  
     [1](x0) = [0 0 0]x0
               [0 0 1]  ,
     
                [0 0 0]     [1]
     [r0](x0) = [1 1 0]x0 + [0]
                [0 0 0]     [1],
     
               [0 0 0]  
     [0](x0) = [0 0 0]x0
               [0 0 1]  
    orientation:
     1#(qr(x1)) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [1] = 1#(x1)
     
     1#(ql(x1)) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [1] = 1#(x1)
     
                 [1]    [0]            
     r0(0(x1)) = [0] >= [0] = 0(r0(x1))
                 [1]    [1]            
     
                 [1]    [0]            
     r0(1(x1)) = [0] >= [0] = 1(r0(x1))
                 [1]    [1]            
     
                 [0 0 0]     [1]    [1]            
     r0(m(x1)) = [0 0 1]x1 + [0] >= [0] = m(r0(x1))
                 [0 0 0]     [1]    [1]            
     
                 [0 0 0]     [1]    [0 0 0]     [0]            
     r1(0(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 0(r1(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [1]    [0 0 0]     [0]            
     r1(1(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 1(r1(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 1]     [1]    [0 0 1]     [1]            
     r1(m(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = m(r1(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [1]    [0]               
     r0(b(x1)) = [0 2 0]x1 + [0] >= [0] = qr(0(b(x1)))
                 [0 0 0]     [1]    [1]               
     
                 [0 1 0]     [1]    [0]               
     r1(b(x1)) = [0 1 0]x1 + [0] >= [0] = qr(1(b(x1)))
                 [0 0 0]     [1]    [1]               
     
                 [0 0 0]     [0]    [0 0 0]     [0]            
     0(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = qr(0(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [0]    [0 0 0]     [0]            
     1(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = qr(1(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 1]     [1]    [0 0 0]     [0]            
     m(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(m(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [0]    [0 0 0]     [0]            
     0(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(0(x1))
                 [0 1 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [0]    [0 0 0]     [0]            
     1(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(1(x1))
                 [0 1 1]     [1]    [0 0 1]     [1]            
     
                    [0]    [0]               
     b(ql(0(x1))) = [0] >= [0] = 0(b(r0(x1)))
                    [0]    [0]               
     
                    [0]    [0]               
     b(ql(1(x1))) = [0] >= [0] = 1(b(r1(x1)))
                    [0]    [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:
    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)))
   Matrix Interpretation Processor: dim=3
    
    interpretation:
     [0#](x0) = [0 1 1]x0 + [1],
     
                [0 0 0]     [0]
     [ql](x0) = [0 0 0]x0 + [0]
                [0 1 1]     [1],
     
                [0 0 0]     [0]
     [qr](x0) = [0 1 0]x0 + [0]
                [0 0 1]     [1],
     
               [0 1 0]  
     [b](x0) = [0 1 0]x0
               [0 0 0]  ,
     
                [1 0 0]     [1]
     [r1](x0) = [0 1 1]x0 + [0]
                [0 0 1]     [1],
     
               [0 0 1]  
     [m](x0) = [0 0 0]x0
               [0 0 1]  ,
     
               [0 0 0]  
     [1](x0) = [0 0 0]x0
               [0 0 1]  ,
     
                [0 0 0]     [1]
     [r0](x0) = [1 1 0]x0 + [0]
                [0 0 0]     [1],
     
               [0 0 0]  
     [0](x0) = [0 0 0]x0
               [0 0 1]  
    orientation:
     0#(qr(x1)) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [1] = 0#(x1)
     
     0#(ql(x1)) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [1] = 0#(x1)
     
                 [1]    [0]            
     r0(0(x1)) = [0] >= [0] = 0(r0(x1))
                 [1]    [1]            
     
                 [1]    [0]            
     r0(1(x1)) = [0] >= [0] = 1(r0(x1))
                 [1]    [1]            
     
                 [0 0 0]     [1]    [1]            
     r0(m(x1)) = [0 0 1]x1 + [0] >= [0] = m(r0(x1))
                 [0 0 0]     [1]    [1]            
     
                 [0 0 0]     [1]    [0 0 0]     [0]            
     r1(0(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 0(r1(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [1]    [0 0 0]     [0]            
     r1(1(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = 1(r1(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 1]     [1]    [0 0 1]     [1]            
     r1(m(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = m(r1(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [1]    [0]               
     r0(b(x1)) = [0 2 0]x1 + [0] >= [0] = qr(0(b(x1)))
                 [0 0 0]     [1]    [1]               
     
                 [0 1 0]     [1]    [0]               
     r1(b(x1)) = [0 1 0]x1 + [0] >= [0] = qr(1(b(x1)))
                 [0 0 0]     [1]    [1]               
     
                 [0 0 0]     [0]    [0 0 0]     [0]            
     0(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = qr(0(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [0]    [0 0 0]     [0]            
     1(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = qr(1(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 1]     [1]    [0 0 0]     [0]            
     m(qr(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(m(x1))
                 [0 0 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [0]    [0 0 0]     [0]            
     0(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(0(x1))
                 [0 1 1]     [1]    [0 0 1]     [1]            
     
                 [0 0 0]     [0]    [0 0 0]     [0]            
     1(ql(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = ql(1(x1))
                 [0 1 1]     [1]    [0 0 1]     [1]            
     
                    [0]    [0]               
     b(ql(0(x1))) = [0] >= [0] = 0(b(r0(x1)))
                    [0]    [0]               
     
                    [0]    [0]               
     b(ql(1(x1))) = [0] >= [0] = 1(b(r1(x1)))
                    [0]    [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