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:
 RT 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
   interpretation:
    [p10] = 7,
    
    [p5] = 18,
    
    [p2] = 0,
    
    [+](x0, x1) = x0 + x1 + 3,
    
    [p1] = 2
   orientation:
    +(p1(),p1()) = 7 >= 0 = p2()
    
    +(p1(),+(p2(),p2())) = 8 >= 18 = p5()
    
    +(p5(),p5()) = 39 >= 7 = p10()
    
    +(+(x,y),z) = x + y + z + 6 >= x + y + z + 6 = +(x,+(y,z))
    
    +(p1(),+(p1(),x)) = x + 10 >= x + 3 = +(p2(),x)
    
    +(p1(),+(p2(),+(p2(),x))) = x + 11 >= x + 21 = +(p5(),x)
    
    +(p2(),p1()) = 5 >= 5 = +(p1(),p2())
    
    +(p2(),+(p1(),x)) = x + 8 >= x + 8 = +(p1(),+(p2(),x))
    
    +(p2(),+(p2(),p2())) = 6 >= 23 = +(p1(),p5())
    
    +(p2(),+(p2(),+(p2(),x))) = x + 9 >= x + 26 = +(p1(),+(p5(),x))
    
    +(p5(),p1()) = 23 >= 23 = +(p1(),p5())
    
    +(p5(),+(p1(),x)) = x + 26 >= x + 26 = +(p1(),+(p5(),x))
    
    +(p5(),p2()) = 21 >= 21 = +(p2(),p5())
    
    +(p5(),+(p2(),x)) = x + 24 >= x + 24 = +(p2(),+(p5(),x))
    
    +(p5(),+(p5(),x)) = x + 42 >= x + 10 = +(p10(),x)
    
    +(p10(),p1()) = 12 >= 12 = +(p1(),p10())
    
    +(p10(),+(p1(),x)) = x + 15 >= x + 15 = +(p1(),+(p10(),x))
    
    +(p10(),p2()) = 10 >= 10 = +(p2(),p10())
    
    +(p10(),+(p2(),x)) = x + 13 >= x + 13 = +(p2(),+(p10(),x))
    
    +(p10(),p5()) = 28 >= 28 = +(p5(),p10())
    
    +(p10(),+(p5(),x)) = x + 31 >= x + 31 = +(p5(),+(p10(),x))
   problem:
    strict:
     +(p1(),+(p2(),p2())) -> p5()
     +(+(x,y),z) -> +(x,+(y,z))
     +(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))
     +(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()
     +(p5(),p5()) -> p10()
     +(p1(),+(p1(),x)) -> +(p2(),x)
     +(p5(),+(p5(),x)) -> +(p10(),x)
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [p10] = 0,
     
     [p5] = 0,
     
     [p2] = 6,
     
     [+](x0, x1) = x0 + x1 + 1,
     
     [p1] = 8
    orientation:
     +(p1(),+(p2(),p2())) = 22 >= 0 = p5()
     
     +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z))
     
     +(p1(),+(p2(),+(p2(),x))) = x + 23 >= x + 1 = +(p5(),x)
     
     +(p2(),p1()) = 15 >= 15 = +(p1(),p2())
     
     +(p2(),+(p1(),x)) = x + 16 >= x + 16 = +(p1(),+(p2(),x))
     
     +(p2(),+(p2(),p2())) = 20 >= 9 = +(p1(),p5())
     
     +(p2(),+(p2(),+(p2(),x))) = x + 21 >= x + 10 = +(p1(),+(p5(),x))
     
     +(p5(),p1()) = 9 >= 9 = +(p1(),p5())
     
     +(p5(),+(p1(),x)) = x + 10 >= x + 10 = +(p1(),+(p5(),x))
     
     +(p5(),p2()) = 7 >= 7 = +(p2(),p5())
     
     +(p5(),+(p2(),x)) = x + 8 >= x + 8 = +(p2(),+(p5(),x))
     
     +(p10(),p1()) = 9 >= 9 = +(p1(),p10())
     
     +(p10(),+(p1(),x)) = x + 10 >= x + 10 = +(p1(),+(p10(),x))
     
     +(p10(),p2()) = 7 >= 7 = +(p2(),p10())
     
     +(p10(),+(p2(),x)) = x + 8 >= x + 8 = +(p2(),+(p10(),x))
     
     +(p10(),p5()) = 1 >= 1 = +(p5(),p10())
     
     +(p10(),+(p5(),x)) = x + 2 >= x + 2 = +(p5(),+(p10(),x))
     
     +(p1(),p1()) = 17 >= 6 = p2()
     
     +(p5(),p5()) = 1 >= 0 = p10()
     
     +(p1(),+(p1(),x)) = x + 18 >= x + 7 = +(p2(),x)
     
     +(p5(),+(p5(),x)) = x + 2 >= x + 1 = +(p10(),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:
      +(p1(),+(p2(),p2())) -> p5()
      +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
      +(p2(),+(p2(),p2())) -> +(p1(),p5())
      +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
      +(p1(),p1()) -> p2()
      +(p5(),p5()) -> p10()
      +(p1(),+(p1(),x)) -> +(p2(),x)
      +(p5(),+(p5(),x)) -> +(p10(),x)
    Matrix Interpretation Processor:
     dimension: 2
     interpretation:
              [0]
      [p10] = [0],
      
             [0]
      [p5] = [0],
      
             [0]
      [p2] = [0],
      
                    [1 0]     [1 8]  
      [+](x0, x1) = [0 0]x0 + [0 0]x1,
      
             [0]
      [p1] = [1]
     orientation:
                    [1 0]    [1 8]    [1 8]     [1 0]    [1 0]    [1 8]               
      +(+(x,y),z) = [0 0]x + [0 0]y + [0 0]z >= [0 0]x + [0 0]y + [0 0]z = +(x,+(y,z))
      
                     [8]    [0]               
      +(p2(),p1()) = [0] >= [0] = +(p1(),p2())
      
                          [1 8]     [1 8]                     
      +(p2(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p1(),+(p2(),x))
      
                     [8]    [0]               
      +(p5(),p1()) = [0] >= [0] = +(p1(),p5())
      
                          [1 8]     [1 8]                     
      +(p5(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p1(),+(p5(),x))
      
                     [0]    [0]               
      +(p5(),p2()) = [0] >= [0] = +(p2(),p5())
      
                          [1 8]     [1 8]                     
      +(p5(),+(p2(),x)) = [0 0]x >= [0 0]x = +(p2(),+(p5(),x))
      
                      [8]    [0]                
      +(p10(),p1()) = [0] >= [0] = +(p1(),p10())
      
                           [1 8]     [1 8]                      
      +(p10(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p1(),+(p10(),x))
      
                      [0]    [0]                
      +(p10(),p2()) = [0] >= [0] = +(p2(),p10())
      
                           [1 8]     [1 8]                      
      +(p10(),+(p2(),x)) = [0 0]x >= [0 0]x = +(p2(),+(p10(),x))
      
                      [0]    [0]                
      +(p10(),p5()) = [0] >= [0] = +(p5(),p10())
      
                           [1 8]     [1 8]                      
      +(p10(),+(p5(),x)) = [0 0]x >= [0 0]x = +(p5(),+(p10(),x))
      
                             [0]    [0]       
      +(p1(),+(p2(),p2())) = [0] >= [0] = p5()
      
                                  [1 8]     [1 8]             
      +(p1(),+(p2(),+(p2(),x))) = [0 0]x >= [0 0]x = +(p5(),x)
      
                             [0]    [0]               
      +(p2(),+(p2(),p2())) = [0] >= [0] = +(p1(),p5())
      
                                  [1 8]     [1 8]                     
      +(p2(),+(p2(),+(p2(),x))) = [0 0]x >= [0 0]x = +(p1(),+(p5(),x))
      
                     [8]    [0]       
      +(p1(),p1()) = [0] >= [0] = p2()
      
                     [0]    [0]        
      +(p5(),p5()) = [0] >= [0] = p10()
      
                          [1 8]     [1 8]             
      +(p1(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p2(),x)
      
                          [1 8]     [1 8]              
      +(p5(),+(p5(),x)) = [0 0]x >= [0 0]x = +(p10(),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:
       +(p2(),p1()) -> +(p1(),p2())
       +(p5(),p1()) -> +(p1(),p5())
       +(p10(),p1()) -> +(p1(),p10())
       +(p1(),+(p2(),p2())) -> p5()
       +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
       +(p2(),+(p2(),p2())) -> +(p1(),p5())
       +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
       +(p1(),p1()) -> p2()
       +(p5(),p5()) -> p10()
       +(p1(),+(p1(),x)) -> +(p2(),x)
       +(p5(),+(p5(),x)) -> +(p10(),x)
     Matrix Interpretation Processor:
      dimension: 2
      interpretation:
               [0]
       [p10] = [0],
       
              [0]
       [p5] = [0],
       
              [0]
       [p2] = [0],
       
                     [1  12]          [0]
       [+](x0, x1) = [0  1 ]x0 + x1 + [1],
       
              [0]
       [p1] = [0]
      orientation:
                     [1  24]    [1  12]        [12]    [1  12]    [1  12]        [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]               
       +(p2(),p1()) = [1] >= [1] = +(p1(),p2())
       
                      [0]    [0]               
       +(p5(),p1()) = [1] >= [1] = +(p1(),p5())
       
                       [0]    [0]                
       +(p10(),p1()) = [1] >= [1] = +(p1(),p10())
       
                              [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))
       
                      [0]    [0]       
       +(p1(),p1()) = [1] >= [0] = p2()
       
                      [0]    [0]        
       +(p5(),p5()) = [1] >= [0] = p10()
       
                               [0]        [0]            
       +(p1(),+(p1(),x)) = x + [2] >= x + [1] = +(p2(),x)
       
                               [0]        [0]             
       +(p5(),+(p5(),x)) = x + [2] >= x + [1] = +(p10(),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))
        +(p2(),p1()) -> +(p1(),p2())
        +(p5(),p1()) -> +(p1(),p5())
        +(p10(),p1()) -> +(p1(),p10())
        +(p1(),+(p2(),p2())) -> p5()
        +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
        +(p2(),+(p2(),p2())) -> +(p1(),p5())
        +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
        +(p1(),p1()) -> p2()
        +(p5(),p5()) -> p10()
        +(p1(),+(p1(),x)) -> +(p2(),x)
        +(p5(),+(p5(),x)) -> +(p10(),x)
      Matrix Interpretation Processor:
       dimension: 2
       interpretation:
                [0]
        [p10] = [2],
        
               [0]
        [p5] = [1],
        
               [1]
        [p2] = [0],
        
                      [1 1]          [0]
        [+](x0, x1) = [0 1]x0 + x1 + [8],
        
               [1]
        [p1] = [0]
       orientation:
                                [2 ]        [2 ]                    
        +(p2(),+(p1(),x)) = x + [16] >= x + [16] = +(p1(),+(p2(),x))
        
                                [2 ]        [2 ]                    
        +(p5(),+(p1(),x)) = x + [17] >= x + [17] = +(p1(),+(p5(),x))
        
                       [2]    [1]               
        +(p5(),p2()) = [9] >= [9] = +(p2(),p5())
        
                                [2 ]        [2 ]                    
        +(p5(),+(p2(),x)) = x + [17] >= x + [17] = +(p2(),+(p5(),x))
        
                                 [3 ]        [3 ]                     
        +(p10(),+(p1(),x)) = x + [18] >= x + [18] = +(p1(),+(p10(),x))
        
                        [3 ]    [1 ]                
        +(p10(),p2()) = [10] >= [10] = +(p2(),p10())
        
                                 [3 ]        [3 ]                     
        +(p10(),+(p2(),x)) = x + [18] >= x + [18] = +(p2(),+(p10(),x))
        
                        [2 ]    [1 ]                
        +(p10(),p5()) = [11] >= [11] = +(p5(),p10())
        
                                 [3 ]        [3 ]                     
        +(p10(),+(p5(),x)) = x + [19] >= x + [19] = +(p5(),+(p10(),x))
        
                      [1 2]    [1 1]        [8 ]    [1 1]    [1 1]        [0 ]              
        +(+(x,y),z) = [0 1]x + [0 1]y + z + [16] >= [0 1]x + [0 1]y + z + [16] = +(x,+(y,z))
        
                       [2]    [2]               
        +(p2(),p1()) = [8] >= [8] = +(p1(),p2())
        
                       [2]    [1]               
        +(p5(),p1()) = [9] >= [9] = +(p1(),p5())
        
                        [3 ]    [1 ]                
        +(p10(),p1()) = [10] >= [10] = +(p1(),p10())
        
                               [3 ]    [0]       
        +(p1(),+(p2(),p2())) = [16] >= [1] = p5()
        
                                        [3 ]        [1]            
        +(p1(),+(p2(),+(p2(),x))) = x + [24] >= x + [9] = +(p5(),x)
        
                               [3 ]    [1]               
        +(p2(),+(p2(),p2())) = [16] >= [9] = +(p1(),p5())
        
                                        [3 ]        [2 ]                    
        +(p2(),+(p2(),+(p2(),x))) = x + [24] >= x + [17] = +(p1(),+(p5(),x))
        
                       [2]    [1]       
        +(p1(),p1()) = [8] >= [0] = p2()
        
                       [1 ]    [0]        
        +(p5(),p5()) = [10] >= [2] = p10()
        
                                [2 ]        [1]            
        +(p1(),+(p1(),x)) = x + [16] >= x + [8] = +(p2(),x)
        
                                [2 ]        [2 ]             
        +(p5(),+(p5(),x)) = x + [18] >= x + [10] = +(p10(),x)
       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))
         +(p2(),p1()) -> +(p1(),p2())
         +(p5(),p1()) -> +(p1(),p5())
         +(p10(),p1()) -> +(p1(),p10())
         +(p1(),+(p2(),p2())) -> p5()
         +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
         +(p2(),+(p2(),p2())) -> +(p1(),p5())
         +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
         +(p1(),p1()) -> p2()
         +(p5(),p5()) -> p10()
         +(p1(),+(p1(),x)) -> +(p2(),x)
         +(p5(),+(p5(),x)) -> +(p10(),x)
       Open