YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 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 (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) -> Vars: x, x, x -> Rlps: (rule: b(a(b(b(x)))) -> b(b(b(a(b(x))))), id: 1, possubterms: b(a(b(b(x))))->[], a(b(b(x)))->[1], b(b(x))->[1, 1], b(x)->[1, 1, 1]) (rule: b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))), id: 2, possubterms: b(a(a(b(b(x)))))->[], a(a(b(b(x))))->[1], a(b(b(x)))->[1, 1], b(b(x))->[1, 1, 1], b(x)->[1, 1, 1, 1]) (rule: b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))), id: 3, possubterms: b(a(a(a(b(b(x))))))->[], a(a(a(b(b(x)))))->[1], a(a(b(b(x))))->[1, 1], a(b(b(x)))->[1, 1, 1], b(b(x))->[1, 1, 1, 1], b(x)->[1, 1, 1, 1, 1]) -> Unifications: (R1 unifies with R1 at p: [1,1,1], l: b(a(b(b(x)))), lp: b(x), sig: {x -> a(b(b(x')))}, l': b(a(b(b(x')))), r: b(b(b(a(b(x))))), r': b(b(b(a(b(x')))))) (R1 unifies with R2 at p: [1,1,1], l: b(a(b(b(x)))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(b(b(a(b(x))))), r': b(a(b(b(a(a(b(x')))))))) (R1 unifies with R3 at p: [1,1,1], l: b(a(b(b(x)))), lp: b(x), sig: {x -> a(a(a(b(b(x')))))}, l': b(a(a(a(b(b(x')))))), r: b(b(b(a(b(x))))), r': b(a(a(b(b(a(a(a(b(x')))))))))) (R2 unifies with R1 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(b(b(x')))}, l': b(a(b(b(x')))), r: b(a(b(b(a(a(b(x))))))), r': b(b(b(a(b(x')))))) (R2 unifies with R2 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(a(b(b(a(a(b(x))))))), r': b(a(b(b(a(a(b(x')))))))) (R2 unifies with R3 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(a(b(b(x')))))}, l': b(a(a(a(b(b(x')))))), r: b(a(b(b(a(a(b(x))))))), r': b(a(a(b(b(a(a(a(b(x')))))))))) (R3 unifies with R1 at p: [1,1,1,1,1], l: b(a(a(a(b(b(x)))))), lp: b(x), sig: {x -> a(b(b(x')))}, l': b(a(b(b(x')))), r: b(a(a(b(b(a(a(a(b(x))))))))), r': b(b(b(a(b(x')))))) (R3 unifies with R2 at p: [1,1,1,1,1], l: b(a(a(a(b(b(x)))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(a(a(b(b(a(a(a(b(x))))))))), r': b(a(b(b(a(a(b(x')))))))) (R3 unifies with R3 at p: [1,1,1,1,1], l: b(a(a(a(b(b(x)))))), lp: b(x), sig: {x -> a(a(a(b(b(x')))))}, l': b(a(a(a(b(b(x')))))), r: b(a(a(b(b(a(a(a(b(x))))))))), r': b(a(a(b(b(a(a(a(b(x')))))))))) -> Critical pairs info: => Not trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Not trivial, Not overlay, Proper, NW0, N3 => Not trivial, Not overlay, Proper, NW0, N4 => Not trivial, Not overlay, Proper, NW0, N5 => Not trivial, Not overlay, Proper, NW0, N6 => Not trivial, Not overlay, Proper, NW0, N7 => Not trivial, Not overlay, Proper, NW0, N8 => Not trivial, Not overlay, Proper, NW0, N9 -> 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 9 subproblems. Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N1 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(b(b(b(a(b(x'))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25] Edges: [(0,1),(1,2),(1,3),(2,4),(3,4),(3,5),(3,6),(4,7),(4,8),(5,7),(5,9),(6,8),(6,9),(6,10),(7,11),(7,12),(8,12),(8,13),(9,12),(9,14),(10,13),(10,14),(11,15),(11,16),(12,16),(12,17),(13,17),(14,17),(14,18),(15,19),(16,19),(16,20),(17,20),(17,21),(18,21),(18,22),(19,23),(20,23),(20,24),(21,24),(21,25),(22,25)] ID: 0 => ('b(a(a(b(b(b(b(a(b(x')))))))))', D0) ID: 1 => ('b(a(b(b(a(a(b(b(b(a(b(x')))))))))))', D1, R2, P[], S{x5 -> b(b(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(b(b(a(b(x')))))))))))' ID: 2 => ('b(b(b(a(b(a(a(b(b(b(a(b(x'))))))))))))', D2, R1, P[], S{x4 -> a(a(b(b(b(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(b(b(a(b(x'))))))))))))' ID: 3 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(x')))))))))))))', D2, R2, P[1, 1, 1], S{x5 -> b(a(b(x')))}), NR: 'b(a(b(b(a(a(b(b(a(b(x'))))))))))' ID: 4 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(x'))))))))))))))', D3, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(x')))}), NR: 'b(a(b(b(a(a(b(b(a(b(x'))))))))))' ID: 5 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(x'))))))))))))))', D3, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(x'))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(x')))))))))))' ID: 6 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(x')))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 7 => ('b(b(b(a(b(b(b(a(b(a(a(b(b(a(b(x')))))))))))))))', D4, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(x'))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(x')))))))))))' ID: 8 => ('b(b(b(a(b(a(b(b(a(b(b(a(a(b(a(b(x'))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 9 => ('b(a(b(b(b(b(a(b(a(b(b(a(a(b(a(b(x'))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 10 => ('b(a(b(b(a(b(b(b(b(a(b(a(a(b(a(b(x'))))))))))))))))', D4, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 11 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(b(a(b(x'))))))))))))))))', D5, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(b(a(b(x'))))))))))))))' ID: 12 => ('b(b(b(a(b(b(b(a(b(a(b(b(a(a(b(a(b(x')))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 13 => ('b(b(b(a(b(a(b(b(b(b(a(b(a(a(b(a(b(x')))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 14 => ('b(a(b(b(b(b(a(b(b(b(a(b(a(a(b(a(b(x')))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 15 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(b(a(b(x')))))))))))))))))', D6, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(b(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(b(a(b(x')))))))))))))' ID: 16 => ('b(b(b(b(b(a(b(b(a(b(a(b(b(a(a(b(a(b(x'))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 17 => ('b(b(b(a(b(b(b(a(b(b(b(a(b(a(a(b(a(b(x'))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 18 => ('b(a(b(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(x'))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(x'))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(x')))))))))))))' ID: 19 => ('b(b(b(b(b(b(b(a(b(a(b(a(b(b(a(a(b(a(b(x')))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 20 => ('b(b(b(b(b(a(b(b(a(b(b(b(a(b(a(a(b(a(b(x')))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 21 => ('b(b(b(a(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(x')))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(x'))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(x')))))))))))))' ID: 22 => ('b(a(b(b(b(b(b(b(b(b(a(b(a(b(a(a(b(a(b(x')))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(b(a(a(b(a(b(x')))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(a(b(x'))))))))))))' ID: 23 => ('b(b(b(b(b(b(b(a(b(a(b(b(b(a(b(a(a(b(a(b(x'))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 24 => ('b(b(b(b(b(a(b(b(b(b(a(b(b(a(b(a(a(b(a(b(x'))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(x'))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(x')))))))))))))' ID: 25 => ('b(b(b(a(b(b(b(b(b(b(b(a(b(a(b(a(a(b(a(b(x'))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(b(a(a(b(a(b(x')))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(a(b(x'))))))))))))' t: b(a(b(b(a(a(b(a(b(b(x')))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26] Edges: [(0,1),(0,2),(1,3),(2,3),(2,4),(3,5),(4,5),(4,6),(4,7),(5,8),(5,9),(6,8),(6,10),(7,9),(7,10),(7,11),(8,12),(8,13),(9,13),(9,14),(10,13),(10,15),(11,14),(11,15),(12,16),(12,17),(13,17),(13,18),(14,18),(15,18),(15,19),(16,20),(17,20),(17,21),(18,21),(18,22),(19,22),(19,23),(20,24),(21,24),(21,25),(22,25),(22,26),(23,26)] ID: 0 => ('b(a(b(b(a(a(b(a(b(b(x'))))))))))', D0) ID: 1 => ('b(b(b(a(b(a(a(b(a(b(b(x')))))))))))', D1, R1, P[], S{x4 -> a(a(b(a(b(b(x'))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(b(x')))))))))))' ID: 2 => ('b(a(b(b(a(a(b(b(b(a(b(x')))))))))))', D1, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(b(a(b(x')))))' ID: 3 => ('b(b(b(a(b(a(a(b(b(b(a(b(x'))))))))))))', D2, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(b(a(b(x')))))' ID: 4 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(x')))))))))))))', D2, R2, P[1, 1, 1], S{x5 -> b(a(b(x')))}), NR: 'b(a(b(b(a(a(b(b(a(b(x'))))))))))' ID: 5 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(x'))))))))))))))', D3, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(x')))}), NR: 'b(a(b(b(a(a(b(b(a(b(x'))))))))))' ID: 6 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(x'))))))))))))))', D3, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(x'))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(x')))))))))))' ID: 7 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(x')))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 8 => ('b(b(b(a(b(b(b(a(b(a(a(b(b(a(b(x')))))))))))))))', D4, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(x'))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(x')))))))))))' ID: 9 => ('b(b(b(a(b(a(b(b(a(b(b(a(a(b(a(b(x'))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 10 => ('b(a(b(b(b(b(a(b(a(b(b(a(a(b(a(b(x'))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 11 => ('b(a(b(b(a(b(b(b(b(a(b(a(a(b(a(b(x'))))))))))))))))', D4, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 12 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(b(a(b(x'))))))))))))))))', D5, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(b(a(b(x'))))))))))))))' ID: 13 => ('b(b(b(a(b(b(b(a(b(a(b(b(a(a(b(a(b(x')))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 14 => ('b(b(b(a(b(a(b(b(b(b(a(b(a(a(b(a(b(x')))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 15 => ('b(a(b(b(b(b(a(b(b(b(a(b(a(a(b(a(b(x')))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 16 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(b(a(b(x')))))))))))))))))', D6, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(b(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(b(a(b(x')))))))))))))' ID: 17 => ('b(b(b(b(b(a(b(b(a(b(a(b(b(a(a(b(a(b(x'))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 18 => ('b(b(b(a(b(b(b(a(b(b(b(a(b(a(a(b(a(b(x'))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 19 => ('b(a(b(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(x'))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(x'))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(x')))))))))))))' ID: 20 => ('b(b(b(b(b(b(b(a(b(a(b(a(b(b(a(a(b(a(b(x')))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(x'))}), NR: 'b(a(b(b(a(a(b(a(b(x')))))))))' ID: 21 => ('b(b(b(b(b(a(b(b(a(b(b(b(a(b(a(a(b(a(b(x')))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 22 => ('b(b(b(a(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(x')))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(x'))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(x')))))))))))))' ID: 23 => ('b(a(b(b(b(b(b(b(b(b(a(b(a(b(a(a(b(a(b(x')))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(b(a(a(b(a(b(x')))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(a(b(x'))))))))))))' ID: 24 => ('b(b(b(b(b(b(b(a(b(a(b(b(b(a(b(a(a(b(a(b(x'))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(x')))))}), NR: 'b(b(b(a(b(a(a(b(a(b(x'))))))))))' ID: 25 => ('b(b(b(b(b(a(b(b(b(b(a(b(b(a(b(a(a(b(a(b(x'))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(x'))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(x')))))))))))))' ID: 26 => ('b(b(b(a(b(b(b(b(b(b(b(a(b(a(b(a(a(b(a(b(x'))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(b(a(a(b(a(b(x')))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(a(b(x'))))))))))))' SNodesPath1: b(a(a(b(b(b(b(a(b(x'))))))))) -> b(a(b(b(a(a(b(b(b(a(b(x'))))))))))) TNodesPath1: SNodesPath2: b(a(a(b(b(b(b(a(b(x'))))))))) -> b(a(b(b(a(a(b(b(b(a(b(x'))))))))))) TNodesPath2: b(a(a(b(b(b(b(a(b(x'))))))))) ->= b(a(b(b(a(a(b(b(b(a(b(x'))))))))))) *<- b(a(b(b(a(a(b(a(b(b(x')))))))))) b(a(b(b(a(a(b(a(b(b(x')))))))))) ->= b(a(b(b(a(a(b(b(b(a(b(x'))))))))))) *<- b(a(a(b(b(b(b(a(b(x'))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.2: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N2 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(a(b(b(b(b(a(b(x')))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56] Edges: [(0,1),(1,2),(1,3),(2,4),(2,5),(3,5),(3,6),(3,7),(4,8),(5,8),(5,9),(5,10),(6,9),(6,11),(6,12),(7,10),(7,12),(7,13),(8,14),(8,15),(9,14),(9,16),(9,17),(10,15),(10,17),(10,18),(11,16),(11,19),(12,17),(12,19),(12,20),(13,18),(13,20),(13,21),(14,22),(14,23),(15,23),(15,24),(16,22),(16,25),(16,26),(17,23),(17,26),(17,27),(18,24),(18,27),(18,28),(19,26),(19,29),(20,27),(20,29),(20,30),(21,28),(21,30),(22,31),(22,32),(23,32),(23,33),(24,33),(24,34),(25,31),(25,35),(25,36),(25,37),(26,32),(26,37),(26,38),(27,33),(27,38),(27,39),(28,34),(28,39),(29,38),(29,40),(30,39),(30,40),(30,41),(31,42),(31,43),(31,44),(32,44),(32,45),(33,45),(33,46),(34,46),(35,42),(35,47),(35,48),(36,43),(36,47),(36,49),(36,50),(37,44),(37,48),(37,50),(37,51),(38,45),(38,51),(38,52),(39,46),(39,52),(39,53),(40,52),(40,54),(41,53),(41,54),(41,55),(41,56)] ID: 0 => ('b(a(a(a(b(b(b(b(a(b(x'))))))))))', D0) ID: 1 => ('b(a(a(b(b(a(a(a(b(b(b(a(b(x')))))))))))))', D1, R3, P[], S{x6 -> b(b(a(b(x'))))}), NR: 'b(a(a(b(b(a(a(a(b(b(b(a(b(x')))))))))))))' ID: 2 => ('b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(x')))))))))))))))', D2, R2, P[], S{x5 -> a(a(a(b(b(b(a(b(x'))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(x')))))))))))))))' ID: 3 => ('b(a(a(b(b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))))))', D2, R3, P[1, 1, 1, 1], S{x6 -> b(a(b(x')))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))' ID: 4 => ('b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(x'))))))))))))))))', D3, R1, P[], S{x4 -> a(a(b(a(a(a(b(b(b(a(b(x')))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(x'))))))))))))))))' ID: 5 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))))))))', D3, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(x')))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))' ID: 6 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))', D3, R2, P[1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(x')))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))' ID: 7 => ('b(a(a(b(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))', D3, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 8 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(x')))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(x')))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))' ID: 9 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(x')))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))' ID: 10 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 11 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))', D4, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(x'))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))' ID: 12 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 13 => ('b(a(a(b(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 14 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(x')))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))' ID: 15 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 16 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(x'))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))' ID: 17 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 18 => ('b(a(b(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 19 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 20 => ('b(a(a(b(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 21 => ('b(a(a(b(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 22 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(x'))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))' ID: 23 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 24 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 25 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))))', D6, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))' ID: 26 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 27 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 28 => ('b(a(b(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 29 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 30 => ('b(a(a(b(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 31 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))' ID: 32 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 33 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 34 => ('b(b(b(a(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 35 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))', D7, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))' ID: 36 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))' ID: 37 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 38 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 39 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 40 => ('b(a(a(b(b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 41 => ('b(a(a(b(b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))' ID: 42 => ('b(b(b(a(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))' ID: 43 => ('b(b(b(a(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))' ID: 44 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 45 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 46 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 47 => ('b(a(b(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))' ID: 48 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 49 => ('b(a(b(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))' ID: 50 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 51 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 52 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 53 => ('b(a(b(b(a(a(b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))' ID: 54 => ('b(a(a(b(b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))' ID: 55 => ('b(a(a(b(b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))' ID: 56 => ('b(a(a(b(b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(a(b(x')))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))' t: b(a(a(b(b(a(a(a(b(a(b(b(x')))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58] Edges: [(0,1),(0,2),(1,3),(1,4),(2,3),(2,5),(3,6),(3,7),(4,7),(4,8),(4,9),(5,6),(6,10),(7,10),(7,11),(7,12),(8,11),(8,13),(8,14),(9,12),(9,14),(9,15),(10,16),(10,17),(11,16),(11,18),(11,19),(12,17),(12,19),(12,20),(13,18),(13,21),(14,19),(14,21),(14,22),(15,20),(15,22),(15,23),(16,24),(16,25),(17,25),(17,26),(18,24),(18,27),(18,28),(19,25),(19,28),(19,29),(20,26),(20,29),(20,30),(21,28),(21,31),(22,29),(22,31),(22,32),(23,30),(23,32),(24,33),(24,34),(25,34),(25,35),(26,35),(26,36),(27,33),(27,37),(27,38),(27,39),(28,34),(28,39),(28,40),(29,35),(29,40),(29,41),(30,36),(30,41),(31,40),(31,42),(32,41),(32,42),(32,43),(33,44),(33,45),(33,46),(34,46),(34,47),(35,47),(35,48),(36,48),(37,44),(37,49),(37,50),(38,45),(38,49),(38,51),(38,52),(39,46),(39,50),(39,52),(39,53),(40,47),(40,53),(40,54),(41,48),(41,54),(41,55),(42,54),(42,56),(43,55),(43,56),(43,57),(43,58)] ID: 0 => ('b(a(a(b(b(a(a(a(b(a(b(b(x'))))))))))))', D0) ID: 1 => ('b(a(a(b(b(a(a(a(b(b(b(a(b(x')))))))))))))', D1, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(b(a(b(x')))))' ID: 2 => ('b(a(b(b(a(a(b(a(a(a(b(a(b(b(x'))))))))))))))', D1, R2, P[], S{x5 -> a(a(a(b(a(b(b(x')))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(b(x'))))))))))))))' ID: 3 => ('b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(x')))))))))))))))', D2, R2, P[], S{x5 -> a(a(a(b(b(b(a(b(x'))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(x')))))))))))))))' ID: 4 => ('b(a(a(b(b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))))))', D2, R3, P[1, 1, 1, 1], S{x6 -> b(a(b(x')))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))' ID: 5 => ('b(b(b(a(b(a(a(b(a(a(a(b(a(b(b(x')))))))))))))))', D2, R1, P[], S{x4 -> a(a(b(a(a(a(b(a(b(b(x'))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(b(x')))))))))))))))' ID: 6 => ('b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(x'))))))))))))))))', D3, R1, P[], S{x4 -> a(a(b(a(a(a(b(b(b(a(b(x')))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(x'))))))))))))))))' ID: 7 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))))))))', D3, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(x')))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))' ID: 8 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))', D3, R2, P[1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(x')))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))' ID: 9 => ('b(a(a(b(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))', D3, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 10 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(x')))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(x')))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(x'))))))))))))' ID: 11 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(x')))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))' ID: 12 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 13 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))', D4, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(x'))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))' ID: 14 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 15 => ('b(a(a(b(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 16 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(x')))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))' ID: 17 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 18 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(x'))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))' ID: 19 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 20 => ('b(a(b(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 21 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 22 => ('b(a(a(b(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 23 => ('b(a(a(b(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 24 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(x'))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))' ID: 25 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 26 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 27 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))))', D6, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))' ID: 28 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 29 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 30 => ('b(a(b(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 31 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 32 => ('b(a(a(b(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 33 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))' ID: 34 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 35 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 36 => ('b(b(b(a(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 37 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))', D7, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))' ID: 38 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))' ID: 39 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 40 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 41 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 42 => ('b(a(a(b(b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 43 => ('b(a(a(b(b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))' ID: 44 => ('b(b(b(a(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))))' ID: 45 => ('b(b(b(a(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))' ID: 46 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 47 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 48 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 49 => ('b(a(b(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))))))' ID: 50 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 51 => ('b(a(b(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x')))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(x'))))))))))))))))))))' ID: 52 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(x'))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(x')))))))))))' ID: 53 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(x')))))))))))))' ID: 54 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))' ID: 55 => ('b(a(b(b(a(a(b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))' ID: 56 => ('b(a(a(b(b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))' ID: 57 => ('b(a(a(b(b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x')))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))' ID: 58 => ('b(a(a(b(b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(a(b(x')))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(a(b(x'))))))))))))))))))' SNodesPath1: b(a(a(a(b(b(b(b(a(b(x')))))))))) -> b(a(a(b(b(a(a(a(b(b(b(a(b(x'))))))))))))) TNodesPath1: b(a(a(b(b(a(a(a(b(a(b(b(x')))))))))))) -> b(a(a(b(b(a(a(a(b(b(b(a(b(x'))))))))))))) SNodesPath2: b(a(a(a(b(b(b(b(a(b(x')))))))))) -> b(a(a(b(b(a(a(a(b(b(b(a(b(x'))))))))))))) TNodesPath2: b(a(a(b(b(a(a(a(b(a(b(b(x')))))))))))) -> b(a(a(b(b(a(a(a(b(b(b(a(b(x'))))))))))))) b(a(a(a(b(b(b(b(a(b(x')))))))))) ->= b(a(a(b(b(a(a(a(b(b(b(a(b(x'))))))))))))) *<- b(a(a(b(b(a(a(a(b(a(b(b(x')))))))))))) b(a(a(b(b(a(a(a(b(a(b(b(x')))))))))))) ->= b(a(a(b(b(a(a(a(b(b(b(a(b(x'))))))))))))) *<- b(a(a(a(b(b(b(b(a(b(x')))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.3: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N3 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(b(a(b(b(a(a(b(x')))))))))) Nodes: [0,1,2,3,4,5] Edges: [(0,1),(0,2),(1,3),(2,3),(3,4),(4,5)] ID: 0 => ('b(a(b(b(a(b(b(a(a(b(x'))))))))))', D0) ID: 1 => ('b(b(b(a(b(a(b(b(a(a(b(x')))))))))))', D1, R1, P[], S{x4 -> a(b(b(a(a(b(x'))))))}), NR: 'b(b(b(a(b(a(b(b(a(a(b(x')))))))))))' ID: 2 => ('b(a(b(b(b(b(a(b(a(a(b(x')))))))))))', D1, R1, P[1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 3 => ('b(b(b(a(b(b(b(a(b(a(a(b(x'))))))))))))', D2, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 4 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(x')))))))))))))', D3, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(x'))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(x')))))))))))' ID: 5 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(x'))))))))))))))', D4, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(x')))))}), NR: 'b(b(b(a(b(a(b(a(a(b(x'))))))))))' t: b(b(b(a(b(a(a(b(b(x'))))))))) Nodes: [0,1,2,3,4] Edges: [(0,1),(1,2),(2,3),(3,4)] ID: 0 => ('b(b(b(a(b(a(a(b(b(x')))))))))', D0) ID: 1 => ('b(b(b(a(b(a(b(b(a(a(b(x')))))))))))', D1, R2, P[1, 1, 1, 1], S{x5 -> x'}), NR: 'b(a(b(b(a(a(b(x')))))))' ID: 2 => ('b(b(b(a(b(b(b(a(b(a(a(b(x'))))))))))))', D2, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 3 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(x')))))))))))))', D3, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(x'))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(x')))))))))))' ID: 4 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(x'))))))))))))))', D4, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(x')))))}), NR: 'b(b(b(a(b(a(b(a(a(b(x'))))))))))' SNodesPath1: b(a(b(b(a(b(b(a(a(b(x')))))))))) -> b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) TNodesPath1: b(b(b(a(b(a(a(b(b(x'))))))))) -> b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) SNodesPath2: b(a(b(b(a(b(b(a(a(b(x')))))))))) -> b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) TNodesPath2: b(b(b(a(b(a(a(b(b(x'))))))))) -> b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) b(a(b(b(a(b(b(a(a(b(x')))))))))) ->= b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) *<- b(b(b(a(b(a(a(b(b(x'))))))))) b(b(b(a(b(a(a(b(b(x'))))))))) ->= b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) *<- b(a(b(b(a(b(b(a(a(b(x')))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.4: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N4 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(a(b(b(a(b(b(a(a(b(x')))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45] Edges: [(0,1),(0,2),(1,3),(2,3),(2,4),(3,5),(3,6),(4,5),(4,7),(5,8),(5,9),(6,9),(6,10),(6,11),(7,8),(8,12),(9,12),(9,13),(9,14),(10,13),(10,15),(10,16),(11,14),(11,16),(11,17),(12,18),(12,19),(13,18),(13,20),(13,21),(14,19),(14,21),(14,22),(15,20),(15,23),(16,21),(16,23),(16,24),(17,22),(17,24),(17,25),(18,26),(18,27),(19,27),(19,28),(20,26),(20,29),(20,30),(21,27),(21,30),(21,31),(22,28),(22,31),(22,32),(23,30),(23,33),(24,31),(24,33),(24,34),(25,32),(25,34),(26,35),(26,36),(27,36),(27,37),(28,37),(28,38),(29,35),(29,39),(29,40),(29,41),(30,36),(30,41),(30,42),(31,37),(31,42),(31,43),(32,38),(32,43),(33,42),(33,44),(34,43),(34,44),(34,45)] ID: 0 => ('b(a(a(a(b(b(a(b(b(a(a(b(x'))))))))))))', D0) ID: 1 => ('b(a(a(a(b(b(b(b(a(b(a(a(b(x')))))))))))))', D1, R1, P[1, 1, 1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 2 => ('b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(x')))))))))))))))', D1, R3, P[], S{x6 -> a(b(b(a(a(b(x'))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(x')))))))))))))))' ID: 3 => ('b(a(a(b(b(a(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))))', D2, R3, P[], S{x6 -> b(b(a(b(a(a(b(x')))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))))' ID: 4 => ('b(a(b(b(a(a(b(a(a(a(b(a(b(b(a(a(b(x')))))))))))))))))', D2, R2, P[], S{x5 -> a(a(a(b(a(b(b(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(b(a(a(b(x')))))))))))))))))' ID: 5 => ('b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))))))', D3, R2, P[], S{x5 -> a(a(a(b(b(b(a(b(a(a(b(x')))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))))))' ID: 6 => ('b(a(a(b(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))', D3, R3, P[1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))' ID: 7 => ('b(b(b(a(b(a(a(b(a(a(a(b(a(b(b(a(a(b(x'))))))))))))))))))', D3, R1, P[], S{x4 -> a(a(b(a(a(a(b(a(b(b(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(b(a(a(b(x'))))))))))))))))))' ID: 8 => ('b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(x')))))))))))))))))))', D4, R1, P[], S{x4 -> a(a(b(a(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(x')))))))))))))))))))' ID: 9 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))' ID: 10 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))', D4, R2, P[1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))' ID: 11 => ('b(a(a(b(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 12 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))' ID: 13 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))' ID: 14 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 15 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))', D5, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))' ID: 16 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 17 => ('b(a(a(b(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 18 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))' ID: 19 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 20 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))' ID: 21 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 22 => ('b(a(b(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 23 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 24 => ('b(a(a(b(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 25 => ('b(a(a(b(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 26 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))' ID: 27 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 28 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 29 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))))', D7, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))' ID: 30 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 31 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 32 => ('b(a(b(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 33 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 34 => ('b(a(a(b(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 35 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))' ID: 36 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 37 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 38 => ('b(b(b(a(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 39 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D8, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))' ID: 40 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))' ID: 41 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 42 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 43 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 44 => ('b(a(a(b(b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 45 => ('b(a(a(b(b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))' t: b(a(a(b(b(a(a(a(b(a(a(b(b(x'))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46] Edges: [(0,1),(0,2),(1,3),(1,4),(2,4),(2,5),(3,6),(4,6),(4,7),(5,7),(5,8),(6,9),(7,9),(7,10),(8,10),(8,11),(8,12),(9,13),(10,13),(10,14),(10,15),(11,14),(11,16),(11,17),(12,15),(12,17),(12,18),(13,19),(13,20),(14,19),(14,21),(14,22),(15,20),(15,22),(15,23),(16,21),(16,24),(17,22),(17,24),(17,25),(18,23),(18,25),(18,26),(19,27),(19,28),(20,28),(20,29),(21,27),(21,30),(21,31),(22,28),(22,31),(22,32),(23,29),(23,32),(23,33),(24,31),(24,34),(25,32),(25,34),(25,35),(26,33),(26,35),(27,36),(27,37),(28,37),(28,38),(29,38),(29,39),(30,36),(30,40),(30,41),(30,42),(31,37),(31,42),(31,43),(32,38),(32,43),(32,44),(33,39),(33,44),(34,43),(34,45),(35,44),(35,45),(35,46)] ID: 0 => ('b(a(a(b(b(a(a(a(b(a(a(b(b(x')))))))))))))', D0) ID: 1 => ('b(a(b(b(a(a(b(a(a(a(b(a(a(b(b(x')))))))))))))))', D1, R2, P[], S{x5 -> a(a(a(b(a(a(b(b(x'))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(a(b(b(x')))))))))))))))' ID: 2 => ('b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(x')))))))))))))))', D1, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'b(a(b(b(a(a(b(x')))))))' ID: 3 => ('b(b(b(a(b(a(a(b(a(a(a(b(a(a(b(b(x'))))))))))))))))', D2, R1, P[], S{x4 -> a(a(b(a(a(a(b(a(a(b(b(x')))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(a(b(b(x'))))))))))))))))' ID: 4 => ('b(a(b(b(a(a(b(a(a(a(b(a(b(b(a(a(b(x')))))))))))))))))', D2, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'b(a(b(b(a(a(b(x')))))))' ID: 5 => ('b(a(a(b(b(a(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))))', D2, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 6 => ('b(b(b(a(b(a(a(b(a(a(a(b(a(b(b(a(a(b(x'))))))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'b(a(b(b(a(a(b(x')))))))' ID: 7 => ('b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))))))', D3, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 8 => ('b(a(a(b(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))', D3, R3, P[1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))' ID: 9 => ('b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(x')))))))))))))))))))', D4, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 10 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))' ID: 11 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))', D4, R2, P[1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))' ID: 12 => ('b(a(a(b(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D4, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 13 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))' ID: 14 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))' ID: 15 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 16 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))', D5, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))' ID: 17 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 18 => ('b(a(a(b(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 19 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))' ID: 20 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 21 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))' ID: 22 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 23 => ('b(a(b(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 24 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 25 => ('b(a(a(b(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 26 => ('b(a(a(b(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 27 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))' ID: 28 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 29 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 30 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))))', D7, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))' ID: 31 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 32 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 33 => ('b(a(b(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 34 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 35 => ('b(a(a(b(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 36 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))' ID: 37 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 38 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 39 => ('b(b(b(a(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 40 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))))))))))', D8, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))' ID: 41 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x')))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))))' ID: 42 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(x')))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))' ID: 43 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 44 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 45 => ('b(a(a(b(b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))' ID: 46 => ('b(a(a(b(b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x')))))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))' SNodesPath1: TNodesPath1: SNodesPath2: TNodesPath2: b(a(a(a(b(b(a(b(b(a(a(b(x')))))))))))) ->= b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(x'))))))))))))))) *<- b(a(a(b(b(a(a(a(b(a(a(b(b(x'))))))))))))) b(a(a(b(b(a(a(a(b(a(a(b(b(x'))))))))))))) ->= b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(x'))))))))))))))) *<- b(a(a(a(b(b(a(b(b(a(a(b(x')))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.5: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N5 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(b(a(b(b(a(a(b(x'))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25] Edges: [(0,1),(0,2),(1,3),(2,3),(2,4),(3,5),(3,6),(4,5),(5,7),(6,7),(6,8),(6,9),(7,10),(7,11),(8,10),(8,12),(9,11),(9,12),(9,13),(10,14),(10,15),(11,15),(11,16),(12,15),(12,17),(13,16),(13,17),(14,18),(14,19),(15,19),(15,20),(16,20),(17,20),(17,21),(18,22),(19,22),(19,23),(20,23),(20,24),(21,24),(21,25)] ID: 0 => ('b(a(a(b(b(a(b(b(a(a(b(x')))))))))))', D0) ID: 1 => ('b(a(a(b(b(b(b(a(b(a(a(b(x'))))))))))))', D1, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 2 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(x')))))))))))))', D1, R2, P[], S{x5 -> a(b(b(a(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(a(b(b(a(a(b(x')))))))))))))' ID: 3 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))', D2, R2, P[], S{x5 -> b(b(a(b(a(a(b(x')))))))}), NR: 'b(a(b(b(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))' ID: 4 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(x'))))))))))))))', D2, R1, P[], S{x4 -> a(a(b(a(b(b(a(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(b(a(a(b(x'))))))))))))))' ID: 5 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(x')))))))))))))))', D3, R1, P[], S{x4 -> a(a(b(b(b(a(b(a(a(b(x'))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(x')))))))))))))))' ID: 6 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))))', D3, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(x')))))))))))))' ID: 7 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(x')))))))))))))))))', D4, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(x')))))))))))))' ID: 8 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(x')))))))))))))))))', D4, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))' ID: 9 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 10 => ('b(b(b(a(b(b(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))', D5, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))' ID: 11 => ('b(b(b(a(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 12 => ('b(a(b(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 13 => ('b(a(b(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 14 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))', D6, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(b(a(b(a(a(b(x')))))))))))))))))' ID: 15 => ('b(b(b(a(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 16 => ('b(b(b(a(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 17 => ('b(a(b(b(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 18 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))', D7, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(b(a(b(a(a(b(x')))))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))))' ID: 19 => ('b(b(b(b(b(a(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 20 => ('b(b(b(a(b(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 21 => ('b(a(b(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(a(a(b(x')))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 22 => ('b(b(b(b(b(b(b(a(b(a(b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 23 => ('b(b(b(b(b(a(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 24 => ('b(b(b(a(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(a(a(b(x')))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 25 => ('b(a(b(b(b(b(b(b(b(b(a(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(b(a(a(b(a(b(a(a(b(x'))))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))))' t: b(a(b(b(a(a(b(a(a(b(b(x'))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25] Edges: [(0,1),(0,2),(1,3),(2,3),(2,4),(3,5),(4,5),(4,6),(5,7),(6,7),(6,8),(6,9),(7,10),(7,11),(8,10),(8,12),(9,11),(9,12),(9,13),(10,14),(10,15),(11,15),(11,16),(12,15),(12,17),(13,16),(13,17),(14,18),(14,19),(15,19),(15,20),(16,20),(17,20),(17,21),(18,22),(19,22),(19,23),(20,23),(20,24),(21,24),(21,25)] ID: 0 => ('b(a(b(b(a(a(b(a(a(b(b(x')))))))))))', D0) ID: 1 => ('b(b(b(a(b(a(a(b(a(a(b(b(x'))))))))))))', D1, R1, P[], S{x4 -> a(a(b(a(a(b(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(b(b(x'))))))))))))' ID: 2 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(x')))))))))))))', D1, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'b(a(b(b(a(a(b(x')))))))' ID: 3 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(x'))))))))))))))', D2, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: 'b(a(b(b(a(a(b(x')))))))' ID: 4 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(x'))))))))))))))', D2, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 5 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(x')))))))))))))))', D3, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(x')))}), NR: 'b(b(b(a(b(a(a(b(x'))))))))' ID: 6 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))))', D3, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(x')))))))))))))' ID: 7 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(x')))))))))))))))))', D4, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(x'))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(x')))))))))))))' ID: 8 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(x')))))))))))))))))', D4, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))' ID: 9 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 10 => ('b(b(b(a(b(b(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))', D5, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))' ID: 11 => ('b(b(b(a(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 12 => ('b(a(b(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 13 => ('b(a(b(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 14 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(b(a(b(a(a(b(x')))))))))))))))))))', D6, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(b(a(b(a(a(b(x')))))))))))))))))' ID: 15 => ('b(b(b(a(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 16 => ('b(b(b(a(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 17 => ('b(a(b(b(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 18 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))))))))', D7, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(b(a(b(a(a(b(x')))))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(b(a(b(a(a(b(x'))))))))))))))))' ID: 19 => ('b(b(b(b(b(a(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 20 => ('b(b(b(a(b(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 21 => ('b(a(b(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(a(a(b(x')))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 22 => ('b(b(b(b(b(b(b(a(b(a(b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(x')))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(x'))))))))))))' ID: 23 => ('b(b(b(b(b(a(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))' ID: 24 => ('b(b(b(a(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(a(a(b(x')))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))' ID: 25 => ('b(a(b(b(b(b(b(b(b(b(a(b(a(b(a(a(b(a(b(a(a(b(x'))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(b(a(a(b(a(b(a(a(b(x'))))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(a(b(a(a(b(x')))))))))))))))' SNodesPath1: TNodesPath1: SNodesPath2: TNodesPath2: b(a(a(b(b(a(b(b(a(a(b(x'))))))))))) ->= b(a(b(b(a(a(b(a(b(b(a(a(b(x'))))))))))))) *<- b(a(b(b(a(a(b(a(a(b(b(x'))))))))))) b(a(b(b(a(a(b(a(a(b(b(x'))))))))))) ->= b(a(b(b(a(a(b(a(b(b(a(a(b(x'))))))))))))) *<- b(a(a(b(b(a(b(b(a(a(b(x'))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.6: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N6 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24] Edges: [(0,1),(0,2),(1,3),(1,4),(2,4),(2,5),(3,6),(4,6),(4,7),(5,7),(6,8),(7,8),(7,9),(8,10),(9,10),(9,11),(9,12),(10,13),(10,14),(11,13),(11,15),(12,14),(12,15),(12,16),(13,17),(13,18),(14,18),(14,19),(15,18),(15,20),(16,19),(16,20),(17,21),(17,22),(18,22),(18,23),(19,23),(20,23),(20,24)] ID: 0 => ('b(a(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))))', D0) ID: 1 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))', D1, R2, P[], S{x5 -> a(a(b(b(a(a(a(b(x'))))))))}), NR: 'b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))' ID: 2 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))', D1, R2, P[1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 3 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))))', D2, R1, P[], S{x4 -> a(a(b(a(a(b(b(a(a(a(b(x')))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))))' ID: 4 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))))', D2, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 5 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))', D2, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 6 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(x'))))))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 7 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))', D3, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 8 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))', D4, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 9 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))', D4, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 10 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))', D5, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 11 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))', D5, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 12 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 13 => ('b(b(b(a(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 14 => ('b(b(b(a(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 15 => ('b(a(b(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 16 => ('b(a(b(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 17 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D7, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 18 => ('b(b(b(a(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 19 => ('b(b(b(a(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 20 => ('b(a(b(b(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 21 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 22 => ('b(b(b(b(b(a(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 23 => ('b(b(b(a(b(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 24 => ('b(a(b(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' t: b(a(b(b(a(a(b(a(a(a(b(b(x')))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] Edges: [(0,1),(0,2),(1,3),(2,3),(2,4),(3,5),(4,5),(4,6),(5,7),(6,7),(6,8),(7,9),(8,9),(8,10),(8,11),(9,12),(9,13),(10,12),(10,14),(11,13),(11,14),(11,15),(12,16),(12,17),(13,17),(13,18),(14,17),(14,19),(15,18),(15,19),(16,20),(16,21),(17,21),(17,22),(18,22),(19,22),(19,23)] ID: 0 => ('b(a(b(b(a(a(b(a(a(a(b(b(x'))))))))))))', D0) ID: 1 => ('b(b(b(a(b(a(a(b(a(a(a(b(b(x')))))))))))))', D1, R1, P[], S{x4 -> a(a(b(a(a(a(b(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(x')))))))))))))' ID: 2 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))', D1, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(b(b(a(a(a(b(x')))))))))' ID: 3 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))))', D2, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(b(b(a(a(a(b(x')))))))))' ID: 4 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))))', D2, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 5 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(x'))))))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 6 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))', D3, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 7 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))', D4, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 8 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))', D4, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 9 => ('b(b(b(a(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))', D5, R2, P[1, 1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 10 => ('b(a(b(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))', D5, R1, P[1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 11 => ('b(a(b(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 12 => ('b(b(b(a(b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 13 => ('b(b(b(a(b(a(b(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 14 => ('b(a(b(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 15 => ('b(a(b(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 16 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D7, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 17 => ('b(b(b(a(b(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 18 => ('b(b(b(a(b(a(b(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 19 => ('b(a(b(b(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 20 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 21 => ('b(b(b(b(b(a(b(b(a(b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))' ID: 22 => ('b(b(b(a(b(b(b(a(b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))' ID: 23 => ('b(a(b(b(b(b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1], S{x4 -> b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' SNodesPath1: b(a(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))) -> b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))) TNodesPath1: SNodesPath2: b(a(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))) -> b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))) TNodesPath2: b(a(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))) ->= b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))) *<- b(a(b(b(a(a(b(a(a(a(b(b(x')))))))))))) b(a(b(b(a(a(b(a(a(a(b(b(x')))))))))))) ->= b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))) *<- b(a(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.7: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N7 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))) Nodes: [0,1,2,3,4,5,6,7] Edges: [(0,1),(0,2),(1,3),(2,3),(2,4),(3,5),(4,5),(5,6),(6,7)] ID: 0 => ('b(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))', D0) ID: 1 => ('b(b(b(a(b(a(a(b(b(a(a(a(b(x')))))))))))))', D1, R1, P[], S{x4 -> a(a(b(b(a(a(a(b(x'))))))))}), NR: 'b(b(b(a(b(a(a(b(b(a(a(a(b(x')))))))))))))' ID: 2 => ('b(a(b(b(a(b(b(a(a(b(a(a(a(b(x'))))))))))))))', D1, R2, P[1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 3 => ('b(b(b(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))', D2, R2, P[1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 4 => ('b(a(b(b(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))', D2, R1, P[1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 5 => ('b(b(b(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))', D3, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 6 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))', D4, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))' ID: 7 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))', D5, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))' t: b(b(b(a(b(a(a(a(b(b(x')))))))))) Nodes: [0,1,2,3,4,5] Edges: [(0,1),(1,2),(2,3),(3,4),(4,5)] ID: 0 => ('b(b(b(a(b(a(a(a(b(b(x'))))))))))', D0) ID: 1 => ('b(b(b(a(b(a(a(b(b(a(a(a(b(x')))))))))))))', D1, R3, P[1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(b(b(a(a(a(b(x')))))))))' ID: 2 => ('b(b(b(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))', D2, R2, P[1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 3 => ('b(b(b(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))', D3, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 4 => ('b(b(b(b(b(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))', D4, R1, P[1, 1], S{x4 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(b(b(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))' ID: 5 => ('b(b(b(b(b(b(b(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))', D5, R1, P[1, 1, 1, 1], S{x4 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(b(b(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))' SNodesPath1: b(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))) -> b(b(b(a(b(a(a(b(b(a(a(a(b(x'))))))))))))) TNodesPath1: b(b(b(a(b(a(a(a(b(b(x')))))))))) -> b(b(b(a(b(a(a(b(b(a(a(a(b(x'))))))))))))) SNodesPath2: b(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))) -> b(b(b(a(b(a(a(b(b(a(a(a(b(x'))))))))))))) TNodesPath2: b(b(b(a(b(a(a(a(b(b(x')))))))))) -> b(b(b(a(b(a(a(b(b(a(a(a(b(x'))))))))))))) b(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))) ->= b(b(b(a(b(a(a(b(b(a(a(a(b(x'))))))))))))) *<- b(b(b(a(b(a(a(a(b(b(x')))))))))) b(b(b(a(b(a(a(a(b(b(x')))))))))) ->= b(b(b(a(b(a(a(b(b(a(a(a(b(x'))))))))))))) *<- b(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.8: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N8 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(a(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38] Edges: [(0,1),(0,2),(1,3),(1,4),(2,4),(2,5),(3,6),(4,6),(4,7),(5,7),(5,8),(6,9),(6,10),(7,9),(7,11),(8,11),(9,12),(9,13),(10,13),(10,14),(10,15),(11,12),(12,16),(13,16),(13,17),(13,18),(14,17),(14,19),(14,20),(15,18),(15,20),(15,21),(16,22),(16,23),(17,22),(17,24),(17,25),(18,23),(18,25),(18,26),(19,24),(19,27),(20,25),(20,27),(20,28),(21,26),(21,28),(21,29),(22,30),(22,31),(23,31),(23,32),(24,30),(24,33),(24,34),(25,31),(25,34),(25,35),(26,32),(26,35),(26,36),(27,34),(27,37),(28,35),(28,37),(28,38),(29,36),(29,38)] ID: 0 => ('b(a(a(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))))', D0) ID: 1 => ('b(a(a(a(b(b(a(b(b(a(a(b(a(a(a(b(x'))))))))))))))))', D1, R2, P[1, 1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 2 => ('b(a(a(b(b(a(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))))', D1, R3, P[], S{x6 -> a(a(b(b(a(a(a(b(x'))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))))' ID: 3 => ('b(a(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))', D2, R1, P[1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 4 => ('b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))))))', D2, R3, P[], S{x6 -> a(b(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))))))' ID: 5 => ('b(a(b(b(a(a(b(a(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))))))', D2, R2, P[], S{x5 -> a(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))))))' ID: 6 => ('b(a(a(b(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))', D3, R3, P[], S{x6 -> b(b(a(b(a(a(b(a(a(a(b(x')))))))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 7 => ('b(a(b(b(a(a(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))))))))', D3, R2, P[], S{x5 -> a(a(a(b(a(b(b(a(a(b(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 8 => ('b(b(b(a(b(a(a(b(a(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))))))))', D3, R1, P[], S{x4 -> a(a(b(a(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))))))))' ID: 9 => ('b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))', D4, R2, P[], S{x5 -> a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))' ID: 10 => ('b(a(a(b(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D4, R3, P[1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))' ID: 11 => ('b(b(b(a(b(a(a(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))', D4, R1, P[], S{x4 -> a(a(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))' ID: 12 => ('b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D5, R1, P[], S{x4 -> a(a(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))' ID: 13 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))' ID: 14 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 15 => ('b(a(a(b(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 16 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))' ID: 17 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 18 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 19 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))' ID: 20 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 21 => ('b(a(a(b(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 22 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 23 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 24 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))' ID: 25 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 26 => ('b(a(b(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 27 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 28 => ('b(a(a(b(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 29 => ('b(a(a(b(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 30 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))' ID: 31 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 32 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 33 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))' ID: 34 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 35 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 36 => ('b(a(b(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 37 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 38 => ('b(a(a(b(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' t: b(a(a(b(b(a(a(a(b(a(a(a(b(b(x')))))))))))))) Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38] Edges: [(0,1),(0,2),(1,3),(1,4),(2,4),(2,5),(3,6),(4,6),(4,7),(5,7),(5,8),(6,9),(7,9),(7,10),(8,10),(8,11),(9,12),(10,12),(10,13),(11,13),(11,14),(11,15),(12,16),(13,16),(13,17),(13,18),(14,17),(14,19),(14,20),(15,18),(15,20),(15,21),(16,22),(16,23),(17,22),(17,24),(17,25),(18,23),(18,25),(18,26),(19,24),(19,27),(20,25),(20,27),(20,28),(21,26),(21,28),(21,29),(22,30),(22,31),(23,31),(23,32),(24,30),(24,33),(24,34),(25,31),(25,34),(25,35),(26,32),(26,35),(26,36),(27,34),(27,37),(28,35),(28,37),(28,38),(29,36),(29,38)] ID: 0 => ('b(a(a(b(b(a(a(a(b(a(a(a(b(b(x'))))))))))))))', D0) ID: 1 => ('b(a(b(b(a(a(b(a(a(a(b(a(a(a(b(b(x'))))))))))))))))', D1, R2, P[], S{x5 -> a(a(a(b(a(a(a(b(b(x')))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(a(a(b(b(x'))))))))))))))))' ID: 2 => ('b(a(a(b(b(a(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))))', D1, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(b(b(a(a(a(b(x')))))))))' ID: 3 => ('b(b(b(a(b(a(a(b(a(a(a(b(a(a(a(b(b(x')))))))))))))))))', D2, R1, P[], S{x4 -> a(a(b(a(a(a(b(a(a(a(b(b(x'))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(a(a(b(b(x')))))))))))))))))' ID: 4 => ('b(a(b(b(a(a(b(a(a(a(b(a(a(b(b(a(a(a(b(x')))))))))))))))))))', D2, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(b(b(a(a(a(b(x')))))))))' ID: 5 => ('b(a(a(b(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))))))', D2, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 6 => ('b(b(b(a(b(a(a(b(a(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))))))))', D3, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> x'}), NR: 'b(a(a(b(b(a(a(a(b(x')))))))))' ID: 7 => ('b(a(b(b(a(a(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x')))))))))))))))))))))', D3, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 8 => ('b(a(a(b(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))', D3, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 9 => ('b(b(b(a(b(a(a(b(a(a(a(b(a(b(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))', D4, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(x'))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(x')))))))))))' ID: 10 => ('b(a(b(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))', D4, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 11 => ('b(a(a(b(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D4, R3, P[1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))' ID: 12 => ('b(b(b(a(b(a(a(b(a(a(a(b(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))', D5, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(x')))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))' ID: 13 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))' ID: 14 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))', D5, R2, P[1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 15 => ('b(a(a(b(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))', D5, R3, P[1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 16 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1], S{x6 -> b(a(b(a(a(b(a(a(a(b(x'))))))))))}), NR: 'b(a(a(b(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))' ID: 17 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 18 => ('b(a(b(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 19 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))', D6, R1, P[1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))' ID: 20 => ('b(a(a(b(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D6, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 21 => ('b(a(a(b(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D6, R2, P[1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 22 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 23 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 24 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))' ID: 25 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 26 => ('b(a(b(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 27 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))', D7, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 28 => ('b(a(a(b(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))', D7, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 29 => ('b(a(a(b(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 30 => ('b(b(b(a(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))' ID: 31 => ('b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 32 => ('b(b(b(a(b(a(a(b(a(a(b(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 33 => ('b(a(b(b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1], S{x5 -> b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))}), NR: 'b(a(b(b(a(a(b(b(a(b(a(a(b(a(a(a(b(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))' ID: 34 => ('b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R3, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x6 -> a(b(a(a(b(a(a(a(b(x')))))))))}), NR: 'b(a(a(b(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))' ID: 35 => ('b(a(b(b(a(a(b(a(b(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 36 => ('b(a(b(b(a(a(b(a(a(b(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' ID: 37 => ('b(a(a(b(b(b(b(a(b(a(a(b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))}), NR: 'b(a(b(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))))))' ID: 38 => ('b(a(a(b(b(a(b(b(a(a(b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x4 -> a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x'))))))))))))))))}), NR: 'b(b(b(a(b(a(a(b(a(a(a(b(a(b(a(a(b(a(a(a(b(x')))))))))))))))))))))' SNodesPath1: TNodesPath1: SNodesPath2: TNodesPath2: b(a(a(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))))) ->= b(a(a(b(b(a(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))))) *<- b(a(a(b(b(a(a(a(b(a(a(a(b(b(x')))))))))))))) b(a(a(b(b(a(a(a(b(a(a(a(b(b(x')))))))))))))) ->= b(a(a(b(b(a(a(a(b(a(a(b(b(a(a(a(b(x'))))))))))))))))) *<- b(a(a(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))))) "Strongly closed critical pair" The problem is confluent. Problem 1.9: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(a(b(b(x)))) -> b(b(b(a(b(x))))) b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N9 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: b(a(b(b(b(b(a(b(x')))))))) Nodes: [0,1,2,3] Edges: [(0,1),(1,2),(2,3)] ID: 0 => ('b(a(b(b(b(b(a(b(x'))))))))', D0) ID: 1 => ('b(b(b(a(b(b(b(a(b(x')))))))))', D1, R1, P[], S{x4 -> b(b(a(b(x'))))}), NR: 'b(b(b(a(b(b(b(a(b(x')))))))))' ID: 2 => ('b(b(b(b(b(a(b(b(a(b(x'))))))))))', D2, R1, P[1, 1], S{x4 -> b(a(b(x')))}), NR: 'b(b(b(a(b(b(a(b(x'))))))))' ID: 3 => ('b(b(b(b(b(b(b(a(b(a(b(x')))))))))))', D3, R1, P[1, 1, 1, 1], S{x4 -> a(b(x'))}), NR: 'b(b(b(a(b(a(b(x')))))))' t: b(b(b(a(b(a(b(b(x')))))))) Nodes: [0,1,2,3] Edges: [(0,1),(1,2),(2,3)] ID: 0 => ('b(b(b(a(b(a(b(b(x'))))))))', D0) ID: 1 => ('b(b(b(a(b(b(b(a(b(x')))))))))', D1, R1, P[1, 1, 1, 1], S{x4 -> x'}), NR: 'b(b(b(a(b(x')))))' ID: 2 => ('b(b(b(b(b(a(b(b(a(b(x'))))))))))', D2, R1, P[1, 1], S{x4 -> b(a(b(x')))}), NR: 'b(b(b(a(b(b(a(b(x'))))))))' ID: 3 => ('b(b(b(b(b(b(b(a(b(a(b(x')))))))))))', D3, R1, P[1, 1, 1, 1], S{x4 -> a(b(x'))}), NR: 'b(b(b(a(b(a(b(x')))))))' SNodesPath1: b(a(b(b(b(b(a(b(x')))))))) -> b(b(b(a(b(b(b(a(b(x'))))))))) TNodesPath1: b(b(b(a(b(a(b(b(x')))))))) -> b(b(b(a(b(b(b(a(b(x'))))))))) SNodesPath2: b(a(b(b(b(b(a(b(x')))))))) -> b(b(b(a(b(b(b(a(b(x'))))))))) TNodesPath2: b(b(b(a(b(a(b(b(x')))))))) -> b(b(b(a(b(b(b(a(b(x'))))))))) b(a(b(b(b(b(a(b(x')))))))) ->= b(b(b(a(b(b(b(a(b(x'))))))))) *<- b(b(b(a(b(a(b(b(x')))))))) b(b(b(a(b(a(b(b(x')))))))) ->= b(b(b(a(b(b(b(a(b(x'))))))))) *<- b(a(b(b(b(b(a(b(x')))))))) "Strongly closed critical pair" The problem is confluent.