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)
(fSNonEmpty)
(h 1, 2)
)
(RULES
f(g(x,a,b)) -> x
f(h(k1(a),k2(b))) -> f(h(c,d))
f(h(k1(a),d)) -> f(h(c,d))
f(h(c,k2(b))) -> f(h(c,d))
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: 
Linearity Procedure:
Linear?
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)
(fSNonEmpty)
(h 1, 2)
)
(RULES
f(g(x,a,b)) -> x
f(h(k1(a),k2(b))) -> f(h(c,d))
f(h(k1(a),d)) -> f(h(c,d))
f(h(c,k2(b))) -> f(h(c,d))
g(f(h(c,d)),x,y) -> h(k1(x),k2(y))
k1(a) -> c
k2(b) -> d
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 f(g(x,a,b)) -> x
 f(h(k1(a),k2(b))) -> f(h(c,d))
 f(h(k1(a),d)) -> f(h(c,d))
 f(h(c,k2(b))) -> f(h(c,d))
 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: f(h(k1(a),k2(b))) -> f(h(c,d)), id: 2, possubterms: f(h(k1(a),k2(b)))->[], h(k1(a),k2(b))->[1], k1(a)->[1, 1], a->[1, 1, 1], k2(b)->[1, 2], b->[1, 2, 1])
 (rule: f(h(k1(a),d)) -> f(h(c,d)), id: 3, possubterms: f(h(k1(a),d))->[], h(k1(a),d)->[1], k1(a)->[1, 1], a->[1, 1, 1], d->[1, 2])
 (rule: f(h(c,k2(b))) -> f(h(c,d)), id: 4, possubterms: f(h(c,k2(b)))->[], h(c,k2(b))->[1], c->[1, 1], k2(b)->[1, 2], b->[1, 2, 1])
 (rule: g(f(h(c,d)),x,y) -> h(k1(x),k2(y)), id: 5, 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: 6, possubterms: k1(a)->[], a->[1])
 (rule: k2(b) -> d, id: 7, possubterms: k2(b)->[], b->[1])

-> Unifications:
(R1 unifies with R5 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)))
(R2 unifies with R6 at p: [1,1], l: f(h(k1(a),k2(b))), lp: k1(a), sig: {}, l': k1(a), r: f(h(c,d)), r': c)
(R2 unifies with R7 at p: [1,2], l: f(h(k1(a),k2(b))), lp: k2(b), sig: {}, l': k2(b), r: f(h(c,d)), r': d)
(R3 unifies with R6 at p: [1,1], l: f(h(k1(a),d)), lp: k1(a), sig: {}, l': k1(a), r: f(h(c,d)), r': c)
(R4 unifies with R7 at p: [1,2], l: f(h(c,k2(b))), lp: k2(b), sig: {}, l': k2(b), r: f(h(c,d)), r': d)

-> Critical pairs info:
<f(h(k1(a),k2(b))),f(h(c,d))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<f(h(c,d)),f(h(c,d))>   =>  Trivial, Not overlay, Proper, NW0, N2
<f(h(k1(a),d)),f(h(c,d))>   =>  Not trivial, Not overlay, Proper, NW0, N3
<f(h(c,d)),f(h(c,d))>   =>  Trivial, Not overlay, Proper, NW0, N4
<f(h(c,k2(b))),f(h(c,d))>   =>  Not trivial, Not overlay, Proper, NW0, N5

-> 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 3 subproblems.

Problem 1.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y)
(REPLACEMENT-MAP
(f 1)
(g 1, 2, 3)
(k1 1)
(k2 1)
(a)
(b)
(c)
(d)
(fSNonEmpty)
(h 1, 2)
)
(RULES
f(g(x,a,b)) -> x
f(h(k1(a),k2(b))) -> f(h(c,d))
f(h(k1(a),d)) -> f(h(c,d))
f(h(c,k2(b))) -> f(h(c,d))
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
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: f(h(k1(a),k2(b)))
Nodes: [0,1,2,3]
Edges: [(0,1),(0,2),(0,3),(2,1),(2,1),(3,1),(3,1)]
ID: 0 => ('f(h(k1(a),k2(b)))', D0)
ID: 1 => ('f(h(c,d))', D1, R2, P[], S{}), NR: 'f(h(c,d))'
ID: 2 => ('f(h(c,k2(b)))', D1, R6, P[1, 1], S{}), NR: 'c'
ID: 3 => ('f(h(k1(a),d))', D1, R7, P[1, 2], S{}), NR: 'd'
t: f(h(c,d))
Nodes: [0]
Edges: []
ID: 0 => ('f(h(c,d))', D0)
SNodesPath1: f(h(k1(a),k2(b))) -> f(h(c,d))
TNodesPath1: f(h(c,d))
SNodesPath2: f(h(k1(a),k2(b))) -> f(h(c,d))
TNodesPath2: f(h(c,d))
f(h(k1(a),k2(b))) ->= f(h(c,d)) *<- f(h(c,d))
f(h(c,d)) ->= f(h(c,d)) *<- f(h(k1(a),k2(b)))
"Strongly closed critical pair"

The problem is confluent.

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y)
(REPLACEMENT-MAP
(f 1)
(g 1, 2, 3)
(k1 1)
(k2 1)
(a)
(b)
(c)
(d)
(fSNonEmpty)
(h 1, 2)
)
(RULES
f(g(x,a,b)) -> x
f(h(k1(a),k2(b))) -> f(h(c,d))
f(h(k1(a),d)) -> f(h(c,d))
f(h(c,k2(b))) -> f(h(c,d))
g(f(h(c,d)),x,y) -> h(k1(x),k2(y))
k1(a) -> c
k2(b) -> d
)
Critical Pairs:
<f(h(k1(a),d)),f(h(c,d))>   =>  Not trivial, Not overlay, Proper, NW0, N3
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: f(h(k1(a),d))
Nodes: [0,1]
Edges: [(0,1),(0,1)]
ID: 0 => ('f(h(k1(a),d))', D0)
ID: 1 => ('f(h(c,d))', D1, R3, P[], S{}), NR: 'f(h(c,d))'
t: f(h(c,d))
Nodes: [0]
Edges: []
ID: 0 => ('f(h(c,d))', D0)
SNodesPath1: f(h(k1(a),d)) -> f(h(c,d))
TNodesPath1: f(h(c,d))
SNodesPath2: f(h(k1(a),d)) -> f(h(c,d))
TNodesPath2: f(h(c,d))
f(h(k1(a),d)) ->= f(h(c,d)) *<- f(h(c,d))
f(h(c,d)) ->= f(h(c,d)) *<- f(h(k1(a),d))
"Strongly closed critical pair"

The problem is confluent.

Problem 1.3: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y)
(REPLACEMENT-MAP
(f 1)
(g 1, 2, 3)
(k1 1)
(k2 1)
(a)
(b)
(c)
(d)
(fSNonEmpty)
(h 1, 2)
)
(RULES
f(g(x,a,b)) -> x
f(h(k1(a),k2(b))) -> f(h(c,d))
f(h(k1(a),d)) -> f(h(c,d))
f(h(c,k2(b))) -> f(h(c,d))
g(f(h(c,d)),x,y) -> h(k1(x),k2(y))
k1(a) -> c
k2(b) -> d
)
Critical Pairs:
<f(h(c,k2(b))),f(h(c,d))>   =>  Not trivial, Not overlay, Proper, NW0, N5
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: f(h(c,k2(b)))
Nodes: [0,1]
Edges: [(0,1),(0,1)]
ID: 0 => ('f(h(c,k2(b)))', D0)
ID: 1 => ('f(h(c,d))', D1, R4, P[], S{}), NR: 'f(h(c,d))'
t: f(h(c,d))
Nodes: [0]
Edges: []
ID: 0 => ('f(h(c,d))', D0)
SNodesPath1: f(h(c,k2(b))) -> f(h(c,d))
TNodesPath1: f(h(c,d))
SNodesPath2: f(h(c,k2(b))) -> f(h(c,d))
TNodesPath2: f(h(c,d))
f(h(c,k2(b))) ->= f(h(c,d)) *<- f(h(c,d))
f(h(c,d)) ->= f(h(c,d)) *<- f(h(c,k2(b)))
"Strongly closed critical pair"

The problem is confluent.