YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty)
(REPLACEMENT-MAP
(+ 1, 2)
(- 1)
(0)
(fSNonEmpty)
(x)
)
(RULES
+(x,-(x)) -> 0
-(+(x,-(x))) -> 0
0 -> -(0)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 
Not CS-TRS Procedure:
R is not a CS-TRS

Problem 1: 
Linearity Procedure:
Linear?
YES

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty)
(REPLACEMENT-MAP
(+ 1, 2)
(- 1)
(0)
(fSNonEmpty)
(x)
)
(RULES
+(x,-(x)) -> 0
-(+(x,-(x))) -> 0
0 -> -(0)
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 +(x,-(x)) -> 0
 -(+(x,-(x))) -> 0
 0 -> -(0)
-> Vars:


-> Rlps:
 (rule: +(x,-(x)) -> 0, id: 1, possubterms: +(x,-(x))->[], x->[1], -(x)->[2], x->[2, 1])
 (rule: -(+(x,-(x))) -> 0, id: 2, possubterms: -(+(x,-(x)))->[], +(x,-(x))->[1], x->[1, 1], -(x)->[1, 2], x->[1, 2, 1])
 (rule: 0 -> -(0), id: 3, possubterms: 0->[])

-> Unifications:
(R2 unifies with R1 at p: [1], l: -(+(x,-(x))), lp: +(x,-(x)), sig: {}, l': +(x,-(x)), r: 0, r': 0)

-> Critical pairs info:
<-(0),0>   =>  Not trivial, Not overlay, Proper, NW0, N1

-> Problem conclusions:
 Left linear, Right linear, Linear
 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
 Not Huet-Levy confluent, Not Newman confluent
 R is a TRS 

Problem 1.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(REPLACEMENT-MAP
(+ 1, 2)
(- 1)
(0)
(fSNonEmpty)
(x)
)
(RULES
+(x,-(x)) -> 0
-(+(x,-(x))) -> 0
0 -> -(0)
)
Critical Pairs:
<-(0),0>   =>  Not trivial, Not overlay, Proper, NW0, N1
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: -(0)
Nodes: [0,1,2,3,4,5,6,7,8]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,7),(7,8)]
ID: 0 => ('-(0)', D0)
ID: 1 => ('-(-(0))', D1, R3, P[1], S{}), NR: '-(0)'
ID: 2 => ('-(-(-(0)))', D2, R3, P[1, 1], S{}), NR: '-(0)'
ID: 3 => ('-(-(-(-(0))))', D3, R3, P[1, 1, 1], S{}), NR: '-(0)'
ID: 4 => ('-(-(-(-(-(0)))))', D4, R3, P[1, 1, 1, 1], S{}), NR: '-(0)'
ID: 5 => ('-(-(-(-(-(-(0))))))', D5, R3, P[1, 1, 1, 1, 1], S{}), NR: '-(0)'
ID: 6 => ('-(-(-(-(-(-(-(0)))))))', D6, R3, P[1, 1, 1, 1, 1, 1], S{}), NR: '-(0)'
ID: 7 => ('-(-(-(-(-(-(-(-(0))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1], S{}), NR: '-(0)'
ID: 8 => ('-(-(-(-(-(-(-(-(-(0)))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{}), NR: '-(0)'
t: 0
Nodes: [0,1,2,3,4,5,6,7,8]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,7),(7,8)]
ID: 0 => ('0', D0)
ID: 1 => ('-(0)', D1, R3, P[], S{}), NR: '-(0)'
ID: 2 => ('-(-(0))', D2, R3, P[1], S{}), NR: '-(0)'
ID: 3 => ('-(-(-(0)))', D3, R3, P[1, 1], S{}), NR: '-(0)'
ID: 4 => ('-(-(-(-(0))))', D4, R3, P[1, 1, 1], S{}), NR: '-(0)'
ID: 5 => ('-(-(-(-(-(0)))))', D5, R3, P[1, 1, 1, 1], S{}), NR: '-(0)'
ID: 6 => ('-(-(-(-(-(-(0))))))', D6, R3, P[1, 1, 1, 1, 1], S{}), NR: '-(0)'
ID: 7 => ('-(-(-(-(-(-(-(0)))))))', D7, R3, P[1, 1, 1, 1, 1, 1], S{}), NR: '-(0)'
ID: 8 => ('-(-(-(-(-(-(-(-(0))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1], S{}), NR: '-(0)'
SNodesPath1: -(0)
TNodesPath1: 0 -> -(0)
SNodesPath2: -(0)
TNodesPath2: 0 -> -(0)
-(0) ->= -(0) *<- 0
0 ->= -(0) *<- -(0)
"Strongly closed critical pair"

The problem is confluent.