NO

Problem 1: 


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


Problem 1: 

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

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

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

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

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

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

-> Problem conclusions:
 Left linear, Not right linear, Not 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',s(y)),s(y))
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('+(*(x',s(y)),s(y))', D0)
ID: 1 => ('+(+(x',*(x',y)),s(y))', D1, R3, P[1], S{x9 -> y, x10 -> x'}), NR: '+(x',*(x',y))'
t: +(s(x'),*(s(x'),y))
Nodes: [0,1,2,3]
Edges: [(0,1),(0,2),(1,3),(2,3)]
ID: 0 => ('+(s(x'),*(s(x'),y))', D0)
ID: 1 => ('+(s(x'),+(*(x',y),y))', D1, R2, P[2], S{x7 -> y, x8 -> x'}), NR: '+(*(x',y),y)'
ID: 2 => ('s(+(x',*(s(x'),y)))', D1, R5, P[], S{x12 -> *(s(x'),y), x13 -> x'}), NR: 's(+(x',*(s(x'),y)))'
ID: 3 => ('s(+(x',+(*(x',y),y)))', D2, R5, P[], S{x12 -> +(*(x',y),y), x13 -> x'}), NR: 's(+(x',+(*(x',y),y)))'
+(*(x',s(y)),s(y)) ->* no union *<- +(s(x'),*(s(x'),y))
"Not joinable"

The problem is not confluent.