YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y z)
(REPLACEMENT-MAP
(F 1, 2)
(H 1)
(Q 1, 2)
(G 1, 2)
(K 1, 2)
(P 1)
(R 1)
(fSNonEmpty)
)
(RULES
F(x,K(y,z)) -> G(P(y),Q(z,x))
H(F(x,y)) -> F(H(R(x)),y)
H(Q(x,y)) -> Q(x,H(R(y)))
H(G(x,y)) -> G(x,H(y))
Q(x,H(R(y))) -> H(Q(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 z)
(REPLACEMENT-MAP
(F 1, 2)
(H 1)
(Q 1, 2)
(G 1, 2)
(K 1, 2)
(P 1)
(R 1)
(fSNonEmpty)
)
(RULES
F(x,K(y,z)) -> G(P(y),Q(z,x))
H(F(x,y)) -> F(H(R(x)),y)
H(Q(x,y)) -> Q(x,H(R(y)))
H(G(x,y)) -> G(x,H(y))
Q(x,H(R(y))) -> H(Q(x,y))
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 F(x,K(y,z)) -> G(P(y),Q(z,x))
 H(F(x,y)) -> F(H(R(x)),y)
 H(Q(x,y)) -> Q(x,H(R(y)))
 H(G(x,y)) -> G(x,H(y))
 Q(x,H(R(y))) -> H(Q(x,y))
-> Vars:
 x, y, z, x, y, x, y, x, y, x, y

-> Rlps:
 (rule: F(x,K(y,z)) -> G(P(y),Q(z,x)), id: 1, possubterms: F(x,K(y,z))->[], K(y,z)->[2])
 (rule: H(F(x,y)) -> F(H(R(x)),y), id: 2, possubterms: H(F(x,y))->[], F(x,y)->[1])
 (rule: H(Q(x,y)) -> Q(x,H(R(y))), id: 3, possubterms: H(Q(x,y))->[], Q(x,y)->[1])
 (rule: H(G(x,y)) -> G(x,H(y)), id: 4, possubterms: H(G(x,y))->[], G(x,y)->[1])
 (rule: Q(x,H(R(y))) -> H(Q(x,y)), id: 5, possubterms: Q(x,H(R(y)))->[], H(R(y))->[2], R(y)->[2, 1])

-> Unifications:
(R2 unifies with R1 at p: [1], l: H(F(x,y)), lp: F(x,y), sig: {x -> x',y -> K(y',z)}, l': F(x',K(y',z)), r: F(H(R(x)),y), r': G(P(y'),Q(z,x')))
(R3 unifies with R5 at p: [1], l: H(Q(x,y)), lp: Q(x,y), sig: {x -> x',y -> H(R(y'))}, l': Q(x',H(R(y'))), r: Q(x,H(R(y))), r': H(Q(x',y')))

-> Critical pairs info:
<H(G(P(y'),Q(z,x'))),F(H(R(x')),K(y',z))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<H(H(Q(x',y'))),Q(x',H(R(H(R(y')))))>   =>  Not trivial, Not overlay, Proper, NW0, N2

-> 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 



The problem is decomposed in 2 subproblems.

Problem 1.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y z x' y' z)
(REPLACEMENT-MAP
(F 1, 2)
(H 1)
(Q 1, 2)
(G 1, 2)
(K 1, 2)
(P 1)
(R 1)
(fSNonEmpty)
)
(RULES
F(x,K(y,z)) -> G(P(y),Q(z,x))
H(F(x,y)) -> F(H(R(x)),y)
H(Q(x,y)) -> Q(x,H(R(y)))
H(G(x,y)) -> G(x,H(y))
Q(x,H(R(y))) -> H(Q(x,y))
)
Critical Pairs:
<H(G(P(y'),Q(z,x'))),F(H(R(x')),K(y',z))>   =>  Not trivial, Not overlay, Proper, NW0, N1
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: H(G(P(y'),Q(z,x')))
Nodes: [0,1,2]
Edges: [(0,1),(1,2),(2,1)]
ID: 0 => ('H(G(P(y'),Q(z,x')))', D0)
ID: 1 => ('G(P(y'),H(Q(z,x')))', D1, R4, P[], S{x15 -> P(y'), x16 -> Q(z,x')}), NR: 'G(P(y'),H(Q(z,x')))'
ID: 2 => ('G(P(y'),Q(z,H(R(x'))))', D2, R3, P[2], S{x13 -> z, x14 -> x'}), NR: 'Q(z,H(R(x')))'
t: F(H(R(x')),K(y',z))
Nodes: [0,1,2]
Edges: [(0,1),(1,2),(2,1)]
ID: 0 => ('F(H(R(x')),K(y',z))', D0)
ID: 1 => ('G(P(y'),Q(z,H(R(x'))))', D1, R1, P[], S{x8 -> H(R(x')), x9 -> y', x10 -> z}), NR: 'G(P(y'),Q(z,H(R(x'))))'
ID: 2 => ('G(P(y'),H(Q(z,x')))', D2, R5, P[2], S{x17 -> z, x18 -> x'}), NR: 'H(Q(z,x'))'
SNodesPath1: H(G(P(y'),Q(z,x'))) -> G(P(y'),H(Q(z,x')))
TNodesPath1: F(H(R(x')),K(y',z)) -> G(P(y'),Q(z,H(R(x')))) -> G(P(y'),H(Q(z,x')))
SNodesPath2: H(G(P(y'),Q(z,x'))) -> G(P(y'),H(Q(z,x'))) -> G(P(y'),Q(z,H(R(x'))))
TNodesPath2: F(H(R(x')),K(y',z)) -> G(P(y'),Q(z,H(R(x'))))
H(G(P(y'),Q(z,x'))) ->= G(P(y'),H(Q(z,x'))) *<- F(H(R(x')),K(y',z))
F(H(R(x')),K(y',z)) ->= G(P(y'),Q(z,H(R(x')))) *<- H(G(P(y'),Q(z,x')))
"Strongly closed critical pair"

The problem is confluent.

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y z x' y' z)
(REPLACEMENT-MAP
(F 1, 2)
(H 1)
(Q 1, 2)
(G 1, 2)
(K 1, 2)
(P 1)
(R 1)
(fSNonEmpty)
)
(RULES
F(x,K(y,z)) -> G(P(y),Q(z,x))
H(F(x,y)) -> F(H(R(x)),y)
H(Q(x,y)) -> Q(x,H(R(y)))
H(G(x,y)) -> G(x,H(y))
Q(x,H(R(y))) -> H(Q(x,y))
)
Critical Pairs:
<H(H(Q(x',y'))),Q(x',H(R(H(R(y')))))>   =>  Not trivial, Not overlay, Proper, NW0, N2
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: H(H(Q(x',y')))
Nodes: [0,1,2]
Edges: [(0,1),(1,0),(1,2),(2,1)]
ID: 0 => ('H(H(Q(x',y')))', D0)
ID: 1 => ('H(Q(x',H(R(y'))))', D1, R3, P[1], S{x13 -> x', x14 -> y'}), NR: 'Q(x',H(R(y')))'
ID: 2 => ('Q(x',H(R(H(R(y')))))', D2, R3, P[], S{x13 -> x', x14 -> H(R(y'))}), NR: 'Q(x',H(R(H(R(y')))))'
t: Q(x',H(R(H(R(y')))))
Nodes: [0,1,2]
Edges: [(0,1),(1,0),(1,2),(2,1)]
ID: 0 => ('Q(x',H(R(H(R(y')))))', D0)
ID: 1 => ('H(Q(x',H(R(y'))))', D1, R5, P[], S{x17 -> x', x18 -> H(R(y'))}), NR: 'H(Q(x',H(R(y'))))'
ID: 2 => ('H(H(Q(x',y')))', D2, R5, P[1], S{x17 -> x', x18 -> y'}), NR: 'H(Q(x',y'))'
SNodesPath1: H(H(Q(x',y')))
TNodesPath1: Q(x',H(R(H(R(y'))))) -> H(Q(x',H(R(y')))) -> H(H(Q(x',y')))
SNodesPath2: H(H(Q(x',y'))) -> H(Q(x',H(R(y')))) -> Q(x',H(R(H(R(y')))))
TNodesPath2: Q(x',H(R(H(R(y')))))
H(H(Q(x',y'))) ->= H(H(Q(x',y'))) *<- Q(x',H(R(H(R(y')))))
Q(x',H(R(H(R(y'))))) ->= Q(x',H(R(H(R(y'))))) *<- H(H(Q(x',y')))
"Strongly closed critical pair"

The problem is confluent.