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) -> +(y,x)
 -(+(x,y)) -> +(-(x),-(y))

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 62
   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 <-0|[]- +(x,0()) -12|[]-> +(0(),x)
   -(x) <-0|0[]- -(+(x,0())) -13|[]-> +(-(x),-(0()))
   s(+(0(),x578)) <-1|[]- +(0(),s(x578)) -3|[]-> s(x578)
   s(+(s(x),x580)) <-1|[]- +(s(x),s(x580)) -4|[]-> s(+(x,s(x580)))
   s(+(p(x),x582)) <-1|[]- +(p(x),s(x582)) -5|[]-> p(+(x,s(x582)))
   s(+(+(x,y),x584)) <-1|[]- +(+(x,y),s(x584)) -11|[]-> +(x,+(y,s(x584)))
   +(s(+(x,x586)),z) <-1|0[]- +(+(x,s(x586)),z) -11|[]-> +(x,+(s(x586),z))
   s(+(x,x588)) <-1|[]- +(x,s(x588)) -12|[]-> +(s(x588),x)
   -(s(+(x,x590))) <-1|0[]- -(+(x,s(x590))) -13|[]-> +(-(x),-(s(x590)))
   p(+(0(),x592)) <-2|[]- +(0(),p(x592)) -3|[]-> p(x592)
   p(+(s(x),x594)) <-2|[]- +(s(x),p(x594)) -4|[]-> s(+(x,p(x594)))
   p(+(p(x),x596)) <-2|[]- +(p(x),p(x596)) -5|[]-> p(+(x,p(x596)))
   p(+(+(x,y),x598)) <-2|[]- +(+(x,y),p(x598)) -11|[]-> +(x,+(y,p(x598)))
   +(p(+(x,x600)),z) <-2|0[]- +(+(x,p(x600)),z) -11|[]-> +(x,+(p(x600),z))
   p(+(x,x602)) <-2|[]- +(x,p(x602)) -12|[]-> +(p(x602),x)
   -(p(+(x,x604))) <-2|0[]- -(+(x,p(x604))) -13|[]-> +(-(x),-(p(x604)))
   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 <-3|[]- +(0(),y) -12|[]-> +(y,0())
   -(y) <-3|0[]- -(+(0(),y)) -13|[]-> +(-(0()),-(y))
   s(+(x611,0())) <-4|[]- +(s(x611),0()) -0|[]-> s(x611)
   s(+(x613,s(y))) <-4|[]- +(s(x613),s(y)) -1|[]-> s(+(s(x613),y))
   s(+(x615,p(y))) <-4|[]- +(s(x615),p(y)) -2|[]-> p(+(s(x615),y))
   +(s(+(x617,y)),z) <-4|0[]- +(+(s(x617),y),z) -11|[]-> +(s(x617),+(y,z))
   s(+(x619,y)) <-4|[]- +(s(x619),y) -12|[]-> +(y,s(x619))
   -(s(+(x621,y))) <-4|0[]- -(+(s(x621),y)) -13|[]-> +(-(s(x621)),-(y))
   p(+(x623,0())) <-5|[]- +(p(x623),0()) -0|[]-> p(x623)
   p(+(x625,s(y))) <-5|[]- +(p(x625),s(y)) -1|[]-> s(+(p(x625),y))
   p(+(x627,p(y))) <-5|[]- +(p(x627),p(y)) -2|[]-> p(+(p(x627),y))
   +(p(+(x629,y)),z) <-5|0[]- +(+(p(x629),y),z) -11|[]-> +(p(x629),+(y,z))
   p(+(x631,y)) <-5|[]- +(p(x631),y) -12|[]-> +(y,p(x631))
   -(p(+(x633,y))) <-5|0[]- -(+(p(x633),y)) -13|[]-> +(-(p(x633)),-(y))
   +(x,x635) <-6|1[]- +(x,s(p(x635))) -1|[]-> s(+(x,p(x635)))
   +(x636,y) <-6|0[]- +(s(p(x636)),y) -4|[]-> s(+(p(x636),y))
   p(x637) <-6|0[]- p(s(p(x637))) -7|[]-> p(x637)
   -(x638) <-6|0[]- -(s(p(x638))) -9|[]-> p(-(p(x638)))
   +(x,x639) <-7|1[]- +(x,p(s(x639))) -2|[]-> p(+(x,s(x639)))
   +(x640,y) <-7|0[]- +(p(s(x640)),y) -5|[]-> p(+(s(x640),y))
   s(x641) <-7|0[]- s(p(s(x641))) -6|[]-> s(x641)
   -(x642) <-7|0[]- -(p(s(x642))) -10|[]-> s(-(s(x642)))
   +(x643,+(x644,0())) <-11|[]- +(+(x643,x644),0()) -0|[]-> +(x643,x644)
   +(x646,+(x647,s(y))) <-11|[]- +(+(x646,x647),s(y)) -1|[]-> s(+(+(x646,x647),y))
   +(x649,+(x650,p(y))) <-11|[]- +(+(x649,x650),p(y)) -2|[]-> p(+(+(x649,x650),y))
   +(+(x652,+(x653,y)),z) <-11|0[]- +(+(+(x652,x653),y),z) -11|[]-> +(+(x652,x653),+(y,z))
   +(x655,+(x656,y)) <-11|[]- +(+(x655,x656),y) -12|[]-> +(y,+(x655,x656))
   -(+(x658,+(x659,y))) <-11|0[]- -(+(+(x658,x659),y)) -13|[]-> +(-(+(x658,x659)),-(y))
   +(0(),x) <-12|[]- +(x,0()) -0|[]-> x
   +(s(y),x) <-12|[]- +(x,s(y)) -1|[]-> s(+(x,y))
   +(p(y),x) <-12|[]- +(x,p(y)) -2|[]-> p(+(x,y))
   +(y,0()) <-12|[]- +(0(),y) -3|[]-> y
   +(y,s(x)) <-12|[]- +(s(x),y) -4|[]-> s(+(x,y))
   +(y,p(x)) <-12|[]- +(p(x),y) -5|[]-> p(+(x,y))
   +(z,+(x,y)) <-12|[]- +(+(x,y),z) -11|[]-> +(x,+(y,z))
   +(+(y,x),z) <-12|0[]- +(+(x,y),z) -11|[]-> +(x,+(y,z))
   -(+(y,x)) <-12|0[]- -(+(x,y)) -13|[]-> +(-(x),-(y))
  Redundant Rules Transformation:
   +(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) -> +(y,x)
   -(+(x,y)) -> +(-(x),-(y))
   Church Rosser Transformation Processor (ac):
    f6_AC(0(),y) -> y
    f6_AC(s(x),y) -> s(f6_AC(x,y))
    f6_AC(p(x),y) -> p(f6_AC(x,y))
    s(p(x)) -> x
    p(s(x)) -> x
    -(0()) -> 0()
    -(s(x)) -> p(-(x))
    -(p(x)) -> s(-(x))
    -(f6_AC(x,y)) -> f6_AC(-(x),-(y))
    AC critical peaks: joinable
    AC-KBO Processor:
     precedence:
      - > f6_AC > s > 0 > p
      weight function:
       w0 = 1
       w(p) = w(s) = 4
       w(0) = 1
       w(f6_AC) = w(-) = 0
      problem:
       
      Qed