YES

Problem 1: 


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


Problem 1: 

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

Problem 1: 
CSR Converter From Canonical u-Replacement Map Procedure [CSUR20]:

Original Replacement Map:
(f 1)
(g 1)
(h 1)
(fSNonEmpty)

New Replacement Map:
(f 1)
(g 1)
(h)
(fSNonEmpty)

New problem:

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


Problem 1: 
Termination Procedure:
Terminating?
YES

Problem 1: 

(VAR vu95NonEmpty vNonEmpty x)
(STRATEGY CONTEXTSENSITIVE
(f 1)
(g 1)
(h)
(fSNonEmpty)
)
(RULES
f(g(h(x))) -> g(f(h(g(x))))
f(x) -> x
g(x) -> x
h(x) -> x
)

Problem 1: 

Dependency Pairs Processor:
-> Pairs:
 F(g(h(x))) -> F(h(g(x)))
 F(g(h(x))) -> G(f(h(g(x))))
 F(g(h(x))) -> H(g(x))
 H(x) -> x
-> Rules:
 f(g(h(x))) -> g(f(h(g(x))))
 f(x) -> x
 g(x) -> x
 h(x) -> x
-> Unhiding Rules:
 g(x) -> G(x)
 g(x3) -> x3

Problem 1: 

SCC Processor:
-> Pairs:
 F(g(h(x))) -> F(h(g(x)))
 F(g(h(x))) -> G(f(h(g(x))))
 F(g(h(x))) -> H(g(x))
 H(x) -> x
-> Rules:
 f(g(h(x))) -> g(f(h(g(x))))
 f(x) -> x
 g(x) -> x
 h(x) -> x
-> Unhiding rules:
 g(x) -> G(x)
 g(x3) -> x3
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 F(g(h(x))) -> F(h(g(x)))
->->-> Rules:
 f(g(h(x))) -> g(f(h(g(x))))
 f(x) -> x
 g(x) -> x
 h(x) -> x
->->-> Unhiding rules:
 Empty

Problem 1: 

Reduction Triple Processor:
-> Pairs:
 F(g(h(x))) -> F(h(g(x)))
-> Rules:
 f(g(h(x))) -> g(f(h(g(x))))
 f(x) -> x
 g(x) -> x
 h(x) -> x
-> Unhiding rules:
 Empty
-> Usable rules:
 g(x) -> x
 h(x) -> x
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[f](X) = 0
[g](X) = 2.X
[h](X) = 2.X + 2
[fSNonEmpty] = 0
[F](X) = 2.X
[G](X) = 0
[H](X) = 0

Problem 1: 

Basic Processor:
-> Pairs:
 Empty
-> Rules:
 f(g(h(x))) -> g(f(h(g(x))))
 f(x) -> x
 g(x) -> x
 h(x) -> x
-> Unhiding rules:
 Empty
-> Result:
 Set P is empty

The problem is finite.


Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(f 1)
(g 1)
(h)
(fSNonEmpty)
)
(RULES
f(g(h(x))) -> g(f(h(g(x))))
f(x) -> x
g(x) -> x
h(x) -> x
)
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy NW Procedure:
-> Rules:
 f(g(h(x))) -> g(f(h(g(x))))
 f(x) -> x
 g(x) -> x
 h(x) -> x
-> Vars:
 x, x, x, x
-> UVars:
 (UV-RuleId: 1, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: [])
 (UV-RuleId: 2, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: [])
 (UV-RuleId: 3, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: [])
 (UV-RuleId: 4, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: [])

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

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

-> Critical pairs info:
<f(g(x')),g(f(h(g(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<g(f(h(g(x')))),g(h(x'))>   =>  Not trivial, Overlay, Proper, NW0, N2
<f(h(x)),g(f(h(g(x))))>   =>  Not trivial, Not overlay, Proper, NW0, N3

-> 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 CS-TRS, Left-homogeneous u-replacing variables



The problem is decomposed in 3 subproblems.

Problem 1.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(f 1)
(g 1)
(h)
(fSNonEmpty)
)
(RULES
f(g(h(x))) -> g(f(h(g(x))))
f(x) -> x
g(x) -> x
h(x) -> x
)
Critical Pairs:
<f(g(x')),g(f(h(g(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N1
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: f(g(x'))
Nodes: [0,1,2,3]
Edges: [(0,1),(0,2),(1,3),(2,3)]
ID: 0 => ('f(g(x'))', D0)
ID: 1 => ('g(x')', D1, R2, P[], S{x5 -> g(x')}), NR: 'g(x')'
ID: 2 => ('f(x')', D1, R3, P[1], S{x6 -> x'}), NR: 'x''
ID: 3 => ('x'', D2, R3, P[], S{x6 -> x'}), NR: 'x''
t: g(f(h(g(x'))))
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
Edges: [(0,1),(0,2),(0,3),(0,4),(1,5),(1,6),(1,7),(2,5),(2,8),(2,9),(3,6),(3,8),(3,10),(4,7),(4,9),(4,10),(5,11),(5,12),(6,11),(6,12),(7,12),(7,12),(8,11),(8,13),(9,12),(9,13),(10,12),(10,13),(11,14),(12,14),(13,14)]
ID: 0 => ('g(f(h(g(x'))))', D0)
ID: 1 => ('g(h(g(x')))', D1, R2, P[1], S{x5 -> h(g(x'))}), NR: 'h(g(x'))'
ID: 2 => ('f(h(g(x')))', D1, R3, P[], S{x6 -> f(h(g(x')))}), NR: 'f(h(g(x')))'
ID: 3 => ('g(f(h(x')))', D1, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'x''
ID: 4 => ('g(f(g(x')))', D1, R4, P[1, 1], S{x7 -> g(x')}), NR: 'g(x')'
ID: 5 => ('h(g(x'))', D2, R3, P[], S{x6 -> h(g(x'))}), NR: 'h(g(x'))'
ID: 6 => ('g(h(x'))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'x''
ID: 7 => ('g(g(x'))', D2, R4, P[1], S{x7 -> g(x')}), NR: 'g(x')'
ID: 8 => ('f(h(x'))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'x''
ID: 9 => ('f(g(x'))', D2, R4, P[1], S{x7 -> g(x')}), NR: 'g(x')'
ID: 10 => ('g(f(x'))', D2, R4, P[1, 1], S{x7 -> x'}), NR: 'x''
ID: 11 => ('h(x')', D3, R3, P[1], S{x6 -> x'}), NR: 'x''
ID: 12 => ('g(x')', D3, R4, P[], S{x7 -> g(x')}), NR: 'g(x')'
ID: 13 => ('f(x')', D3, R4, P[1], S{x7 -> x'}), NR: 'x''
ID: 14 => ('x'', D4, R4, P[], S{x7 -> x'}), NR: 'x''
SNodesPath: f(g(x'))
TNodesPath: 
f(g(x')) ->* f(g(x')) *<- g(f(h(g(x'))))
"Joinable"

The problem is confluent.

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(f 1)
(g 1)
(h)
(fSNonEmpty)
)
(RULES
f(g(h(x))) -> g(f(h(g(x))))
f(x) -> x
g(x) -> x
h(x) -> x
)
Critical Pairs:
<g(f(h(g(x')))),g(h(x'))>   =>  Not trivial, Overlay, Proper, NW0, N2
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: g(f(h(g(x'))))
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
Edges: [(0,1),(0,2),(0,3),(0,4),(1,5),(1,6),(1,7),(2,5),(2,8),(2,9),(3,6),(3,8),(3,10),(4,7),(4,9),(4,10),(5,11),(5,12),(6,11),(6,12),(7,12),(7,12),(8,11),(8,13),(9,12),(9,13),(10,12),(10,13),(11,14),(12,14),(13,14)]
ID: 0 => ('g(f(h(g(x'))))', D0)
ID: 1 => ('g(h(g(x')))', D1, R2, P[1], S{x5 -> h(g(x'))}), NR: 'h(g(x'))'
ID: 2 => ('f(h(g(x')))', D1, R3, P[], S{x6 -> f(h(g(x')))}), NR: 'f(h(g(x')))'
ID: 3 => ('g(f(h(x')))', D1, R3, P[1, 1, 1], S{x6 -> x'}), NR: 'x''
ID: 4 => ('g(f(g(x')))', D1, R4, P[1, 1], S{x7 -> g(x')}), NR: 'g(x')'
ID: 5 => ('h(g(x'))', D2, R3, P[], S{x6 -> h(g(x'))}), NR: 'h(g(x'))'
ID: 6 => ('g(h(x'))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'x''
ID: 7 => ('g(g(x'))', D2, R4, P[1], S{x7 -> g(x')}), NR: 'g(x')'
ID: 8 => ('f(h(x'))', D2, R3, P[1, 1], S{x6 -> x'}), NR: 'x''
ID: 9 => ('f(g(x'))', D2, R4, P[1], S{x7 -> g(x')}), NR: 'g(x')'
ID: 10 => ('g(f(x'))', D2, R4, P[1, 1], S{x7 -> x'}), NR: 'x''
ID: 11 => ('h(x')', D3, R3, P[1], S{x6 -> x'}), NR: 'x''
ID: 12 => ('g(x')', D3, R4, P[], S{x7 -> g(x')}), NR: 'g(x')'
ID: 13 => ('f(x')', D3, R4, P[1], S{x7 -> x'}), NR: 'x''
ID: 14 => ('x'', D4, R4, P[], S{x7 -> x'}), NR: 'x''
t: g(h(x'))
Nodes: [0,1,2,3]
Edges: [(0,1),(0,2),(1,3),(2,3)]
ID: 0 => ('g(h(x'))', D0)
ID: 1 => ('h(x')', D1, R3, P[], S{x6 -> h(x')}), NR: 'h(x')'
ID: 2 => ('g(x')', D1, R4, P[1], S{x7 -> x'}), NR: 'x''
ID: 3 => ('x'', D2, R4, P[], S{x7 -> x'}), NR: 'x''
SNodesPath: 
TNodesPath: g(h(x'))
g(f(h(g(x')))) ->* g(h(x')) *<- g(h(x'))
"Joinable"

The problem is confluent.

Problem 1.3: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(f 1)
(g 1)
(h)
(fSNonEmpty)
)
(RULES
f(g(h(x))) -> g(f(h(g(x))))
f(x) -> x
g(x) -> x
h(x) -> x
)
Critical Pairs:
<f(h(x)),g(f(h(g(x))))>   =>  Not trivial, Not overlay, Proper, NW0, N3
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: f(h(x))
Nodes: [0,1,2,3]
Edges: [(0,1),(0,2),(1,3),(2,3)]
ID: 0 => ('f(h(x))', D0)
ID: 1 => ('h(x)', D1, R2, P[], S{x5 -> h(x)}), NR: 'h(x)'
ID: 2 => ('f(x)', D1, R4, P[1], S{x7 -> x}), NR: 'x'
ID: 3 => ('x', D2, R4, P[], S{x7 -> x}), NR: 'x'
t: g(f(h(g(x))))
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
Edges: [(0,1),(0,2),(0,3),(0,4),(1,5),(1,6),(1,7),(2,5),(2,8),(2,9),(3,6),(3,8),(3,10),(4,7),(4,9),(4,10),(5,11),(5,12),(6,11),(6,12),(7,12),(7,12),(8,11),(8,13),(9,12),(9,13),(10,12),(10,13),(11,14),(12,14),(13,14)]
ID: 0 => ('g(f(h(g(x))))', D0)
ID: 1 => ('g(h(g(x)))', D1, R2, P[1], S{x5 -> h(g(x))}), NR: 'h(g(x))'
ID: 2 => ('f(h(g(x)))', D1, R3, P[], S{x6 -> f(h(g(x)))}), NR: 'f(h(g(x)))'
ID: 3 => ('g(f(h(x)))', D1, R3, P[1, 1, 1], S{x6 -> x}), NR: 'x'
ID: 4 => ('g(f(g(x)))', D1, R4, P[1, 1], S{x7 -> g(x)}), NR: 'g(x)'
ID: 5 => ('h(g(x))', D2, R3, P[], S{x6 -> h(g(x))}), NR: 'h(g(x))'
ID: 6 => ('g(h(x))', D2, R3, P[1, 1], S{x6 -> x}), NR: 'x'
ID: 7 => ('g(g(x))', D2, R4, P[1], S{x7 -> g(x)}), NR: 'g(x)'
ID: 8 => ('f(h(x))', D2, R3, P[1, 1], S{x6 -> x}), NR: 'x'
ID: 9 => ('f(g(x))', D2, R4, P[1], S{x7 -> g(x)}), NR: 'g(x)'
ID: 10 => ('g(f(x))', D2, R4, P[1, 1], S{x7 -> x}), NR: 'x'
ID: 11 => ('h(x)', D3, R3, P[1], S{x6 -> x}), NR: 'x'
ID: 12 => ('g(x)', D3, R4, P[], S{x7 -> g(x)}), NR: 'g(x)'
ID: 13 => ('f(x)', D3, R4, P[1], S{x7 -> x}), NR: 'x'
ID: 14 => ('x', D4, R4, P[], S{x7 -> x}), NR: 'x'
SNodesPath: f(h(x))
TNodesPath: 
f(h(x)) ->* f(h(x)) *<- g(f(h(g(x))))
"Joinable"

The problem is confluent.