YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(g 1, 2)
(a)
(b)
(c)
(d)
(e)
(fSNonEmpty)
)
(RULES
g(g(g(c,d),g(b,e)),b) -> a
g(a,y) -> g(b,b)
g(x,y) -> g(y,x)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 

Commutativity Transform Procedure:

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(g 1, 2)
(a)
(b)
(c)
(d)
(e)
(fSNonEmpty)
)
(RULES
g(g(g(b,e),g(c,d)),b) -> a
g(g(g(b,e),g(d,c)),b) -> a
g(g(g(c,d),g(b,e)),b) -> a
g(g(g(c,d),g(e,b)),b) -> a
g(g(g(d,c),g(b,e)),b) -> a
g(g(g(d,c),g(e,b)),b) -> a
g(g(g(e,b),g(c,d)),b) -> a
g(g(g(e,b),g(d,c)),b) -> a
g(a,y) -> g(b,b)
g(b,g(g(b,e),g(c,d))) -> a
g(b,g(g(b,e),g(d,c))) -> a
g(b,g(g(c,d),g(b,e))) -> a
g(b,g(g(c,d),g(e,b))) -> a
g(b,g(g(d,c),g(b,e))) -> a
g(b,g(g(d,c),g(e,b))) -> a
g(b,g(g(e,b),g(c,d))) -> a
g(b,g(g(e,b),g(d,c))) -> a
g(y,a) -> g(b,b)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(g 1, 2)
(a)
(b)
(c)
(d)
(e)
(fSNonEmpty)
)
(RULES
g(g(g(b,e),g(c,d)),b) -> a
g(g(g(b,e),g(d,c)),b) -> a
g(g(g(c,d),g(b,e)),b) -> a
g(g(g(c,d),g(e,b)),b) -> a
g(g(g(d,c),g(b,e)),b) -> a
g(g(g(d,c),g(e,b)),b) -> a
g(g(g(e,b),g(c,d)),b) -> a
g(g(g(e,b),g(d,c)),b) -> a
g(a,y) -> g(b,b)
g(b,g(g(b,e),g(c,d))) -> a
g(b,g(g(b,e),g(d,c))) -> a
g(b,g(g(c,d),g(b,e))) -> a
g(b,g(g(c,d),g(e,b))) -> a
g(b,g(g(d,c),g(b,e))) -> a
g(b,g(g(d,c),g(e,b))) -> a
g(b,g(g(e,b),g(c,d))) -> a
g(b,g(g(e,b),g(d,c))) -> a
g(y,a) -> g(b,b)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


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
(g 1, 2)
(a)
(b)
(c)
(d)
(e)
(fSNonEmpty)
)
(RULES
g(g(g(b,e),g(c,d)),b) -> a
g(g(g(b,e),g(d,c)),b) -> a
g(g(g(c,d),g(b,e)),b) -> a
g(g(g(c,d),g(e,b)),b) -> a
g(g(g(d,c),g(b,e)),b) -> a
g(g(g(d,c),g(e,b)),b) -> a
g(g(g(e,b),g(c,d)),b) -> a
g(g(g(e,b),g(d,c)),b) -> a
g(a,y) -> g(b,b)
g(b,g(g(b,e),g(c,d))) -> a
g(b,g(g(b,e),g(d,c))) -> a
g(b,g(g(c,d),g(b,e))) -> a
g(b,g(g(c,d),g(e,b))) -> a
g(b,g(g(d,c),g(b,e))) -> a
g(b,g(g(d,c),g(e,b))) -> a
g(b,g(g(e,b),g(c,d))) -> a
g(b,g(g(e,b),g(d,c))) -> a
g(y,a) -> g(b,b)
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 g(g(g(b,e),g(c,d)),b) -> a
 g(g(g(b,e),g(d,c)),b) -> a
 g(g(g(c,d),g(b,e)),b) -> a
 g(g(g(c,d),g(e,b)),b) -> a
 g(g(g(d,c),g(b,e)),b) -> a
 g(g(g(d,c),g(e,b)),b) -> a
 g(g(g(e,b),g(c,d)),b) -> a
 g(g(g(e,b),g(d,c)),b) -> a
 g(a,y) -> g(b,b)
 g(b,g(g(b,e),g(c,d))) -> a
 g(b,g(g(b,e),g(d,c))) -> a
 g(b,g(g(c,d),g(b,e))) -> a
 g(b,g(g(c,d),g(e,b))) -> a
 g(b,g(g(d,c),g(b,e))) -> a
 g(b,g(g(d,c),g(e,b))) -> a
 g(b,g(g(e,b),g(c,d))) -> a
 g(b,g(g(e,b),g(d,c))) -> a
 g(y,a) -> g(b,b)
-> Vars:
 y, y

-> Rlps:
 (rule: g(g(g(b,e),g(c,d)),b) -> a, id: 1, possubterms: g(g(g(b,e),g(c,d)),b)->[], g(g(b,e),g(c,d))->[1], g(b,e)->[1, 1], b->[1, 1, 1], e->[1, 1, 2], g(c,d)->[1, 2], c->[1, 2, 1], d->[1, 2, 2], b->[2])
 (rule: g(g(g(b,e),g(d,c)),b) -> a, id: 2, possubterms: g(g(g(b,e),g(d,c)),b)->[], g(g(b,e),g(d,c))->[1], g(b,e)->[1, 1], b->[1, 1, 1], e->[1, 1, 2], g(d,c)->[1, 2], d->[1, 2, 1], c->[1, 2, 2], b->[2])
 (rule: g(g(g(c,d),g(b,e)),b) -> a, id: 3, possubterms: g(g(g(c,d),g(b,e)),b)->[], g(g(c,d),g(b,e))->[1], g(c,d)->[1, 1], c->[1, 1, 1], d->[1, 1, 2], g(b,e)->[1, 2], b->[1, 2, 1], e->[1, 2, 2], b->[2])
 (rule: g(g(g(c,d),g(e,b)),b) -> a, id: 4, possubterms: g(g(g(c,d),g(e,b)),b)->[], g(g(c,d),g(e,b))->[1], g(c,d)->[1, 1], c->[1, 1, 1], d->[1, 1, 2], g(e,b)->[1, 2], e->[1, 2, 1], b->[1, 2, 2], b->[2])
 (rule: g(g(g(d,c),g(b,e)),b) -> a, id: 5, possubterms: g(g(g(d,c),g(b,e)),b)->[], g(g(d,c),g(b,e))->[1], g(d,c)->[1, 1], d->[1, 1, 1], c->[1, 1, 2], g(b,e)->[1, 2], b->[1, 2, 1], e->[1, 2, 2], b->[2])
 (rule: g(g(g(d,c),g(e,b)),b) -> a, id: 6, possubterms: g(g(g(d,c),g(e,b)),b)->[], g(g(d,c),g(e,b))->[1], g(d,c)->[1, 1], d->[1, 1, 1], c->[1, 1, 2], g(e,b)->[1, 2], e->[1, 2, 1], b->[1, 2, 2], b->[2])
 (rule: g(g(g(e,b),g(c,d)),b) -> a, id: 7, possubterms: g(g(g(e,b),g(c,d)),b)->[], g(g(e,b),g(c,d))->[1], g(e,b)->[1, 1], e->[1, 1, 1], b->[1, 1, 2], g(c,d)->[1, 2], c->[1, 2, 1], d->[1, 2, 2], b->[2])
 (rule: g(g(g(e,b),g(d,c)),b) -> a, id: 8, possubterms: g(g(g(e,b),g(d,c)),b)->[], g(g(e,b),g(d,c))->[1], g(e,b)->[1, 1], e->[1, 1, 1], b->[1, 1, 2], g(d,c)->[1, 2], d->[1, 2, 1], c->[1, 2, 2], b->[2])
 (rule: g(a,y) -> g(b,b), id: 9, possubterms: g(a,y)->[], a->[1])
 (rule: g(b,g(g(b,e),g(c,d))) -> a, id: 10, possubterms: g(b,g(g(b,e),g(c,d)))->[], b->[1], g(g(b,e),g(c,d))->[2], g(b,e)->[2, 1], b->[2, 1, 1], e->[2, 1, 2], g(c,d)->[2, 2], c->[2, 2, 1], d->[2, 2, 2])
 (rule: g(b,g(g(b,e),g(d,c))) -> a, id: 11, possubterms: g(b,g(g(b,e),g(d,c)))->[], b->[1], g(g(b,e),g(d,c))->[2], g(b,e)->[2, 1], b->[2, 1, 1], e->[2, 1, 2], g(d,c)->[2, 2], d->[2, 2, 1], c->[2, 2, 2])
 (rule: g(b,g(g(c,d),g(b,e))) -> a, id: 12, possubterms: g(b,g(g(c,d),g(b,e)))->[], b->[1], g(g(c,d),g(b,e))->[2], g(c,d)->[2, 1], c->[2, 1, 1], d->[2, 1, 2], g(b,e)->[2, 2], b->[2, 2, 1], e->[2, 2, 2])
 (rule: g(b,g(g(c,d),g(e,b))) -> a, id: 13, possubterms: g(b,g(g(c,d),g(e,b)))->[], b->[1], g(g(c,d),g(e,b))->[2], g(c,d)->[2, 1], c->[2, 1, 1], d->[2, 1, 2], g(e,b)->[2, 2], e->[2, 2, 1], b->[2, 2, 2])
 (rule: g(b,g(g(d,c),g(b,e))) -> a, id: 14, possubterms: g(b,g(g(d,c),g(b,e)))->[], b->[1], g(g(d,c),g(b,e))->[2], g(d,c)->[2, 1], d->[2, 1, 1], c->[2, 1, 2], g(b,e)->[2, 2], b->[2, 2, 1], e->[2, 2, 2])
 (rule: g(b,g(g(d,c),g(e,b))) -> a, id: 15, possubterms: g(b,g(g(d,c),g(e,b)))->[], b->[1], g(g(d,c),g(e,b))->[2], g(d,c)->[2, 1], d->[2, 1, 1], c->[2, 1, 2], g(e,b)->[2, 2], e->[2, 2, 1], b->[2, 2, 2])
 (rule: g(b,g(g(e,b),g(c,d))) -> a, id: 16, possubterms: g(b,g(g(e,b),g(c,d)))->[], b->[1], g(g(e,b),g(c,d))->[2], g(e,b)->[2, 1], e->[2, 1, 1], b->[2, 1, 2], g(c,d)->[2, 2], c->[2, 2, 1], d->[2, 2, 2])
 (rule: g(b,g(g(e,b),g(d,c))) -> a, id: 17, possubterms: g(b,g(g(e,b),g(d,c)))->[], b->[1], g(g(e,b),g(d,c))->[2], g(e,b)->[2, 1], e->[2, 1, 1], b->[2, 1, 2], g(d,c)->[2, 2], d->[2, 2, 1], c->[2, 2, 2])
 (rule: g(y,a) -> g(b,b), id: 18, possubterms: g(y,a)->[], a->[2])

-> Unifications:
(R18 unifies with R9 at p: [], l: g(y,a), lp: g(y,a), sig: {y -> a,y' -> a}, l': g(a,y'), r: g(b,b), r': g(b,b))

-> Critical pairs info:
<g(b,b),g(b,b)>   =>  Trivial, Overlay, Proper, NW0, N1

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


The problem is confluent.