YES

Problem:
 s(p(x)) -> x
 p(s(x)) -> x
 +(x,s(y)) -> s(+(x,y))
 +(x,p(y)) -> p(+(x,y))
 -(x,s(y)) -> p(-(x,y))
 -(x,p(y)) -> s(-(x,y))
 -(p(x),y) -> p(-(x,y))
 -(s(x),y) -> s(-(x,y))

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  +(x251,p(x250)) -> p(+(x251,x250))
  s(p(x254)) -> x254
  -(x256,p(x255)) -> s(-(x256,x255))
  p(s(x259)) -> x259
  -(p(x261),x260) -> p(-(x261,x260))
  +(x266,s(x265)) -> s(+(x266,x265))
  -(x271,s(x270)) -> p(-(x271,x270))
  -(s(x276),x275) -> s(-(x276,x275))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [s](x0) = x0 + 1,
    
    [-](x0, x1) = x0 + x1,
    
    [p](x0) = x0 + 1,
    
    [+](x0, x1) = 4x0 + 2x1 + 1
   orientation:
    +(x251,p(x250)) = 2x250 + 4x251 + 3 >= 2x250 + 4x251 + 2 = p(+(x251,x250))
    
    s(p(x254)) = x254 + 2 >= x254 = x254
    
    -(x256,p(x255)) = x255 + x256 + 1 >= x255 + x256 + 1 = s(-(x256,x255))
    
    p(s(x259)) = x259 + 2 >= x259 = x259
    
    -(p(x261),x260) = x260 + x261 + 1 >= x260 + x261 + 1 = p(-(x261,x260))
    
    +(x266,s(x265)) = 2x265 + 4x266 + 3 >= 2x265 + 4x266 + 2 = s(+(x266,x265))
    
    -(x271,s(x270)) = x270 + x271 + 1 >= x270 + x271 + 1 = p(-(x271,x270))
    
    -(s(x276),x275) = x275 + x276 + 1 >= x275 + x276 + 1 = s(-(x276,x275))
   problem:
    -(x256,p(x255)) -> s(-(x256,x255))
    -(p(x261),x260) -> p(-(x261,x260))
    -(x271,s(x270)) -> p(-(x271,x270))
    -(s(x276),x275) -> s(-(x276,x275))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [s](x0) = x0 + 1,
     
     [-](x0, x1) = 4x0 + x1,
     
     [p](x0) = x0 + 1
    orientation:
     -(x256,p(x255)) = x255 + 4x256 + 1 >= x255 + 4x256 + 1 = s(-(x256,x255))
     
     -(p(x261),x260) = x260 + 4x261 + 4 >= x260 + 4x261 + 1 = p(-(x261,x260))
     
     -(x271,s(x270)) = x270 + 4x271 + 1 >= x270 + 4x271 + 1 = p(-(x271,x270))
     
     -(s(x276),x275) = x275 + 4x276 + 4 >= x275 + 4x276 + 1 = s(-(x276,x275))
    problem:
     -(x256,p(x255)) -> s(-(x256,x255))
     -(x271,s(x270)) -> p(-(x271,x270))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [s](x0) = x0 + 1,
      
      [-](x0, x1) = x0 + 2x1,
      
      [p](x0) = x0 + 2
     orientation:
      -(x256,p(x255)) = 2x255 + x256 + 4 >= 2x255 + x256 + 1 = s(-(x256,x255))
      
      -(x271,s(x270)) = 2x270 + x271 + 2 >= 2x270 + x271 + 2 = p(-(x271,x270))
     problem:
      -(x271,s(x270)) -> p(-(x271,x270))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [s](x0) = x0 + 4,
       
       [-](x0, x1) = x0 + x1 + 5,
       
       [p](x0) = x0 + 3
      orientation:
       -(x271,s(x270)) = x270 + x271 + 9 >= x270 + x271 + 8 = p(-(x271,x270))
      problem:
       
      Qed