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

Proof:
 sorted: (order)
 0:-(x,x) -> 0()
   -(x,0()) -> x
 1:+(x,y) -> +(y,x)
   +(0(),x) -> x
   +(x,0()) -> x
   +(s(x),y) -> s(+(x,y))
   +(x,s(y)) -> s(+(y,x))
   +(p(x),y) -> p(+(x,y))
   +(x,p(y)) -> p(+(y,x))
   s(p(x)) -> x
   p(s(x)) -> x
 -----
 sorts
   [0>1, 1>3, 2>3]
 sort attachment (non-strict)
   - : 1 x 1 -> 0
   0 : 3
   + : 2 x 2 -> 2
   s : 2 -> 2
   p : 2 -> 2
 -----
 0:-(x,x) -> 0()
   -(x,0()) -> x
   Church Rosser Transformation Processor (kb):
    -(x,x) -> 0()
    -(x,0()) -> x
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [0] = 0,
      
      [-](x0, x1) = 2x0 + 2x1 + 1
     orientation:
      -(x,x) = 4x + 1 >= 0 = 0()
      
      -(x,0()) = 2x + 1 >= x = x
     problem:
      
     Qed
 
 
 1:+(x,y) -> +(y,x)
   +(0(),x) -> x
   +(x,0()) -> x
   +(s(x),y) -> s(+(x,y))
   +(x,s(y)) -> s(+(y,x))
   +(p(x),y) -> p(+(x,y))
   +(x,p(y)) -> p(+(y,x))
   s(p(x)) -> x
   p(s(x)) -> x
   AT confluence processor
    Complete TRS T' of input TRS:
    +(0(),x) -> x
    +(x,0()) -> x
    +(s(x),y) -> s(+(x,y))
    +(x,s(y)) -> s(+(y,x))
    +(p(x),y) -> p(+(x,y))
    +(x,p(y)) -> p(+(y,x))
    s(p(x)) -> x
    p(s(x)) -> x
    +(x,y) -> +(y,x)
    
     T' = (P union S) with
    
     TRS P:+(x,y) -> +(y,x)
    
     TRS S:+(0(),x) -> x
           +(x,0()) -> x
           +(s(x),y) -> s(+(x,y))
           +(x,s(y)) -> s(+(y,x))
           +(p(x),y) -> p(+(x,y))
           +(x,p(y)) -> p(+(y,x))
           s(p(x)) -> x
           p(s(x)) -> x
    
    S is linear and P is reversible.
    
     CP(S,S) = 
    0() = 0(), s(y) = s(+(y,0())), p(y) = p(+(y,0())), s(x) = s(+(x,0())), 
    p(x) = p(+(x,0())), s(+(x568,0())) = s(x568), s(+(x570,s(y))) = s(+(y,s(x570))), 
    s(+(x572,p(y))) = p(+(y,s(x572))), s(+(x575,0())) = s(x575), s(+(x577,s(x))) = 
    s(+(x,s(x577))), s(+(x579,p(x))) = p(+(x,s(x579))), p(+(x580,0())) = 
    p(x580), p(+(x582,s(y))) = s(+(y,p(x582))), p(+(x584,p(y))) = p(+(y,p(x584))), 
    p(+(x587,0())) = p(x587), p(+(x589,s(x))) = s(+(x,p(x589))), p(+(x591,p(x))) = 
    p(+(x,p(x591))), +(x592,y) = s(+(p(x592),y)), +(x,x593) = s(+(p(x593),x)), 
    p(x594) = p(x594), +(x595,y) = p(+(s(x595),y)), +(x,x596) = p(+(s(x596),x)), 
    s(x597) = s(x597)
    
     CP(S,P union P^-1) = 
    y = +(y,0()), x = +(x,0()), x = +(0(),x), y = +(0(),y), s(+(x626,y)) = 
    +(y,s(x626)), s(+(x628,x)) = +(x,s(x628)), s(+(x631,x)) = +(s(x631),x), 
    s(+(x633,y)) = +(s(x633),y), p(+(x634,y)) = +(y,p(x634)), p(+(x636,x)) = 
    +(x,p(x636)), p(+(x639,x)) = +(p(x639),x), p(+(x641,y)) = +(p(x641),y)
    
     CP(P union P^-1,S) = 
    +(x,0()) = x, +(0(),x) = x, +(y,s(x)) = s(+(x,y)), +(s(y),x) = s(+(y,x)), 
    +(y,p(x)) = p(+(x,y)), +(p(y),x) = p(+(y,x))
    
    
    We have to check termination of S:
    
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [p](x0) = x0,
      
      [s](x0) = x0,
      
      [+](x0, x1) = x0 + x1,
      
      [0] = 2
     orientation:
      +(0(),x) = x + 2 >= x = x
      
      +(x,0()) = x + 2 >= x = x
      
      +(s(x),y) = x + y >= x + y = s(+(x,y))
      
      +(x,s(y)) = x + y >= x + y = s(+(y,x))
      
      +(p(x),y) = x + y >= x + y = p(+(x,y))
      
      +(x,p(y)) = x + y >= x + y = p(+(y,x))
      
      s(p(x)) = x >= x = x
      
      p(s(x)) = x >= x = x
     problem:
      +(s(x),y) -> s(+(x,y))
      +(x,s(y)) -> s(+(y,x))
      +(p(x),y) -> p(+(x,y))
      +(x,p(y)) -> p(+(y,x))
      s(p(x)) -> x
      p(s(x)) -> x
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [p](x0) = x0,
       
       [s](x0) = x0 + 3,
       
       [+](x0, x1) = x0 + x1 + 2
      orientation:
       +(s(x),y) = x + y + 5 >= x + y + 5 = s(+(x,y))
       
       +(x,s(y)) = x + y + 5 >= x + y + 5 = s(+(y,x))
       
       +(p(x),y) = x + y + 2 >= x + y + 2 = p(+(x,y))
       
       +(x,p(y)) = x + y + 2 >= x + y + 2 = p(+(y,x))
       
       s(p(x)) = x + 3 >= x = x
       
       p(s(x)) = x + 3 >= x = x
      problem:
       +(s(x),y) -> s(+(x,y))
       +(x,s(y)) -> s(+(y,x))
       +(p(x),y) -> p(+(x,y))
       +(x,p(y)) -> p(+(y,x))
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [p](x0) = x0,
        
        [s](x0) = x0 + 2,
        
        [+](x0, x1) = 4x0 + 4x1
       orientation:
        +(s(x),y) = 4x + 4y + 8 >= 4x + 4y + 2 = s(+(x,y))
        
        +(x,s(y)) = 4x + 4y + 8 >= 4x + 4y + 2 = s(+(y,x))
        
        +(p(x),y) = 4x + 4y >= 4x + 4y = p(+(x,y))
        
        +(x,p(y)) = 4x + 4y >= 4x + 4y = p(+(y,x))
       problem:
        +(p(x),y) -> p(+(x,y))
        +(x,p(y)) -> p(+(y,x))
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [p](x0) = x0 + 4,
         
         [+](x0, x1) = 2x0 + 2x1 + 1
        orientation:
         +(p(x),y) = 2x + 2y + 9 >= 2x + 2y + 5 = p(+(x,y))
         
         +(x,p(y)) = 2x + 2y + 9 >= 2x + 2y + 5 = p(+(y,x))
        problem:
         
        Qed