YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(f 1)
(a)
(fSNonEmpty)
)
(RULES
f(a) -> f(f(a))
f(x) -> f(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)
(a)
(fSNonEmpty)
)
(RULES
f(a) -> f(f(a))
f(x) -> f(a)
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

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

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

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

Strong Confluence Procedure:
-> Rewritings:
s: f(f(a))
Nodes: [0,1,2,3,4,5,6,7,8,9]
Edges: [(0,0),(0,1),(0,2),(1,0),(1,1),(1,2),(1,3),(2,0),(2,2),(3,0),(3,1),(3,2),(3,3),(3,4),(4,0),(4,1),(4,2),(4,3),(4,4),(4,5),(5,0),(5,1),(5,2),(5,3),(5,4),(5,5),(5,6),(6,0),(6,1),(6,2),(6,3),(6,4),(6,5),(6,6),(6,7),(7,0),(7,1),(7,2),(7,3),(7,4),(7,5),(7,6),(7,7),(7,8),(8,0),(8,1),(8,2),(8,3),(8,4),(8,5),(8,6),(8,7),(8,8),(8,9)]
ID: 0 => ('f(f(a))', D0)
ID: 1 => ('f(f(f(a)))', D1, R1, P[1], S{}), NR: 'f(f(a))'
ID: 2 => ('f(a)', D1, R2, P[], S{x2 -> f(a)}), NR: 'f(a)'
ID: 3 => ('f(f(f(f(a))))', D2, R1, P[1, 1], S{}), NR: 'f(f(a))'
ID: 4 => ('f(f(f(f(f(a)))))', D3, R1, P[1, 1, 1], S{}), NR: 'f(f(a))'
ID: 5 => ('f(f(f(f(f(f(a))))))', D4, R1, P[1, 1, 1, 1], S{}), NR: 'f(f(a))'
ID: 6 => ('f(f(f(f(f(f(f(a)))))))', D5, R1, P[1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
ID: 7 => ('f(f(f(f(f(f(f(f(a))))))))', D6, R1, P[1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
ID: 8 => ('f(f(f(f(f(f(f(f(f(a)))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
ID: 9 => ('f(f(f(f(f(f(f(f(f(f(a))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
t: f(a)
Nodes: [0,1,2,3,4,5,6,7,8]
Edges: [(0,0),(0,1),(1,0),(1,1),(1,2),(2,0),(2,1),(2,2),(2,3),(3,0),(3,1),(3,2),(3,3),(3,4),(4,0),(4,1),(4,2),(4,3),(4,4),(4,5),(5,0),(5,1),(5,2),(5,3),(5,4),(5,5),(5,6),(6,0),(6,1),(6,2),(6,3),(6,4),(6,5),(6,6),(6,7),(7,0),(7,1),(7,2),(7,3),(7,4),(7,5),(7,6),(7,7),(7,8)]
ID: 0 => ('f(a)', D0)
ID: 1 => ('f(f(a))', D1, R1, P[], S{}), NR: 'f(f(a))'
ID: 2 => ('f(f(f(a)))', D2, R1, P[1], S{}), NR: 'f(f(a))'
ID: 3 => ('f(f(f(f(a))))', D3, R1, P[1, 1], S{}), NR: 'f(f(a))'
ID: 4 => ('f(f(f(f(f(a)))))', D4, R1, P[1, 1, 1], S{}), NR: 'f(f(a))'
ID: 5 => ('f(f(f(f(f(f(a))))))', D5, R1, P[1, 1, 1, 1], S{}), NR: 'f(f(a))'
ID: 6 => ('f(f(f(f(f(f(f(a)))))))', D6, R1, P[1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
ID: 7 => ('f(f(f(f(f(f(f(f(a))))))))', D7, R1, P[1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
ID: 8 => ('f(f(f(f(f(f(f(f(f(a)))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
SNodesPath1: f(f(a))
TNodesPath1: f(a) -> f(f(a))
SNodesPath2: f(f(a)) -> f(f(f(a))) -> f(a)
TNodesPath2: f(a)
f(f(a)) ->= f(f(a)) *<- f(a)
f(a) ->= f(a) *<- f(f(a))
"Strongly closed critical pair"

The problem is confluent.