YES

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:
 Matrix Interpretation Processor: dim=3
  
  interpretation:
           [0]
   [p10] = [0]
           [0],
   
          [0]
   [p5] = [0]
          [0],
   
          [0]
   [p2] = [0]
          [0],
   
                 [1 0 0]     [1 1 0]  
   [+](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                 [0 0 1]     [1 1 0]  ,
   
          [0]
   [p1] = [1]
          [0]
  orientation:
                  [1]    [0]       
   +(p1(),p1()) = [0] >= [0] = p2()
                  [1]    [0]       
   
                          [0]    [0]       
   +(p1(),+(p2(),p2())) = [0] >= [0] = p5()
                          [0]    [0]       
   
                  [0]    [0]        
   +(p5(),p5()) = [0] >= [0] = p10()
                  [0]    [0]        
   
                 [1 0 0]    [1 1 0]    [1 1 0]     [1 0 0]    [1 0 0]    [1 1 0]               
   +(+(x,y),z) = [0 0 0]x + [0 0 0]y + [0 0 0]z >= [0 0 0]x + [0 0 0]y + [0 0 0]z = +(x,+(y,z))
                 [0 0 1]    [1 1 0]    [1 1 0]     [0 0 1]    [1 0 0]    [1 1 0]               
   
                       [1 1 0]     [1 1 0]             
   +(p1(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),x)
                       [1 1 0]     [1 1 0]             
   
                               [1 1 0]     [1 1 0]             
   +(p1(),+(p2(),+(p2(),x))) = [0 0 0]x >= [0 0 0]x = +(p5(),x)
                               [1 1 0]     [1 1 0]             
   
                  [1]    [0]               
   +(p2(),p1()) = [0] >= [0] = +(p1(),p2())
                  [1]    [0]               
   
                       [1 1 0]     [1 1 0]                     
   +(p2(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p2(),x))
                       [1 1 0]     [1 1 0]                     
   
                          [0]    [0]               
   +(p2(),+(p2(),p2())) = [0] >= [0] = +(p1(),p5())
                          [0]    [0]               
   
                               [1 1 0]     [1 1 0]                     
   +(p2(),+(p2(),+(p2(),x))) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p5(),x))
                               [1 1 0]     [1 1 0]                     
   
                  [1]    [0]               
   +(p5(),p1()) = [0] >= [0] = +(p1(),p5())
                  [1]    [0]               
   
                       [1 1 0]     [1 1 0]                     
   +(p5(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p5(),x))
                       [1 1 0]     [1 1 0]                     
   
                  [0]    [0]               
   +(p5(),p2()) = [0] >= [0] = +(p2(),p5())
                  [0]    [0]               
   
                       [1 1 0]     [1 1 0]                     
   +(p5(),+(p2(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),+(p5(),x))
                       [1 1 0]     [1 1 0]                     
   
                       [1 1 0]     [1 1 0]              
   +(p5(),+(p5(),x)) = [0 0 0]x >= [0 0 0]x = +(p10(),x)
                       [1 1 0]     [1 1 0]              
   
                   [1]    [0]                
   +(p10(),p1()) = [0] >= [0] = +(p1(),p10())
                   [1]    [0]                
   
                        [1 1 0]     [1 1 0]                      
   +(p10(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p10(),x))
                        [1 1 0]     [1 1 0]                      
   
                   [0]    [0]                
   +(p10(),p2()) = [0] >= [0] = +(p2(),p10())
                   [0]    [0]                
   
                        [1 1 0]     [1 1 0]                      
   +(p10(),+(p2(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),+(p10(),x))
                        [1 1 0]     [1 1 0]                      
   
                   [0]    [0]                
   +(p10(),p5()) = [0] >= [0] = +(p5(),p10())
                   [0]    [0]                
   
                        [1 1 0]     [1 1 0]                      
   +(p10(),+(p5(),x)) = [0 0 0]x >= [0 0 0]x = +(p5(),+(p10(),x))
                        [1 1 0]     [1 1 0]                      
  problem:
   +(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(),x)) -> +(p1(),+(p2(),x))
   +(p2(),+(p2(),p2())) -> +(p1(),p5())
   +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
   +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
   +(p5(),p2()) -> +(p2(),p5())
   +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
   +(p5(),+(p5(),x)) -> +(p10(),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))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
            [0]
    [p10] = [0]
            [0],
    
           [0]
    [p5] = [0]
           [0],
    
           [0]
    [p2] = [1]
           [0],
    
                  [1 0 0]     [1 1 0]  
    [+](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                  [0 0 0]     [0 0 0]  ,
    
           [0]
    [p1] = [0]
           [0]
   orientation:
                           [1]    [0]       
    +(p1(),+(p2(),p2())) = [0] >= [0] = p5()
                           [0]    [0]       
    
                   [0]    [0]        
    +(p5(),p5()) = [0] >= [0] = p10()
                   [0]    [0]        
    
                  [1 0 0]    [1 1 0]    [1 1 0]     [1 0 0]    [1 0 0]    [1 1 0]               
    +(+(x,y),z) = [0 0 0]x + [0 0 0]y + [0 0 0]z >= [0 0 0]x + [0 0 0]y + [0 0 0]z = +(x,+(y,z))
                  [0 0 0]    [0 0 0]    [0 0 0]     [0 0 0]    [0 0 0]    [0 0 0]               
    
                        [1 1 0]     [1 1 0]             
    +(p1(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),x)
                        [0 0 0]     [0 0 0]             
    
                                [1 1 0]     [1 1 0]             
    +(p1(),+(p2(),+(p2(),x))) = [0 0 0]x >= [0 0 0]x = +(p5(),x)
                                [0 0 0]     [0 0 0]             
    
                        [1 1 0]     [1 1 0]                     
    +(p2(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p2(),x))
                        [0 0 0]     [0 0 0]                     
    
                           [1]    [0]               
    +(p2(),+(p2(),p2())) = [0] >= [0] = +(p1(),p5())
                           [0]    [0]               
    
                                [1 1 0]     [1 1 0]                     
    +(p2(),+(p2(),+(p2(),x))) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p5(),x))
                                [0 0 0]     [0 0 0]                     
    
                        [1 1 0]     [1 1 0]                     
    +(p5(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p5(),x))
                        [0 0 0]     [0 0 0]                     
    
                   [1]    [0]               
    +(p5(),p2()) = [0] >= [0] = +(p2(),p5())
                   [0]    [0]               
    
                        [1 1 0]     [1 1 0]                     
    +(p5(),+(p2(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),+(p5(),x))
                        [0 0 0]     [0 0 0]                     
    
                        [1 1 0]     [1 1 0]              
    +(p5(),+(p5(),x)) = [0 0 0]x >= [0 0 0]x = +(p10(),x)
                        [0 0 0]     [0 0 0]              
    
                         [1 1 0]     [1 1 0]                      
    +(p10(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p10(),x))
                         [0 0 0]     [0 0 0]                      
    
                    [1]    [0]                
    +(p10(),p2()) = [0] >= [0] = +(p2(),p10())
                    [0]    [0]                
    
                         [1 1 0]     [1 1 0]                      
    +(p10(),+(p2(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),+(p10(),x))
                         [0 0 0]     [0 0 0]                      
    
                    [0]    [0]                
    +(p10(),p5()) = [0] >= [0] = +(p5(),p10())
                    [0]    [0]                
    
                         [1 1 0]     [1 1 0]                      
    +(p10(),+(p5(),x)) = [0 0 0]x >= [0 0 0]x = +(p5(),+(p10(),x))
                         [0 0 0]     [0 0 0]                      
   problem:
    +(p5(),p5()) -> p10()
    +(+(x,y),z) -> +(x,+(y,z))
    +(p1(),+(p1(),x)) -> +(p2(),x)
    +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
    +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
    +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
    +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
    +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
    +(p5(),+(p5(),x)) -> +(p10(),x)
    +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
    +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
    +(p10(),p5()) -> +(p5(),p10())
    +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
   Matrix Interpretation Processor: dim=3
    
    interpretation:
             [0]
     [p10] = [0]
             [0],
     
            [0]
     [p5] = [1]
            [0],
     
            [0]
     [p2] = [0]
            [0],
     
                   [1 0 0]     [1 1 0]  
     [+](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                   [0 0 1]     [1 1 0]  ,
     
            [0]
     [p1] = [0]
            [0]
    orientation:
                    [1]    [0]        
     +(p5(),p5()) = [0] >= [0] = p10()
                    [1]    [0]        
     
                   [1 0 0]    [1 1 0]    [1 1 0]     [1 0 0]    [1 0 0]    [1 1 0]               
     +(+(x,y),z) = [0 0 0]x + [0 0 0]y + [0 0 0]z >= [0 0 0]x + [0 0 0]y + [0 0 0]z = +(x,+(y,z))
                   [0 0 1]    [1 1 0]    [1 1 0]     [0 0 1]    [1 0 0]    [1 1 0]               
     
                         [1 1 0]     [1 1 0]             
     +(p1(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),x)
                         [1 1 0]     [1 1 0]             
     
                                 [1 1 0]     [1 1 0]             
     +(p1(),+(p2(),+(p2(),x))) = [0 0 0]x >= [0 0 0]x = +(p5(),x)
                                 [1 1 0]     [1 1 0]             
     
                         [1 1 0]     [1 1 0]                     
     +(p2(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p2(),x))
                         [1 1 0]     [1 1 0]                     
     
                                 [1 1 0]     [1 1 0]                     
     +(p2(),+(p2(),+(p2(),x))) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p5(),x))
                                 [1 1 0]     [1 1 0]                     
     
                         [1 1 0]     [1 1 0]                     
     +(p5(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p5(),x))
                         [1 1 0]     [1 1 0]                     
     
                         [1 1 0]     [1 1 0]                     
     +(p5(),+(p2(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),+(p5(),x))
                         [1 1 0]     [1 1 0]                     
     
                         [1 1 0]     [1 1 0]              
     +(p5(),+(p5(),x)) = [0 0 0]x >= [0 0 0]x = +(p10(),x)
                         [1 1 0]     [1 1 0]              
     
                          [1 1 0]     [1 1 0]                      
     +(p10(),+(p1(),x)) = [0 0 0]x >= [0 0 0]x = +(p1(),+(p10(),x))
                          [1 1 0]     [1 1 0]                      
     
                          [1 1 0]     [1 1 0]                      
     +(p10(),+(p2(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),+(p10(),x))
                          [1 1 0]     [1 1 0]                      
     
                     [1]    [0]                
     +(p10(),p5()) = [0] >= [0] = +(p5(),p10())
                     [1]    [0]                
     
                          [1 1 0]     [1 1 0]                      
     +(p10(),+(p5(),x)) = [0 0 0]x >= [0 0 0]x = +(p5(),+(p10(),x))
                          [1 1 0]     [1 1 0]                      
    problem:
     +(+(x,y),z) -> +(x,+(y,z))
     +(p1(),+(p1(),x)) -> +(p2(),x)
     +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
     +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
     +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
     +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
     +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
     +(p5(),+(p5(),x)) -> +(p10(),x)
     +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
     +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
     +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [p10] = 0,
      
      [p5] = 0,
      
      [p2] = 0,
      
      [+](x0, x1) = 5x0 + x1 + 1,
      
      [p1] = 0
     orientation:
      +(+(x,y),z) = 25x + 5y + z + 6 >= 5x + 5y + z + 2 = +(x,+(y,z))
      
      +(p1(),+(p1(),x)) = x + 2 >= x + 1 = +(p2(),x)
      
      +(p1(),+(p2(),+(p2(),x))) = x + 3 >= x + 1 = +(p5(),x)
      
      +(p2(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p2(),x))
      
      +(p2(),+(p2(),+(p2(),x))) = x + 3 >= x + 2 = +(p1(),+(p5(),x))
      
      +(p5(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p5(),x))
      
      +(p5(),+(p2(),x)) = x + 2 >= x + 2 = +(p2(),+(p5(),x))
      
      +(p5(),+(p5(),x)) = x + 2 >= x + 1 = +(p10(),x)
      
      +(p10(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p10(),x))
      
      +(p10(),+(p2(),x)) = x + 2 >= x + 2 = +(p2(),+(p10(),x))
      
      +(p10(),+(p5(),x)) = x + 2 >= x + 2 = +(p5(),+(p10(),x))
     problem:
      +(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))
     Matrix Interpretation Processor: dim=3
      
      interpretation:
               [0]
       [p10] = [0]
               [0],
       
              [0]
       [p5] = [0]
              [0],
       
              [0]
       [p2] = [0]
              [0],
       
                     [1 0 0]     [1 0 1]  
       [+](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                     [0 0 1]     [0 0 1]  ,
       
              [0]
       [p1] = [0]
              [1]
      orientation:
                           [1 0 2]    [1]    [1 0 2]    [0]                    
       +(p2(),+(p1(),x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = +(p1(),+(p2(),x))
                           [0 0 1]    [1]    [0 0 1]    [1]                    
       
                           [1 0 2]    [1]    [1 0 2]    [0]                    
       +(p5(),+(p1(),x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = +(p1(),+(p5(),x))
                           [0 0 1]    [1]    [0 0 1]    [1]                    
       
                           [1 0 2]     [1 0 2]                     
       +(p5(),+(p2(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),+(p5(),x))
                           [0 0 1]     [0 0 1]                     
       
                            [1 0 2]    [1]    [1 0 2]    [0]                     
       +(p10(),+(p1(),x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = +(p1(),+(p10(),x))
                            [0 0 1]    [1]    [0 0 1]    [1]                     
       
                            [1 0 2]     [1 0 2]                      
       +(p10(),+(p2(),x)) = [0 0 0]x >= [0 0 0]x = +(p2(),+(p10(),x))
                            [0 0 1]     [0 0 1]                      
       
                            [1 0 2]     [1 0 2]                      
       +(p10(),+(p5(),x)) = [0 0 0]x >= [0 0 0]x = +(p5(),+(p10(),x))
                            [0 0 1]     [0 0 1]                      
      problem:
       +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
       +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
       +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
      Matrix Interpretation Processor: dim=3
       
       interpretation:
                [0]
        [p10] = [0]
                [0],
        
               [0]
        [p5] = [0]
               [0],
        
               [0]
        [p2] = [0]
               [1],
        
                      [1 0 0]     [1 0 1]  
        [+](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                      [0 0 1]     [0 0 1]  
       orientation:
                            [1 0 2]    [1]    [1 0 2]    [0]                    
        +(p5(),+(p2(),x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = +(p2(),+(p5(),x))
                            [0 0 1]    [1]    [0 0 1]    [1]                    
        
                             [1 0 2]    [1]    [1 0 2]    [0]                     
        +(p10(),+(p2(),x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = +(p2(),+(p10(),x))
                             [0 0 1]    [1]    [0 0 1]    [1]                     
        
                             [1 0 2]     [1 0 2]                      
        +(p10(),+(p5(),x)) = [0 0 0]x >= [0 0 0]x = +(p5(),+(p10(),x))
                             [0 0 1]     [0 0 1]                      
       problem:
        +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
       KBO Processor:
        weight function:
         w0 = 1
         w(p10) = w(p5) = 1
         w(+) = 0
        precedence:
         p10 > p5 ~ +
        problem:
         
        Qed