MAYBE

Problem:
 +(p1(),p1()) -> p2()
 +(p1(),+(p2(),p2())) -> p5()
 +(p5(),p5()) -> p10()
 +(+(x,y),z) -> +(x,+(y,z))
 +(p1(),+(p1(),x)) -> +(p2(),x)
 +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
 +(p2(),p1()) -> +(p1(),p2())
 +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
 +(p2(),+(p2(),p2())) -> +(p1(),p5())
 +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
 +(p5(),p1()) -> +(p1(),p5())
 +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
 +(p5(),p2()) -> +(p2(),p5())
 +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
 +(p5(),+(p5(),x)) -> +(p10(),x)
 +(p10(),p1()) -> +(p1(),p10())
 +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
 +(p10(),p2()) -> +(p2(),p10())
 +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
 +(p10(),p5()) -> +(p5(),p10())
 +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))

Proof:
 Complexity Transformation Processor:
  strict:
   +(p1(),p1()) -> p2()
   +(p1(),+(p2(),p2())) -> p5()
   +(p5(),p5()) -> p10()
   +(+(x,y),z) -> +(x,+(y,z))
   +(p1(),+(p1(),x)) -> +(p2(),x)
   +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
   +(p2(),p1()) -> +(p1(),p2())
   +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
   +(p2(),+(p2(),p2())) -> +(p1(),p5())
   +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
   +(p5(),p1()) -> +(p1(),p5())
   +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
   +(p5(),p2()) -> +(p2(),p5())
   +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
   +(p5(),+(p5(),x)) -> +(p10(),x)
   +(p10(),p1()) -> +(p1(),p10())
   +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
   +(p10(),p2()) -> +(p2(),p10())
   +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
   +(p10(),p5()) -> +(p5(),p10())
   +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [p10] = 0,
     
     [p5] = 0,
     
     [p2] = 1,
     
     [+](x0, x1) = x0 + x1,
     
     [p1] = 0
    orientation:
     +(p1(),p1()) = 0 >= 1 = p2()
     
     +(p1(),+(p2(),p2())) = 2 >= 0 = p5()
     
     +(p5(),p5()) = 0 >= 0 = p10()
     
     +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
     
     +(p1(),+(p1(),x)) = x >= x + 1 = +(p2(),x)
     
     +(p1(),+(p2(),+(p2(),x))) = x + 2 >= x = +(p5(),x)
     
     +(p2(),p1()) = 1 >= 1 = +(p1(),p2())
     
     +(p2(),+(p1(),x)) = x + 1 >= x + 1 = +(p1(),+(p2(),x))
     
     +(p2(),+(p2(),p2())) = 3 >= 0 = +(p1(),p5())
     
     +(p2(),+(p2(),+(p2(),x))) = x + 3 >= x = +(p1(),+(p5(),x))
     
     +(p5(),p1()) = 0 >= 0 = +(p1(),p5())
     
     +(p5(),+(p1(),x)) = x >= x = +(p1(),+(p5(),x))
     
     +(p5(),p2()) = 1 >= 1 = +(p2(),p5())
     
     +(p5(),+(p2(),x)) = x + 1 >= x + 1 = +(p2(),+(p5(),x))
     
     +(p5(),+(p5(),x)) = x >= x = +(p10(),x)
     
     +(p10(),p1()) = 0 >= 0 = +(p1(),p10())
     
     +(p10(),+(p1(),x)) = x >= x = +(p1(),+(p10(),x))
     
     +(p10(),p2()) = 1 >= 1 = +(p2(),p10())
     
     +(p10(),+(p2(),x)) = x + 1 >= x + 1 = +(p2(),+(p10(),x))
     
     +(p10(),p5()) = 0 >= 0 = +(p5(),p10())
     
     +(p10(),+(p5(),x)) = x >= x = +(p5(),+(p10(),x))
    problem:
     strict:
      +(p1(),p1()) -> p2()
      +(p5(),p5()) -> p10()
      +(+(x,y),z) -> +(x,+(y,z))
      +(p1(),+(p1(),x)) -> +(p2(),x)
      +(p2(),p1()) -> +(p1(),p2())
      +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
      +(p5(),p1()) -> +(p1(),p5())
      +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
      +(p5(),p2()) -> +(p2(),p5())
      +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
      +(p5(),+(p5(),x)) -> +(p10(),x)
      +(p10(),p1()) -> +(p1(),p10())
      +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
      +(p10(),p2()) -> +(p2(),p10())
      +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
      +(p10(),p5()) -> +(p5(),p10())
      +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
     weak:
      +(p1(),+(p2(),p2())) -> p5()
      +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
      +(p2(),+(p2(),p2())) -> +(p1(),p5())
      +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [p10] = 1,
       
       [p5] = 0,
       
       [p2] = 0,
       
       [+](x0, x1) = x0 + x1 + 1,
       
       [p1] = 0
      orientation:
       +(p1(),p1()) = 1 >= 0 = p2()
       
       +(p5(),p5()) = 1 >= 1 = p10()
       
       +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z))
       
       +(p1(),+(p1(),x)) = x + 2 >= x + 1 = +(p2(),x)
       
       +(p2(),p1()) = 1 >= 1 = +(p1(),p2())
       
       +(p2(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p2(),x))
       
       +(p5(),p1()) = 1 >= 1 = +(p1(),p5())
       
       +(p5(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p5(),x))
       
       +(p5(),p2()) = 1 >= 1 = +(p2(),p5())
       
       +(p5(),+(p2(),x)) = x + 2 >= x + 2 = +(p2(),+(p5(),x))
       
       +(p5(),+(p5(),x)) = x + 2 >= x + 2 = +(p10(),x)
       
       +(p10(),p1()) = 2 >= 2 = +(p1(),p10())
       
       +(p10(),+(p1(),x)) = x + 3 >= x + 3 = +(p1(),+(p10(),x))
       
       +(p10(),p2()) = 2 >= 2 = +(p2(),p10())
       
       +(p10(),+(p2(),x)) = x + 3 >= x + 3 = +(p2(),+(p10(),x))
       
       +(p10(),p5()) = 2 >= 2 = +(p5(),p10())
       
       +(p10(),+(p5(),x)) = x + 3 >= x + 3 = +(p5(),+(p10(),x))
       
       +(p1(),+(p2(),p2())) = 2 >= 0 = p5()
       
       +(p1(),+(p2(),+(p2(),x))) = x + 3 >= x + 1 = +(p5(),x)
       
       +(p2(),+(p2(),p2())) = 2 >= 1 = +(p1(),p5())
       
       +(p2(),+(p2(),+(p2(),x))) = x + 3 >= x + 2 = +(p1(),+(p5(),x))
      problem:
       strict:
        +(p5(),p5()) -> p10()
        +(+(x,y),z) -> +(x,+(y,z))
        +(p2(),p1()) -> +(p1(),p2())
        +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
        +(p5(),p1()) -> +(p1(),p5())
        +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
        +(p5(),p2()) -> +(p2(),p5())
        +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
        +(p5(),+(p5(),x)) -> +(p10(),x)
        +(p10(),p1()) -> +(p1(),p10())
        +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
        +(p10(),p2()) -> +(p2(),p10())
        +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
        +(p10(),p5()) -> +(p5(),p10())
        +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
       weak:
        +(p1(),p1()) -> p2()
        +(p1(),+(p1(),x)) -> +(p2(),x)
        +(p1(),+(p2(),p2())) -> p5()
        +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
        +(p2(),+(p2(),p2())) -> +(p1(),p5())
        +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [p10] = 0,
         
         [p5] = 1,
         
         [p2] = 1,
         
         [+](x0, x1) = x0 + x1,
         
         [p1] = 1
        orientation:
         +(p5(),p5()) = 2 >= 0 = p10()
         
         +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
         
         +(p2(),p1()) = 2 >= 2 = +(p1(),p2())
         
         +(p2(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p2(),x))
         
         +(p5(),p1()) = 2 >= 2 = +(p1(),p5())
         
         +(p5(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p5(),x))
         
         +(p5(),p2()) = 2 >= 2 = +(p2(),p5())
         
         +(p5(),+(p2(),x)) = x + 2 >= x + 2 = +(p2(),+(p5(),x))
         
         +(p5(),+(p5(),x)) = x + 2 >= x = +(p10(),x)
         
         +(p10(),p1()) = 1 >= 1 = +(p1(),p10())
         
         +(p10(),+(p1(),x)) = x + 1 >= x + 1 = +(p1(),+(p10(),x))
         
         +(p10(),p2()) = 1 >= 1 = +(p2(),p10())
         
         +(p10(),+(p2(),x)) = x + 1 >= x + 1 = +(p2(),+(p10(),x))
         
         +(p10(),p5()) = 1 >= 1 = +(p5(),p10())
         
         +(p10(),+(p5(),x)) = x + 1 >= x + 1 = +(p5(),+(p10(),x))
         
         +(p1(),p1()) = 2 >= 1 = p2()
         
         +(p1(),+(p1(),x)) = x + 2 >= x + 1 = +(p2(),x)
         
         +(p1(),+(p2(),p2())) = 3 >= 1 = p5()
         
         +(p1(),+(p2(),+(p2(),x))) = x + 3 >= x + 1 = +(p5(),x)
         
         +(p2(),+(p2(),p2())) = 3 >= 2 = +(p1(),p5())
         
         +(p2(),+(p2(),+(p2(),x))) = x + 3 >= x + 2 = +(p1(),+(p5(),x))
        problem:
         strict:
          +(+(x,y),z) -> +(x,+(y,z))
          +(p2(),p1()) -> +(p1(),p2())
          +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
          +(p5(),p1()) -> +(p1(),p5())
          +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
          +(p5(),p2()) -> +(p2(),p5())
          +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
          +(p10(),p1()) -> +(p1(),p10())
          +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
          +(p10(),p2()) -> +(p2(),p10())
          +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
          +(p10(),p5()) -> +(p5(),p10())
          +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
         weak:
          +(p5(),p5()) -> p10()
          +(p5(),+(p5(),x)) -> +(p10(),x)
          +(p1(),p1()) -> p2()
          +(p1(),+(p1(),x)) -> +(p2(),x)
          +(p1(),+(p2(),p2())) -> p5()
          +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
          +(p2(),+(p2(),p2())) -> +(p1(),p5())
          +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
        Bounds Processor:
         bound: 1
         enrichment: match
         automaton:
          final states: {6}
          transitions:
           +1(11,6) -> 11*
           +1(6,6) -> 6*
           +1(12,11) -> 11,6
           +1(11,11) -> 6,11
           +1(6,11) -> 11*
           p11() -> 12*
           p21() -> 6,11
           p51() -> 6,11
           p101() -> 6,11
           +0(6,6) -> 6*
           p20() -> 6*
           p10() -> 6*
           p50() -> 6*
           p100() -> 6*
         problem:
          strict:
           +(+(x,y),z) -> +(x,+(y,z))
           +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
           +(p5(),p1()) -> +(p1(),p5())
           +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
           +(p5(),p2()) -> +(p2(),p5())
           +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
           +(p10(),p1()) -> +(p1(),p10())
           +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
           +(p10(),p2()) -> +(p2(),p10())
           +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
           +(p10(),p5()) -> +(p5(),p10())
           +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
          weak:
           +(p2(),p1()) -> +(p1(),p2())
           +(p5(),p5()) -> p10()
           +(p5(),+(p5(),x)) -> +(p10(),x)
           +(p1(),p1()) -> p2()
           +(p1(),+(p1(),x)) -> +(p2(),x)
           +(p1(),+(p2(),p2())) -> p5()
           +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
           +(p2(),+(p2(),p2())) -> +(p1(),p5())
           +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
         Matrix Interpretation Processor:
          dimension: 2
          max_matrix:
           [1 1]
           [0 0]
           interpretation:
                    [0]
            [p10] = [0],
            
                   [0]
            [p5] = [0],
            
                   [0]
            [p2] = [0],
            
                          [1 0]     [1 1]  
            [+](x0, x1) = [0 0]x0 + [0 0]x1,
            
                   [0]
            [p1] = [1]
           orientation:
                          [1 0]    [1 1]    [1 1]     [1 0]    [1 0]    [1 1]               
            +(+(x,y),z) = [0 0]x + [0 0]y + [0 0]z >= [0 0]x + [0 0]y + [0 0]z = +(x,+(y,z))
            
                                [1 1]     [1 1]                     
            +(p2(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p1(),+(p2(),x))
            
                           [1]    [0]               
            +(p5(),p1()) = [0] >= [0] = +(p1(),p5())
            
                                [1 1]     [1 1]                     
            +(p5(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p1(),+(p5(),x))
            
                           [0]    [0]               
            +(p5(),p2()) = [0] >= [0] = +(p2(),p5())
            
                                [1 1]     [1 1]                     
            +(p5(),+(p2(),x)) = [0 0]x >= [0 0]x = +(p2(),+(p5(),x))
            
                            [1]    [0]                
            +(p10(),p1()) = [0] >= [0] = +(p1(),p10())
            
                                 [1 1]     [1 1]                      
            +(p10(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p1(),+(p10(),x))
            
                            [0]    [0]                
            +(p10(),p2()) = [0] >= [0] = +(p2(),p10())
            
                                 [1 1]     [1 1]                      
            +(p10(),+(p2(),x)) = [0 0]x >= [0 0]x = +(p2(),+(p10(),x))
            
                            [0]    [0]                
            +(p10(),p5()) = [0] >= [0] = +(p5(),p10())
            
                                 [1 1]     [1 1]                      
            +(p10(),+(p5(),x)) = [0 0]x >= [0 0]x = +(p5(),+(p10(),x))
            
                           [1]    [0]               
            +(p2(),p1()) = [0] >= [0] = +(p1(),p2())
            
                           [0]    [0]        
            +(p5(),p5()) = [0] >= [0] = p10()
            
                                [1 1]     [1 1]              
            +(p5(),+(p5(),x)) = [0 0]x >= [0 0]x = +(p10(),x)
            
                           [1]    [0]       
            +(p1(),p1()) = [0] >= [0] = p2()
            
                                [1 1]     [1 1]             
            +(p1(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p2(),x)
            
                                   [0]    [0]       
            +(p1(),+(p2(),p2())) = [0] >= [0] = p5()
            
                                        [1 1]     [1 1]             
            +(p1(),+(p2(),+(p2(),x))) = [0 0]x >= [0 0]x = +(p5(),x)
            
                                   [0]    [0]               
            +(p2(),+(p2(),p2())) = [0] >= [0] = +(p1(),p5())
            
                                        [1 1]     [1 1]                     
            +(p2(),+(p2(),+(p2(),x))) = [0 0]x >= [0 0]x = +(p1(),+(p5(),x))
           problem:
            strict:
             +(+(x,y),z) -> +(x,+(y,z))
             +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
             +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
             +(p5(),p2()) -> +(p2(),p5())
             +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
             +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
             +(p10(),p2()) -> +(p2(),p10())
             +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
             +(p10(),p5()) -> +(p5(),p10())
             +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
            weak:
             +(p5(),p1()) -> +(p1(),p5())
             +(p10(),p1()) -> +(p1(),p10())
             +(p2(),p1()) -> +(p1(),p2())
             +(p5(),p5()) -> p10()
             +(p5(),+(p5(),x)) -> +(p10(),x)
             +(p1(),p1()) -> p2()
             +(p1(),+(p1(),x)) -> +(p2(),x)
             +(p1(),+(p2(),p2())) -> p5()
             +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
             +(p2(),+(p2(),p2())) -> +(p1(),p5())
             +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
           Matrix Interpretation Processor:
            dimension: 2
            max_matrix:
             [1 1]
             [0 1]
             interpretation:
                      [0]
              [p10] = [0],
              
                     [0]
              [p5] = [0],
              
                     [0]
              [p2] = [0],
              
                            [1 1]          [0]
              [+](x0, x1) = [0 1]x0 + x1 + [1],
              
                     [0]
              [p1] = [0]
             orientation:
                            [1 2]    [1 1]        [1]    [1 1]    [1 1]        [0]              
              +(+(x,y),z) = [0 1]x + [0 1]y + z + [2] >= [0 1]x + [0 1]y + z + [2] = +(x,+(y,z))
              
                                      [0]        [0]                    
              +(p2(),+(p1(),x)) = x + [2] >= x + [2] = +(p1(),+(p2(),x))
              
                                      [0]        [0]                    
              +(p5(),+(p1(),x)) = x + [2] >= x + [2] = +(p1(),+(p5(),x))
              
                             [0]    [0]               
              +(p5(),p2()) = [1] >= [1] = +(p2(),p5())
              
                                      [0]        [0]                    
              +(p5(),+(p2(),x)) = x + [2] >= x + [2] = +(p2(),+(p5(),x))
              
                                       [0]        [0]                     
              +(p10(),+(p1(),x)) = x + [2] >= x + [2] = +(p1(),+(p10(),x))
              
                              [0]    [0]                
              +(p10(),p2()) = [1] >= [1] = +(p2(),p10())
              
                                       [0]        [0]                     
              +(p10(),+(p2(),x)) = x + [2] >= x + [2] = +(p2(),+(p10(),x))
              
                              [0]    [0]                
              +(p10(),p5()) = [1] >= [1] = +(p5(),p10())
              
                                       [0]        [0]                     
              +(p10(),+(p5(),x)) = x + [2] >= x + [2] = +(p5(),+(p10(),x))
              
                             [0]    [0]               
              +(p5(),p1()) = [1] >= [1] = +(p1(),p5())
              
                              [0]    [0]                
              +(p10(),p1()) = [1] >= [1] = +(p1(),p10())
              
                             [0]    [0]               
              +(p2(),p1()) = [1] >= [1] = +(p1(),p2())
              
                             [0]    [0]        
              +(p5(),p5()) = [1] >= [0] = p10()
              
                                      [0]        [0]             
              +(p5(),+(p5(),x)) = x + [2] >= x + [1] = +(p10(),x)
              
                             [0]    [0]       
              +(p1(),p1()) = [1] >= [0] = p2()
              
                                      [0]        [0]            
              +(p1(),+(p1(),x)) = x + [2] >= x + [1] = +(p2(),x)
              
                                     [0]    [0]       
              +(p1(),+(p2(),p2())) = [2] >= [0] = p5()
              
                                              [0]        [0]            
              +(p1(),+(p2(),+(p2(),x))) = x + [3] >= x + [1] = +(p5(),x)
              
                                     [0]    [0]               
              +(p2(),+(p2(),p2())) = [2] >= [1] = +(p1(),p5())
              
                                              [0]        [0]                    
              +(p2(),+(p2(),+(p2(),x))) = x + [3] >= x + [2] = +(p1(),+(p5(),x))
             problem:
              strict:
               +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
               +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
               +(p5(),p2()) -> +(p2(),p5())
               +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
               +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
               +(p10(),p2()) -> +(p2(),p10())
               +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
               +(p10(),p5()) -> +(p5(),p10())
               +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
              weak:
               +(+(x,y),z) -> +(x,+(y,z))
               +(p5(),p1()) -> +(p1(),p5())
               +(p10(),p1()) -> +(p1(),p10())
               +(p2(),p1()) -> +(p1(),p2())
               +(p5(),p5()) -> p10()
               +(p5(),+(p5(),x)) -> +(p10(),x)
               +(p1(),p1()) -> p2()
               +(p1(),+(p1(),x)) -> +(p2(),x)
               +(p1(),+(p2(),p2())) -> p5()
               +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
               +(p2(),+(p2(),p2())) -> +(p1(),p5())
               +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
             Matrix Interpretation Processor:
              dimension: 2
              max_matrix:
               [1 1]
               [0 1]
               interpretation:
                        [1]
                [p10] = [1],
                
                       [1]
                [p5] = [0],
                
                       [1]
                [p2] = [0],
                
                              [1 1]          [0]
                [+](x0, x1) = [0 1]x0 + x1 + [1],
                
                       [1]
                [p1] = [0]
               orientation:
                                        [2]        [2]                    
                +(p2(),+(p1(),x)) = x + [2] >= x + [2] = +(p1(),+(p2(),x))
                
                                        [2]        [2]                    
                +(p5(),+(p1(),x)) = x + [2] >= x + [2] = +(p1(),+(p5(),x))
                
                               [2]    [2]               
                +(p5(),p2()) = [1] >= [1] = +(p2(),p5())
                
                                        [2]        [2]                    
                +(p5(),+(p2(),x)) = x + [2] >= x + [2] = +(p2(),+(p5(),x))
                
                                         [3]        [3]                     
                +(p10(),+(p1(),x)) = x + [3] >= x + [3] = +(p1(),+(p10(),x))
                
                                [3]    [2]                
                +(p10(),p2()) = [2] >= [2] = +(p2(),p10())
                
                                         [3]        [3]                     
                +(p10(),+(p2(),x)) = x + [3] >= x + [3] = +(p2(),+(p10(),x))
                
                                [3]    [2]                
                +(p10(),p5()) = [2] >= [2] = +(p5(),p10())
                
                                         [3]        [3]                     
                +(p10(),+(p5(),x)) = x + [3] >= x + [3] = +(p5(),+(p10(),x))
                
                              [1 2]    [1 1]        [1]    [1 1]    [1 1]        [0]              
                +(+(x,y),z) = [0 1]x + [0 1]y + z + [2] >= [0 1]x + [0 1]y + z + [2] = +(x,+(y,z))
                
                               [2]    [2]               
                +(p5(),p1()) = [1] >= [1] = +(p1(),p5())
                
                                [3]    [2]                
                +(p10(),p1()) = [2] >= [2] = +(p1(),p10())
                
                               [2]    [2]               
                +(p2(),p1()) = [1] >= [1] = +(p1(),p2())
                
                               [2]    [1]        
                +(p5(),p5()) = [1] >= [1] = p10()
                
                                        [2]        [2]             
                +(p5(),+(p5(),x)) = x + [2] >= x + [2] = +(p10(),x)
                
                               [2]    [1]       
                +(p1(),p1()) = [1] >= [0] = p2()
                
                                        [2]        [1]            
                +(p1(),+(p1(),x)) = x + [2] >= x + [1] = +(p2(),x)
                
                                       [3]    [1]       
                +(p1(),+(p2(),p2())) = [2] >= [0] = p5()
                
                                                [3]        [1]            
                +(p1(),+(p2(),+(p2(),x))) = x + [3] >= x + [1] = +(p5(),x)
                
                                       [3]    [2]               
                +(p2(),+(p2(),p2())) = [2] >= [1] = +(p1(),p5())
                
                                                [3]        [2]                    
                +(p2(),+(p2(),+(p2(),x))) = x + [3] >= x + [2] = +(p1(),+(p5(),x))
               problem:
                strict:
                 +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                 +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                 +(p5(),p2()) -> +(p2(),p5())
                 +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                 +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                 +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                 +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                weak:
                 +(p10(),p2()) -> +(p2(),p10())
                 +(p10(),p5()) -> +(p5(),p10())
                 +(+(x,y),z) -> +(x,+(y,z))
                 +(p5(),p1()) -> +(p1(),p5())
                 +(p10(),p1()) -> +(p1(),p10())
                 +(p2(),p1()) -> +(p1(),p2())
                 +(p5(),p5()) -> p10()
                 +(p5(),+(p5(),x)) -> +(p10(),x)
                 +(p1(),p1()) -> p2()
                 +(p1(),+(p1(),x)) -> +(p2(),x)
                 +(p1(),+(p2(),p2())) -> p5()
                 +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                 +(p2(),+(p2(),p2())) -> +(p1(),p5())
                 +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
               Matrix Interpretation Processor:
                dimension: 3
                max_matrix:
                 [1 1 1]
                 [0 1 0]
                 [0 0 0]
                 interpretation:
                          [0]
                  [p10] = [0]
                          [0],
                  
                         [0]
                  [p5] = [0]
                         [0],
                  
                         [0]
                  [p2] = [0]
                         [1],
                  
                                [1 1 0]     [1 0 1]     [0]
                  [+](x0, x1) = [0 1 0]x0 + [0 1 0]x1 + [1]
                                [0 0 0]     [0 0 0]     [1],
                  
                         [1]
                  [p1] = [0]
                         [1]
                 orientation:
                                      [1 0 1]    [2]    [1 0 1]    [2]                    
                  +(p2(),+(p1(),x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = +(p1(),+(p2(),x))
                                      [0 0 0]    [1]    [0 0 0]    [1]                    
                  
                                      [1 0 1]    [2]    [1 0 1]    [2]                    
                  +(p5(),+(p1(),x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = +(p1(),+(p5(),x))
                                      [0 0 0]    [1]    [0 0 0]    [1]                    
                  
                                 [1]    [0]               
                  +(p5(),p2()) = [1] >= [1] = +(p2(),p5())
                                 [1]    [1]               
                  
                                      [1 0 1]    [1]    [1 0 1]    [1]                    
                  +(p5(),+(p2(),x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = +(p2(),+(p5(),x))
                                      [0 0 0]    [1]    [0 0 0]    [1]                    
                  
                                       [1 0 1]    [2]    [1 0 1]    [2]                     
                  +(p10(),+(p1(),x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = +(p1(),+(p10(),x))
                                       [0 0 0]    [1]    [0 0 0]    [1]                     
                  
                                       [1 0 1]    [1]    [1 0 1]    [1]                     
                  +(p10(),+(p2(),x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = +(p2(),+(p10(),x))
                                       [0 0 0]    [1]    [0 0 0]    [1]                     
                  
                                       [1 0 1]    [1]    [1 0 1]    [1]                     
                  +(p10(),+(p5(),x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = +(p5(),+(p10(),x))
                                       [0 0 0]    [1]    [0 0 0]    [1]                     
                  
                                  [1]    [0]                
                  +(p10(),p2()) = [1] >= [1] = +(p2(),p10())
                                  [1]    [1]                
                  
                                  [0]    [0]                
                  +(p10(),p5()) = [1] >= [1] = +(p5(),p10())
                                  [1]    [1]                
                  
                                [1 2 0]    [1 1 1]    [1 0 1]    [1]    [1 1 0]    [1 1 0]    [1 0 1]    [1]              
                  +(+(x,y),z) = [0 1 0]x + [0 1 0]y + [0 1 0]z + [2] >= [0 1 0]x + [0 1 0]y + [0 1 0]z + [2] = +(x,+(y,z))
                                [0 0 0]    [0 0 0]    [0 0 0]    [1]    [0 0 0]    [0 0 0]    [0 0 0]    [1]              
                  
                                 [2]    [1]               
                  +(p5(),p1()) = [1] >= [1] = +(p1(),p5())
                                 [1]    [1]               
                  
                                  [2]    [1]                
                  +(p10(),p1()) = [1] >= [1] = +(p1(),p10())
                                  [1]    [1]                
                  
                                 [2]    [2]               
                  +(p2(),p1()) = [1] >= [1] = +(p1(),p2())
                                 [1]    [1]               
                  
                                 [0]    [0]        
                  +(p5(),p5()) = [1] >= [0] = p10()
                                 [1]    [0]        
                  
                                      [1 0 1]    [1]    [1 0 1]    [0]             
                  +(p5(),+(p5(),x)) = [0 1 0]x + [2] >= [0 1 0]x + [1] = +(p10(),x)
                                      [0 0 0]    [1]    [0 0 0]    [1]             
                  
                                 [3]    [0]       
                  +(p1(),p1()) = [1] >= [0] = p2()
                                 [1]    [1]       
                  
                                      [1 0 1]    [3]    [1 0 1]    [0]            
                  +(p1(),+(p1(),x)) = [0 1 0]x + [2] >= [0 1 0]x + [1] = +(p2(),x)
                                      [0 0 0]    [1]    [0 0 0]    [1]            
                  
                                         [3]    [0]       
                  +(p1(),+(p2(),p2())) = [2] >= [0] = p5()
                                         [1]    [0]       
                  
                                              [1 0 1]    [3]    [1 0 1]    [0]            
                  +(p1(),+(p2(),+(p2(),x))) = [0 1 0]x + [3] >= [0 1 0]x + [1] = +(p5(),x)
                                              [0 0 0]    [1]    [0 0 0]    [1]            
                  
                                         [2]    [1]               
                  +(p2(),+(p2(),p2())) = [2] >= [1] = +(p1(),p5())
                                         [1]    [1]               
                  
                                              [1 0 1]    [2]    [1 0 1]    [2]                    
                  +(p2(),+(p2(),+(p2(),x))) = [0 1 0]x + [3] >= [0 1 0]x + [2] = +(p1(),+(p5(),x))
                                              [0 0 0]    [1]    [0 0 0]    [1]                    
                 problem:
                  strict:
                   +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                   +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                   +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                   +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                   +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                   +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                  weak:
                   +(p5(),p2()) -> +(p2(),p5())
                   +(p10(),p2()) -> +(p2(),p10())
                   +(p10(),p5()) -> +(p5(),p10())
                   +(+(x,y),z) -> +(x,+(y,z))
                   +(p5(),p1()) -> +(p1(),p5())
                   +(p10(),p1()) -> +(p1(),p10())
                   +(p2(),p1()) -> +(p1(),p2())
                   +(p5(),p5()) -> p10()
                   +(p5(),+(p5(),x)) -> +(p10(),x)
                   +(p1(),p1()) -> p2()
                   +(p1(),+(p1(),x)) -> +(p2(),x)
                   +(p1(),+(p2(),p2())) -> p5()
                   +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                   +(p2(),+(p2(),p2())) -> +(p1(),p5())
                   +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
                 Open