YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a1) (a2) (a3) (a4) (a5) (b1) (b2) (b3) (b4) (b5) (c1) (c2) (c3) (c4) (c5) (b6) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 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) (RULES a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 ) Problem 1: Dependency Pairs Processor: -> Pairs: A1 -> B1 A1 -> C1 A2 -> B2 A2 -> C2 A3 -> B3 A3 -> C3 A4 -> B4 A4 -> C4 B1 -> B2 B2 -> B3 B3 -> B4 B4 -> B5 C1 -> C2 C2 -> C3 C3 -> C4 C4 -> C5 -> Rules: a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 Problem 1: SCC Processor: -> Pairs: A1 -> B1 A1 -> C1 A2 -> B2 A2 -> C2 A3 -> B3 A3 -> C3 A4 -> B4 A4 -> C4 B1 -> B2 B2 -> B3 B3 -> B4 B4 -> B5 C1 -> C2 C2 -> C3 C3 -> C4 C4 -> C5 -> Rules: a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 ->Strongly Connected Components: There is no strongly connected component The problem is finite. Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty) (REPLACEMENT-MAP (a1) (a2) (a3) (a4) (a5) (b1) (b2) (b3) (b4) (b5) (c1) (c2) (c3) (c4) (c5) (b6) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 ) Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy NW Procedure: -> Rules: a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 -> 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 -> b6, id: 9, possubterms: a5->[]) (rule: b1 -> b2, id: 10, possubterms: b1->[]) (rule: b2 -> b3, id: 11, possubterms: b2->[]) (rule: b3 -> b4, id: 12, possubterms: b3->[]) (rule: b4 -> b5, id: 13, possubterms: b4->[]) (rule: b5 -> b6, id: 14, possubterms: b5->[]) (rule: c1 -> c2, id: 15, possubterms: c1->[]) (rule: c2 -> c3, id: 16, possubterms: c2->[]) (rule: c3 -> c4, id: 17, possubterms: c3->[]) (rule: c4 -> c5, id: 18, possubterms: c4->[]) (rule: c5 -> b6, id: 19, possubterms: c5->[]) -> 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) -> Critical pairs info: => Not trivial, Overlay, Proper, NW0, N1 => Not trivial, Overlay, Proper, NW0, N2 => Not trivial, Overlay, Proper, NW0, N3 => Not trivial, Overlay, Proper, NW0, N4 -> 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 4 subproblems. Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a2) (a3) (a4) (a5) (b1) (b2) (b3) (b4) (b5) (c1) (c2) (c3) (c4) (c5) (b6) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N1 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b3 Nodes: [0,1,2,3] Edges: [(0,1),(1,2),(2,3)] ID: 0 => ('b3', D0) ID: 1 => ('b4', D1, R12, P[], S{}), NR: 'b4' ID: 2 => ('b5', D2, R13, P[], S{}), NR: 'b5' ID: 3 => ('b6', D3, R14, P[], S{}), NR: 'b6' t: c3 Nodes: [0,1,2,3] Edges: [(0,1),(1,2),(2,3)] ID: 0 => ('c3', D0) ID: 1 => ('c4', D1, R17, P[], S{}), NR: 'c4' ID: 2 => ('c5', D2, R18, P[], S{}), NR: 'c5' ID: 3 => ('b6', D3, R19, P[], S{}), NR: 'b6' SNodesPath: b3 -> b4 -> b5 -> b6 TNodesPath: c3 -> c4 -> c5 -> b6 b3 ->* b6 *<- c3 "Joinable" The problem is confluent. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a2) (a3) (a4) (a5) (b1) (b2) (b3) (b4) (b5) (c1) (c2) (c3) (c4) (c5) (b6) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N2 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b4 Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('b4', D0) ID: 1 => ('b5', D1, R13, P[], S{}), NR: 'b5' ID: 2 => ('b6', D2, R14, P[], S{}), NR: 'b6' t: c4 Nodes: [0,1,2] Edges: [(0,1),(1,2)] ID: 0 => ('c4', D0) ID: 1 => ('c5', D1, R18, P[], S{}), NR: 'c5' ID: 2 => ('b6', D2, R19, P[], S{}), NR: 'b6' SNodesPath: b4 -> b5 -> b6 TNodesPath: c4 -> c5 -> b6 b4 ->* b6 *<- c4 "Joinable" The problem is confluent. Problem 1.3: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a2) (a3) (a4) (a5) (b1) (b2) (b3) (b4) (b5) (c1) (c2) (c3) (c4) (c5) (b6) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N3 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b1 Nodes: [0,1,2,3,4,5] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5)] ID: 0 => ('b1', D0) ID: 1 => ('b2', D1, R10, P[], S{}), NR: 'b2' ID: 2 => ('b3', D2, R11, P[], S{}), NR: 'b3' ID: 3 => ('b4', D3, R12, P[], S{}), NR: 'b4' ID: 4 => ('b5', D4, R13, P[], S{}), NR: 'b5' ID: 5 => ('b6', D5, R14, P[], S{}), NR: 'b6' t: c1 Nodes: [0,1,2,3,4,5] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5)] ID: 0 => ('c1', D0) ID: 1 => ('c2', D1, R15, P[], S{}), NR: 'c2' ID: 2 => ('c3', D2, R16, P[], S{}), NR: 'c3' ID: 3 => ('c4', D3, R17, P[], S{}), NR: 'c4' ID: 4 => ('c5', D4, R18, P[], S{}), NR: 'c5' ID: 5 => ('b6', D5, R19, P[], S{}), NR: 'b6' SNodesPath: b1 -> b2 -> b3 -> b4 -> b5 -> b6 TNodesPath: c1 -> c2 -> c3 -> c4 -> c5 -> b6 b1 ->* b6 *<- c1 "Joinable" The problem is confluent. Problem 1.4: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (REPLACEMENT-MAP (a1) (a2) (a3) (a4) (a5) (b1) (b2) (b3) (b4) (b5) (c1) (c2) (c3) (c4) (c5) (b6) (fSNonEmpty) ) (RULES a1 -> b1 a1 -> c1 a2 -> b2 a2 -> c2 a3 -> b3 a3 -> c3 a4 -> b4 a4 -> c4 a5 -> b6 b1 -> b2 b2 -> b3 b3 -> b4 b4 -> b5 b5 -> b6 c1 -> c2 c2 -> c3 c3 -> c4 c4 -> c5 c5 -> b6 ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N4 Terminating:"YES" ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Brute Force Joinability Procedure: -> Rewritings: s: b2 Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(2,3),(3,4)] ID: 0 => ('b2', D0) ID: 1 => ('b3', D1, R11, P[], S{}), NR: 'b3' ID: 2 => ('b4', D2, R12, P[], S{}), NR: 'b4' ID: 3 => ('b5', D3, R13, P[], S{}), NR: 'b5' ID: 4 => ('b6', D4, R14, P[], S{}), NR: 'b6' t: c2 Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(2,3),(3,4)] ID: 0 => ('c2', D0) ID: 1 => ('c3', D1, R16, P[], S{}), NR: 'c3' ID: 2 => ('c4', D2, R17, P[], S{}), NR: 'c4' ID: 3 => ('c5', D3, R18, P[], S{}), NR: 'c5' ID: 4 => ('b6', D4, R19, P[], S{}), NR: 'b6' SNodesPath: b2 -> b3 -> b4 -> b5 -> b6 TNodesPath: c2 -> c3 -> c4 -> c5 -> b6 b2 ->* b6 *<- c2 "Joinable" The problem is confluent.