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:
    [s](x0) = x0 + 3,
    
    [+](x0, x1) = x0 + x1,
    
    [p](x0) = x0 + 2,
    
    [0] = 0
   orientation:
    +(x231,p(x230)) = x230 + x231 + 2 >= x230 + x231 + 2 = p(+(x231,x230))
    
    s(p(x234)) = x234 + 5 >= x234 = x234
    
    +(p(x236),x235) = x235 + x236 + 2 >= x235 + x236 + 2 = p(+(x236,x235))
    
    +(x241,s(x240)) = x240 + x241 + 3 >= x240 + x241 + 3 = s(+(x241,x240))
    
    p(s(x244)) = x244 + 5 >= x244 = x244
    
    +(s(x246),x245) = x245 + x246 + 3 >= x245 + x246 + 3 = s(+(x246,x245))
    
    +(x250,0()) = x250 >= x250 = x250
    
    +(0(),x252) = x252 >= x252 = x252
   problem:
    +(x231,p(x230)) -> p(+(x231,x230))
    +(p(x236),x235) -> p(+(x236,x235))
    +(x241,s(x240)) -> s(+(x241,x240))
    +(s(x246),x245) -> s(+(x246,x245))
    +(x250,0()) -> x250
    +(0(),x252) -> x252
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [s](x0) = x0,
     
     [+](x0, x1) = x0 + x1,
     
     [p](x0) = x0,
     
     [0] = 2
    orientation:
     +(x231,p(x230)) = x230 + x231 >= x230 + x231 = p(+(x231,x230))
     
     +(p(x236),x235) = x235 + x236 >= x235 + x236 = p(+(x236,x235))
     
     +(x241,s(x240)) = x240 + x241 >= x240 + x241 = s(+(x241,x240))
     
     +(s(x246),x245) = x245 + x246 >= x245 + x246 = s(+(x246,x245))
     
     +(x250,0()) = x250 + 2 >= x250 = x250
     
     +(0(),x252) = x252 + 2 >= x252 = x252
    problem:
     +(x231,p(x230)) -> p(+(x231,x230))
     +(p(x236),x235) -> p(+(x236,x235))
     +(x241,s(x240)) -> s(+(x241,x240))
     +(s(x246),x245) -> s(+(x246,x245))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [s](x0) = x0 + 1,
      
      [+](x0, x1) = 2x0 + x1 + 1,
      
      [p](x0) = x0
     orientation:
      +(x231,p(x230)) = x230 + 2x231 + 1 >= x230 + 2x231 + 1 = p(+(x231,x230))
      
      +(p(x236),x235) = x235 + 2x236 + 1 >= x235 + 2x236 + 1 = p(+(x236,x235))
      
      +(x241,s(x240)) = x240 + 2x241 + 2 >= x240 + 2x241 + 2 = s(+(x241,x240))
      
      +(s(x246),x245) = x245 + 2x246 + 3 >= x245 + 2x246 + 2 = s(+(x246,x245))
     problem:
      +(x231,p(x230)) -> p(+(x231,x230))
      +(p(x236),x235) -> p(+(x236,x235))
      +(x241,s(x240)) -> s(+(x241,x240))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [s](x0) = x0 + 1,
       
       [+](x0, x1) = x0 + 2x1 + 7,
       
       [p](x0) = x0
      orientation:
       +(x231,p(x230)) = 2x230 + x231 + 7 >= 2x230 + x231 + 7 = p(+(x231,x230))
       
       +(p(x236),x235) = 2x235 + x236 + 7 >= 2x235 + x236 + 7 = p(+(x236,x235))
       
       +(x241,s(x240)) = 2x240 + x241 + 9 >= 2x240 + x241 + 8 = s(+(x241,x240))
      problem:
       +(x231,p(x230)) -> p(+(x231,x230))
       +(p(x236),x235) -> p(+(x236,x235))
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [+](x0, x1) = 4x0 + x1 + 7,
        
        [p](x0) = x0 + 1
       orientation:
        +(x231,p(x230)) = x230 + 4x231 + 8 >= x230 + 4x231 + 8 = p(+(x231,x230))
        
        +(p(x236),x235) = x235 + 4x236 + 11 >= x235 + 4x236 + 8 = p(+(x236,x235))
       problem:
        +(x231,p(x230)) -> p(+(x231,x230))
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [+](x0, x1) = x0 + 4x1 + 7,
         
         [p](x0) = x0 + 1
        orientation:
         +(x231,p(x230)) = 4x230 + x231 + 11 >= 4x230 + x231 + 8 = p(+(x231,x230))
        problem:
         
        Qed