YES

Problem:
 s(p(x)) -> x
 p(s(x)) -> x
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 +(x,p(y)) -> p(+(x,y))
 +(0(),y) -> 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):
  +(x231,p(x230)) -> p(+(x231,x230))
  s(p(x234)) -> x234
  +(p(x236),x235) -> p(+(x236,x235))
  +(x241,s(x240)) -> s(+(x241,x240))
  p(s(x244)) -> x244
  +(s(x246),x245) -> s(+(x246,x245))
  +(x250,0()) -> x250
  +(0(),x252) -> x252
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [+](x0, x1) = x0 + 5x1 + 2,
    
    [0] = 1,
    
    [s](x0) = x0 + 4,
    
    [p](x0) = x0 + 1
   orientation:
    +(x231,p(x230)) = 5x230 + x231 + 7 >= 5x230 + x231 + 3 = p(+(x231,x230))
    
    s(p(x234)) = x234 + 5 >= x234 = x234
    
    +(p(x236),x235) = 5x235 + x236 + 3 >= 5x235 + x236 + 3 = p(+(x236,x235))
    
    +(x241,s(x240)) = 5x240 + x241 + 22 >= 5x240 + x241 + 6 = s(+(x241,x240))
    
    p(s(x244)) = x244 + 5 >= x244 = x244
    
    +(s(x246),x245) = 5x245 + x246 + 6 >= 5x245 + x246 + 6 = s(+(x246,x245))
    
    +(x250,0()) = x250 + 7 >= x250 = x250
    
    +(0(),x252) = 5x252 + 3 >= x252 = x252
   problem:
    +(p(x236),x235) -> p(+(x236,x235))
    +(s(x246),x245) -> s(+(x246,x245))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [+](x0, x1) = 4x0 + x1 + 2,
     
     [s](x0) = x0 + 2,
     
     [p](x0) = x0 + 4
    orientation:
     +(p(x236),x235) = x235 + 4x236 + 18 >= x235 + 4x236 + 6 = p(+(x236,x235))
     
     +(s(x246),x245) = x245 + 4x246 + 10 >= x245 + 4x246 + 4 = s(+(x246,x245))
    problem:
     
    Qed