YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     -(0,?x) -> 0,
     -(?x,0) -> ?x,
     -(s(?x),s(?y)) -> -(?x,?y) ]
Constructors: {0,s}
Defined function symbols: {+,-}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     -(0,?x) -> 0,
     -(?x,0) -> ?x,
     -(s(?x),s(?y)) -> -(?x,?y) ]
   [ ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ + : Nat,Nat -> Nat,
     - : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     -(0,?x) -> 0,
     -(?x,0) -> ?x,
     -(s(?x),s(?y)) -> -(?x,?y) ]
Conjecture Part:
   [ ]
Precedence (by weight): {(+,3),(-,1),(0,2),(s,0)}
Rule part is confluent.
R0 is ground confluent.
Conjucture part is empty.
examples/additions/minus1.trs: Success(GCR)
(17 msec.)