YES

Problem 1: 


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


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
(a)
(f 1)
(b)
(fSNonEmpty)
)
(RULES
a -> b
f(a) -> f(f(a))
f(x) -> f(b)
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

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

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

-> Critical pairs info:
<f(f(a)),f(b)>   =>  Not trivial, Overlay, Proper, NW0, N1
<f(b),f(f(a))>   =>  Not trivial, Not overlay, Proper, NW0, N2

-> 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
(a)
(f 1)
(b)
(fSNonEmpty)
)
(RULES
a -> b
f(a) -> f(f(a))
f(x) -> f(b)
)
Critical Pairs:
<f(b),f(f(a))>   =>  Not trivial, Not overlay, Proper, NW0, N2
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

The problem is confluent.