0.00/0.08 YES 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 0.00/0.08 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 Confluence Problem: 0.00/0.08 (VAR vNonEmpty x) 0.00/0.08 (REPLACEMENT-MAP 0.00/0.08 (b 1) 0.00/0.08 (a 1) 0.00/0.08 (fSNonEmpty) 0.00/0.08 ) 0.00/0.08 (RULES 0.00/0.08 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.08 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.08 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.08 ) 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 Not CS-TRS Procedure: 0.00/0.08 R is not a CS-TRS 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 Linearity Procedure: 0.00/0.08 Linear? 0.00/0.08 YES 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 Confluence Problem: 0.00/0.08 (VAR vNonEmpty x) 0.00/0.08 (REPLACEMENT-MAP 0.00/0.08 (b 1) 0.00/0.08 (a 1) 0.00/0.08 (fSNonEmpty) 0.00/0.08 ) 0.00/0.08 (RULES 0.00/0.08 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.08 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.08 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.08 ) 0.00/0.08 Linear:YES 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 0.00/0.08 Huet Levy Procedure: 0.00/0.08 -> Rules: 0.00/0.08 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.08 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.08 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.08 -> Vars: 0.00/0.08 x, x, x 0.00/0.08 0.00/0.08 -> Rlps: 0.00/0.08 (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]) 0.00/0.08 (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]) 0.00/0.08 (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]) 0.00/0.08 0.00/0.08 -> Unifications: 0.00/0.08 (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')))))) 0.00/0.08 (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')))))))) 0.00/0.08 (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')))))))))) 0.00/0.08 (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')))))) 0.00/0.08 (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')))))))) 0.00/0.08 (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')))))))))) 0.00/0.08 (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')))))) 0.00/0.08 (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')))))))) 0.00/0.08 (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')))))))))) 0.00/0.08 0.00/0.08 -> Critical pairs info: 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N1 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N2 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N3 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N4 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N5 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N6 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N7 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N8 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N9 0.00/0.08 0.00/0.08 -> Problem conclusions: 0.00/0.08 Left linear, Right linear, Linear 0.00/0.08 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.00/0.08 Not Huet-Levy confluent, Not Newman confluent 0.00/0.08 R is a TRS 0.00/0.08 0.00/0.08 0.00/0.08 0.00/0.08 The problem is decomposed in 9 subproblems. 0.00/0.08 0.00/0.08 Problem 1.1: 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 Confluence Problem: 0.00/0.08 (VAR x x') 0.00/0.08 (REPLACEMENT-MAP 0.00/0.08 (b 1) 0.00/0.08 (a 1) 0.00/0.08 (fSNonEmpty) 0.00/0.08 ) 0.00/0.08 (RULES 0.00/0.08 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.08 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.08 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.08 ) 0.00/0.08 Critical Pairs: 0.00/0.08 => Not trivial, Not overlay, Proper, NW0, N1 0.00/0.08 Linear:YES 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 0.00/0.08 Strong Confluence Procedure: 0.00/0.08 -> Rewritings: 0.00/0.08 s: b(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))) 0.00/0.08 Nodes: [0,1,2,3,4,5,6,7] 0.00/0.08 Edges: [(0,1),(0,2),(1,3),(2,3),(2,4),(3,5),(4,5),(5,6),(6,7)] 0.00/0.08 ID: 0 => ('b(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))', D0) 0.00/0.08 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')))))))))))))' 0.00/0.08 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')))))))))))' 0.00/0.08 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')))))))))))' 0.00/0.08 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'))))))))))))' 0.00/0.08 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'))))))))))))' 0.00/0.08 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')))))))))))))))' 0.00/0.08 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'))))))))))))))' 0.00/0.08 t: b(b(b(a(b(a(a(a(b(b(x')))))))))) 0.00/0.08 Nodes: [0,1,2,3,4,5] 0.00/0.08 Edges: [(0,1),(1,2),(2,3),(3,4),(4,5)] 0.00/0.08 ID: 0 => ('b(b(b(a(b(a(a(a(b(b(x'))))))))))', D0) 0.00/0.08 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')))))))))' 0.00/0.08 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')))))))))))' 0.00/0.08 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'))))))))))))' 0.00/0.08 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')))))))))))))))' 0.00/0.08 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'))))))))))))))' 0.00/0.08 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'))))))))))))) 0.00/0.08 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'))))))))))))) 0.00/0.08 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'))))))))))))) 0.00/0.08 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'))))))))))))) 0.00/0.08 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')))))))))) 0.00/0.08 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')))))))))))) 0.00/0.08 "Strongly closed critical pair" 0.00/0.09 0.00/0.09 The problem is confluent. 0.00/0.09 0.00/0.09 Problem 1.2: 0.00/0.09 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.09 Confluence Problem: 0.00/0.09 (VAR x x') 0.00/0.09 (REPLACEMENT-MAP 0.00/0.09 (b 1) 0.00/0.09 (a 1) 0.00/0.09 (fSNonEmpty) 0.00/0.09 ) 0.00/0.09 (RULES 0.00/0.09 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.09 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.09 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.09 ) 0.00/0.09 Critical Pairs: 0.00/0.09 => Not trivial, Not overlay, Proper, NW0, N2 0.00/0.09 Linear:YES 0.00/0.09 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.09 0.00/0.09 Strong Confluence Procedure: 0.00/0.09 -> Rewritings: 0.00/0.09 s: b(a(a(a(b(b(a(b(b(a(a(b(x')))))))))))) 0.00/0.09 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] 0.00/0.09 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)] 0.00/0.09 ID: 0 => ('b(a(a(a(b(b(a(b(b(a(a(b(x'))))))))))))', D0) 0.00/0.09 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'))))))))' 0.00/0.09 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')))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))))))' 0.00/0.09 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')))))))))))))))' 0.00/0.09 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'))))))))))))))))))' 0.00/0.09 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')))))))))))))))))))' 0.00/0.09 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')))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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')))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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')))))))))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))))))))))))' 0.00/0.09 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'))))))))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))))))))))' 0.00/0.09 t: b(a(a(b(b(a(a(a(b(a(a(b(b(x'))))))))))))) 0.00/0.09 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] 0.00/0.09 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)] 0.00/0.09 ID: 0 => ('b(a(a(b(b(a(a(a(b(a(a(b(b(x')))))))))))))', D0) 0.00/0.09 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')))))))))))))))' 0.00/0.09 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')))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))' 0.00/0.09 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'))))))))' 0.00/0.09 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')))))))' 0.00/0.09 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'))))))))' 0.00/0.09 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')))))))))))))))' 0.00/0.09 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'))))))))' 0.00/0.09 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')))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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')))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.09 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'))))))))))))))))' 0.00/0.09 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')))))))))))))))))' 0.00/0.09 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'))))))))))))))' 0.00/0.10 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'))))))))))))))))))' 0.00/0.10 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'))))))))))))))' 0.00/0.10 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'))))))))))))))))' 0.00/0.10 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'))))))))))))))' 0.00/0.10 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'))))))))))))))))' 0.00/0.10 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')))))))))))))))))' 0.00/0.10 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'))))))))))))))))))' 0.00/0.10 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'))))))))))))))' 0.00/0.10 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'))))))))))))))))' 0.00/0.10 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')))))))))))))))))))))))' 0.00/0.10 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'))))))))))))))' 0.00/0.10 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'))))))))))))))))' 0.00/0.10 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')))))))))))))))))' 0.00/0.10 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'))))))))))))))))' 0.00/0.10 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')))))))))))))))))' 0.00/0.10 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')))))))))))))))))))))))' 0.00/0.10 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'))))))))))))))' 0.00/0.10 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'))))))))))))))))' 0.00/0.10 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')))))))))))))))))' 0.00/0.10 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'))))))))))))))))))))))))' 0.00/0.10 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'))))))))))))))))))))))' 0.00/0.10 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'))))))))))))))' 0.00/0.10 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'))))))))))))))))' 0.00/0.10 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')))))))))))))))))' 0.00/0.10 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')))))))))))))))))' 0.00/0.10 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'))))))))))))))))))))))' 0.00/0.10 SNodesPath1: 0.00/0.10 TNodesPath1: 0.00/0.10 SNodesPath2: 0.00/0.10 TNodesPath2: 0.00/0.10 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'))))))))))))) 0.00/0.10 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')))))))))))) 0.00/0.10 "Strongly closed critical pair" 0.00/0.10 0.00/0.10 The problem is confluent. 0.00/0.10 0.00/0.10 Problem 1.3: 0.00/0.10 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.10 Confluence Problem: 0.00/0.10 (VAR x x') 0.00/0.10 (REPLACEMENT-MAP 0.00/0.10 (b 1) 0.00/0.10 (a 1) 0.00/0.10 (fSNonEmpty) 0.00/0.10 ) 0.00/0.10 (RULES 0.00/0.10 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.10 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.10 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.10 ) 0.00/0.10 Critical Pairs: 0.00/0.10 => Not trivial, Not overlay, Proper, NW0, N3 0.00/0.10 Linear:YES 0.00/0.10 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.10 0.00/0.10 Strong Confluence Procedure: 0.00/0.10 -> Rewritings: 0.00/0.10 s: b(a(b(b(a(b(b(a(a(b(x')))))))))) 0.00/0.10 Nodes: [0,1,2,3,4,5] 0.00/0.10 Edges: [(0,1),(0,2),(1,3),(2,3),(3,4),(4,5)] 0.00/0.10 ID: 0 => ('b(a(b(b(a(b(b(a(a(b(x'))))))))))', D0) 0.00/0.10 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')))))))))))' 0.00/0.10 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'))))))))' 0.00/0.10 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'))))))))' 0.00/0.10 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')))))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 t: b(b(b(a(b(a(a(b(b(x'))))))))) 0.00/0.11 Nodes: [0,1,2,3,4] 0.00/0.11 Edges: [(0,1),(1,2),(2,3),(3,4)] 0.00/0.11 ID: 0 => ('b(b(b(a(b(a(a(b(b(x')))))))))', D0) 0.00/0.11 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')))))))' 0.00/0.11 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'))))))))' 0.00/0.11 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')))))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 SNodesPath1: b(a(b(b(a(b(b(a(a(b(x')))))))))) -> b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) 0.00/0.11 TNodesPath1: b(b(b(a(b(a(a(b(b(x'))))))))) -> b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) 0.00/0.11 SNodesPath2: b(a(b(b(a(b(b(a(a(b(x')))))))))) -> b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) 0.00/0.11 TNodesPath2: b(b(b(a(b(a(a(b(b(x'))))))))) -> b(b(b(a(b(a(b(b(a(a(b(x'))))))))))) 0.00/0.11 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'))))))))) 0.00/0.11 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')))))))))) 0.00/0.11 "Strongly closed critical pair" 0.00/0.11 0.00/0.11 The problem is confluent. 0.00/0.11 0.00/0.11 Problem 1.4: 0.00/0.11 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.11 Confluence Problem: 0.00/0.11 (VAR x x') 0.00/0.11 (REPLACEMENT-MAP 0.00/0.11 (b 1) 0.00/0.11 (a 1) 0.00/0.11 (fSNonEmpty) 0.00/0.11 ) 0.00/0.11 (RULES 0.00/0.11 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.11 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.11 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.11 ) 0.00/0.11 Critical Pairs: 0.00/0.11 => Not trivial, Not overlay, Proper, NW0, N4 0.00/0.11 Linear:YES 0.00/0.11 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.11 0.00/0.11 Strong Confluence Procedure: 0.00/0.11 -> Rewritings: 0.00/0.11 s: b(a(a(b(b(b(b(a(b(x'))))))))) 0.00/0.11 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] 0.00/0.11 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)] 0.00/0.11 ID: 0 => ('b(a(a(b(b(b(b(a(b(x')))))))))', D0) 0.00/0.11 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')))))))))))' 0.00/0.11 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'))))))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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')))))))))))' 0.00/0.11 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')))))))))' 0.00/0.11 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')))))))))))' 0.00/0.11 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')))))))))' 0.00/0.11 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')))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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'))))))))))))))' 0.00/0.11 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')))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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')))))))))))))' 0.00/0.11 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')))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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')))))))))))))' 0.00/0.11 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')))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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')))))))))))))' 0.00/0.11 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'))))))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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')))))))))))))' 0.00/0.11 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'))))))))))))' 0.00/0.11 t: b(a(b(b(a(a(b(a(b(b(x')))))))))) 0.00/0.11 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] 0.00/0.11 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)] 0.00/0.11 ID: 0 => ('b(a(b(b(a(a(b(a(b(b(x'))))))))))', D0) 0.00/0.11 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')))))))))))' 0.00/0.11 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')))))' 0.00/0.11 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')))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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'))))))))))' 0.00/0.11 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')))))))))))' 0.00/0.11 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')))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))' 0.00/0.15 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')))))))))' 0.00/0.15 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'))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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')))))))))' 0.00/0.15 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'))))))))))' 0.00/0.15 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'))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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')))))))))' 0.00/0.15 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'))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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')))))))))' 0.00/0.15 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'))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))' 0.00/0.15 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'))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))' 0.00/0.15 SNodesPath1: b(a(a(b(b(b(b(a(b(x'))))))))) -> b(a(b(b(a(a(b(b(b(a(b(x'))))))))))) 0.00/0.15 TNodesPath1: 0.00/0.15 SNodesPath2: b(a(a(b(b(b(b(a(b(x'))))))))) -> b(a(b(b(a(a(b(b(b(a(b(x'))))))))))) 0.00/0.15 TNodesPath2: 0.00/0.15 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')))))))))) 0.00/0.15 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'))))))))) 0.00/0.15 "Strongly closed critical pair" 0.00/0.15 0.00/0.15 The problem is confluent. 0.00/0.15 0.00/0.15 Problem 1.5: 0.00/0.15 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.15 Confluence Problem: 0.00/0.15 (VAR x x') 0.00/0.15 (REPLACEMENT-MAP 0.00/0.15 (b 1) 0.00/0.15 (a 1) 0.00/0.15 (fSNonEmpty) 0.00/0.15 ) 0.00/0.15 (RULES 0.00/0.15 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.15 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.15 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.15 ) 0.00/0.15 Critical Pairs: 0.00/0.15 => Not trivial, Not overlay, Proper, NW0, N5 0.00/0.15 Linear:YES 0.00/0.15 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.15 0.00/0.15 Strong Confluence Procedure: 0.00/0.15 -> Rewritings: 0.00/0.15 s: b(a(a(a(b(b(b(b(a(b(x')))))))))) 0.00/0.15 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] 0.00/0.15 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)] 0.00/0.15 ID: 0 => ('b(a(a(a(b(b(b(b(a(b(x'))))))))))', D0) 0.00/0.15 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')))))))))))))' 0.00/0.15 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')))))))))))))))' 0.00/0.15 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'))))))))))))' 0.00/0.15 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'))))))))))))))))' 0.00/0.15 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'))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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'))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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')))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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'))))))))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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')))))))))))))))))))))' 0.00/0.15 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')))))))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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')))))))))))))))))))' 0.00/0.15 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')))))))))))))))))))))' 0.00/0.15 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')))))))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.15 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')))))))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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'))))))))))))))))))))' 0.00/0.15 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')))))))))))' 0.00/0.15 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')))))))))))))' 0.00/0.15 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'))))))))))))))' 0.00/0.16 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')))))))))))))))))))' 0.00/0.16 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')))))))))))))))))))' 0.00/0.16 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'))))))))))))))))))))' 0.00/0.16 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'))))))))))))))))))' 0.00/0.16 t: b(a(a(b(b(a(a(a(b(a(b(b(x')))))))))))) 0.00/0.16 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] 0.00/0.16 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)] 0.00/0.16 ID: 0 => ('b(a(a(b(b(a(a(a(b(a(b(b(x'))))))))))))', D0) 0.00/0.16 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')))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))))))' 0.00/0.16 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'))))))))))))' 0.00/0.16 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')))))))))))))))' 0.00/0.16 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'))))))))))))))))' 0.00/0.16 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'))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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'))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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'))))))))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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'))))))))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))))))))))))' 0.00/0.16 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')))))))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))))))))))' 0.00/0.16 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')))))))))))))))))))))' 0.00/0.16 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')))))))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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'))))))))))))))))))))' 0.00/0.16 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')))))))))))' 0.00/0.16 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')))))))))))))' 0.00/0.16 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'))))))))))))))' 0.00/0.16 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')))))))))))))))))))' 0.00/0.16 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')))))))))))))))))))' 0.00/0.16 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'))))))))))))))))))))' 0.00/0.16 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'))))))))))))))))))' 0.00/0.16 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'))))))))))))) 0.00/0.16 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'))))))))))))) 0.00/0.16 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'))))))))))))) 0.00/0.16 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'))))))))))))) 0.00/0.16 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')))))))))))) 0.00/0.16 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')))))))))) 0.00/0.16 "Strongly closed critical pair" 0.00/0.16 0.00/0.16 The problem is confluent. 0.00/0.16 0.00/0.16 Problem 1.6: 0.00/0.16 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.16 Confluence Problem: 0.00/0.16 (VAR x x') 0.00/0.16 (REPLACEMENT-MAP 0.00/0.16 (b 1) 0.00/0.16 (a 1) 0.00/0.16 (fSNonEmpty) 0.00/0.16 ) 0.00/0.16 (RULES 0.00/0.16 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.16 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.16 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.16 ) 0.00/0.16 Critical Pairs: 0.00/0.16 => Not trivial, Not overlay, Proper, NW0, N6 0.00/0.16 Linear:YES 0.00/0.16 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.16 0.00/0.16 Strong Confluence Procedure: 0.00/0.16 -> Rewritings: 0.00/0.16 s: b(a(a(b(b(a(b(b(a(a(b(x'))))))))))) 0.00/0.16 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] 0.00/0.16 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)] 0.00/0.18 ID: 0 => ('b(a(a(b(b(a(b(b(a(a(b(x')))))))))))', D0) 0.00/0.18 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'))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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'))))))))))))))' 0.00/0.18 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'))))))))))))))' 0.00/0.18 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')))))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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'))))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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'))))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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')))))))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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'))))))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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'))))))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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'))))))))))))))))' 0.00/0.18 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')))))))))))))))' 0.00/0.18 t: b(a(b(b(a(a(b(a(a(b(b(x'))))))))))) 0.00/0.18 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] 0.00/0.18 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)] 0.00/0.18 ID: 0 => ('b(a(b(b(a(a(b(a(a(b(b(x')))))))))))', D0) 0.00/0.18 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'))))))))))))' 0.00/0.18 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')))))))' 0.00/0.18 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')))))))' 0.00/0.18 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'))))))))' 0.00/0.18 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'))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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'))))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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'))))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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')))))))))))))))))' 0.00/0.18 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'))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.18 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')))))))))))))' 0.00/0.19 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'))))))))))))))))' 0.00/0.19 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'))))))))))))' 0.00/0.19 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')))))))))))))' 0.00/0.19 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'))))))))))))))))' 0.00/0.19 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'))))))))))))' 0.00/0.19 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')))))))))))))' 0.00/0.19 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'))))))))))))))))' 0.00/0.19 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')))))))))))))))' 0.00/0.19 SNodesPath1: 0.00/0.19 TNodesPath1: 0.00/0.19 SNodesPath2: 0.00/0.19 TNodesPath2: 0.00/0.19 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'))))))))))) 0.00/0.19 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'))))))))))) 0.00/0.19 "Strongly closed critical pair" 0.00/0.19 0.00/0.19 The problem is confluent. 0.00/0.19 0.00/0.19 Problem 1.7: 0.00/0.19 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.19 Confluence Problem: 0.00/0.19 (VAR x x') 0.00/0.19 (REPLACEMENT-MAP 0.00/0.19 (b 1) 0.00/0.19 (a 1) 0.00/0.19 (fSNonEmpty) 0.00/0.19 ) 0.00/0.19 (RULES 0.00/0.19 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.19 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.19 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.19 ) 0.00/0.19 Critical Pairs: 0.00/0.19 => Not trivial, Not overlay, Proper, NW0, N7 0.00/0.19 Linear:YES 0.00/0.19 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.19 0.00/0.19 Strong Confluence Procedure: 0.00/0.19 -> Rewritings: 0.00/0.19 s: b(a(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))) 0.00/0.19 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] 0.00/0.19 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)] 0.00/0.19 ID: 0 => ('b(a(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))))', D0) 0.00/0.19 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')))))))))))))))' 0.00/0.19 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')))))))))))' 0.00/0.19 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'))))))))))))))))' 0.00/0.19 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')))))))))))' 0.00/0.19 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'))))))))))))' 0.00/0.19 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')))))))))))' 0.00/0.19 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'))))))))))))' 0.00/0.19 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'))))))))))))' 0.00/0.19 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')))))))))))))))))' 0.00/0.19 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')))))))))))))))))' 0.00/0.19 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'))))))))))))))))))' 0.00/0.19 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'))))))))))))))))' 0.00/0.19 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'))))))))))))))))))' 0.00/0.19 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'))))))))))))))))' 0.00/0.19 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'))))))))))))))))' 0.00/0.19 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')))))))))))))))))' 0.00/0.19 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')))))))))))))))))))))' 0.00/0.19 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'))))))))))))))))' 0.00/0.19 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')))))))))))))))))' 0.00/0.19 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')))))))))))))))))' 0.00/0.19 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'))))))))))))))))))))' 0.00/0.19 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'))))))))))))))))' 0.00/0.19 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')))))))))))))))))' 0.00/0.19 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'))))))))))))))))))))' 0.00/0.19 t: b(a(b(b(a(a(b(a(a(a(b(b(x')))))))))))) 0.00/0.19 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] 0.00/0.21 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)] 0.00/0.21 ID: 0 => ('b(a(b(b(a(a(b(a(a(a(b(b(x'))))))))))))', D0) 0.00/0.21 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')))))))))))))' 0.00/0.21 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')))))))))' 0.00/0.21 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')))))))))' 0.00/0.21 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')))))))))))' 0.00/0.21 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')))))))))))' 0.00/0.21 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'))))))))))))' 0.00/0.21 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'))))))))))))' 0.00/0.21 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')))))))))))))))))' 0.00/0.21 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')))))))))))))))))' 0.00/0.21 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'))))))))))))))))))' 0.00/0.21 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'))))))))))))))))' 0.00/0.21 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'))))))))))))))))))' 0.00/0.21 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'))))))))))))))))' 0.00/0.21 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'))))))))))))))))' 0.00/0.21 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')))))))))))))))))' 0.00/0.21 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')))))))))))))))))))))' 0.00/0.21 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'))))))))))))))))' 0.00/0.21 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')))))))))))))))))' 0.00/0.21 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')))))))))))))))))' 0.00/0.21 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'))))))))))))))))))))' 0.00/0.21 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'))))))))))))))))' 0.00/0.21 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')))))))))))))))))' 0.00/0.21 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'))))))))))))))))))))' 0.00/0.21 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'))))))))))))))) 0.00/0.21 TNodesPath1: 0.00/0.21 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'))))))))))))))) 0.00/0.21 TNodesPath2: 0.00/0.21 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')))))))))))) 0.00/0.21 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'))))))))))))) 0.00/0.21 "Strongly closed critical pair" 0.00/0.21 0.00/0.21 The problem is confluent. 0.00/0.21 0.00/0.21 Problem 1.8: 0.00/0.21 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.21 Confluence Problem: 0.00/0.21 (VAR x x') 0.00/0.21 (REPLACEMENT-MAP 0.00/0.21 (b 1) 0.00/0.21 (a 1) 0.00/0.21 (fSNonEmpty) 0.00/0.21 ) 0.00/0.21 (RULES 0.00/0.21 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.21 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.21 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.21 ) 0.00/0.21 Critical Pairs: 0.00/0.21 => Not trivial, Not overlay, Proper, NW0, N8 0.00/0.21 Linear:YES 0.00/0.21 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.21 0.00/0.21 Strong Confluence Procedure: 0.00/0.21 -> Rewritings: 0.00/0.21 s: b(a(a(a(b(b(a(a(b(b(a(a(a(b(x')))))))))))))) 0.00/0.21 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] 0.00/0.21 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)] 0.00/0.21 ID: 0 => ('b(a(a(a(b(b(a(a(b(b(a(a(a(b(x'))))))))))))))', D0) 0.00/0.21 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')))))))))))' 0.00/0.21 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')))))))))))))))))' 0.00/0.21 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'))))))))))))' 0.00/0.21 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')))))))))))))))))))' 0.00/0.21 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')))))))))))))))))))' 0.00/0.21 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'))))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))))' 0.00/0.23 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'))))))))))))))))))))' 0.00/0.23 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')))))))))))))))))))))' 0.00/0.24 t: b(a(a(b(b(a(a(a(b(a(a(a(b(b(x')))))))))))))) 0.00/0.24 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] 0.00/0.24 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)] 0.00/0.24 ID: 0 => ('b(a(a(b(b(a(a(a(b(a(a(a(b(b(x'))))))))))))))', D0) 0.00/0.24 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'))))))))))))))))' 0.00/0.24 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')))))))))' 0.00/0.24 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')))))))))))))))))' 0.00/0.24 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')))))))))' 0.00/0.24 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')))))))))))' 0.00/0.24 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')))))))))' 0.00/0.24 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')))))))))))' 0.00/0.24 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'))))))))))))' 0.00/0.24 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')))))))))))' 0.00/0.24 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'))))))))))))' 0.00/0.24 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')))))))))))))))))))' 0.00/0.24 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'))))))))))))' 0.00/0.24 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')))))))))))))))))))' 0.00/0.24 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')))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))' 0.00/0.24 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')))))))))))))))))))' 0.00/0.24 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')))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))))' 0.00/0.24 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')))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))))' 0.00/0.24 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')))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))))' 0.00/0.24 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')))))))))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))))' 0.00/0.24 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')))))))))))))))))))))' 0.00/0.24 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'))))))))))))))))))))' 0.00/0.24 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')))))))))))))))))))))' 0.00/0.24 SNodesPath1: 0.00/0.24 TNodesPath1: 0.00/0.24 SNodesPath2: 0.00/0.24 TNodesPath2: 0.00/0.24 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')))))))))))))) 0.00/0.24 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')))))))))))))) 0.00/0.24 "Strongly closed critical pair" 0.00/0.24 0.00/0.24 The problem is confluent. 0.00/0.24 0.00/0.24 Problem 1.9: 0.00/0.24 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.24 Confluence Problem: 0.00/0.24 (VAR x x') 0.00/0.24 (REPLACEMENT-MAP 0.00/0.24 (b 1) 0.00/0.24 (a 1) 0.00/0.24 (fSNonEmpty) 0.00/0.24 ) 0.00/0.24 (RULES 0.00/0.24 b(a(b(b(x)))) -> b(b(b(a(b(x))))) 0.00/0.24 b(a(a(b(b(x))))) -> b(a(b(b(a(a(b(x))))))) 0.00/0.24 b(a(a(a(b(b(x)))))) -> b(a(a(b(b(a(a(a(b(x))))))))) 0.00/0.24 ) 0.00/0.24 Critical Pairs: 0.00/0.24 => Not trivial, Not overlay, Proper, NW0, N9 0.00/0.24 Linear:YES 0.00/0.24 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.24 0.00/0.24 Strong Confluence Procedure: 0.00/0.24 -> Rewritings: 0.00/0.24 s: b(a(b(b(b(b(a(b(x')))))))) 0.00/0.24 Nodes: [0,1,2,3] 0.00/0.24 Edges: [(0,1),(1,2),(2,3)] 0.00/0.24 ID: 0 => ('b(a(b(b(b(b(a(b(x'))))))))', D0) 0.00/0.24 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')))))))))' 0.00/0.24 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'))))))))' 0.00/0.24 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')))))))' 0.00/0.24 t: b(b(b(a(b(a(b(b(x')))))))) 0.00/0.24 Nodes: [0,1,2,3] 0.00/0.24 Edges: [(0,1),(1,2),(2,3)] 0.00/0.24 ID: 0 => ('b(b(b(a(b(a(b(b(x'))))))))', D0) 0.00/0.24 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')))))' 0.00/0.24 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'))))))))' 0.00/0.24 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')))))))' 0.00/0.24 SNodesPath1: b(a(b(b(b(b(a(b(x')))))))) -> b(b(b(a(b(b(b(a(b(x'))))))))) 0.00/0.24 TNodesPath1: b(b(b(a(b(a(b(b(x')))))))) -> b(b(b(a(b(b(b(a(b(x'))))))))) 0.00/0.24 SNodesPath2: b(a(b(b(b(b(a(b(x')))))))) -> b(b(b(a(b(b(b(a(b(x'))))))))) 0.00/0.24 TNodesPath2: b(b(b(a(b(a(b(b(x')))))))) -> b(b(b(a(b(b(b(a(b(x'))))))))) 0.00/0.24 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')))))))) 0.00/0.24 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')))))))) 0.00/0.24 "Strongly closed critical pair" 0.00/0.24 0.00/0.24 The problem is confluent. 0.00/0.24 EOF