NO

Problem 1: 


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


Problem 1: 

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

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

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

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

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

-> Critical pairs info:
<+(x,y'),+(+(x,0),y')>   =>  Not trivial, Not overlay, Proper, NW0, N1
<+(y,z),+(+(0,y),z)>   =>  Not trivial, Overlay, Proper, NW0, N2
<+(x,+(+(x',y'),z')),+(+(x,x'),+(y',z'))>   =>  Not trivial, Not overlay, Proper, NW0, N3
<s(+(x',+(y,z))),+(+(s(x'),y),z)>   =>  Not trivial, Overlay, Proper, NW0, N4
<+(x,s(+(x',y'))),+(+(x,s(x')),y')>   =>  Not trivial, Not overlay, Proper, NW0, N5

-> 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: 
No Convergence Brute Force Procedure:
-> Rewritings:
s: +(x,y')
Nodes: [0]
Edges: []
ID: 0 => ('+(x,y')', D0)
t: +(+(x,0),y')
Nodes: [0]
Edges: []
ID: 0 => ('+(+(x,0),y')', D0)
+(x,y') ->* no union *<- +(+(x,0),y')
"Not joinable"

The problem is not confluent.