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(),0()) -> 0()
 -(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):
  +(x342,p(x341)) -> p(+(x342,x341))
  s(p(x345)) -> x345
  -(x347,p(x346)) -> s(-(x347,x346))
  p(s(x350)) -> x350
  -(p(x352),x351) -> p(-(x352,x351))
  +(x357,s(x356)) -> s(+(x357,x356))
  -(x362,s(x361)) -> p(-(x362,x361))
  -(s(x367),x366) -> s(-(x367,x366))
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [-](x0, x1) = x0 + x1,
    
    [s](x0) = x0 + 1,
    
    [+](x0, x1) = 4x0 + 2x1 + 1,
    
    [p](x0) = x0 + 1
   orientation:
    +(x342,p(x341)) = 2x341 + 4x342 + 3 >= 2x341 + 4x342 + 2 = p(+(x342,x341))
    
    s(p(x345)) = x345 + 2 >= x345 = x345
    
    -(x347,p(x346)) = x346 + x347 + 1 >= x346 + x347 + 1 = s(-(x347,x346))
    
    p(s(x350)) = x350 + 2 >= x350 = x350
    
    -(p(x352),x351) = x351 + x352 + 1 >= x351 + x352 + 1 = p(-(x352,x351))
    
    +(x357,s(x356)) = 2x356 + 4x357 + 3 >= 2x356 + 4x357 + 2 = s(+(x357,x356))
    
    -(x362,s(x361)) = x361 + x362 + 1 >= x361 + x362 + 1 = p(-(x362,x361))
    
    -(s(x367),x366) = x366 + x367 + 1 >= x366 + x367 + 1 = s(-(x367,x366))
   problem:
    -(x347,p(x346)) -> s(-(x347,x346))
    -(p(x352),x351) -> p(-(x352,x351))
    -(x362,s(x361)) -> p(-(x362,x361))
    -(s(x367),x366) -> s(-(x367,x366))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [-](x0, x1) = 4x0 + x1,
     
     [s](x0) = x0 + 1,
     
     [p](x0) = x0 + 1
    orientation:
     -(x347,p(x346)) = x346 + 4x347 + 1 >= x346 + 4x347 + 1 = s(-(x347,x346))
     
     -(p(x352),x351) = x351 + 4x352 + 4 >= x351 + 4x352 + 1 = p(-(x352,x351))
     
     -(x362,s(x361)) = x361 + 4x362 + 1 >= x361 + 4x362 + 1 = p(-(x362,x361))
     
     -(s(x367),x366) = x366 + 4x367 + 4 >= x366 + 4x367 + 1 = s(-(x367,x366))
    problem:
     -(x347,p(x346)) -> s(-(x347,x346))
     -(x362,s(x361)) -> p(-(x362,x361))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [-](x0, x1) = x0 + 2x1,
      
      [s](x0) = x0 + 1,
      
      [p](x0) = x0 + 2
     orientation:
      -(x347,p(x346)) = 2x346 + x347 + 4 >= 2x346 + x347 + 1 = s(-(x347,x346))
      
      -(x362,s(x361)) = 2x361 + x362 + 2 >= 2x361 + x362 + 2 = p(-(x362,x361))
     problem:
      -(x362,s(x361)) -> p(-(x362,x361))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [-](x0, x1) = x0 + x1 + 5,
       
       [s](x0) = x0 + 4,
       
       [p](x0) = x0 + 3
      orientation:
       -(x362,s(x361)) = x361 + x362 + 9 >= x361 + x362 + 8 = p(-(x362,x361))
      problem:
       
      Qed