YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(F 1, 2)
(H 1)
(G 1)
(I 1)
(fSNonEmpty)
)
(RULES
F(H(x),y) -> G(H(x))
F(I(x),y) -> G(I(x))
H(I(x)) -> I(x)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


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
(F 1, 2)
(H 1)
(G 1)
(I 1)
(fSNonEmpty)
)
(RULES
F(H(x),y) -> G(H(x))
F(I(x),y) -> G(I(x))
H(I(x)) -> I(x)
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 F(H(x),y) -> G(H(x))
 F(I(x),y) -> G(I(x))
 H(I(x)) -> I(x)
-> Vars:
 x, y, x, y, x

-> Rlps:
 (rule: F(H(x),y) -> G(H(x)), id: 1, possubterms: F(H(x),y)->[], H(x)->[1])
 (rule: F(I(x),y) -> G(I(x)), id: 2, possubterms: F(I(x),y)->[], I(x)->[1])
 (rule: H(I(x)) -> I(x), id: 3, possubterms: H(I(x))->[], I(x)->[1])

-> Unifications:
(R1 unifies with R3 at p: [1], l: F(H(x),y), lp: H(x), sig: {x -> I(x')}, l': H(I(x')), r: G(H(x)), r': I(x'))

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

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

The problem is confluent.