YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(F 1)
(G 1, 2, 3)
(K1 1)
(K2 1)
(A)
(B)
(C)
(D)
(H 1, 2)
(fSNonEmpty)
)
(RULES
F(G(x,A,B)) -> x
G(F(H(C,D)),x,y) -> H(K1(x),K2(y))
K1(A) -> C
K2(B) -> D
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
Termination Procedure:
Terminating?
YES

Problem 1: 

(VAR vu95NonEmpty vNonEmpty x y)
(RULES
F(G(x,A,B)) -> x
G(F(H(C,D)),x,y) -> H(K1(x),K2(y))
K1(A) -> C
K2(B) -> D
)

Problem 1: 

Dependency Pairs Processor:
-> Pairs:
 GSharp(F(H(C,D)),x,y) -> K1Sharp(x)
 GSharp(F(H(C,D)),x,y) -> K2Sharp(y)
-> Rules:
 F(G(x,A,B)) -> x
 G(F(H(C,D)),x,y) -> H(K1(x),K2(y))
 K1(A) -> C
 K2(B) -> D

Problem 1: 

SCC Processor:
-> Pairs:
 GSharp(F(H(C,D)),x,y) -> K1Sharp(x)
 GSharp(F(H(C,D)),x,y) -> K2Sharp(y)
-> Rules:
 F(G(x,A,B)) -> x
 G(F(H(C,D)),x,y) -> H(K1(x),K2(y))
 K1(A) -> C
 K2(B) -> D
->Strongly Connected Components:
 There is no strongly connected component

The problem is finite.


Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(F 1)
(G 1, 2, 3)
(K1 1)
(K2 1)
(A)
(B)
(C)
(D)
(H 1, 2)
(fSNonEmpty)
)
(RULES
F(G(x,A,B)) -> x
G(F(H(C,D)),x,y) -> H(K1(x),K2(y))
K1(A) -> C
K2(B) -> D
)
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy NW Procedure:
-> Rules:
 F(G(x,A,B)) -> x
 G(F(H(C,D)),x,y) -> H(K1(x),K2(y))
 K1(A) -> C
 K2(B) -> D
-> Vars:
 x, x, y

-> Rlps:
 (rule: F(G(x,A,B)) -> x, id: 1, possubterms: F(G(x,A,B))->[], G(x,A,B)->[1], A->[1, 2], B->[1, 3])
 (rule: G(F(H(C,D)),x,y) -> H(K1(x),K2(y)), id: 2, possubterms: G(F(H(C,D)),x,y)->[], F(H(C,D))->[1], H(C,D)->[1, 1], C->[1, 1, 1], D->[1, 1, 2])
 (rule: K1(A) -> C, id: 3, possubterms: K1(A)->[], A->[1])
 (rule: K2(B) -> D, id: 4, possubterms: K2(B)->[], B->[1])

-> Unifications:
(R1 unifies with R2 at p: [1], l: F(G(x,A,B)), lp: G(x,A,B), sig: {x -> F(H(C,D)),x' -> A,y -> B}, l': G(F(H(C,D)),x',y), r: x, r': H(K1(x'),K2(y)))

-> Critical pairs info:
<F(H(K1(A),K2(B))),F(H(C,D))>   =>  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)
(REPLACEMENT-MAP
(F 1)
(G 1, 2, 3)
(K1 1)
(K2 1)
(A)
(B)
(C)
(D)
(H 1, 2)
(fSNonEmpty)
)
(RULES
F(G(x,A,B)) -> x
G(F(H(C,D)),x,y) -> H(K1(x),K2(y))
K1(A) -> C
K2(B) -> D
)
Critical Pairs:
<F(H(K1(A),K2(B))),F(H(C,D))>   =>  Not trivial, Not overlay, Proper, NW0, N1
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: F(H(K1(A),K2(B)))
Nodes: [0,1,2,3]
Edges: [(0,1),(0,2),(1,3),(2,3)]
ID: 0 => ('F(H(K1(A),K2(B)))', D0)
ID: 1 => ('F(H(C,K2(B)))', D1, R3, P[1, 1], S{}), NR: 'C'
ID: 2 => ('F(H(K1(A),D))', D1, R4, P[1, 2], S{}), NR: 'D'
ID: 3 => ('F(H(C,D))', D2, R4, P[1, 2], S{}), NR: 'D'
t: F(H(C,D))
Nodes: [0]
Edges: []
ID: 0 => ('F(H(C,D))', D0)
SNodesPath: F(H(K1(A),K2(B))) -> F(H(C,K2(B))) -> F(H(C,D))
TNodesPath: F(H(C,D))
F(H(K1(A),K2(B))) ->* F(H(C,D)) *<- F(H(C,D))
"Joinable"

The problem is confluent.