MAYBE

Problem:
 1(2(1(x1))) -> 2(0(2(x1)))
 0(2(1(x1))) -> 1(0(2(x1)))
 L(2(1(x1))) -> L(1(0(2(x1))))
 1(2(0(x1))) -> 2(0(1(x1)))
 1(2(R(x1))) -> 2(0(1(R(x1))))
 0(2(0(x1))) -> 1(0(1(x1)))
 L(2(0(x1))) -> L(1(0(1(x1))))
 0(2(R(x1))) -> 1(0(1(R(x1))))

Proof:
 Complexity Transformation Processor:
  strict:
   1(2(1(x1))) -> 2(0(2(x1)))
   0(2(1(x1))) -> 1(0(2(x1)))
   L(2(1(x1))) -> L(1(0(2(x1))))
   1(2(0(x1))) -> 2(0(1(x1)))
   1(2(R(x1))) -> 2(0(1(R(x1))))
   0(2(0(x1))) -> 1(0(1(x1)))
   L(2(0(x1))) -> L(1(0(1(x1))))
   0(2(R(x1))) -> 1(0(1(R(x1))))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [R](x0) = x0 + 1,
     
     [L](x0) = x0,
     
     [0](x0) = x0,
     
     [2](x0) = x0,
     
     [1](x0) = x0 + 1
    orientation:
     1(2(1(x1))) = x1 + 2 >= x1 = 2(0(2(x1)))
     
     0(2(1(x1))) = x1 + 1 >= x1 + 1 = 1(0(2(x1)))
     
     L(2(1(x1))) = x1 + 1 >= x1 + 1 = L(1(0(2(x1))))
     
     1(2(0(x1))) = x1 + 1 >= x1 + 1 = 2(0(1(x1)))
     
     1(2(R(x1))) = x1 + 2 >= x1 + 2 = 2(0(1(R(x1))))
     
     0(2(0(x1))) = x1 >= x1 + 2 = 1(0(1(x1)))
     
     L(2(0(x1))) = x1 >= x1 + 2 = L(1(0(1(x1))))
     
     0(2(R(x1))) = x1 + 1 >= x1 + 3 = 1(0(1(R(x1))))
    problem:
     strict:
      0(2(1(x1))) -> 1(0(2(x1)))
      L(2(1(x1))) -> L(1(0(2(x1))))
      1(2(0(x1))) -> 2(0(1(x1)))
      1(2(R(x1))) -> 2(0(1(R(x1))))
      0(2(0(x1))) -> 1(0(1(x1)))
      L(2(0(x1))) -> L(1(0(1(x1))))
      0(2(R(x1))) -> 1(0(1(R(x1))))
     weak:
      1(2(1(x1))) -> 2(0(2(x1)))
    Matrix Interpretation Processor:
     dimension: 2
     max_matrix:
      [1 1]
      [0 1]
      interpretation:
                 [1 0]     [1]
       [R](x0) = [0 0]x0 + [1],
       
                 [1 0]  
       [L](x0) = [0 0]x0,
       
                 [1 0]  
       [0](x0) = [0 0]x0,
       
                 [1 1]  
       [2](x0) = [0 0]x0,
       
                   
       [1](x0) = x0
      orientation:
                     [1 1]      [1 1]                
       0(2(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(0(2(x1)))
       
                     [1 1]      [1 1]                   
       L(2(1(x1))) = [0 0]x1 >= [0 0]x1 = L(1(0(2(x1))))
       
                     [1 0]      [1 0]                
       1(2(0(x1))) = [0 0]x1 >= [0 0]x1 = 2(0(1(x1)))
       
                     [1 0]     [2]    [1 0]     [1]                 
       1(2(R(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 2(0(1(R(x1))))
       
                     [1 0]      [1 0]                
       0(2(0(x1))) = [0 0]x1 >= [0 0]x1 = 1(0(1(x1)))
       
                     [1 0]      [1 0]                   
       L(2(0(x1))) = [0 0]x1 >= [0 0]x1 = L(1(0(1(x1))))
       
                     [1 0]     [2]    [1 0]     [1]                 
       0(2(R(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = 1(0(1(R(x1))))
       
                     [1 1]      [1 1]                
       1(2(1(x1))) = [0 0]x1 >= [0 0]x1 = 2(0(2(x1)))
      problem:
       strict:
        0(2(1(x1))) -> 1(0(2(x1)))
        L(2(1(x1))) -> L(1(0(2(x1))))
        1(2(0(x1))) -> 2(0(1(x1)))
        0(2(0(x1))) -> 1(0(1(x1)))
        L(2(0(x1))) -> L(1(0(1(x1))))
       weak:
        1(2(R(x1))) -> 2(0(1(R(x1))))
        0(2(R(x1))) -> 1(0(1(R(x1))))
        1(2(1(x1))) -> 2(0(2(x1)))
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
                   [1 0]     [0]
         [R](x0) = [0 0]x0 + [1],
         
                   [1 1]     [1]
         [L](x0) = [0 1]x0 + [0],
         
                   [1 0]  
         [0](x0) = [0 0]x0,
         
                        [0]
         [2](x0) = x0 + [1],
         
                     
         [1](x0) = x0
        orientation:
                       [1 0]      [1 0]                
         0(2(1(x1))) = [0 0]x1 >= [0 0]x1 = 1(0(2(x1)))
         
                       [1 1]     [2]    [1 0]     [1]                 
         L(2(1(x1))) = [0 1]x1 + [1] >= [0 0]x1 + [0] = L(1(0(2(x1))))
         
                       [1 0]     [0]    [1 0]     [0]              
         1(2(0(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = 2(0(1(x1)))
         
                       [1 0]      [1 0]                
         0(2(0(x1))) = [0 0]x1 >= [0 0]x1 = 1(0(1(x1)))
         
                       [1 0]     [2]    [1 0]     [1]                 
         L(2(0(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [0] = L(1(0(1(x1))))
         
                       [1 0]     [0]    [1 0]     [0]                 
         1(2(R(x1))) = [0 0]x1 + [2] >= [0 0]x1 + [1] = 2(0(1(R(x1))))
         
                       [1 0]      [1 0]                   
         0(2(R(x1))) = [0 0]x1 >= [0 0]x1 = 1(0(1(R(x1))))
         
                            [0]    [1 0]     [0]              
         1(2(1(x1))) = x1 + [1] >= [0 0]x1 + [1] = 2(0(2(x1)))
        problem:
         strict:
          0(2(1(x1))) -> 1(0(2(x1)))
          1(2(0(x1))) -> 2(0(1(x1)))
          0(2(0(x1))) -> 1(0(1(x1)))
         weak:
          L(2(1(x1))) -> L(1(0(2(x1))))
          L(2(0(x1))) -> L(1(0(1(x1))))
          1(2(R(x1))) -> 2(0(1(R(x1))))
          0(2(R(x1))) -> 1(0(1(R(x1))))
          1(2(1(x1))) -> 2(0(2(x1)))
        Open