YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (p 1) (q 1) (r 1) (s 1) (f 1) (fSNonEmpty) ) (RULES p(x) -> q(x) p(x) -> r(x) q(x) -> s(p(x)) r(x) -> s(p(x)) s(x) -> f(p(x)) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: Linearity Procedure: Linear? YES Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (p 1) (q 1) (r 1) (s 1) (f 1) (fSNonEmpty) ) (RULES p(x) -> q(x) p(x) -> r(x) q(x) -> s(p(x)) r(x) -> s(p(x)) s(x) -> f(p(x)) ) Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: p(x) -> q(x) p(x) -> r(x) q(x) -> s(p(x)) r(x) -> s(p(x)) s(x) -> f(p(x)) -> Vars: x, x, x, x, x -> Rlps: (rule: p(x) -> q(x), id: 1, possubterms: p(x)->[]) (rule: p(x) -> r(x), id: 2, possubterms: p(x)->[]) (rule: q(x) -> s(p(x)), id: 3, possubterms: q(x)->[]) (rule: r(x) -> s(p(x)), id: 4, possubterms: r(x)->[]) (rule: s(x) -> f(p(x)), id: 5, possubterms: s(x)->[]) -> Unifications: (R2 unifies with R1 at p: [], l: p(x), lp: p(x), sig: {x -> x'}, l': p(x'), r: r(x), r': q(x')) -> Critical pairs info: => Not trivial, Overlay, Proper, NW0, N1 -> Problem conclusions: Left linear, Right linear, Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a TRS Problem 1.1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (p 1) (q 1) (r 1) (s 1) (f 1) (fSNonEmpty) ) (RULES p(x) -> q(x) p(x) -> r(x) q(x) -> s(p(x)) r(x) -> s(p(x)) s(x) -> f(p(x)) ) Critical Pairs: => Not trivial, Overlay, Proper, NW0, N1 Linear:YES ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Strong Confluence Procedure: -> Rewritings: s: q(x') Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241] Edges: [(0,1),(1,2),(1,3),(1,4),(2,5),(2,6),(3,5),(3,7),(4,6),(4,7),(4,8),(4,9),(5,10),(5,11),(5,12),(5,13),(6,12),(6,14),(6,15),(7,12),(7,16),(7,17),(8,14),(8,16),(8,18),(9,15),(9,17),(9,18),(10,19),(10,20),(10,21),(11,19),(11,22),(11,23),(12,20),(12,22),(12,24),(12,25),(12,26),(13,21),(13,23),(13,26),(13,27),(13,28),(14,24),(14,29),(15,25),(15,29),(16,24),(16,30),(17,25),(17,30),(18,29),(18,30),(18,31),(18,32),(18,33),(19,34),(19,35),(19,36),(19,37),(19,38),(20,36),(20,39),(20,40),(20,41),(21,37),(21,41),(21,42),(21,43),(22,36),(22,44),(22,45),(22,46),(23,37),(23,46),(23,47),(23,48),(24,39),(24,44),(24,49),(24,50),(25,40),(25,45),(25,49),(25,51),(26,41),(26,46),(26,50),(26,51),(26,52),(26,53),(27,42),(27,47),(27,52),(27,54),(28,43),(28,48),(28,53),(28,54),(29,49),(29,55),(29,56),(29,57),(30,49),(30,58),(30,59),(30,60),(31,55),(31,58),(31,61),(31,62),(32,56),(32,59),(32,61),(32,63),(33,57),(33,60),(33,62),(33,63),(33,64),(33,65),(34,66),(34,67),(34,68),(34,69),(35,66),(35,70),(35,71),(35,72),(36,67),(36,70),(36,73),(36,74),(36,75),(36,76),(37,68),(37,71),(37,75),(37,77),(37,78),(37,79),(38,69),(38,72),(38,76),(38,79),(38,80),(38,81),(39,73),(39,82),(39,83),(40,74),(40,82),(40,84),(41,75),(41,83),(41,84),(41,85),(41,86),(42,77),(42,85),(42,87),(43,78),(43,86),(43,87),(44,73),(44,88),(44,89),(45,74),(45,88),(45,90),(46,75),(46,89),(46,90),(46,91),(46,92),(47,77),(47,91),(47,93),(48,78),(48,92),(48,93),(49,82),(49,88),(49,94),(49,95),(49,96),(49,97),(50,83),(50,89),(50,97),(50,98),(50,99),(51,84),(51,90),(51,97),(51,100),(51,101),(52,85),(52,91),(52,98),(52,100),(52,102),(53,86),(53,92),(53,99),(53,101),(53,102),(54,87),(54,93),(54,102),(54,103),(54,104),(54,105),(55,94),(55,106),(55,107),(56,95),(56,106),(56,108),(57,96),(57,107),(57,108),(57,109),(57,110),(58,94),(58,111),(58,112),(59,95),(59,111),(59,113),(60,96),(60,112),(60,113),(60,114),(60,115),(61,106),(61,111),(61,116),(61,117),(61,118),(61,119),(62,107),(62,112),(62,118),(62,120),(62,121),(63,108),(63,113),(63,118),(63,122),(63,123),(64,109),(64,114),(64,120),(64,122),(64,124),(65,110),(65,115),(65,121),(65,123),(65,124),(66,125),(66,126),(66,127),(66,128),(66,129),(66,130),(67,127),(67,131),(67,132),(67,133),(67,134),(68,128),(68,133),(68,135),(68,136),(68,137),(69,129),(69,134),(69,137),(69,138),(69,139),(70,127),(70,140),(70,141),(70,142),(70,143),(71,128),(71,142),(71,144),(71,145),(71,146),(72,129),(72,143),(72,146),(72,147),(72,148),(73,131),(73,140),(73,149),(73,150),(73,151),(74,132),(74,141),(74,149),(74,152),(74,153),(75,133),(75,142),(75,150),(75,152),(75,154),(75,155),(75,156),(76,134),(76,143),(76,151),(76,153),(76,156),(76,157),(76,158),(77,135),(77,144),(77,154),(77,159),(77,160),(78,136),(78,145),(78,155),(78,159),(78,161),(79,137),(79,146),(79,156),(79,160),(79,161),(79,162),(79,163),(80,138),(80,147),(80,157),(80,162),(80,164),(81,139),(81,148),(81,158),(81,163),(81,164),(82,149),(82,165),(82,166),(82,167),(82,168),(83,150),(83,168),(83,169),(83,170),(84,152),(84,168),(84,171),(84,172),(85,154),(85,169),(85,171),(85,173),(86,155),(86,170),(86,172),(86,173),(87,159),(87,173),(87,174),(87,175),(87,176),(88,149),(88,177),(88,178),(88,179),(88,180),(89,150),(89,180),(89,181),(89,182),(90,152),(90,180),(90,183),(90,184),(91,154),(91,181),(91,183),(91,185),(92,155),(92,182),(92,184),(92,185),(93,159),(93,185),(93,186),(93,187),(93,188),(94,165),(94,177),(94,189),(94,190),(94,191),(95,166),(95,178),(95,189),(95,192),(95,193),(96,167),(96,179),(96,190),(96,192),(96,194),(96,195),(96,196),(97,168),(97,180),(97,191),(97,193),(97,196),(97,197),(97,198),(98,169),(98,181),(98,197),(98,199),(99,170),(99,182),(99,198),(99,199),(100,171),(100,183),(100,197),(100,200),(101,172),(101,184),(101,198),(101,200),(102,173),(102,185),(102,199),(102,200),(102,201),(102,202),(102,203),(103,174),(103,186),(103,201),(103,204),(103,205),(104,175),(104,187),(104,202),(104,204),(104,206),(105,176),(105,188),(105,203),(105,205),(105,206),(105,207),(105,208),(106,189),(106,209),(106,210),(106,211),(106,212),(107,190),(107,211),(107,213),(107,214),(108,192),(108,211),(108,215),(108,216),(109,194),(109,213),(109,215),(109,217),(110,195),(110,214),(110,216),(110,217),(111,189),(111,218),(111,219),(111,220),(111,221),(112,190),(112,220),(112,222),(112,223),(113,192),(113,220),(113,224),(113,225),(114,194),(114,222),(114,224),(114,226),(115,195),(115,223),(115,225),(115,226),(116,209),(116,218),(116,227),(116,228),(116,229),(117,210),(117,219),(117,227),(117,230),(117,231),(118,211),(118,220),(118,228),(118,230),(118,232),(118,233),(118,234),(119,212),(119,221),(119,229),(119,231),(119,234),(119,235),(119,236),(120,213),(120,222),(120,232),(120,237),(121,214),(121,223),(121,233),(121,237),(122,215),(122,224),(122,232),(122,238),(123,216),(123,225),(123,233),(123,238),(124,217),(124,226),(124,237),(124,238),(124,239),(124,240),(124,241)] ID: 0 => ('q(x')', D0) ID: 1 => ('s(p(x'))', D1, R3, P[], S{x6 -> x'}), NR: 's(p(x'))' ID: 2 => ('s(q(x'))', D2, R1, P[1], S{x4 -> x'}), NR: 'q(x')' ID: 3 => ('s(r(x'))', D2, R2, P[1], S{x5 -> x'}), NR: 'r(x')' ID: 4 => ('f(p(p(x')))', D2, R5, P[], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 5 => ('s(s(p(x')))', D3, R3, P[1], S{x6 -> x'}), NR: 's(p(x'))' ID: 6 => ('f(p(q(x')))', D3, R5, P[], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 7 => ('f(p(r(x')))', D3, R5, P[], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 8 => ('f(q(p(x')))', D3, R1, P[1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 9 => ('f(r(p(x')))', D3, R2, P[1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 10 => ('s(s(q(x')))', D4, R1, P[1, 1], S{x4 -> x'}), NR: 'q(x')' ID: 11 => ('s(s(r(x')))', D4, R2, P[1, 1], S{x5 -> x'}), NR: 'r(x')' ID: 12 => ('f(p(s(p(x'))))', D4, R5, P[], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 13 => ('s(f(p(p(x'))))', D4, R5, P[1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 14 => ('f(q(q(x')))', D4, R1, P[1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 15 => ('f(r(q(x')))', D4, R2, P[1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 16 => ('f(q(r(x')))', D4, R1, P[1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 17 => ('f(r(r(x')))', D4, R2, P[1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 18 => ('f(s(p(p(x'))))', D4, R3, P[1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 19 => ('s(s(s(p(x'))))', D5, R3, P[1, 1], S{x6 -> x'}), NR: 's(p(x'))' ID: 20 => ('f(p(s(q(x'))))', D5, R5, P[], S{x8 -> s(q(x'))}), NR: 'f(p(s(q(x'))))' ID: 21 => ('s(f(p(q(x'))))', D5, R5, P[1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 22 => ('f(p(s(r(x'))))', D5, R5, P[], S{x8 -> s(r(x'))}), NR: 'f(p(s(r(x'))))' ID: 23 => ('s(f(p(r(x'))))', D5, R5, P[1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 24 => ('f(q(s(p(x'))))', D5, R1, P[1], S{x4 -> s(p(x'))}), NR: 'q(s(p(x')))' ID: 25 => ('f(r(s(p(x'))))', D5, R2, P[1], S{x5 -> s(p(x'))}), NR: 'r(s(p(x')))' ID: 26 => ('f(p(f(p(p(x')))))', D5, R5, P[1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 27 => ('s(f(q(p(x'))))', D5, R1, P[1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 28 => ('s(f(r(p(x'))))', D5, R2, P[1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 29 => ('f(s(p(q(x'))))', D5, R3, P[1], S{x6 -> q(x')}), NR: 's(p(q(x')))' ID: 30 => ('f(s(p(r(x'))))', D5, R3, P[1], S{x6 -> r(x')}), NR: 's(p(r(x')))' ID: 31 => ('f(s(q(p(x'))))', D5, R1, P[1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 32 => ('f(s(r(p(x'))))', D5, R2, P[1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 33 => ('f(f(p(p(p(x')))))', D5, R5, P[1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 34 => ('s(s(s(q(x'))))', D6, R1, P[1, 1, 1], S{x4 -> x'}), NR: 'q(x')' ID: 35 => ('s(s(s(r(x'))))', D6, R2, P[1, 1, 1], S{x5 -> x'}), NR: 'r(x')' ID: 36 => ('f(p(s(s(p(x')))))', D6, R5, P[], S{x8 -> s(s(p(x')))}), NR: 'f(p(s(s(p(x')))))' ID: 37 => ('s(f(p(s(p(x')))))', D6, R5, P[1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 38 => ('s(s(f(p(p(x')))))', D6, R5, P[1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 39 => ('f(q(s(q(x'))))', D6, R1, P[1], S{x4 -> s(q(x'))}), NR: 'q(s(q(x')))' ID: 40 => ('f(r(s(q(x'))))', D6, R2, P[1], S{x5 -> s(q(x'))}), NR: 'r(s(q(x')))' ID: 41 => ('f(p(f(p(q(x')))))', D6, R5, P[1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 42 => ('s(f(q(q(x'))))', D6, R1, P[1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 43 => ('s(f(r(q(x'))))', D6, R2, P[1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 44 => ('f(q(s(r(x'))))', D6, R1, P[1], S{x4 -> s(r(x'))}), NR: 'q(s(r(x')))' ID: 45 => ('f(r(s(r(x'))))', D6, R2, P[1], S{x5 -> s(r(x'))}), NR: 'r(s(r(x')))' ID: 46 => ('f(p(f(p(r(x')))))', D6, R5, P[1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 47 => ('s(f(q(r(x'))))', D6, R1, P[1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 48 => ('s(f(r(r(x'))))', D6, R2, P[1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 49 => ('f(s(p(s(p(x')))))', D6, R3, P[1], S{x6 -> s(p(x'))}), NR: 's(p(s(p(x'))))' ID: 50 => ('f(q(f(p(p(x')))))', D6, R5, P[1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 51 => ('f(r(f(p(p(x')))))', D6, R5, P[1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 52 => ('f(p(f(q(p(x')))))', D6, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 53 => ('f(p(f(r(p(x')))))', D6, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 54 => ('s(f(s(p(p(x')))))', D6, R3, P[1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 55 => ('f(s(q(q(x'))))', D6, R1, P[1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 56 => ('f(s(r(q(x'))))', D6, R2, P[1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 57 => ('f(f(p(p(q(x')))))', D6, R5, P[1], S{x8 -> p(q(x'))}), NR: 'f(p(p(q(x'))))' ID: 58 => ('f(s(q(r(x'))))', D6, R1, P[1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 59 => ('f(s(r(r(x'))))', D6, R2, P[1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 60 => ('f(f(p(p(r(x')))))', D6, R5, P[1], S{x8 -> p(r(x'))}), NR: 'f(p(p(r(x'))))' ID: 61 => ('f(s(s(p(p(x')))))', D6, R3, P[1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 62 => ('f(f(p(q(p(x')))))', D6, R5, P[1], S{x8 -> q(p(x'))}), NR: 'f(p(q(p(x'))))' ID: 63 => ('f(f(p(r(p(x')))))', D6, R5, P[1], S{x8 -> r(p(x'))}), NR: 'f(p(r(p(x'))))' ID: 64 => ('f(f(q(p(p(x')))))', D6, R1, P[1, 1], S{x4 -> p(p(x'))}), NR: 'q(p(p(x')))' ID: 65 => ('f(f(r(p(p(x')))))', D6, R2, P[1, 1], S{x5 -> p(p(x'))}), NR: 'r(p(p(x')))' ID: 66 => ('s(s(s(s(p(x')))))', D7, R3, P[1, 1, 1], S{x6 -> x'}), NR: 's(p(x'))' ID: 67 => ('f(p(s(s(q(x')))))', D7, R5, P[], S{x8 -> s(s(q(x')))}), NR: 'f(p(s(s(q(x')))))' ID: 68 => ('s(f(p(s(q(x')))))', D7, R5, P[1], S{x8 -> s(q(x'))}), NR: 'f(p(s(q(x'))))' ID: 69 => ('s(s(f(p(q(x')))))', D7, R5, P[1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 70 => ('f(p(s(s(r(x')))))', D7, R5, P[], S{x8 -> s(s(r(x')))}), NR: 'f(p(s(s(r(x')))))' ID: 71 => ('s(f(p(s(r(x')))))', D7, R5, P[1], S{x8 -> s(r(x'))}), NR: 'f(p(s(r(x'))))' ID: 72 => ('s(s(f(p(r(x')))))', D7, R5, P[1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 73 => ('f(q(s(s(p(x')))))', D7, R1, P[1], S{x4 -> s(s(p(x')))}), NR: 'q(s(s(p(x'))))' ID: 74 => ('f(r(s(s(p(x')))))', D7, R2, P[1], S{x5 -> s(s(p(x')))}), NR: 'r(s(s(p(x'))))' ID: 75 => ('f(p(f(p(s(p(x'))))))', D7, R5, P[1, 1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 76 => ('f(p(s(f(p(p(x'))))))', D7, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 77 => ('s(f(q(s(p(x')))))', D7, R1, P[1, 1], S{x4 -> s(p(x'))}), NR: 'q(s(p(x')))' ID: 78 => ('s(f(r(s(p(x')))))', D7, R2, P[1, 1], S{x5 -> s(p(x'))}), NR: 'r(s(p(x')))' ID: 79 => ('s(f(p(f(p(p(x'))))))', D7, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 80 => ('s(s(f(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 81 => ('s(s(f(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 82 => ('f(s(p(s(q(x')))))', D7, R3, P[1], S{x6 -> s(q(x'))}), NR: 's(p(s(q(x'))))' ID: 83 => ('f(q(f(p(q(x')))))', D7, R5, P[1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 84 => ('f(r(f(p(q(x')))))', D7, R5, P[1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 85 => ('f(p(f(q(q(x')))))', D7, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 86 => ('f(p(f(r(q(x')))))', D7, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 87 => ('s(f(s(p(q(x')))))', D7, R3, P[1, 1], S{x6 -> q(x')}), NR: 's(p(q(x')))' ID: 88 => ('f(s(p(s(r(x')))))', D7, R3, P[1], S{x6 -> s(r(x'))}), NR: 's(p(s(r(x'))))' ID: 89 => ('f(q(f(p(r(x')))))', D7, R5, P[1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 90 => ('f(r(f(p(r(x')))))', D7, R5, P[1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 91 => ('f(p(f(q(r(x')))))', D7, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 92 => ('f(p(f(r(r(x')))))', D7, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 93 => ('s(f(s(p(r(x')))))', D7, R3, P[1, 1], S{x6 -> r(x')}), NR: 's(p(r(x')))' ID: 94 => ('f(s(q(s(p(x')))))', D7, R1, P[1, 1], S{x4 -> s(p(x'))}), NR: 'q(s(p(x')))' ID: 95 => ('f(s(r(s(p(x')))))', D7, R2, P[1, 1], S{x5 -> s(p(x'))}), NR: 'r(s(p(x')))' ID: 96 => ('f(f(p(p(s(p(x'))))))', D7, R5, P[1], S{x8 -> p(s(p(x')))}), NR: 'f(p(p(s(p(x')))))' ID: 97 => ('f(s(p(f(p(p(x'))))))', D7, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 98 => ('f(q(f(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 99 => ('f(q(f(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 100 => ('f(r(f(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 101 => ('f(r(f(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 102 => ('f(p(f(s(p(p(x'))))))', D7, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 103 => ('s(f(s(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 104 => ('s(f(s(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 105 => ('s(f(f(p(p(p(x'))))))', D7, R5, P[1, 1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 106 => ('f(s(s(p(q(x')))))', D7, R3, P[1, 1], S{x6 -> q(x')}), NR: 's(p(q(x')))' ID: 107 => ('f(f(p(q(q(x')))))', D7, R5, P[1], S{x8 -> q(q(x'))}), NR: 'f(p(q(q(x'))))' ID: 108 => ('f(f(p(r(q(x')))))', D7, R5, P[1], S{x8 -> r(q(x'))}), NR: 'f(p(r(q(x'))))' ID: 109 => ('f(f(q(p(q(x')))))', D7, R1, P[1, 1], S{x4 -> p(q(x'))}), NR: 'q(p(q(x')))' ID: 110 => ('f(f(r(p(q(x')))))', D7, R2, P[1, 1], S{x5 -> p(q(x'))}), NR: 'r(p(q(x')))' ID: 111 => ('f(s(s(p(r(x')))))', D7, R3, P[1, 1], S{x6 -> r(x')}), NR: 's(p(r(x')))' ID: 112 => ('f(f(p(q(r(x')))))', D7, R5, P[1], S{x8 -> q(r(x'))}), NR: 'f(p(q(r(x'))))' ID: 113 => ('f(f(p(r(r(x')))))', D7, R5, P[1], S{x8 -> r(r(x'))}), NR: 'f(p(r(r(x'))))' ID: 114 => ('f(f(q(p(r(x')))))', D7, R1, P[1, 1], S{x4 -> p(r(x'))}), NR: 'q(p(r(x')))' ID: 115 => ('f(f(r(p(r(x')))))', D7, R2, P[1, 1], S{x5 -> p(r(x'))}), NR: 'r(p(r(x')))' ID: 116 => ('f(s(s(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 117 => ('f(s(s(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 118 => ('f(f(p(s(p(p(x'))))))', D7, R5, P[1], S{x8 -> s(p(p(x')))}), NR: 'f(p(s(p(p(x')))))' ID: 119 => ('f(s(f(p(p(p(x'))))))', D7, R5, P[1, 1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 120 => ('f(f(q(q(p(x')))))', D7, R1, P[1, 1], S{x4 -> q(p(x'))}), NR: 'q(q(p(x')))' ID: 121 => ('f(f(r(q(p(x')))))', D7, R2, P[1, 1], S{x5 -> q(p(x'))}), NR: 'r(q(p(x')))' ID: 122 => ('f(f(q(r(p(x')))))', D7, R1, P[1, 1], S{x4 -> r(p(x'))}), NR: 'q(r(p(x')))' ID: 123 => ('f(f(r(r(p(x')))))', D7, R2, P[1, 1], S{x5 -> r(p(x'))}), NR: 'r(r(p(x')))' ID: 124 => ('f(f(s(p(p(p(x'))))))', D7, R3, P[1, 1], S{x6 -> p(p(x'))}), NR: 's(p(p(p(x'))))' ID: 125 => ('s(s(s(s(q(x')))))', D8, R1, P[1, 1, 1, 1], S{x4 -> x'}), NR: 'q(x')' ID: 126 => ('s(s(s(s(r(x')))))', D8, R2, P[1, 1, 1, 1], S{x5 -> x'}), NR: 'r(x')' ID: 127 => ('f(p(s(s(s(p(x'))))))', D8, R5, P[], S{x8 -> s(s(s(p(x'))))}), NR: 'f(p(s(s(s(p(x'))))))' ID: 128 => ('s(f(p(s(s(p(x'))))))', D8, R5, P[1], S{x8 -> s(s(p(x')))}), NR: 'f(p(s(s(p(x')))))' ID: 129 => ('s(s(f(p(s(p(x'))))))', D8, R5, P[1, 1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 130 => ('s(s(s(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 131 => ('f(q(s(s(q(x')))))', D8, R1, P[1], S{x4 -> s(s(q(x')))}), NR: 'q(s(s(q(x'))))' ID: 132 => ('f(r(s(s(q(x')))))', D8, R2, P[1], S{x5 -> s(s(q(x')))}), NR: 'r(s(s(q(x'))))' ID: 133 => ('f(p(f(p(s(q(x'))))))', D8, R5, P[1, 1], S{x8 -> s(q(x'))}), NR: 'f(p(s(q(x'))))' ID: 134 => ('f(p(s(f(p(q(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 135 => ('s(f(q(s(q(x')))))', D8, R1, P[1, 1], S{x4 -> s(q(x'))}), NR: 'q(s(q(x')))' ID: 136 => ('s(f(r(s(q(x')))))', D8, R2, P[1, 1], S{x5 -> s(q(x'))}), NR: 'r(s(q(x')))' ID: 137 => ('s(f(p(f(p(q(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 138 => ('s(s(f(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 139 => ('s(s(f(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 140 => ('f(q(s(s(r(x')))))', D8, R1, P[1], S{x4 -> s(s(r(x')))}), NR: 'q(s(s(r(x'))))' ID: 141 => ('f(r(s(s(r(x')))))', D8, R2, P[1], S{x5 -> s(s(r(x')))}), NR: 'r(s(s(r(x'))))' ID: 142 => ('f(p(f(p(s(r(x'))))))', D8, R5, P[1, 1], S{x8 -> s(r(x'))}), NR: 'f(p(s(r(x'))))' ID: 143 => ('f(p(s(f(p(r(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 144 => ('s(f(q(s(r(x')))))', D8, R1, P[1, 1], S{x4 -> s(r(x'))}), NR: 'q(s(r(x')))' ID: 145 => ('s(f(r(s(r(x')))))', D8, R2, P[1, 1], S{x5 -> s(r(x'))}), NR: 'r(s(r(x')))' ID: 146 => ('s(f(p(f(p(r(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 147 => ('s(s(f(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 148 => ('s(s(f(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 149 => ('f(s(p(s(s(p(x'))))))', D8, R3, P[1], S{x6 -> s(s(p(x')))}), NR: 's(p(s(s(p(x')))))' ID: 150 => ('f(q(f(p(s(p(x'))))))', D8, R5, P[1, 1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 151 => ('f(q(s(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 152 => ('f(r(f(p(s(p(x'))))))', D8, R5, P[1, 1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 153 => ('f(r(s(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 154 => ('f(p(f(q(s(p(x'))))))', D8, R1, P[1, 1, 1], S{x4 -> s(p(x'))}), NR: 'q(s(p(x')))' ID: 155 => ('f(p(f(r(s(p(x'))))))', D8, R2, P[1, 1, 1], S{x5 -> s(p(x'))}), NR: 'r(s(p(x')))' ID: 156 => ('f(p(f(p(f(p(p(x')))))))', D8, R5, P[1, 1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 157 => ('f(p(s(f(q(p(x'))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 158 => ('f(p(s(f(r(p(x'))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 159 => ('s(f(s(p(s(p(x'))))))', D8, R3, P[1, 1], S{x6 -> s(p(x'))}), NR: 's(p(s(p(x'))))' ID: 160 => ('s(f(q(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 161 => ('s(f(r(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 162 => ('s(f(p(f(q(p(x'))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 163 => ('s(f(p(f(r(p(x'))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 164 => ('s(s(f(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 165 => ('f(s(q(s(q(x')))))', D8, R1, P[1, 1], S{x4 -> s(q(x'))}), NR: 'q(s(q(x')))' ID: 166 => ('f(s(r(s(q(x')))))', D8, R2, P[1, 1], S{x5 -> s(q(x'))}), NR: 'r(s(q(x')))' ID: 167 => ('f(f(p(p(s(q(x'))))))', D8, R5, P[1], S{x8 -> p(s(q(x')))}), NR: 'f(p(p(s(q(x')))))' ID: 168 => ('f(s(p(f(p(q(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 169 => ('f(q(f(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 170 => ('f(q(f(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 171 => ('f(r(f(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 172 => ('f(r(f(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 173 => ('f(p(f(s(p(q(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> q(x')}), NR: 's(p(q(x')))' ID: 174 => ('s(f(s(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 175 => ('s(f(s(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 176 => ('s(f(f(p(p(q(x'))))))', D8, R5, P[1, 1], S{x8 -> p(q(x'))}), NR: 'f(p(p(q(x'))))' ID: 177 => ('f(s(q(s(r(x')))))', D8, R1, P[1, 1], S{x4 -> s(r(x'))}), NR: 'q(s(r(x')))' ID: 178 => ('f(s(r(s(r(x')))))', D8, R2, P[1, 1], S{x5 -> s(r(x'))}), NR: 'r(s(r(x')))' ID: 179 => ('f(f(p(p(s(r(x'))))))', D8, R5, P[1], S{x8 -> p(s(r(x')))}), NR: 'f(p(p(s(r(x')))))' ID: 180 => ('f(s(p(f(p(r(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 181 => ('f(q(f(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 182 => ('f(q(f(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 183 => ('f(r(f(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 184 => ('f(r(f(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 185 => ('f(p(f(s(p(r(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> r(x')}), NR: 's(p(r(x')))' ID: 186 => ('s(f(s(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 187 => ('s(f(s(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 188 => ('s(f(f(p(p(r(x'))))))', D8, R5, P[1, 1], S{x8 -> p(r(x'))}), NR: 'f(p(p(r(x'))))' ID: 189 => ('f(s(s(p(s(p(x'))))))', D8, R3, P[1, 1], S{x6 -> s(p(x'))}), NR: 's(p(s(p(x'))))' ID: 190 => ('f(f(p(q(s(p(x'))))))', D8, R5, P[1], S{x8 -> q(s(p(x')))}), NR: 'f(p(q(s(p(x')))))' ID: 191 => ('f(s(q(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 192 => ('f(f(p(r(s(p(x'))))))', D8, R5, P[1], S{x8 -> r(s(p(x')))}), NR: 'f(p(r(s(p(x')))))' ID: 193 => ('f(s(r(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 194 => ('f(f(q(p(s(p(x'))))))', D8, R1, P[1, 1], S{x4 -> p(s(p(x')))}), NR: 'q(p(s(p(x'))))' ID: 195 => ('f(f(r(p(s(p(x'))))))', D8, R2, P[1, 1], S{x5 -> p(s(p(x')))}), NR: 'r(p(s(p(x'))))' ID: 196 => ('f(f(p(p(f(p(p(x')))))))', D8, R5, P[1, 1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 197 => ('f(s(p(f(q(p(x'))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 198 => ('f(s(p(f(r(p(x'))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 199 => ('f(q(f(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 200 => ('f(r(f(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 201 => ('f(p(f(s(q(p(x'))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 202 => ('f(p(f(s(r(p(x'))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 203 => ('f(p(f(f(p(p(p(x')))))))', D8, R5, P[1, 1, 1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 204 => ('s(f(s(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 205 => ('s(f(f(p(q(p(x'))))))', D8, R5, P[1, 1], S{x8 -> q(p(x'))}), NR: 'f(p(q(p(x'))))' ID: 206 => ('s(f(f(p(r(p(x'))))))', D8, R5, P[1, 1], S{x8 -> r(p(x'))}), NR: 'f(p(r(p(x'))))' ID: 207 => ('s(f(f(q(p(p(x'))))))', D8, R1, P[1, 1, 1], S{x4 -> p(p(x'))}), NR: 'q(p(p(x')))' ID: 208 => ('s(f(f(r(p(p(x'))))))', D8, R2, P[1, 1, 1], S{x5 -> p(p(x'))}), NR: 'r(p(p(x')))' ID: 209 => ('f(s(s(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 210 => ('f(s(s(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 211 => ('f(f(p(s(p(q(x'))))))', D8, R5, P[1], S{x8 -> s(p(q(x')))}), NR: 'f(p(s(p(q(x')))))' ID: 212 => ('f(s(f(p(p(q(x'))))))', D8, R5, P[1, 1], S{x8 -> p(q(x'))}), NR: 'f(p(p(q(x'))))' ID: 213 => ('f(f(q(q(q(x')))))', D8, R1, P[1, 1], S{x4 -> q(q(x'))}), NR: 'q(q(q(x')))' ID: 214 => ('f(f(r(q(q(x')))))', D8, R2, P[1, 1], S{x5 -> q(q(x'))}), NR: 'r(q(q(x')))' ID: 215 => ('f(f(q(r(q(x')))))', D8, R1, P[1, 1], S{x4 -> r(q(x'))}), NR: 'q(r(q(x')))' ID: 216 => ('f(f(r(r(q(x')))))', D8, R2, P[1, 1], S{x5 -> r(q(x'))}), NR: 'r(r(q(x')))' ID: 217 => ('f(f(s(p(p(q(x'))))))', D8, R3, P[1, 1], S{x6 -> p(q(x'))}), NR: 's(p(p(q(x'))))' ID: 218 => ('f(s(s(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 219 => ('f(s(s(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 220 => ('f(f(p(s(p(r(x'))))))', D8, R5, P[1], S{x8 -> s(p(r(x')))}), NR: 'f(p(s(p(r(x')))))' ID: 221 => ('f(s(f(p(p(r(x'))))))', D8, R5, P[1, 1], S{x8 -> p(r(x'))}), NR: 'f(p(p(r(x'))))' ID: 222 => ('f(f(q(q(r(x')))))', D8, R1, P[1, 1], S{x4 -> q(r(x'))}), NR: 'q(q(r(x')))' ID: 223 => ('f(f(r(q(r(x')))))', D8, R2, P[1, 1], S{x5 -> q(r(x'))}), NR: 'r(q(r(x')))' ID: 224 => ('f(f(q(r(r(x')))))', D8, R1, P[1, 1], S{x4 -> r(r(x'))}), NR: 'q(r(r(x')))' ID: 225 => ('f(f(r(r(r(x')))))', D8, R2, P[1, 1], S{x5 -> r(r(x'))}), NR: 'r(r(r(x')))' ID: 226 => ('f(f(s(p(p(r(x'))))))', D8, R3, P[1, 1], S{x6 -> p(r(x'))}), NR: 's(p(p(r(x'))))' ID: 227 => ('f(s(s(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 228 => ('f(f(p(s(q(p(x'))))))', D8, R5, P[1], S{x8 -> s(q(p(x')))}), NR: 'f(p(s(q(p(x')))))' ID: 229 => ('f(s(f(p(q(p(x'))))))', D8, R5, P[1, 1], S{x8 -> q(p(x'))}), NR: 'f(p(q(p(x'))))' ID: 230 => ('f(f(p(s(r(p(x'))))))', D8, R5, P[1], S{x8 -> s(r(p(x')))}), NR: 'f(p(s(r(p(x')))))' ID: 231 => ('f(s(f(p(r(p(x'))))))', D8, R5, P[1, 1], S{x8 -> r(p(x'))}), NR: 'f(p(r(p(x'))))' ID: 232 => ('f(f(q(s(p(p(x'))))))', D8, R1, P[1, 1], S{x4 -> s(p(p(x')))}), NR: 'q(s(p(p(x'))))' ID: 233 => ('f(f(r(s(p(p(x'))))))', D8, R2, P[1, 1], S{x5 -> s(p(p(x')))}), NR: 'r(s(p(p(x'))))' ID: 234 => ('f(f(p(f(p(p(p(x')))))))', D8, R5, P[1, 1, 1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 235 => ('f(s(f(q(p(p(x'))))))', D8, R1, P[1, 1, 1], S{x4 -> p(p(x'))}), NR: 'q(p(p(x')))' ID: 236 => ('f(s(f(r(p(p(x'))))))', D8, R2, P[1, 1, 1], S{x5 -> p(p(x'))}), NR: 'r(p(p(x')))' ID: 237 => ('f(f(s(p(q(p(x'))))))', D8, R3, P[1, 1], S{x6 -> q(p(x'))}), NR: 's(p(q(p(x'))))' ID: 238 => ('f(f(s(p(r(p(x'))))))', D8, R3, P[1, 1], S{x6 -> r(p(x'))}), NR: 's(p(r(p(x'))))' ID: 239 => ('f(f(s(q(p(p(x'))))))', D8, R1, P[1, 1, 1], S{x4 -> p(p(x'))}), NR: 'q(p(p(x')))' ID: 240 => ('f(f(s(r(p(p(x'))))))', D8, R2, P[1, 1, 1], S{x5 -> p(p(x'))}), NR: 'r(p(p(x')))' ID: 241 => ('f(f(f(p(p(p(p(x')))))))', D8, R5, P[1, 1], S{x8 -> p(p(p(x')))}), NR: 'f(p(p(p(p(x')))))' t: r(x') Nodes: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241] Edges: [(0,1),(1,2),(1,3),(1,4),(2,5),(2,6),(3,5),(3,7),(4,6),(4,7),(4,8),(4,9),(5,10),(5,11),(5,12),(5,13),(6,12),(6,14),(6,15),(7,12),(7,16),(7,17),(8,14),(8,16),(8,18),(9,15),(9,17),(9,18),(10,19),(10,20),(10,21),(11,19),(11,22),(11,23),(12,20),(12,22),(12,24),(12,25),(12,26),(13,21),(13,23),(13,26),(13,27),(13,28),(14,24),(14,29),(15,25),(15,29),(16,24),(16,30),(17,25),(17,30),(18,29),(18,30),(18,31),(18,32),(18,33),(19,34),(19,35),(19,36),(19,37),(19,38),(20,36),(20,39),(20,40),(20,41),(21,37),(21,41),(21,42),(21,43),(22,36),(22,44),(22,45),(22,46),(23,37),(23,46),(23,47),(23,48),(24,39),(24,44),(24,49),(24,50),(25,40),(25,45),(25,49),(25,51),(26,41),(26,46),(26,50),(26,51),(26,52),(26,53),(27,42),(27,47),(27,52),(27,54),(28,43),(28,48),(28,53),(28,54),(29,49),(29,55),(29,56),(29,57),(30,49),(30,58),(30,59),(30,60),(31,55),(31,58),(31,61),(31,62),(32,56),(32,59),(32,61),(32,63),(33,57),(33,60),(33,62),(33,63),(33,64),(33,65),(34,66),(34,67),(34,68),(34,69),(35,66),(35,70),(35,71),(35,72),(36,67),(36,70),(36,73),(36,74),(36,75),(36,76),(37,68),(37,71),(37,75),(37,77),(37,78),(37,79),(38,69),(38,72),(38,76),(38,79),(38,80),(38,81),(39,73),(39,82),(39,83),(40,74),(40,82),(40,84),(41,75),(41,83),(41,84),(41,85),(41,86),(42,77),(42,85),(42,87),(43,78),(43,86),(43,87),(44,73),(44,88),(44,89),(45,74),(45,88),(45,90),(46,75),(46,89),(46,90),(46,91),(46,92),(47,77),(47,91),(47,93),(48,78),(48,92),(48,93),(49,82),(49,88),(49,94),(49,95),(49,96),(49,97),(50,83),(50,89),(50,97),(50,98),(50,99),(51,84),(51,90),(51,97),(51,100),(51,101),(52,85),(52,91),(52,98),(52,100),(52,102),(53,86),(53,92),(53,99),(53,101),(53,102),(54,87),(54,93),(54,102),(54,103),(54,104),(54,105),(55,94),(55,106),(55,107),(56,95),(56,106),(56,108),(57,96),(57,107),(57,108),(57,109),(57,110),(58,94),(58,111),(58,112),(59,95),(59,111),(59,113),(60,96),(60,112),(60,113),(60,114),(60,115),(61,106),(61,111),(61,116),(61,117),(61,118),(61,119),(62,107),(62,112),(62,118),(62,120),(62,121),(63,108),(63,113),(63,118),(63,122),(63,123),(64,109),(64,114),(64,120),(64,122),(64,124),(65,110),(65,115),(65,121),(65,123),(65,124),(66,125),(66,126),(66,127),(66,128),(66,129),(66,130),(67,127),(67,131),(67,132),(67,133),(67,134),(68,128),(68,133),(68,135),(68,136),(68,137),(69,129),(69,134),(69,137),(69,138),(69,139),(70,127),(70,140),(70,141),(70,142),(70,143),(71,128),(71,142),(71,144),(71,145),(71,146),(72,129),(72,143),(72,146),(72,147),(72,148),(73,131),(73,140),(73,149),(73,150),(73,151),(74,132),(74,141),(74,149),(74,152),(74,153),(75,133),(75,142),(75,150),(75,152),(75,154),(75,155),(75,156),(76,134),(76,143),(76,151),(76,153),(76,156),(76,157),(76,158),(77,135),(77,144),(77,154),(77,159),(77,160),(78,136),(78,145),(78,155),(78,159),(78,161),(79,137),(79,146),(79,156),(79,160),(79,161),(79,162),(79,163),(80,138),(80,147),(80,157),(80,162),(80,164),(81,139),(81,148),(81,158),(81,163),(81,164),(82,149),(82,165),(82,166),(82,167),(82,168),(83,150),(83,168),(83,169),(83,170),(84,152),(84,168),(84,171),(84,172),(85,154),(85,169),(85,171),(85,173),(86,155),(86,170),(86,172),(86,173),(87,159),(87,173),(87,174),(87,175),(87,176),(88,149),(88,177),(88,178),(88,179),(88,180),(89,150),(89,180),(89,181),(89,182),(90,152),(90,180),(90,183),(90,184),(91,154),(91,181),(91,183),(91,185),(92,155),(92,182),(92,184),(92,185),(93,159),(93,185),(93,186),(93,187),(93,188),(94,165),(94,177),(94,189),(94,190),(94,191),(95,166),(95,178),(95,189),(95,192),(95,193),(96,167),(96,179),(96,190),(96,192),(96,194),(96,195),(96,196),(97,168),(97,180),(97,191),(97,193),(97,196),(97,197),(97,198),(98,169),(98,181),(98,197),(98,199),(99,170),(99,182),(99,198),(99,199),(100,171),(100,183),(100,197),(100,200),(101,172),(101,184),(101,198),(101,200),(102,173),(102,185),(102,199),(102,200),(102,201),(102,202),(102,203),(103,174),(103,186),(103,201),(103,204),(103,205),(104,175),(104,187),(104,202),(104,204),(104,206),(105,176),(105,188),(105,203),(105,205),(105,206),(105,207),(105,208),(106,189),(106,209),(106,210),(106,211),(106,212),(107,190),(107,211),(107,213),(107,214),(108,192),(108,211),(108,215),(108,216),(109,194),(109,213),(109,215),(109,217),(110,195),(110,214),(110,216),(110,217),(111,189),(111,218),(111,219),(111,220),(111,221),(112,190),(112,220),(112,222),(112,223),(113,192),(113,220),(113,224),(113,225),(114,194),(114,222),(114,224),(114,226),(115,195),(115,223),(115,225),(115,226),(116,209),(116,218),(116,227),(116,228),(116,229),(117,210),(117,219),(117,227),(117,230),(117,231),(118,211),(118,220),(118,228),(118,230),(118,232),(118,233),(118,234),(119,212),(119,221),(119,229),(119,231),(119,234),(119,235),(119,236),(120,213),(120,222),(120,232),(120,237),(121,214),(121,223),(121,233),(121,237),(122,215),(122,224),(122,232),(122,238),(123,216),(123,225),(123,233),(123,238),(124,217),(124,226),(124,237),(124,238),(124,239),(124,240),(124,241)] ID: 0 => ('r(x')', D0) ID: 1 => ('s(p(x'))', D1, R4, P[], S{x7 -> x'}), NR: 's(p(x'))' ID: 2 => ('s(q(x'))', D2, R1, P[1], S{x4 -> x'}), NR: 'q(x')' ID: 3 => ('s(r(x'))', D2, R2, P[1], S{x5 -> x'}), NR: 'r(x')' ID: 4 => ('f(p(p(x')))', D2, R5, P[], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 5 => ('s(s(p(x')))', D3, R3, P[1], S{x6 -> x'}), NR: 's(p(x'))' ID: 6 => ('f(p(q(x')))', D3, R5, P[], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 7 => ('f(p(r(x')))', D3, R5, P[], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 8 => ('f(q(p(x')))', D3, R1, P[1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 9 => ('f(r(p(x')))', D3, R2, P[1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 10 => ('s(s(q(x')))', D4, R1, P[1, 1], S{x4 -> x'}), NR: 'q(x')' ID: 11 => ('s(s(r(x')))', D4, R2, P[1, 1], S{x5 -> x'}), NR: 'r(x')' ID: 12 => ('f(p(s(p(x'))))', D4, R5, P[], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 13 => ('s(f(p(p(x'))))', D4, R5, P[1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 14 => ('f(q(q(x')))', D4, R1, P[1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 15 => ('f(r(q(x')))', D4, R2, P[1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 16 => ('f(q(r(x')))', D4, R1, P[1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 17 => ('f(r(r(x')))', D4, R2, P[1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 18 => ('f(s(p(p(x'))))', D4, R3, P[1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 19 => ('s(s(s(p(x'))))', D5, R3, P[1, 1], S{x6 -> x'}), NR: 's(p(x'))' ID: 20 => ('f(p(s(q(x'))))', D5, R5, P[], S{x8 -> s(q(x'))}), NR: 'f(p(s(q(x'))))' ID: 21 => ('s(f(p(q(x'))))', D5, R5, P[1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 22 => ('f(p(s(r(x'))))', D5, R5, P[], S{x8 -> s(r(x'))}), NR: 'f(p(s(r(x'))))' ID: 23 => ('s(f(p(r(x'))))', D5, R5, P[1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 24 => ('f(q(s(p(x'))))', D5, R1, P[1], S{x4 -> s(p(x'))}), NR: 'q(s(p(x')))' ID: 25 => ('f(r(s(p(x'))))', D5, R2, P[1], S{x5 -> s(p(x'))}), NR: 'r(s(p(x')))' ID: 26 => ('f(p(f(p(p(x')))))', D5, R5, P[1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 27 => ('s(f(q(p(x'))))', D5, R1, P[1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 28 => ('s(f(r(p(x'))))', D5, R2, P[1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 29 => ('f(s(p(q(x'))))', D5, R3, P[1], S{x6 -> q(x')}), NR: 's(p(q(x')))' ID: 30 => ('f(s(p(r(x'))))', D5, R3, P[1], S{x6 -> r(x')}), NR: 's(p(r(x')))' ID: 31 => ('f(s(q(p(x'))))', D5, R1, P[1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 32 => ('f(s(r(p(x'))))', D5, R2, P[1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 33 => ('f(f(p(p(p(x')))))', D5, R5, P[1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 34 => ('s(s(s(q(x'))))', D6, R1, P[1, 1, 1], S{x4 -> x'}), NR: 'q(x')' ID: 35 => ('s(s(s(r(x'))))', D6, R2, P[1, 1, 1], S{x5 -> x'}), NR: 'r(x')' ID: 36 => ('f(p(s(s(p(x')))))', D6, R5, P[], S{x8 -> s(s(p(x')))}), NR: 'f(p(s(s(p(x')))))' ID: 37 => ('s(f(p(s(p(x')))))', D6, R5, P[1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 38 => ('s(s(f(p(p(x')))))', D6, R5, P[1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 39 => ('f(q(s(q(x'))))', D6, R1, P[1], S{x4 -> s(q(x'))}), NR: 'q(s(q(x')))' ID: 40 => ('f(r(s(q(x'))))', D6, R2, P[1], S{x5 -> s(q(x'))}), NR: 'r(s(q(x')))' ID: 41 => ('f(p(f(p(q(x')))))', D6, R5, P[1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 42 => ('s(f(q(q(x'))))', D6, R1, P[1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 43 => ('s(f(r(q(x'))))', D6, R2, P[1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 44 => ('f(q(s(r(x'))))', D6, R1, P[1], S{x4 -> s(r(x'))}), NR: 'q(s(r(x')))' ID: 45 => ('f(r(s(r(x'))))', D6, R2, P[1], S{x5 -> s(r(x'))}), NR: 'r(s(r(x')))' ID: 46 => ('f(p(f(p(r(x')))))', D6, R5, P[1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 47 => ('s(f(q(r(x'))))', D6, R1, P[1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 48 => ('s(f(r(r(x'))))', D6, R2, P[1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 49 => ('f(s(p(s(p(x')))))', D6, R3, P[1], S{x6 -> s(p(x'))}), NR: 's(p(s(p(x'))))' ID: 50 => ('f(q(f(p(p(x')))))', D6, R5, P[1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 51 => ('f(r(f(p(p(x')))))', D6, R5, P[1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 52 => ('f(p(f(q(p(x')))))', D6, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 53 => ('f(p(f(r(p(x')))))', D6, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 54 => ('s(f(s(p(p(x')))))', D6, R3, P[1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 55 => ('f(s(q(q(x'))))', D6, R1, P[1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 56 => ('f(s(r(q(x'))))', D6, R2, P[1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 57 => ('f(f(p(p(q(x')))))', D6, R5, P[1], S{x8 -> p(q(x'))}), NR: 'f(p(p(q(x'))))' ID: 58 => ('f(s(q(r(x'))))', D6, R1, P[1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 59 => ('f(s(r(r(x'))))', D6, R2, P[1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 60 => ('f(f(p(p(r(x')))))', D6, R5, P[1], S{x8 -> p(r(x'))}), NR: 'f(p(p(r(x'))))' ID: 61 => ('f(s(s(p(p(x')))))', D6, R3, P[1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 62 => ('f(f(p(q(p(x')))))', D6, R5, P[1], S{x8 -> q(p(x'))}), NR: 'f(p(q(p(x'))))' ID: 63 => ('f(f(p(r(p(x')))))', D6, R5, P[1], S{x8 -> r(p(x'))}), NR: 'f(p(r(p(x'))))' ID: 64 => ('f(f(q(p(p(x')))))', D6, R1, P[1, 1], S{x4 -> p(p(x'))}), NR: 'q(p(p(x')))' ID: 65 => ('f(f(r(p(p(x')))))', D6, R2, P[1, 1], S{x5 -> p(p(x'))}), NR: 'r(p(p(x')))' ID: 66 => ('s(s(s(s(p(x')))))', D7, R3, P[1, 1, 1], S{x6 -> x'}), NR: 's(p(x'))' ID: 67 => ('f(p(s(s(q(x')))))', D7, R5, P[], S{x8 -> s(s(q(x')))}), NR: 'f(p(s(s(q(x')))))' ID: 68 => ('s(f(p(s(q(x')))))', D7, R5, P[1], S{x8 -> s(q(x'))}), NR: 'f(p(s(q(x'))))' ID: 69 => ('s(s(f(p(q(x')))))', D7, R5, P[1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 70 => ('f(p(s(s(r(x')))))', D7, R5, P[], S{x8 -> s(s(r(x')))}), NR: 'f(p(s(s(r(x')))))' ID: 71 => ('s(f(p(s(r(x')))))', D7, R5, P[1], S{x8 -> s(r(x'))}), NR: 'f(p(s(r(x'))))' ID: 72 => ('s(s(f(p(r(x')))))', D7, R5, P[1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 73 => ('f(q(s(s(p(x')))))', D7, R1, P[1], S{x4 -> s(s(p(x')))}), NR: 'q(s(s(p(x'))))' ID: 74 => ('f(r(s(s(p(x')))))', D7, R2, P[1], S{x5 -> s(s(p(x')))}), NR: 'r(s(s(p(x'))))' ID: 75 => ('f(p(f(p(s(p(x'))))))', D7, R5, P[1, 1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 76 => ('f(p(s(f(p(p(x'))))))', D7, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 77 => ('s(f(q(s(p(x')))))', D7, R1, P[1, 1], S{x4 -> s(p(x'))}), NR: 'q(s(p(x')))' ID: 78 => ('s(f(r(s(p(x')))))', D7, R2, P[1, 1], S{x5 -> s(p(x'))}), NR: 'r(s(p(x')))' ID: 79 => ('s(f(p(f(p(p(x'))))))', D7, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 80 => ('s(s(f(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 81 => ('s(s(f(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 82 => ('f(s(p(s(q(x')))))', D7, R3, P[1], S{x6 -> s(q(x'))}), NR: 's(p(s(q(x'))))' ID: 83 => ('f(q(f(p(q(x')))))', D7, R5, P[1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 84 => ('f(r(f(p(q(x')))))', D7, R5, P[1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 85 => ('f(p(f(q(q(x')))))', D7, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 86 => ('f(p(f(r(q(x')))))', D7, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 87 => ('s(f(s(p(q(x')))))', D7, R3, P[1, 1], S{x6 -> q(x')}), NR: 's(p(q(x')))' ID: 88 => ('f(s(p(s(r(x')))))', D7, R3, P[1], S{x6 -> s(r(x'))}), NR: 's(p(s(r(x'))))' ID: 89 => ('f(q(f(p(r(x')))))', D7, R5, P[1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 90 => ('f(r(f(p(r(x')))))', D7, R5, P[1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 91 => ('f(p(f(q(r(x')))))', D7, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 92 => ('f(p(f(r(r(x')))))', D7, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 93 => ('s(f(s(p(r(x')))))', D7, R3, P[1, 1], S{x6 -> r(x')}), NR: 's(p(r(x')))' ID: 94 => ('f(s(q(s(p(x')))))', D7, R1, P[1, 1], S{x4 -> s(p(x'))}), NR: 'q(s(p(x')))' ID: 95 => ('f(s(r(s(p(x')))))', D7, R2, P[1, 1], S{x5 -> s(p(x'))}), NR: 'r(s(p(x')))' ID: 96 => ('f(f(p(p(s(p(x'))))))', D7, R5, P[1], S{x8 -> p(s(p(x')))}), NR: 'f(p(p(s(p(x')))))' ID: 97 => ('f(s(p(f(p(p(x'))))))', D7, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 98 => ('f(q(f(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 99 => ('f(q(f(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 100 => ('f(r(f(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 101 => ('f(r(f(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 102 => ('f(p(f(s(p(p(x'))))))', D7, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 103 => ('s(f(s(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 104 => ('s(f(s(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 105 => ('s(f(f(p(p(p(x'))))))', D7, R5, P[1, 1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 106 => ('f(s(s(p(q(x')))))', D7, R3, P[1, 1], S{x6 -> q(x')}), NR: 's(p(q(x')))' ID: 107 => ('f(f(p(q(q(x')))))', D7, R5, P[1], S{x8 -> q(q(x'))}), NR: 'f(p(q(q(x'))))' ID: 108 => ('f(f(p(r(q(x')))))', D7, R5, P[1], S{x8 -> r(q(x'))}), NR: 'f(p(r(q(x'))))' ID: 109 => ('f(f(q(p(q(x')))))', D7, R1, P[1, 1], S{x4 -> p(q(x'))}), NR: 'q(p(q(x')))' ID: 110 => ('f(f(r(p(q(x')))))', D7, R2, P[1, 1], S{x5 -> p(q(x'))}), NR: 'r(p(q(x')))' ID: 111 => ('f(s(s(p(r(x')))))', D7, R3, P[1, 1], S{x6 -> r(x')}), NR: 's(p(r(x')))' ID: 112 => ('f(f(p(q(r(x')))))', D7, R5, P[1], S{x8 -> q(r(x'))}), NR: 'f(p(q(r(x'))))' ID: 113 => ('f(f(p(r(r(x')))))', D7, R5, P[1], S{x8 -> r(r(x'))}), NR: 'f(p(r(r(x'))))' ID: 114 => ('f(f(q(p(r(x')))))', D7, R1, P[1, 1], S{x4 -> p(r(x'))}), NR: 'q(p(r(x')))' ID: 115 => ('f(f(r(p(r(x')))))', D7, R2, P[1, 1], S{x5 -> p(r(x'))}), NR: 'r(p(r(x')))' ID: 116 => ('f(s(s(q(p(x')))))', D7, R1, P[1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 117 => ('f(s(s(r(p(x')))))', D7, R2, P[1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 118 => ('f(f(p(s(p(p(x'))))))', D7, R5, P[1], S{x8 -> s(p(p(x')))}), NR: 'f(p(s(p(p(x')))))' ID: 119 => ('f(s(f(p(p(p(x'))))))', D7, R5, P[1, 1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 120 => ('f(f(q(q(p(x')))))', D7, R1, P[1, 1], S{x4 -> q(p(x'))}), NR: 'q(q(p(x')))' ID: 121 => ('f(f(r(q(p(x')))))', D7, R2, P[1, 1], S{x5 -> q(p(x'))}), NR: 'r(q(p(x')))' ID: 122 => ('f(f(q(r(p(x')))))', D7, R1, P[1, 1], S{x4 -> r(p(x'))}), NR: 'q(r(p(x')))' ID: 123 => ('f(f(r(r(p(x')))))', D7, R2, P[1, 1], S{x5 -> r(p(x'))}), NR: 'r(r(p(x')))' ID: 124 => ('f(f(s(p(p(p(x'))))))', D7, R3, P[1, 1], S{x6 -> p(p(x'))}), NR: 's(p(p(p(x'))))' ID: 125 => ('s(s(s(s(q(x')))))', D8, R1, P[1, 1, 1, 1], S{x4 -> x'}), NR: 'q(x')' ID: 126 => ('s(s(s(s(r(x')))))', D8, R2, P[1, 1, 1, 1], S{x5 -> x'}), NR: 'r(x')' ID: 127 => ('f(p(s(s(s(p(x'))))))', D8, R5, P[], S{x8 -> s(s(s(p(x'))))}), NR: 'f(p(s(s(s(p(x'))))))' ID: 128 => ('s(f(p(s(s(p(x'))))))', D8, R5, P[1], S{x8 -> s(s(p(x')))}), NR: 'f(p(s(s(p(x')))))' ID: 129 => ('s(s(f(p(s(p(x'))))))', D8, R5, P[1, 1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 130 => ('s(s(s(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 131 => ('f(q(s(s(q(x')))))', D8, R1, P[1], S{x4 -> s(s(q(x')))}), NR: 'q(s(s(q(x'))))' ID: 132 => ('f(r(s(s(q(x')))))', D8, R2, P[1], S{x5 -> s(s(q(x')))}), NR: 'r(s(s(q(x'))))' ID: 133 => ('f(p(f(p(s(q(x'))))))', D8, R5, P[1, 1], S{x8 -> s(q(x'))}), NR: 'f(p(s(q(x'))))' ID: 134 => ('f(p(s(f(p(q(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 135 => ('s(f(q(s(q(x')))))', D8, R1, P[1, 1], S{x4 -> s(q(x'))}), NR: 'q(s(q(x')))' ID: 136 => ('s(f(r(s(q(x')))))', D8, R2, P[1, 1], S{x5 -> s(q(x'))}), NR: 'r(s(q(x')))' ID: 137 => ('s(f(p(f(p(q(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 138 => ('s(s(f(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 139 => ('s(s(f(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 140 => ('f(q(s(s(r(x')))))', D8, R1, P[1], S{x4 -> s(s(r(x')))}), NR: 'q(s(s(r(x'))))' ID: 141 => ('f(r(s(s(r(x')))))', D8, R2, P[1], S{x5 -> s(s(r(x')))}), NR: 'r(s(s(r(x'))))' ID: 142 => ('f(p(f(p(s(r(x'))))))', D8, R5, P[1, 1], S{x8 -> s(r(x'))}), NR: 'f(p(s(r(x'))))' ID: 143 => ('f(p(s(f(p(r(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 144 => ('s(f(q(s(r(x')))))', D8, R1, P[1, 1], S{x4 -> s(r(x'))}), NR: 'q(s(r(x')))' ID: 145 => ('s(f(r(s(r(x')))))', D8, R2, P[1, 1], S{x5 -> s(r(x'))}), NR: 'r(s(r(x')))' ID: 146 => ('s(f(p(f(p(r(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 147 => ('s(s(f(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 148 => ('s(s(f(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 149 => ('f(s(p(s(s(p(x'))))))', D8, R3, P[1], S{x6 -> s(s(p(x')))}), NR: 's(p(s(s(p(x')))))' ID: 150 => ('f(q(f(p(s(p(x'))))))', D8, R5, P[1, 1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 151 => ('f(q(s(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 152 => ('f(r(f(p(s(p(x'))))))', D8, R5, P[1, 1], S{x8 -> s(p(x'))}), NR: 'f(p(s(p(x'))))' ID: 153 => ('f(r(s(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 154 => ('f(p(f(q(s(p(x'))))))', D8, R1, P[1, 1, 1], S{x4 -> s(p(x'))}), NR: 'q(s(p(x')))' ID: 155 => ('f(p(f(r(s(p(x'))))))', D8, R2, P[1, 1, 1], S{x5 -> s(p(x'))}), NR: 'r(s(p(x')))' ID: 156 => ('f(p(f(p(f(p(p(x')))))))', D8, R5, P[1, 1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 157 => ('f(p(s(f(q(p(x'))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 158 => ('f(p(s(f(r(p(x'))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 159 => ('s(f(s(p(s(p(x'))))))', D8, R3, P[1, 1], S{x6 -> s(p(x'))}), NR: 's(p(s(p(x'))))' ID: 160 => ('s(f(q(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 161 => ('s(f(r(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 162 => ('s(f(p(f(q(p(x'))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 163 => ('s(f(p(f(r(p(x'))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 164 => ('s(s(f(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 165 => ('f(s(q(s(q(x')))))', D8, R1, P[1, 1], S{x4 -> s(q(x'))}), NR: 'q(s(q(x')))' ID: 166 => ('f(s(r(s(q(x')))))', D8, R2, P[1, 1], S{x5 -> s(q(x'))}), NR: 'r(s(q(x')))' ID: 167 => ('f(f(p(p(s(q(x'))))))', D8, R5, P[1], S{x8 -> p(s(q(x')))}), NR: 'f(p(p(s(q(x')))))' ID: 168 => ('f(s(p(f(p(q(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> q(x')}), NR: 'f(p(q(x')))' ID: 169 => ('f(q(f(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 170 => ('f(q(f(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 171 => ('f(r(f(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 172 => ('f(r(f(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 173 => ('f(p(f(s(p(q(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> q(x')}), NR: 's(p(q(x')))' ID: 174 => ('s(f(s(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 175 => ('s(f(s(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 176 => ('s(f(f(p(p(q(x'))))))', D8, R5, P[1, 1], S{x8 -> p(q(x'))}), NR: 'f(p(p(q(x'))))' ID: 177 => ('f(s(q(s(r(x')))))', D8, R1, P[1, 1], S{x4 -> s(r(x'))}), NR: 'q(s(r(x')))' ID: 178 => ('f(s(r(s(r(x')))))', D8, R2, P[1, 1], S{x5 -> s(r(x'))}), NR: 'r(s(r(x')))' ID: 179 => ('f(f(p(p(s(r(x'))))))', D8, R5, P[1], S{x8 -> p(s(r(x')))}), NR: 'f(p(p(s(r(x')))))' ID: 180 => ('f(s(p(f(p(r(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> r(x')}), NR: 'f(p(r(x')))' ID: 181 => ('f(q(f(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 182 => ('f(q(f(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 183 => ('f(r(f(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 184 => ('f(r(f(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 185 => ('f(p(f(s(p(r(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> r(x')}), NR: 's(p(r(x')))' ID: 186 => ('s(f(s(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 187 => ('s(f(s(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 188 => ('s(f(f(p(p(r(x'))))))', D8, R5, P[1, 1], S{x8 -> p(r(x'))}), NR: 'f(p(p(r(x'))))' ID: 189 => ('f(s(s(p(s(p(x'))))))', D8, R3, P[1, 1], S{x6 -> s(p(x'))}), NR: 's(p(s(p(x'))))' ID: 190 => ('f(f(p(q(s(p(x'))))))', D8, R5, P[1], S{x8 -> q(s(p(x')))}), NR: 'f(p(q(s(p(x')))))' ID: 191 => ('f(s(q(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 192 => ('f(f(p(r(s(p(x'))))))', D8, R5, P[1], S{x8 -> r(s(p(x')))}), NR: 'f(p(r(s(p(x')))))' ID: 193 => ('f(s(r(f(p(p(x'))))))', D8, R5, P[1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 194 => ('f(f(q(p(s(p(x'))))))', D8, R1, P[1, 1], S{x4 -> p(s(p(x')))}), NR: 'q(p(s(p(x'))))' ID: 195 => ('f(f(r(p(s(p(x'))))))', D8, R2, P[1, 1], S{x5 -> p(s(p(x')))}), NR: 'r(p(s(p(x'))))' ID: 196 => ('f(f(p(p(f(p(p(x')))))))', D8, R5, P[1, 1, 1, 1], S{x8 -> p(x')}), NR: 'f(p(p(x')))' ID: 197 => ('f(s(p(f(q(p(x'))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 198 => ('f(s(p(f(r(p(x'))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 199 => ('f(q(f(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 200 => ('f(r(f(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 201 => ('f(p(f(s(q(p(x'))))))', D8, R1, P[1, 1, 1, 1], S{x4 -> p(x')}), NR: 'q(p(x'))' ID: 202 => ('f(p(f(s(r(p(x'))))))', D8, R2, P[1, 1, 1, 1], S{x5 -> p(x')}), NR: 'r(p(x'))' ID: 203 => ('f(p(f(f(p(p(p(x')))))))', D8, R5, P[1, 1, 1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 204 => ('s(f(s(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 205 => ('s(f(f(p(q(p(x'))))))', D8, R5, P[1, 1], S{x8 -> q(p(x'))}), NR: 'f(p(q(p(x'))))' ID: 206 => ('s(f(f(p(r(p(x'))))))', D8, R5, P[1, 1], S{x8 -> r(p(x'))}), NR: 'f(p(r(p(x'))))' ID: 207 => ('s(f(f(q(p(p(x'))))))', D8, R1, P[1, 1, 1], S{x4 -> p(p(x'))}), NR: 'q(p(p(x')))' ID: 208 => ('s(f(f(r(p(p(x'))))))', D8, R2, P[1, 1, 1], S{x5 -> p(p(x'))}), NR: 'r(p(p(x')))' ID: 209 => ('f(s(s(q(q(x')))))', D8, R1, P[1, 1, 1], S{x4 -> q(x')}), NR: 'q(q(x'))' ID: 210 => ('f(s(s(r(q(x')))))', D8, R2, P[1, 1, 1], S{x5 -> q(x')}), NR: 'r(q(x'))' ID: 211 => ('f(f(p(s(p(q(x'))))))', D8, R5, P[1], S{x8 -> s(p(q(x')))}), NR: 'f(p(s(p(q(x')))))' ID: 212 => ('f(s(f(p(p(q(x'))))))', D8, R5, P[1, 1], S{x8 -> p(q(x'))}), NR: 'f(p(p(q(x'))))' ID: 213 => ('f(f(q(q(q(x')))))', D8, R1, P[1, 1], S{x4 -> q(q(x'))}), NR: 'q(q(q(x')))' ID: 214 => ('f(f(r(q(q(x')))))', D8, R2, P[1, 1], S{x5 -> q(q(x'))}), NR: 'r(q(q(x')))' ID: 215 => ('f(f(q(r(q(x')))))', D8, R1, P[1, 1], S{x4 -> r(q(x'))}), NR: 'q(r(q(x')))' ID: 216 => ('f(f(r(r(q(x')))))', D8, R2, P[1, 1], S{x5 -> r(q(x'))}), NR: 'r(r(q(x')))' ID: 217 => ('f(f(s(p(p(q(x'))))))', D8, R3, P[1, 1], S{x6 -> p(q(x'))}), NR: 's(p(p(q(x'))))' ID: 218 => ('f(s(s(q(r(x')))))', D8, R1, P[1, 1, 1], S{x4 -> r(x')}), NR: 'q(r(x'))' ID: 219 => ('f(s(s(r(r(x')))))', D8, R2, P[1, 1, 1], S{x5 -> r(x')}), NR: 'r(r(x'))' ID: 220 => ('f(f(p(s(p(r(x'))))))', D8, R5, P[1], S{x8 -> s(p(r(x')))}), NR: 'f(p(s(p(r(x')))))' ID: 221 => ('f(s(f(p(p(r(x'))))))', D8, R5, P[1, 1], S{x8 -> p(r(x'))}), NR: 'f(p(p(r(x'))))' ID: 222 => ('f(f(q(q(r(x')))))', D8, R1, P[1, 1], S{x4 -> q(r(x'))}), NR: 'q(q(r(x')))' ID: 223 => ('f(f(r(q(r(x')))))', D8, R2, P[1, 1], S{x5 -> q(r(x'))}), NR: 'r(q(r(x')))' ID: 224 => ('f(f(q(r(r(x')))))', D8, R1, P[1, 1], S{x4 -> r(r(x'))}), NR: 'q(r(r(x')))' ID: 225 => ('f(f(r(r(r(x')))))', D8, R2, P[1, 1], S{x5 -> r(r(x'))}), NR: 'r(r(r(x')))' ID: 226 => ('f(f(s(p(p(r(x'))))))', D8, R3, P[1, 1], S{x6 -> p(r(x'))}), NR: 's(p(p(r(x'))))' ID: 227 => ('f(s(s(s(p(p(x'))))))', D8, R3, P[1, 1, 1], S{x6 -> p(x')}), NR: 's(p(p(x')))' ID: 228 => ('f(f(p(s(q(p(x'))))))', D8, R5, P[1], S{x8 -> s(q(p(x')))}), NR: 'f(p(s(q(p(x')))))' ID: 229 => ('f(s(f(p(q(p(x'))))))', D8, R5, P[1, 1], S{x8 -> q(p(x'))}), NR: 'f(p(q(p(x'))))' ID: 230 => ('f(f(p(s(r(p(x'))))))', D8, R5, P[1], S{x8 -> s(r(p(x')))}), NR: 'f(p(s(r(p(x')))))' ID: 231 => ('f(s(f(p(r(p(x'))))))', D8, R5, P[1, 1], S{x8 -> r(p(x'))}), NR: 'f(p(r(p(x'))))' ID: 232 => ('f(f(q(s(p(p(x'))))))', D8, R1, P[1, 1], S{x4 -> s(p(p(x')))}), NR: 'q(s(p(p(x'))))' ID: 233 => ('f(f(r(s(p(p(x'))))))', D8, R2, P[1, 1], S{x5 -> s(p(p(x')))}), NR: 'r(s(p(p(x'))))' ID: 234 => ('f(f(p(f(p(p(p(x')))))))', D8, R5, P[1, 1, 1], S{x8 -> p(p(x'))}), NR: 'f(p(p(p(x'))))' ID: 235 => ('f(s(f(q(p(p(x'))))))', D8, R1, P[1, 1, 1], S{x4 -> p(p(x'))}), NR: 'q(p(p(x')))' ID: 236 => ('f(s(f(r(p(p(x'))))))', D8, R2, P[1, 1, 1], S{x5 -> p(p(x'))}), NR: 'r(p(p(x')))' ID: 237 => ('f(f(s(p(q(p(x'))))))', D8, R3, P[1, 1], S{x6 -> q(p(x'))}), NR: 's(p(q(p(x'))))' ID: 238 => ('f(f(s(p(r(p(x'))))))', D8, R3, P[1, 1], S{x6 -> r(p(x'))}), NR: 's(p(r(p(x'))))' ID: 239 => ('f(f(s(q(p(p(x'))))))', D8, R1, P[1, 1, 1], S{x4 -> p(p(x'))}), NR: 'q(p(p(x')))' ID: 240 => ('f(f(s(r(p(p(x'))))))', D8, R2, P[1, 1, 1], S{x5 -> p(p(x'))}), NR: 'r(p(p(x')))' ID: 241 => ('f(f(f(p(p(p(p(x')))))))', D8, R5, P[1, 1], S{x8 -> p(p(p(x')))}), NR: 'f(p(p(p(p(x')))))' SNodesPath1: q(x') -> s(p(x')) TNodesPath1: r(x') -> s(p(x')) SNodesPath2: q(x') -> s(p(x')) TNodesPath2: r(x') -> s(p(x')) q(x') ->= s(p(x')) *<- r(x') r(x') ->= s(p(x')) *<- q(x') "Strongly closed critical pair" The problem is confluent.