YES

Problem 1: 


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


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)
(RULES
f(f(f(x))) -> a
f(f(g(g(x)))) -> f(a)
f(f(a)) -> a
f(a) -> a
g(f(a)) -> a
g(a) -> a
)

Problem 1: 

Dependency Pairs Processor:
-> Pairs:
 F(f(g(g(x)))) -> F(a)
-> Rules:
 f(f(f(x))) -> a
 f(f(g(g(x)))) -> f(a)
 f(f(a)) -> a
 f(a) -> a
 g(f(a)) -> a
 g(a) -> a

Problem 1: 

SCC Processor:
-> Pairs:
 F(f(g(g(x)))) -> F(a)
-> Rules:
 f(f(f(x))) -> a
 f(f(g(g(x)))) -> f(a)
 f(f(a)) -> a
 f(a) -> a
 g(f(a)) -> a
 g(a) -> a
->Strongly Connected Components:
 There is no strongly connected component

The problem is finite.


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

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

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

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

-> Critical pairs info:
<f(f(a)),a>   =>  Not trivial, Not overlay, Proper, NW1, N1
<f(a),a>   =>  Not trivial, Not overlay, Proper, NW1, N2
<f(f(a)),a>   =>  Not trivial, Not overlay, Proper, NW1, N3
<f(f(a)),a>   =>  Not trivial, Not overlay, Proper, NW1, N4
<f(f(a)),a>   =>  Not trivial, Not overlay, Proper, NW1, N5
<f(a),a>   =>  Not trivial, Not overlay, Proper, NW1, N6
<g(a),a>   =>  Not trivial, Not overlay, Proper, NW1, N7
<f(f(f(a))),a>   =>  Not trivial, Not overlay, Proper, NW1, N8
<f(a),a>   =>  Not trivial, Not overlay, Proper, NW1, N9
<f(f(g(a))),f(a)>   =>  Not trivial, Not overlay, Proper, NW0, N10
<f(f(g(a))),f(a)>   =>  Not trivial, Not overlay, Proper, NW0, N11

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

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

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: f(f(a))
Nodes: [0,1,2]
Edges: [(0,1),(0,2),(2,1)]
ID: 0 => ('f(f(a))', D0)
ID: 1 => ('a', D1, R3, P[], S{}), NR: 'a'
ID: 2 => ('f(a)', D1, R4, P[1], S{}), NR: 'a'
t: a
Nodes: [0]
Edges: []
ID: 0 => ('a', D0)
SNodesPath: f(f(a)) -> a
TNodesPath: a
f(f(a)) ->* a *<- a
"Joinable"

The problem is confluent.

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(f 1)
(g 1)
(a)
(fSNonEmpty)
)
(RULES
f(f(f(x))) -> a
f(f(g(g(x)))) -> f(a)
f(f(a)) -> a
f(a) -> a
g(f(a)) -> a
g(a) -> a
)
Critical Pairs:
<g(a),a>   =>  Not trivial, Not overlay, Proper, NW1, N7
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: g(a)
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('g(a)', D0)
ID: 1 => ('a', D1, R6, P[], S{}), NR: 'a'
t: a
Nodes: [0]
Edges: []
ID: 0 => ('a', D0)
SNodesPath: g(a) -> a
TNodesPath: a
g(a) ->* a *<- a
"Joinable"

The problem is confluent.

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

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: f(f(f(a)))
Nodes: [0,1,2,3]
Edges: [(0,1),(0,2),(0,3),(2,1),(3,1),(3,2)]
ID: 0 => ('f(f(f(a)))', D0)
ID: 1 => ('a', D1, R1, P[], S{x2 -> a}), NR: 'a'
ID: 2 => ('f(a)', D1, R3, P[1], S{}), NR: 'a'
ID: 3 => ('f(f(a))', D1, R4, P[1, 1], S{}), NR: 'a'
t: a
Nodes: [0]
Edges: []
ID: 0 => ('a', D0)
SNodesPath: f(f(f(a))) -> a
TNodesPath: a
f(f(f(a))) ->* a *<- a
"Joinable"

The problem is confluent.

Problem 1.4: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(f 1)
(g 1)
(a)
(fSNonEmpty)
)
(RULES
f(f(f(x))) -> a
f(f(g(g(x)))) -> f(a)
f(f(a)) -> a
f(a) -> a
g(f(a)) -> a
g(a) -> a
)
Critical Pairs:
<f(a),a>   =>  Not trivial, Not overlay, Proper, NW1, N9
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: f(a)
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('f(a)', D0)
ID: 1 => ('a', D1, R4, P[], S{}), NR: 'a'
t: a
Nodes: [0]
Edges: []
ID: 0 => ('a', D0)
SNodesPath: f(a) -> a
TNodesPath: a
f(a) ->* a *<- a
"Joinable"

The problem is confluent.

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

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: f(f(g(a)))
Nodes: [0,1,2,3]
Edges: [(0,1),(1,2),(1,3),(3,2)]
ID: 0 => ('f(f(g(a)))', D0)
ID: 1 => ('f(f(a))', D1, R6, P[1, 1], S{}), NR: 'a'
ID: 2 => ('a', D2, R3, P[], S{}), NR: 'a'
ID: 3 => ('f(a)', D2, R4, P[1], S{}), NR: 'a'
t: f(a)
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('f(a)', D0)
ID: 1 => ('a', D1, R4, P[], S{}), NR: 'a'
SNodesPath: f(f(g(a))) -> f(f(a)) -> a
TNodesPath: f(a) -> a
f(f(g(a))) ->* a *<- f(a)
"Joinable"

The problem is confluent.