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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 64
   0() <-0|[]- +(0(),0()) -3|[]-> 0()
   s(x) <-0|[]- +(s(x),0()) -4|[]-> s(+(x,0()))
   p(x) <-0|[]- +(p(x),0()) -5|[]-> p(+(x,0()))
   +(x,y) <-0|[]- +(+(x,y),0()) -11|[]-> +(x,+(y,0()))
   +(x,z) <-0|0[]- +(+(x,0()),z) -11|[]-> +(x,+(0(),z))
   +(x,y) <-0|1[]- +(x,+(y,0())) -12|[]-> +(+(x,y),0())
   -(x) <-0|0[]- -(+(x,0())) -13|[]-> +(-(x),-(0()))
   s(+(0(),x627)) <-1|[]- +(0(),s(x627)) -3|[]-> s(x627)
   s(+(s(x),x629)) <-1|[]- +(s(x),s(x629)) -4|[]-> s(+(x,s(x629)))
   s(+(p(x),x631)) <-1|[]- +(p(x),s(x631)) -5|[]-> p(+(x,s(x631)))
   s(+(+(x,y),x633)) <-1|[]- +(+(x,y),s(x633)) -11|[]-> +(x,+(y,s(x633)))
   +(s(+(x,x635)),z) <-1|0[]- +(+(x,s(x635)),z) -11|[]-> +(x,+(s(x635),z))
   +(x,s(+(y,x637))) <-1|1[]- +(x,+(y,s(x637))) -12|[]-> +(+(x,y),s(x637))
   -(s(+(x,x639))) <-1|0[]- -(+(x,s(x639))) -13|[]-> +(-(x),-(s(x639)))
   p(+(0(),x641)) <-2|[]- +(0(),p(x641)) -3|[]-> p(x641)
   p(+(s(x),x643)) <-2|[]- +(s(x),p(x643)) -4|[]-> s(+(x,p(x643)))
   p(+(p(x),x645)) <-2|[]- +(p(x),p(x645)) -5|[]-> p(+(x,p(x645)))
   p(+(+(x,y),x647)) <-2|[]- +(+(x,y),p(x647)) -11|[]-> +(x,+(y,p(x647)))
   +(p(+(x,x649)),z) <-2|0[]- +(+(x,p(x649)),z) -11|[]-> +(x,+(p(x649),z))
   +(x,p(+(y,x651))) <-2|1[]- +(x,+(y,p(x651))) -12|[]-> +(+(x,y),p(x651))
   -(p(+(x,x653))) <-2|0[]- -(+(x,p(x653))) -13|[]-> +(-(x),-(p(x653)))
   0() <-3|[]- +(0(),0()) -0|[]-> 0()
   s(y) <-3|[]- +(0(),s(y)) -1|[]-> s(+(0(),y))
   p(y) <-3|[]- +(0(),p(y)) -2|[]-> p(+(0(),y))
   +(y,z) <-3|0[]- +(+(0(),y),z) -11|[]-> +(0(),+(y,z))
   +(y,z) <-3|[]- +(0(),+(y,z)) -12|[]-> +(+(0(),y),z)
   +(x,z) <-3|1[]- +(x,+(0(),z)) -12|[]-> +(+(x,0()),z)
   -(y) <-3|0[]- -(+(0(),y)) -13|[]-> +(-(0()),-(y))
   s(+(x661,0())) <-4|[]- +(s(x661),0()) -0|[]-> s(x661)
   s(+(x663,s(y))) <-4|[]- +(s(x663),s(y)) -1|[]-> s(+(s(x663),y))
   s(+(x665,p(y))) <-4|[]- +(s(x665),p(y)) -2|[]-> p(+(s(x665),y))
   +(s(+(x667,y)),z) <-4|0[]- +(+(s(x667),y),z) -11|[]-> +(s(x667),+(y,z))
   s(+(x669,+(y,z))) <-4|[]- +(s(x669),+(y,z)) -12|[]-> +(+(s(x669),y),z)
   +(x,s(+(x671,z))) <-4|1[]- +(x,+(s(x671),z)) -12|[]-> +(+(x,s(x671)),z)
   -(s(+(x673,y))) <-4|0[]- -(+(s(x673),y)) -13|[]-> +(-(s(x673)),-(y))
   p(+(x675,0())) <-5|[]- +(p(x675),0()) -0|[]-> p(x675)
   p(+(x677,s(y))) <-5|[]- +(p(x677),s(y)) -1|[]-> s(+(p(x677),y))
   p(+(x679,p(y))) <-5|[]- +(p(x679),p(y)) -2|[]-> p(+(p(x679),y))
   +(p(+(x681,y)),z) <-5|0[]- +(+(p(x681),y),z) -11|[]-> +(p(x681),+(y,z))
   p(+(x683,+(y,z))) <-5|[]- +(p(x683),+(y,z)) -12|[]-> +(+(p(x683),y),z)
   +(x,p(+(x685,z))) <-5|1[]- +(x,+(p(x685),z)) -12|[]-> +(+(x,p(x685)),z)
   -(p(+(x687,y))) <-5|0[]- -(+(p(x687),y)) -13|[]-> +(-(p(x687)),-(y))
   +(x,x689) <-6|1[]- +(x,s(p(x689))) -1|[]-> s(+(x,p(x689)))
   +(x690,y) <-6|0[]- +(s(p(x690)),y) -4|[]-> s(+(p(x690),y))
   p(x691) <-6|0[]- p(s(p(x691))) -7|[]-> p(x691)
   -(x692) <-6|0[]- -(s(p(x692))) -9|[]-> p(-(p(x692)))
   +(x,x693) <-7|1[]- +(x,p(s(x693))) -2|[]-> p(+(x,s(x693)))
   +(x694,y) <-7|0[]- +(p(s(x694)),y) -5|[]-> p(+(s(x694),y))
   s(x695) <-7|0[]- s(p(s(x695))) -6|[]-> s(x695)
   -(x696) <-7|0[]- -(p(s(x696))) -10|[]-> s(-(s(x696)))
   +(x697,+(x698,0())) <-11|[]- +(+(x697,x698),0()) -0|[]-> +(x697,x698)
   +(x700,+(x701,s(y))) <-11|[]- +(+(x700,x701),s(y)) -1|[]-> s(+(+(x700,x701),y))
   +(x703,+(x704,p(y))) <-11|[]- +(+(x703,x704),p(y)) -2|[]-> p(+(+(x703,x704),y))
   +(+(x706,+(x707,y)),z) <-11|0[]- +(+(+(x706,x707),y),z) -11|[]-> +(+(x706,x707),+(y,z))
   +(x709,+(x710,+(y,z))) <-11|[]- +(+(x709,x710),+(y,z)) -12|[]-> +(+(+(x709,x710),y),z)
   +(x,+(x712,+(x713,z))) <-11|1[]- +(x,+(+(x712,x713),z)) -12|[]-> +(+(x,+(x712,x713)),z)
   -(+(x715,+(x716,y))) <-11|0[]- -(+(+(x715,x716),y)) -13|[]-> +(-(+(x715,x716)),-(y))
   +(+(0(),x719),x720) <-12|[]- +(0(),+(x719,x720)) -3|[]-> +(x719,x720)
   +(+(s(x),x722),x723) <-12|[]- +(s(x),+(x722,x723)) -4|[]-> s(+(x,+(x722,x723)))
   +(+(p(x),x725),x726) <-12|[]- +(p(x),+(x725,x726)) -5|[]-> p(+(x,+(x725,x726)))
   +(+(+(x,y),x728),x729) <-12|[]- +(+(x,y),+(x728,x729)) -11|[]-> +(x,+(y,+(x728,x729)))
   +(+(+(x,x731),x732),z) <-12|0[]- +(+(x,+(x731,x732)),z) -11|[]-> +(x,+(+(x731,x732),z))
   +(x,+(+(y,x734),x735)) <-12|1[]- +(x,+(y,+(x734,x735))) -12|[]-> +(+(x,y),+(x734,x735))
   -(+(+(x,x737),x738)) <-12|0[]- -(+(x,+(x737,x738))) -13|[]-> +(-(x),-(+(x737,x738)))
  Redundant Rules Transformation:
   +(x,0()) -> x
   +(x,s(y)) -> s(+(x,y))
   +(x,p(y)) -> p(+(x,y))
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   +(p(x),y) -> p(+(x,y))
   s(p(x)) -> x
   p(s(x)) -> x
   -(0()) -> 0()
   -(s(x)) -> p(-(x))
   -(p(x)) -> s(-(x))
   +(x,+(y,z)) -> +(+(x,y),z)
   -(+(x,y)) -> +(-(x),-(y))
   Church Rosser Transformation Processor (kb):
    +(x,0()) -> x
    +(x,s(y)) -> s(+(x,y))
    +(x,p(y)) -> p(+(x,y))
    +(0(),y) -> y
    +(s(x),y) -> s(+(x,y))
    +(p(x),y) -> p(+(x,y))
    s(p(x)) -> x
    p(s(x)) -> x
    -(0()) -> 0()
    -(s(x)) -> p(-(x))
    -(p(x)) -> s(-(x))
    +(x,+(y,z)) -> +(+(x,y),z)
    -(+(x,y)) -> +(-(x),-(y))
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [-](x0) = 2x0,
      
      [p](x0) = x0 + 2,
      
      [s](x0) = x0 + 1,
      
      [+](x0, x1) = x0 + x1 + 1,
      
      [0] = 0
     orientation:
      +(x,0()) = x + 1 >= x = x
      
      +(x,s(y)) = x + y + 2 >= x + y + 2 = s(+(x,y))
      
      +(x,p(y)) = x + y + 3 >= x + y + 3 = p(+(x,y))
      
      +(0(),y) = y + 1 >= y = y
      
      +(s(x),y) = x + y + 2 >= x + y + 2 = s(+(x,y))
      
      +(p(x),y) = x + y + 3 >= x + y + 3 = p(+(x,y))
      
      s(p(x)) = x + 3 >= x = x
      
      p(s(x)) = x + 3 >= x = x
      
      -(0()) = 0 >= 0 = 0()
      
      -(s(x)) = 2x + 2 >= 2x + 2 = p(-(x))
      
      -(p(x)) = 2x + 4 >= 2x + 1 = s(-(x))
      
      +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z)
      
      -(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 1 = +(-(x),-(y))
     problem:
      +(x,s(y)) -> s(+(x,y))
      +(x,p(y)) -> p(+(x,y))
      +(s(x),y) -> s(+(x,y))
      +(p(x),y) -> p(+(x,y))
      -(0()) -> 0()
      -(s(x)) -> p(-(x))
      +(x,+(y,z)) -> +(+(x,y),z)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [-](x0) = x0,
       
       [p](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [+](x0, x1) = x0 + 2x1,
       
       [0] = 0
      orientation:
       +(x,s(y)) = x + 2y + 2 >= x + 2y + 1 = s(+(x,y))
       
       +(x,p(y)) = x + 2y + 2 >= x + 2y + 1 = p(+(x,y))
       
       +(s(x),y) = x + 2y + 1 >= x + 2y + 1 = s(+(x,y))
       
       +(p(x),y) = x + 2y + 1 >= x + 2y + 1 = p(+(x,y))
       
       -(0()) = 0 >= 0 = 0()
       
       -(s(x)) = x + 1 >= x + 1 = p(-(x))
       
       +(x,+(y,z)) = x + 2y + 4z >= x + 2y + 2z = +(+(x,y),z)
      problem:
       +(s(x),y) -> s(+(x,y))
       +(p(x),y) -> p(+(x,y))
       -(0()) -> 0()
       -(s(x)) -> p(-(x))
       +(x,+(y,z)) -> +(+(x,y),z)
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [-](x0) = x0,
        
        [p](x0) = x0 + 4,
        
        [s](x0) = x0 + 4,
        
        [+](x0, x1) = x0 + 2x1 + 1,
        
        [0] = 0
       orientation:
        +(s(x),y) = x + 2y + 5 >= x + 2y + 5 = s(+(x,y))
        
        +(p(x),y) = x + 2y + 5 >= x + 2y + 5 = p(+(x,y))
        
        -(0()) = 0 >= 0 = 0()
        
        -(s(x)) = x + 4 >= x + 4 = p(-(x))
        
        +(x,+(y,z)) = x + 2y + 4z + 3 >= x + 2y + 2z + 2 = +(+(x,y),z)
       problem:
        +(s(x),y) -> s(+(x,y))
        +(p(x),y) -> p(+(x,y))
        -(0()) -> 0()
        -(s(x)) -> p(-(x))
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [-](x0) = 2x0,
         
         [p](x0) = x0,
         
         [s](x0) = x0,
         
         [+](x0, x1) = 4x0 + x1,
         
         [0] = 2
        orientation:
         +(s(x),y) = 4x + y >= 4x + y = s(+(x,y))
         
         +(p(x),y) = 4x + y >= 4x + y = p(+(x,y))
         
         -(0()) = 4 >= 2 = 0()
         
         -(s(x)) = 2x >= 2x = p(-(x))
        problem:
         +(s(x),y) -> s(+(x,y))
         +(p(x),y) -> p(+(x,y))
         -(s(x)) -> p(-(x))
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [-](x0) = 4x0,
          
          [p](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [+](x0, x1) = 4x0 + x1
         orientation:
          +(s(x),y) = 4x + y + 4 >= 4x + y + 1 = s(+(x,y))
          
          +(p(x),y) = 4x + y + 4 >= 4x + y + 1 = p(+(x,y))
          
          -(s(x)) = 4x + 4 >= 4x + 1 = p(-(x))
         problem:
          
         Qed