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