YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ 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)) ]
Constructors: {0,p,s}
Defined function symbols: {+,-}
Constructor subsystem:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
Rule part & Conj Part:
   [ 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)) ]
   [ ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Int}
Signature:
   [ + : Int,Int -> Int,
     - : Int,Int -> Int,
     s : Int -> Int,
     p : Int -> Int,
     0 : Int ]
Rule Part:
   [ 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)) ]
Conjecture Part:
   [ ]
Precedence (by weight): {(+,6),(-,7),(0,0),(p,5),(s,4)}
Rule part is confluent.
R0 is ground confluent.
Conjucture part is empty.
examples/additions/int5.trs: Success(GCR)
(41 msec.)