YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty)
(REPLACEMENT-MAP
(a1)
(a2)
(a3)
(a4)
(a5)
(a6)
(b1)
(b2)
(b3)
(b4)
(b5)
(b6)
(b7)
(c1)
(c2)
(c3)
(c4)
(c5)
(c6)
(fSNonEmpty)
)
(RULES
a1 -> b1
a1 -> c1
a2 -> b2
a2 -> c2
a3 -> b3
a3 -> c3
a4 -> b4
a4 -> c4
a5 -> b5
a5 -> c5
a6 -> b6
a6 -> c6
b1 -> b2
b2 -> b3
b3 -> b4
b4 -> b5
b5 -> b6
b6 -> b7
b7 -> b1
b7 -> c1
c1 -> c2
c2 -> c3
c3 -> c4
c4 -> c5
c5 -> c6
c6 -> b7
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


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)
(REPLACEMENT-MAP
(a1)
(a2)
(a3)
(a4)
(a5)
(a6)
(b1)
(b2)
(b3)
(b4)
(b5)
(b6)
(b7)
(c1)
(c2)
(c3)
(c4)
(c5)
(c6)
(fSNonEmpty)
)
(RULES
a1 -> b1
a1 -> c1
a2 -> b2
a2 -> c2
a3 -> b3
a3 -> c3
a4 -> b4
a4 -> c4
a5 -> b5
a5 -> c5
a6 -> b6
a6 -> c6
b1 -> b2
b2 -> b3
b3 -> b4
b4 -> b5
b5 -> b6
b6 -> b7
b7 -> b1
b7 -> c1
c1 -> c2
c2 -> c3
c3 -> c4
c4 -> c5
c5 -> c6
c6 -> b7
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 a1 -> b1
 a1 -> c1
 a2 -> b2
 a2 -> c2
 a3 -> b3
 a3 -> c3
 a4 -> b4
 a4 -> c4
 a5 -> b5
 a5 -> c5
 a6 -> b6
 a6 -> c6
 b1 -> b2
 b2 -> b3
 b3 -> b4
 b4 -> b5
 b5 -> b6
 b6 -> b7
 b7 -> b1
 b7 -> c1
 c1 -> c2
 c2 -> c3
 c3 -> c4
 c4 -> c5
 c5 -> c6
 c6 -> b7
-> Vars:


-> Rlps:
 (rule: a1 -> b1, id: 1, possubterms: a1->[])
 (rule: a1 -> c1, id: 2, possubterms: a1->[])
 (rule: a2 -> b2, id: 3, possubterms: a2->[])
 (rule: a2 -> c2, id: 4, possubterms: a2->[])
 (rule: a3 -> b3, id: 5, possubterms: a3->[])
 (rule: a3 -> c3, id: 6, possubterms: a3->[])
 (rule: a4 -> b4, id: 7, possubterms: a4->[])
 (rule: a4 -> c4, id: 8, possubterms: a4->[])
 (rule: a5 -> b5, id: 9, possubterms: a5->[])
 (rule: a5 -> c5, id: 10, possubterms: a5->[])
 (rule: a6 -> b6, id: 11, possubterms: a6->[])
 (rule: a6 -> c6, id: 12, possubterms: a6->[])
 (rule: b1 -> b2, id: 13, possubterms: b1->[])
 (rule: b2 -> b3, id: 14, possubterms: b2->[])
 (rule: b3 -> b4, id: 15, possubterms: b3->[])
 (rule: b4 -> b5, id: 16, possubterms: b4->[])
 (rule: b5 -> b6, id: 17, possubterms: b5->[])
 (rule: b6 -> b7, id: 18, possubterms: b6->[])
 (rule: b7 -> b1, id: 19, possubterms: b7->[])
 (rule: b7 -> c1, id: 20, possubterms: b7->[])
 (rule: c1 -> c2, id: 21, possubterms: c1->[])
 (rule: c2 -> c3, id: 22, possubterms: c2->[])
 (rule: c3 -> c4, id: 23, possubterms: c3->[])
 (rule: c4 -> c5, id: 24, possubterms: c4->[])
 (rule: c5 -> c6, id: 25, possubterms: c5->[])
 (rule: c6 -> b7, id: 26, possubterms: c6->[])

-> Unifications:
(R2 unifies with R1 at p: [], l: a1, lp: a1, sig: {}, l': a1, r: c1, r': b1)
(R4 unifies with R3 at p: [], l: a2, lp: a2, sig: {}, l': a2, r: c2, r': b2)
(R6 unifies with R5 at p: [], l: a3, lp: a3, sig: {}, l': a3, r: c3, r': b3)
(R8 unifies with R7 at p: [], l: a4, lp: a4, sig: {}, l': a4, r: c4, r': b4)
(R10 unifies with R9 at p: [], l: a5, lp: a5, sig: {}, l': a5, r: c5, r': b5)
(R12 unifies with R11 at p: [], l: a6, lp: a6, sig: {}, l': a6, r: c6, r': b6)
(R20 unifies with R19 at p: [], l: b7, lp: b7, sig: {}, l': b7, r: c1, r': b1)

-> Critical pairs info:
<b3,c3>   =>  Not trivial, Overlay, Proper, NW0, N1
<b1,c1>   =>  Not trivial, Overlay, Proper, NW0, N2
<b6,c6>   =>  Not trivial, Overlay, Proper, NW0, N3
<b5,c5>   =>  Not trivial, Overlay, Proper, NW0, N4
<b1,c1>   =>  Not trivial, Overlay, Proper, NW0, N5
<b2,c2>   =>  Not trivial, Overlay, Proper, NW0, N6
<b4,c4>   =>  Not trivial, Overlay, Proper, NW0, N7

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

Problem 1.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(REPLACEMENT-MAP
(a1)
(a2)
(a3)
(a4)
(a5)
(a6)
(b1)
(b2)
(b3)
(b4)
(b5)
(b6)
(b7)
(c1)
(c2)
(c3)
(c4)
(c5)
(c6)
(fSNonEmpty)
)
(RULES
a1 -> b1
a1 -> c1
a2 -> b2
a2 -> c2
a3 -> b3
a3 -> c3
a4 -> b4
a4 -> c4
a5 -> b5
a5 -> c5
a6 -> b6
a6 -> c6
b1 -> b2
b2 -> b3
b3 -> b4
b4 -> b5
b5 -> b6
b6 -> b7
b7 -> b1
b7 -> c1
c1 -> c2
c2 -> c3
c3 -> c4
c4 -> c5
c5 -> c6
c6 -> b7
)
Critical Pairs:
<b3,c3>   =>  Not trivial, Overlay, Proper, NW0, N1
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: b3
Nodes: [0,1,2,3,4,5,6,7,8,9,10]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(4,6),(5,7),(6,8),(7,0),(8,9),(9,10)]
ID: 0 => ('b3', D0)
ID: 1 => ('b4', D1, R15, P[], S{}), NR: 'b4'
ID: 2 => ('b5', D2, R16, P[], S{}), NR: 'b5'
ID: 3 => ('b6', D3, R17, P[], S{}), NR: 'b6'
ID: 4 => ('b7', D4, R18, P[], S{}), NR: 'b7'
ID: 5 => ('b1', D5, R19, P[], S{}), NR: 'b1'
ID: 6 => ('c1', D5, R20, P[], S{}), NR: 'c1'
ID: 7 => ('b2', D6, R13, P[], S{}), NR: 'b2'
ID: 8 => ('c2', D6, R21, P[], S{}), NR: 'c2'
ID: 9 => ('c3', D7, R22, P[], S{}), NR: 'c3'
ID: 10 => ('c4', D8, R23, P[], S{}), NR: 'c4'
t: c3
Nodes: [0,1,2,3,4,5,6,7,8,9,10]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(4,6),(5,7),(6,8),(7,9),(8,0),(9,10)]
ID: 0 => ('c3', D0)
ID: 1 => ('c4', D1, R23, P[], S{}), NR: 'c4'
ID: 2 => ('c5', D2, R24, P[], S{}), NR: 'c5'
ID: 3 => ('c6', D3, R25, P[], S{}), NR: 'c6'
ID: 4 => ('b7', D4, R26, P[], S{}), NR: 'b7'
ID: 5 => ('b1', D5, R19, P[], S{}), NR: 'b1'
ID: 6 => ('c1', D5, R20, P[], S{}), NR: 'c1'
ID: 7 => ('b2', D6, R13, P[], S{}), NR: 'b2'
ID: 8 => ('c2', D6, R21, P[], S{}), NR: 'c2'
ID: 9 => ('b3', D7, R14, P[], S{}), NR: 'b3'
ID: 10 => ('b4', D8, R15, P[], S{}), NR: 'b4'
SNodesPath1: b3
TNodesPath1: c3 -> c4 -> c5 -> c6 -> b7 -> b1 -> b2 -> b3
SNodesPath2: 
TNodesPath2: c3
b3 ->= b3 *<- c3
c3 ->= c3 *<- b3
"Strongly closed critical pair"

The problem is confluent.

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(REPLACEMENT-MAP
(a1)
(a2)
(a3)
(a4)
(a5)
(a6)
(b1)
(b2)
(b3)
(b4)
(b5)
(b6)
(b7)
(c1)
(c2)
(c3)
(c4)
(c5)
(c6)
(fSNonEmpty)
)
(RULES
a1 -> b1
a1 -> c1
a2 -> b2
a2 -> c2
a3 -> b3
a3 -> c3
a4 -> b4
a4 -> c4
a5 -> b5
a5 -> c5
a6 -> b6
a6 -> c6
b1 -> b2
b2 -> b3
b3 -> b4
b4 -> b5
b5 -> b6
b6 -> b7
b7 -> b1
b7 -> c1
c1 -> c2
c2 -> c3
c3 -> c4
c4 -> c5
c5 -> c6
c6 -> b7
)
Critical Pairs:
<b6,c6>   =>  Not trivial, Overlay, Proper, NW0, N3
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: b6
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12]
Edges: [(0,1),(1,2),(1,3),(2,4),(3,5),(4,6),(5,7),(6,8),(7,9),(8,10),(9,11),(10,0),(11,12),(12,1)]
ID: 0 => ('b6', D0)
ID: 1 => ('b7', D1, R18, P[], S{}), NR: 'b7'
ID: 2 => ('b1', D2, R19, P[], S{}), NR: 'b1'
ID: 3 => ('c1', D2, R20, P[], S{}), NR: 'c1'
ID: 4 => ('b2', D3, R13, P[], S{}), NR: 'b2'
ID: 5 => ('c2', D3, R21, P[], S{}), NR: 'c2'
ID: 6 => ('b3', D4, R14, P[], S{}), NR: 'b3'
ID: 7 => ('c3', D4, R22, P[], S{}), NR: 'c3'
ID: 8 => ('b4', D5, R15, P[], S{}), NR: 'b4'
ID: 9 => ('c4', D5, R23, P[], S{}), NR: 'c4'
ID: 10 => ('b5', D6, R16, P[], S{}), NR: 'b5'
ID: 11 => ('c5', D6, R24, P[], S{}), NR: 'c5'
ID: 12 => ('c6', D7, R25, P[], S{}), NR: 'c6'
t: c6
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12]
Edges: [(0,1),(1,2),(1,3),(2,4),(3,5),(4,6),(5,7),(6,8),(7,9),(8,10),(9,11),(10,12),(11,0),(12,1)]
ID: 0 => ('c6', D0)
ID: 1 => ('b7', D1, R26, P[], S{}), NR: 'b7'
ID: 2 => ('b1', D2, R19, P[], S{}), NR: 'b1'
ID: 3 => ('c1', D2, R20, P[], S{}), NR: 'c1'
ID: 4 => ('b2', D3, R13, P[], S{}), NR: 'b2'
ID: 5 => ('c2', D3, R21, P[], S{}), NR: 'c2'
ID: 6 => ('b3', D4, R14, P[], S{}), NR: 'b3'
ID: 7 => ('c3', D4, R22, P[], S{}), NR: 'c3'
ID: 8 => ('b4', D5, R15, P[], S{}), NR: 'b4'
ID: 9 => ('c4', D5, R23, P[], S{}), NR: 'c4'
ID: 10 => ('b5', D6, R16, P[], S{}), NR: 'b5'
ID: 11 => ('c5', D6, R24, P[], S{}), NR: 'c5'
ID: 12 => ('b6', D7, R17, P[], S{}), NR: 'b6'
SNodesPath1: b6
TNodesPath1: c6 -> b7 -> b1 -> b2 -> b3 -> b4 -> b5 -> b6
SNodesPath2: 
TNodesPath2: c6
b6 ->= b6 *<- c6
c6 ->= c6 *<- b6
"Strongly closed critical pair"

The problem is confluent.

Problem 1.3: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(REPLACEMENT-MAP
(a1)
(a2)
(a3)
(a4)
(a5)
(a6)
(b1)
(b2)
(b3)
(b4)
(b5)
(b6)
(b7)
(c1)
(c2)
(c3)
(c4)
(c5)
(c6)
(fSNonEmpty)
)
(RULES
a1 -> b1
a1 -> c1
a2 -> b2
a2 -> c2
a3 -> b3
a3 -> c3
a4 -> b4
a4 -> c4
a5 -> b5
a5 -> c5
a6 -> b6
a6 -> c6
b1 -> b2
b2 -> b3
b3 -> b4
b4 -> b5
b5 -> b6
b6 -> b7
b7 -> b1
b7 -> c1
c1 -> c2
c2 -> c3
c3 -> c4
c4 -> c5
c5 -> c6
c6 -> b7
)
Critical Pairs:
<b5,c5>   =>  Not trivial, Overlay, Proper, NW0, N4
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: b5
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12]
Edges: [(0,1),(1,2),(2,3),(2,4),(3,5),(4,6),(5,7),(6,8),(7,9),(8,10),(9,0),(10,11),(11,12)]
ID: 0 => ('b5', D0)
ID: 1 => ('b6', D1, R17, P[], S{}), NR: 'b6'
ID: 2 => ('b7', D2, R18, P[], S{}), NR: 'b7'
ID: 3 => ('b1', D3, R19, P[], S{}), NR: 'b1'
ID: 4 => ('c1', D3, R20, P[], S{}), NR: 'c1'
ID: 5 => ('b2', D4, R13, P[], S{}), NR: 'b2'
ID: 6 => ('c2', D4, R21, P[], S{}), NR: 'c2'
ID: 7 => ('b3', D5, R14, P[], S{}), NR: 'b3'
ID: 8 => ('c3', D5, R22, P[], S{}), NR: 'c3'
ID: 9 => ('b4', D6, R15, P[], S{}), NR: 'b4'
ID: 10 => ('c4', D6, R23, P[], S{}), NR: 'c4'
ID: 11 => ('c5', D7, R24, P[], S{}), NR: 'c5'
ID: 12 => ('c6', D8, R25, P[], S{}), NR: 'c6'
t: c5
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12]
Edges: [(0,1),(1,2),(2,3),(2,4),(3,5),(4,6),(5,7),(6,8),(7,9),(8,10),(9,11),(10,0),(11,12)]
ID: 0 => ('c5', D0)
ID: 1 => ('c6', D1, R25, P[], S{}), NR: 'c6'
ID: 2 => ('b7', D2, R26, P[], S{}), NR: 'b7'
ID: 3 => ('b1', D3, R19, P[], S{}), NR: 'b1'
ID: 4 => ('c1', D3, R20, P[], S{}), NR: 'c1'
ID: 5 => ('b2', D4, R13, P[], S{}), NR: 'b2'
ID: 6 => ('c2', D4, R21, P[], S{}), NR: 'c2'
ID: 7 => ('b3', D5, R14, P[], S{}), NR: 'b3'
ID: 8 => ('c3', D5, R22, P[], S{}), NR: 'c3'
ID: 9 => ('b4', D6, R15, P[], S{}), NR: 'b4'
ID: 10 => ('c4', D6, R23, P[], S{}), NR: 'c4'
ID: 11 => ('b5', D7, R16, P[], S{}), NR: 'b5'
ID: 12 => ('b6', D8, R17, P[], S{}), NR: 'b6'
SNodesPath1: b5
TNodesPath1: c5 -> c6 -> b7 -> b1 -> b2 -> b3 -> b4 -> b5
SNodesPath2: 
TNodesPath2: c5
b5 ->= b5 *<- c5
c5 ->= c5 *<- b5
"Strongly closed critical pair"

The problem is confluent.

Problem 1.4: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(REPLACEMENT-MAP
(a1)
(a2)
(a3)
(a4)
(a5)
(a6)
(b1)
(b2)
(b3)
(b4)
(b5)
(b6)
(b7)
(c1)
(c2)
(c3)
(c4)
(c5)
(c6)
(fSNonEmpty)
)
(RULES
a1 -> b1
a1 -> c1
a2 -> b2
a2 -> c2
a3 -> b3
a3 -> c3
a4 -> b4
a4 -> c4
a5 -> b5
a5 -> c5
a6 -> b6
a6 -> c6
b1 -> b2
b2 -> b3
b3 -> b4
b4 -> b5
b5 -> b6
b6 -> b7
b7 -> b1
b7 -> c1
c1 -> c2
c2 -> c3
c3 -> c4
c4 -> c5
c5 -> c6
c6 -> b7
)
Critical Pairs:
<b1,c1>   =>  Not trivial, Overlay, Proper, NW0, N5
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: b1
Nodes: [0,1,2,3,4,5,6,7,8]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,0),(6,7),(7,8)]
ID: 0 => ('b1', D0)
ID: 1 => ('b2', D1, R13, P[], S{}), NR: 'b2'
ID: 2 => ('b3', D2, R14, P[], S{}), NR: 'b3'
ID: 3 => ('b4', D3, R15, P[], S{}), NR: 'b4'
ID: 4 => ('b5', D4, R16, P[], S{}), NR: 'b5'
ID: 5 => ('b6', D5, R17, P[], S{}), NR: 'b6'
ID: 6 => ('b7', D6, R18, P[], S{}), NR: 'b7'
ID: 7 => ('c1', D7, R20, P[], S{}), NR: 'c1'
ID: 8 => ('c2', D8, R21, P[], S{}), NR: 'c2'
t: c1
Nodes: [0,1,2,3,4,5,6,7,8]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,0),(6,7),(7,8)]
ID: 0 => ('c1', D0)
ID: 1 => ('c2', D1, R21, P[], S{}), NR: 'c2'
ID: 2 => ('c3', D2, R22, P[], S{}), NR: 'c3'
ID: 3 => ('c4', D3, R23, P[], S{}), NR: 'c4'
ID: 4 => ('c5', D4, R24, P[], S{}), NR: 'c5'
ID: 5 => ('c6', D5, R25, P[], S{}), NR: 'c6'
ID: 6 => ('b7', D6, R26, P[], S{}), NR: 'b7'
ID: 7 => ('b1', D7, R19, P[], S{}), NR: 'b1'
ID: 8 => ('b2', D8, R13, P[], S{}), NR: 'b2'
SNodesPath1: b1
TNodesPath1: c1 -> c2 -> c3 -> c4 -> c5 -> c6 -> b7 -> b1
SNodesPath2: b1 -> b2 -> b3 -> b4 -> b5 -> b6 -> b7 -> c1
TNodesPath2: c1
b1 ->= b1 *<- c1
c1 ->= c1 *<- b1
"Strongly closed critical pair"

The problem is confluent.

Problem 1.5: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(REPLACEMENT-MAP
(a1)
(a2)
(a3)
(a4)
(a5)
(a6)
(b1)
(b2)
(b3)
(b4)
(b5)
(b6)
(b7)
(c1)
(c2)
(c3)
(c4)
(c5)
(c6)
(fSNonEmpty)
)
(RULES
a1 -> b1
a1 -> c1
a2 -> b2
a2 -> c2
a3 -> b3
a3 -> c3
a4 -> b4
a4 -> c4
a5 -> b5
a5 -> c5
a6 -> b6
a6 -> c6
b1 -> b2
b2 -> b3
b3 -> b4
b4 -> b5
b5 -> b6
b6 -> b7
b7 -> b1
b7 -> c1
c1 -> c2
c2 -> c3
c3 -> c4
c4 -> c5
c5 -> c6
c6 -> b7
)
Critical Pairs:
<b2,c2>   =>  Not trivial, Overlay, Proper, NW0, N6
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: b2
Nodes: [0,1,2,3,4,5,6,7,8,9]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(5,7),(6,0),(7,8),(8,9)]
ID: 0 => ('b2', D0)
ID: 1 => ('b3', D1, R14, P[], S{}), NR: 'b3'
ID: 2 => ('b4', D2, R15, P[], S{}), NR: 'b4'
ID: 3 => ('b5', D3, R16, P[], S{}), NR: 'b5'
ID: 4 => ('b6', D4, R17, P[], S{}), NR: 'b6'
ID: 5 => ('b7', D5, R18, P[], S{}), NR: 'b7'
ID: 6 => ('b1', D6, R19, P[], S{}), NR: 'b1'
ID: 7 => ('c1', D6, R20, P[], S{}), NR: 'c1'
ID: 8 => ('c2', D7, R21, P[], S{}), NR: 'c2'
ID: 9 => ('c3', D8, R22, P[], S{}), NR: 'c3'
t: c2
Nodes: [0,1,2,3,4,5,6,7,8,9]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(5,7),(6,8),(7,0),(8,9)]
ID: 0 => ('c2', D0)
ID: 1 => ('c3', D1, R22, P[], S{}), NR: 'c3'
ID: 2 => ('c4', D2, R23, P[], S{}), NR: 'c4'
ID: 3 => ('c5', D3, R24, P[], S{}), NR: 'c5'
ID: 4 => ('c6', D4, R25, P[], S{}), NR: 'c6'
ID: 5 => ('b7', D5, R26, P[], S{}), NR: 'b7'
ID: 6 => ('b1', D6, R19, P[], S{}), NR: 'b1'
ID: 7 => ('c1', D6, R20, P[], S{}), NR: 'c1'
ID: 8 => ('b2', D7, R13, P[], S{}), NR: 'b2'
ID: 9 => ('b3', D8, R14, P[], S{}), NR: 'b3'
SNodesPath1: b2
TNodesPath1: c2 -> c3 -> c4 -> c5 -> c6 -> b7 -> b1 -> b2
SNodesPath2: 
TNodesPath2: c2
b2 ->= b2 *<- c2
c2 ->= c2 *<- b2
"Strongly closed critical pair"

The problem is confluent.

Problem 1.6: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(REPLACEMENT-MAP
(a1)
(a2)
(a3)
(a4)
(a5)
(a6)
(b1)
(b2)
(b3)
(b4)
(b5)
(b6)
(b7)
(c1)
(c2)
(c3)
(c4)
(c5)
(c6)
(fSNonEmpty)
)
(RULES
a1 -> b1
a1 -> c1
a2 -> b2
a2 -> c2
a3 -> b3
a3 -> c3
a4 -> b4
a4 -> c4
a5 -> b5
a5 -> c5
a6 -> b6
a6 -> c6
b1 -> b2
b2 -> b3
b3 -> b4
b4 -> b5
b5 -> b6
b6 -> b7
b7 -> b1
b7 -> c1
c1 -> c2
c2 -> c3
c3 -> c4
c4 -> c5
c5 -> c6
c6 -> b7
)
Critical Pairs:
<b4,c4>   =>  Not trivial, Overlay, Proper, NW0, N7
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: b4
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11]
Edges: [(0,1),(1,2),(2,3),(3,4),(3,5),(4,6),(5,7),(6,8),(7,9),(8,0),(9,10),(10,11)]
ID: 0 => ('b4', D0)
ID: 1 => ('b5', D1, R16, P[], S{}), NR: 'b5'
ID: 2 => ('b6', D2, R17, P[], S{}), NR: 'b6'
ID: 3 => ('b7', D3, R18, P[], S{}), NR: 'b7'
ID: 4 => ('b1', D4, R19, P[], S{}), NR: 'b1'
ID: 5 => ('c1', D4, R20, P[], S{}), NR: 'c1'
ID: 6 => ('b2', D5, R13, P[], S{}), NR: 'b2'
ID: 7 => ('c2', D5, R21, P[], S{}), NR: 'c2'
ID: 8 => ('b3', D6, R14, P[], S{}), NR: 'b3'
ID: 9 => ('c3', D6, R22, P[], S{}), NR: 'c3'
ID: 10 => ('c4', D7, R23, P[], S{}), NR: 'c4'
ID: 11 => ('c5', D8, R24, P[], S{}), NR: 'c5'
t: c4
Nodes: [0,1,2,3,4,5,6,7,8,9,10,11]
Edges: [(0,1),(1,2),(2,3),(3,4),(3,5),(4,6),(5,7),(6,8),(7,9),(8,10),(9,0),(10,11)]
ID: 0 => ('c4', D0)
ID: 1 => ('c5', D1, R24, P[], S{}), NR: 'c5'
ID: 2 => ('c6', D2, R25, P[], S{}), NR: 'c6'
ID: 3 => ('b7', D3, R26, P[], S{}), NR: 'b7'
ID: 4 => ('b1', D4, R19, P[], S{}), NR: 'b1'
ID: 5 => ('c1', D4, R20, P[], S{}), NR: 'c1'
ID: 6 => ('b2', D5, R13, P[], S{}), NR: 'b2'
ID: 7 => ('c2', D5, R21, P[], S{}), NR: 'c2'
ID: 8 => ('b3', D6, R14, P[], S{}), NR: 'b3'
ID: 9 => ('c3', D6, R22, P[], S{}), NR: 'c3'
ID: 10 => ('b4', D7, R15, P[], S{}), NR: 'b4'
ID: 11 => ('b5', D8, R16, P[], S{}), NR: 'b5'
SNodesPath1: b4
TNodesPath1: c4 -> c5 -> c6 -> b7 -> b1 -> b2 -> b3 -> b4
SNodesPath2: 
TNodesPath2: c4
b4 ->= b4 *<- c4
c4 ->= c4 *<- b4
"Strongly closed critical pair"

The problem is confluent.