YES

Problem 1: 


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


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 x y)
(REPLACEMENT-MAP
(+ 1, 2)
(- 1)
(fSNonEmpty)
)
(RULES
+(x,y) -> +(y,x)
-(+(x,y)) -> +(-(x),-(y))
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

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

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

-> Critical pairs info:
<-(+(y',x')),+(-(x'),-(y'))>   =>  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:
(VAR x y x' y')
(REPLACEMENT-MAP
(+ 1, 2)
(- 1)
(fSNonEmpty)
)
(RULES
+(x,y) -> +(y,x)
-(+(x,y)) -> +(-(x),-(y))
)
Critical Pairs:
<-(+(y',x')),+(-(x'),-(y'))>   =>  Not trivial, Not overlay, Proper, NW0, N1
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: -(+(y',x'))
Nodes: [0,1,2,3]
Edges: [(0,1),(0,2),(1,0),(1,3),(2,3),(3,2)]
ID: 0 => ('-(+(y',x'))', D0)
ID: 1 => ('-(+(x',y'))', D1, R1, P[1], S{x6 -> y', x7 -> x'}), NR: '+(x',y')'
ID: 2 => ('+(-(y'),-(x'))', D1, R2, P[], S{x8 -> y', x9 -> x'}), NR: '+(-(y'),-(x'))'
ID: 3 => ('+(-(x'),-(y'))', D2, R2, P[], S{x8 -> x', x9 -> y'}), NR: '+(-(x'),-(y'))'
t: +(-(x'),-(y'))
Nodes: [0,1]
Edges: [(0,1),(1,0)]
ID: 0 => ('+(-(x'),-(y'))', D0)
ID: 1 => ('+(-(y'),-(x'))', D1, R1, P[], S{x6 -> -(x'), x7 -> -(y')}), NR: '+(-(y'),-(x'))'
SNodesPath1: 
TNodesPath1: +(-(x'),-(y')) -> +(-(y'),-(x'))
SNodesPath2: -(+(y',x')) -> -(+(x',y')) -> +(-(x'),-(y'))
TNodesPath2: +(-(x'),-(y'))
-(+(y',x')) ->= +(-(y'),-(x')) *<- +(-(x'),-(y'))
+(-(x'),-(y')) ->= +(-(x'),-(y')) *<- -(+(y',x'))
"Strongly closed critical pair"

The problem is confluent.