YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y z)
(REPLACEMENT-MAP
(f 1, 2)
(1)
(fSNonEmpty)
)
(RULES
f(f(x,y),z) -> f(x,f(y,z))
f(1,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 2)
(1)
(fSNonEmpty)

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

New problem:

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y z)
(REPLACEMENT-MAP
(f 1)
(1)
(fSNonEmpty)
)
(RULES
f(f(x,y),z) -> f(x,f(y,z))
f(1,x) -> x
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 
Termination Procedure:
Terminating?
YES

Problem 1: 

(VAR vu95NonEmpty vNonEmpty x y z)
(STRATEGY CONTEXTSENSITIVE
(f 1)
(num1)
(fSNonEmpty)
)
(RULES
f(f(x,y),z) -> f(x,f(y,z))
f(num1,x) -> x
)

Problem 1: 

Dependency Pairs Processor:
-> Pairs:
 F(f(x,y),z) -> F(x,f(y,z))
 F(num1,x) -> x
-> Rules:
 f(f(x,y),z) -> f(x,f(y,z))
 f(num1,x) -> x
-> Unhiding Rules:
 f(y,z) -> F(y,z)
 f(x5,z) -> x5

Problem 1: 

SCC Processor:
-> Pairs:
 F(f(x,y),z) -> F(x,f(y,z))
 F(num1,x) -> x
-> Rules:
 f(f(x,y),z) -> f(x,f(y,z))
 f(num1,x) -> x
-> Unhiding rules:
 f(y,z) -> F(y,z)
 f(x5,z) -> x5
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 F(f(x,y),z) -> F(x,f(y,z))
 F(num1,x) -> x
->->-> Rules:
 f(f(x,y),z) -> f(x,f(y,z))
 f(num1,x) -> x
->->-> Unhiding rules:
 f(y,z) -> F(y,z)
 f(x5,z) -> x5

Problem 1: 

Reduction Triple Processor:
-> Pairs:
 F(f(x,y),z) -> F(x,f(y,z))
 F(num1,x) -> x
-> Rules:
 f(f(x,y),z) -> f(x,f(y,z))
 f(num1,x) -> x
-> Unhiding rules:
 f(y,z) -> F(y,z)
 f(x5,z) -> x5
-> Usable rules:
 Empty
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[f](X1,X2) = X1 + X2 + 1
[num1] = 0
[fSNonEmpty] = 0
[F](X1,X2) = X1 + X2

Problem 1: 

SCC Processor:
-> Pairs:
 F(f(x,y),z) -> F(x,f(y,z))
 F(num1,x) -> x
-> Rules:
 f(f(x,y),z) -> f(x,f(y,z))
 f(num1,x) -> x
-> Unhiding rules:
 f(x5,z) -> x5
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 F(f(x,y),z) -> F(x,f(y,z))
->->-> Rules:
 f(f(x,y),z) -> f(x,f(y,z))
 f(num1,x) -> x
->->-> Unhiding rules:
 Empty

Problem 1: 

SubNColl Processor:
-> Pairs:
 F(f(x,y),z) -> F(x,f(y,z))
-> Rules:
 f(f(x,y),z) -> f(x,f(y,z))
 f(num1,x) -> x
-> Unhiding rules:
 Empty
->Projection:
 pi(F) = 1

Problem 1: 

Basic Processor:
-> Pairs:
 Empty
-> Rules:
 f(f(x,y),z) -> f(x,f(y,z))
 f(num1,x) -> x
-> Unhiding rules:
 Empty
-> Result:
 Set P is empty

The problem is finite.


Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y z)
(REPLACEMENT-MAP
(f 1)
(1)
(fSNonEmpty)
)
(RULES
f(f(x,y),z) -> f(x,f(y,z))
f(1,x) -> x
)
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

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

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

-> Critical pairs info:
<f(x',z),f(1,f(x',z))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<f(f(x',f(y',z')),z),f(f(x',y'),f(z',z))>   =>  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 CS-TRS, Left-homogeneous u-replacing variables



The problem is decomposed in 2 subproblems.

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

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

The problem is confluent.

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

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: f(f(x',f(y',z')),z)
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('f(f(x',f(y',z')),z)', D0)
ID: 1 => ('f(x',f(f(y',z'),z))', D1, R1, P[], S{x8 -> x', x9 -> f(y',z'), x10 -> z}), NR: 'f(x',f(f(y',z'),z))'
ID: 2 => ('f(x',f(y',f(z',z)))', D2, R1, P[2], S{x8 -> y', x9 -> z', x10 -> z}), NR: 'f(y',f(z',z))'
t: f(f(x',y'),f(z',z))
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('f(f(x',y'),f(z',z))', D0)
ID: 1 => ('f(x',f(y',f(z',z)))', D1, R1, P[], S{x8 -> x', x9 -> y', x10 -> f(z',z)}), NR: 'f(x',f(y',f(z',z)))'
SNodesPath: f(f(x',f(y',z')),z) -> f(x',f(f(y',z'),z)) -> f(x',f(y',f(z',z)))
TNodesPath: f(f(x',y'),f(z',z)) -> f(x',f(y',f(z',z)))
f(f(x',f(y',z')),z) ->* f(x',f(y',f(z',z))) *<- f(f(x',y'),f(z',z))
"Joinable"

The problem is confluent.