YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(f 1)
(g 1)
(k 1)
(a)
(fSNonEmpty)
)
(RULES
f(x) -> g(k(x))
f(x) -> a
g(x) -> a
k(a) -> k(k(a))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


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)
(REPLACEMENT-MAP
(f 1)
(g 1)
(k 1)
(a)
(fSNonEmpty)
)
(RULES
f(x) -> g(k(x))
f(x) -> a
g(x) -> a
k(a) -> k(k(a))
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 f(x) -> g(k(x))
 f(x) -> a
 g(x) -> a
 k(a) -> k(k(a))
-> Vars:
 x, x, x

-> Rlps:
 (rule: f(x) -> g(k(x)), id: 1, possubterms: f(x)->[])
 (rule: f(x) -> a, id: 2, possubterms: f(x)->[])
 (rule: g(x) -> a, id: 3, possubterms: g(x)->[])
 (rule: k(a) -> k(k(a)), id: 4, possubterms: k(a)->[], a->[1])

-> Unifications:
(R2 unifies with R1 at p: [], l: f(x), lp: f(x), sig: {x -> x'}, l': f(x'), r: a, r': g(k(x')))

-> Critical pairs info:
<g(k(x')),a>   =>  Not trivial, 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 x')
(REPLACEMENT-MAP
(f 1)
(g 1)
(k 1)
(a)
(fSNonEmpty)
)
(RULES
f(x) -> g(k(x))
f(x) -> a
g(x) -> a
k(a) -> k(k(a))
)
Critical Pairs:
<g(k(x')),a>   =>  Not trivial, Overlay, Proper, NW0, N1
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

The problem is confluent.