Certificate for #21729 ⟨a, b | aaa=1, ababbba=b⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(b) = 0; deg(a) = 1

Axiom: aaa=1.

Defines rule #11.

Referenced 265 times.

Axiom: ababbba=b.

Referenced by [3], [4], [7], [11], [14].

Overlap of [1] aaa=1 with [2] ababbba=b:

Critical pair: aab=babbba.

Flip LHS and RHS.

Defines rule #5.

Referenced 217 times.

Overlap of [2] ababbba=b with [1] aaa=1:

Critical pair: ababbb=baa.

Flip LHS and RHS.

Defines rule #4.

Referenced 292 times.

Overlap of [3] babbba=aab with [3] babbba=aab:

Critical pair: babbaab=aabbbba.

Reduce LHS:

Referenced by [7], [10], [15], [19], [20], [22], [26], [28], [30], [33], [35], [37], [39], [48], [51], [52], [53], [55], [57], [60], [62], [66], [68], [71], [89], [90], [92], [98], [101], [102], [104], [108], [117], [118], [120], [122], [125], [129], [130], [131], [132], [134], [135], [136], [137], [138], [140], [146], [156], [157], [159], [160], [162], [167], [170], [172], [178], [191], [195], [198], [208], [213], [215], [229], [234], [255], [256], [260], [265], [271], [272], [276], [279], [283], [285], [289], [296], [314], [315], [318], [319], [353].

Overlap of [3] babbba=aab with [4] baa=ababbb:

Critical pair: babbababbb=aaba.

Referenced by [11], [18], [23], [30], [49], [52], [60], [61], [67], [75], [89], [92], [94], [96], [101], [119], [121], [126], [138], [139], [140], [141], [155], [158], [162], [176], [182].

Overlap of [5] babababbbb=aabbbba with [3] babbba=aab:

Critical pair: babababbbaab=aabbbbaabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [8].

Overlap of [1] aaa=1 with [7] aabbbababbbbbba=babbab:

Critical pair: ababbab=bbbababbbbbba.

Flip LHS and RHS.

Referenced by [9], [10], [11], [12], [13], [34], [35], [47], [57], [58], [59], [60], [61], [65], [72], [74], [76], [91], [94], [96], [103], [112], [121], [127], [128], [131], [145], [148], [163], [164], [256], [262], [264], [270].

Overlap of [3] babbba=aab with [8] bbbababbbbbba=ababbab:

Critical pair: baababbab=aabbabbbbbba.

Reduce LHS:

Referenced by [21], [22], [23].

Overlap of [5] babababbbb=aabbbba with [8] bbbababbbbbba=ababbab:

Critical pair: babababababbab=aabbbbaababbbbbba.

Reduce RHS:

Referenced by [43].

Overlap of [6] babbababbb=aaba with [8] bbbababbbbbba=ababbab:

Critical pair: babbababbababbab=aababbababbbbbba.

Reduce RHS:

Referenced by [14], [15], [16], [19].

Overlap of [8] bbbababbbbbba=ababbab with [3] babbba=aab:

Critical pair: bbbababbbbbaab=ababbabbbba.

Reduce LHS:

Referenced by [51], [70], [139], [158], [245], [250].

Overlap of [8] bbbababbbbbba=ababbab with [4] baa=ababbb:

Critical pair: bbbababbbbbababbb=ababbaba.

Referenced by [23], [57], [58], [71], [92], [139], [140], [141], [158], [159], [165], [183].

Overlap of [2] ababbba=b with [11] babbababbababbab=b:

Critical pair: ababbb=bbbababbababbab.

Flip LHS and RHS.

Referenced by [17].

Overlap of [11] babbababbababbab=b with [3] babbba=aab:

Critical pair: babbababbababaab=bbba.

Reduce LHS:

Referenced by [59], [60], [61], [62], [70], [128], [181].

Overlap of [11] babbababbababbab=b with [11] babbababbababbab=b:

Critical pair: babbababbababb=bbababbababbab.

Flip LHS and RHS.

Referenced by [17].

Simplify [14] bbbababbababbab=ababbb.

Reduce LHS:

Referenced by [18], [19].

Overlap of [6] babbababbb=aaba with [17] bbabbababbababb=ababbb:

Critical pair: babbababbababbb=aabababbababbababb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [11] babbababbababbab=b with [17] bbabbababbababb=ababbb:

Critical pair: babbababbabaababbb=bbababbababb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [18] aabababbababbababb=aab with [19] bbababbababb=babbbbbababbbbbbbabbb:

Critical pair: aababababbbbbababbbbbbbabbb=aab.

Reduce LHS:

Referenced by [50], [51].

Overlap of [1] aaa=1 with [9] ababbbbabbab=aabbabbbbbba:

Critical pair: aaaabbabbbbbba=babbbbabbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31], [32], [41], [45], [48], [49], [61], [62], [64], [72], [110], [117], [121], [128], [131], [141], [150], [156], [166], [173], [186], [199], [210], [255], [259], [260], [263], [268], [271], [276], [280], [281], [290], [297], [298], [316], [317], [328], [331], [332], [334], [338], [341], [345], [349], [351], [368], [377], [384], [386], [389], [396], [397], [441].

Overlap of [5] babababbbb=aabbbba with [9] ababbbbabbab=aabbabbbbbba:

Critical pair: babaabbabbbbbba=aabbbbaabbab.

Reduce LHS:

Reduce RHS:

Referenced by [71].

Overlap of [9] ababbbbabbab=aabbabbbbbba with [6] babbababbb=aaba:

Critical pair: ababbbbabbaaaba=aabbabbbbbbaabbababbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [1] aaa=1 with [23] aabbabbababbaba=bab:

Critical pair: abab=bbabbababbaba.

Flip LHS and RHS.

Referenced by [25], [26].

Overlap of [3] babbba=aab with [24] bbabbababbaba=abab:

Critical pair: bababab=aabbbababbaba.

Flip LHS and RHS.

Referenced by [27], [28].

Overlap of [24] bbabbababbaba=abab with [4] baa=ababbb:

Critical pair: bbabbababbaababbb=ababa.

Reduce LHS:

Referenced by [33], [34], [35], [53], [66], [67], [93], [97], [104], [105], [106], [111], [117], [118], [122], [129], [132], [142], [143], [144], [160], [184].

Overlap of [1] aaa=1 with [25] aabbbababbaba=bababab:

Critical pair: abababab=bbbababbaba.

Flip LHS and RHS.

Referenced by [29], [30], [62], [73], [112], [117], [130], [134], [174], [185].

Overlap of [25] aabbbababbaba=bababab with [4] baa=ababbb:

Critical pair: aabbbababbaababbb=babababa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30], [43], [54], [55], [56], [57], [74], [104], [113], [117], [129], [164], [165], [181], [251], [252], [272], [284].

Overlap of [3] babbba=aab with [27] bbbababbaba=abababab:

Critical pair: baabababab=aabbabbaba.

Reduce LHS:

Referenced by [36], [37], [38], [39].

Overlap of [6] babbababbb=aaba with [27] bbbababbaba=abababab:

Critical pair: babbababbabababab=aababbababbaba.

Reduce LHS:

Referenced by [77].

Overlap of [3] babbba=aab with [21] babbbbabbab=abbabbbbbba:

Critical pair: babbabbabbbbbba=aabbbbbabbab.

Referenced by [97], [98], [99], [133], [134], [273], [333], [335], [336], [344], [350], [360].

Overlap of [21] babbbbabbab=abbabbbbbba with [3] babbba=aab:

Critical pair: babbbbabaab=abbabbbbbbabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [223], [246].

Overlap of [5] babababbbb=aabbbba with [26] bbabbbbbababbbbbb=ababa:

Critical pair: babababbababa=aabbbbaabbbbbababbbbbb.

Reduce RHS:

Referenced by [102].

Overlap of [8] bbbababbbbbba=ababbab with [26] bbabbbbbababbbbbb=ababa:

Critical pair: bbbababbbbababa=ababbabbbbbbababbbbbb.

Referenced by [106].

Overlap of [26] bbabbbbbababbbbbb=ababa with [8] bbbababbbbbba=ababbab:

Critical pair: bbabbbbbababbbbababbab=abababababbbbbba.

Reduce RHS:

Referenced by [186].

Overlap of [1] aaa=1 with [29] ababbbbababab=aabbabbaba:

Critical pair: aaaabbabbaba=babbbbababab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [40], [41], [42], [79].

Overlap of [29] ababbbbababab=aabbabbaba with [3] babbba=aab:

Critical pair: ababbbbababaaab=aabbabbabaabbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [128].

Overlap of [29] ababbbbababab=aabbabbaba with [4] baa=ababbb:

Critical pair: ababbbbababaababbb=aabbabbabaaa.

Reduce LHS:

Reduce RHS:

Referenced by [280], [281], [282], [283], [358], [359].

Overlap of [29] ababbbbababab=aabbabbaba with [5] babababbbb=aabbbba:

Critical pair: ababbbbaaabbbba=aabbabbabaabbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [74], [162].

Overlap of [3] babbba=aab with [36] babbbbababab=abbabbaba:

Critical pair: babbabbabbaba=aabbbbbababab.

Referenced by [58], [64], [80].

Overlap of [21] babbbbabbab=abbabbbbbba with [36] babbbbababab=abbabbaba:

Critical pair: babbbbababbabbaba=abbabbbbbbabbbababab.

Reduce RHS:

Referenced by [188].

Overlap of [36] babbbbababab=abbabbaba with [3] babbba=aab:

Critical pair: babbbbabaaab=abbabbababba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [44], [45], [49].

Overlap of [10] babababababbab=aabbbababbbbabbbbbba with [28] babababa=aabbbbbbababbbbbb:

Critical pair: aabbbbbbababbbbbbbabbab=aabbbababbbbabbbbbba.

Referenced by [81].

Overlap of [1] aaa=1 with [42] abbabbababba=babbbbabb:

Critical pair: aababbbbabb=bbabbababba.

Flip LHS and RHS.

Referenced by [46], [47], [48], [49], [51], [64], [99], [106], [121], [131], [151], [167].

Overlap of [21] babbbbabbab=abbabbbbbba with [42] abbabbababba=babbbbabb:

Critical pair: babbbbbabbbbabb=abbabbbbbbabababba.

Flip LHS and RHS.

Referenced by [82].

Overlap of [3] babbba=aab with [44] bbabbababba=aababbbbabb:

Critical pair: babaababbbbabb=aabbbababba.

Reduce LHS:

Referenced by [311].

Overlap of [8] bbbababbbbbba=ababbab with [44] bbabbababba=aababbbbabb:

Critical pair: bbbababbbbaababbbbabb=ababbabbbababba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [189].

Overlap of [21] babbbbabbab=abbabbbbbba with [44] bbabbababba=aababbbbabb:

Critical pair: babbaababbbbabb=abbabbbbbbaabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [190].

Overlap of [44] bbabbababba=aababbbbabb with [42] abbabbababba=babbbbabb:

Critical pair: bbabbababbbabbbbabb=aababbbbabbbbabbababba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [108], [191].

Overlap of [1] aaa=1 with [20] abbababbbbbababbbbbbb=aab:

Critical pair: aaaab=bbababbbbbababbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [52], [53], [58], [68], [69], [70], [83].

Overlap of [20] abbababbbbbababbbbbbb=aab with [44] bbabbababba=aababbbbabb:

Critical pair: abbababbbbbababbbbbaababbbbabb=aababbababba.

Reduce LHS:

Referenced by [84].

Overlap of [6] babbababbb=aaba with [50] bbababbbbbababbbbbbb=ab:

Critical pair: babbababbab=aababababbbbbababbbbbbb.

Reduce RHS:

Referenced by [60], [70], [77], [119], [126], [128].

Overlap of [26] bbabbbbbababbbbbb=ababa with [50] bbababbbbbababbbbbbb=ab:

Critical pair: bbabbbbbababbbbbab=abababababbbbbababbbbbbb.

Reduce RHS:

Referenced by [71], [144], [192].

Overlap of [28] babababa=aabbbbbbababbbbbb with [3] babbba=aab:

Critical pair: bababaaab=aabbbbbbababbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [100].

Overlap of [28] babababa=aabbbbbbababbbbbb with [5] babababbbb=aabbbba:

Critical pair: baaabbbba=aabbbbbbababbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [88].

Overlap of [28] babababa=aabbbbbbababbbbbb with [28] babababa=aabbbbbbababbbbbb:

Critical pair: baaabbbbbbababbbbbb=aabbbbbbababbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [74], [81], [104], [117].

Overlap of [13] bbbababbbbbababbb=ababbaba with [8] bbbababbbbbba=ababbab:

Critical pair: bbbababbbbbababababbab=ababbababababbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [85].

Overlap of [50] bbababbbbbababbbbbbb=ab with [13] bbbababbbbbababbb=ababbaba:

Critical pair: bbababbbbbababbbbbbababbaba=abbbababbbbbababbb.

Reduce LHS:

Reduce RHS:

Referenced by [59], [62], [75].

Overlap of [15] babbbbbababbbbbbbabbbb=bbba with [8] bbbababbbbbba=ababbab:

Critical pair: babbbbbababbbbbbbabababbab=bbbaababbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [193].

Overlap of [15] babbbbbababbbbbbbabbbb=bbba with [8] bbbababbbbbba=ababbab:

Critical pair: babbbbbababbbbbbbabbbababbab=bbbabbababbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [63], [84].

Overlap of [15] babbbbbababbbbbbbabbbb=bbba with [21] babbbbabbab=abbabbbbbba:

Critical pair: babbbbbababbbbbbbabbbabbabbbbbba=bbbaabbbbabbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [71], [73], [95], [107], [119], [120].

Overlap of [15] babbbbbababbbbbbbabbbb=bbba with [27] bbbababbaba=abababab:

Critical pair: babbbbbababbbbbbbababababab=bbbaababbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [113].

Overlap of [1] aaa=1 with [60] abbbbbababbbbbbbabbbbb=bbab:

Critical pair: aabbab=bbbbbababbbbbbbabbbbb.

Flip LHS and RHS.

Referenced by [65], [66], [67], [68], [69], [70], [71], [72], [73], [74], [75], [76], [94], [95], [98], [107], [114], [120], [121], [145], [146], [149], [152], [168].

Overlap of [44] bbabbababba=aababbbbabb with [40] babbabbabbaba=aabbbbbababab:

Critical pair: bbabbaaabbbbbababab=aababbbbabbbbabbaba.

Reduce LHS:

Reduce RHS:

Referenced by [86].

Overlap of [8] bbbababbbbbba=ababbab with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: bbbababaabbab=ababbabbabbbbbbbabbbbb.

Reduce LHS:

Referenced by [132].

Overlap of [26] bbabbbbbababbbbbb=ababa with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: bbabbbbbababbaabbab=abababababbbbbbbabbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [74], [78], [85], [197], [238], [255], [272], [274], [276], [285].

Overlap of [26] bbabbbbbababbbbbb=ababa with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: bbabbbbbababbbaabbab=abababbababbbbbbbabbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [118], [122], [125], [253].

Overlap of [50] bbababbbbbababbbbbbb=ab with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: bbababbbbbababbaabbab=abababbbbbbbabbbbb.

Reduce LHS:

Referenced by [117], [272].

Overlap of [50] bbababbbbbababbbbbbb=ab with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: bbababbbbbababbbbaabbab=abbbababbbbbbbabbbbb.

Reduce LHS:

Referenced by [194].

Overlap of [50] bbababbbbbababbbbbbb=ab with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: bbababbbbbababbbbbaabbab=abbbbababbbbbbbabbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [76].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [13] bbbababbbbbababbb=ababbaba:

Critical pair: bbbbbababbbbbbbabbababbaba=aabbabababbbbbababbb.

Reduce LHS:

Reduce RHS:

Referenced by [87].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [21] babbbbabbab=abbabbbbbba:

Critical pair: bbbbbababbbbbbbabbbbabbabbbbbba=aabbababbbbabbab.

Reduce LHS:

Reduce RHS:

Referenced by [196].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [27] bbbababbaba=abababab:

Critical pair: bbbbbababbbbbbbabbabababab=aabbabababbaba.

Reduce LHS:

Referenced by [197].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [28] babababa=aabbbbbbababbbbbb:

Critical pair: bbbbbababbbbbbbabbbbaabbbbbbababbbbbb=aabbababababa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [117].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: bbbbbababbbbbbbabbaabbab=aabbabbbababbbbbbbabbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [79], [80], [82], [86], [87], [118], [119], [121], [122], [125], [154], [249], [256], [277].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: bbbbbababbbbbbbabbbaabbab=aabbabbbbababbbbbbbabbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [199].

Simplify [30] aabbbababbbbbbbabbbbbbbbbababbbbbbb=aababbababbaba.

Reduce RHS:

Referenced by [78].

Overlap of [77] aabbbababbbbbbbabbbbbbbbbababbbbbbb=bbababbbbbababbbb with [66] bbabbbbbbbbbabab=abbbababbbbbbbbb:

Critical pair: aabbbababbbbbabbbababbbbbbbbbbbbbbb=bbababbbbbababbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [83].

Overlap of [36] babbbbababab=abbabbaba with [75] bbbababab=babbbbbabbbbbbbabbbbb:

Critical pair: babbabbbbbabbbbbbbabbbbb=abbabbaba.

Referenced by [200].

Simplify [40] babbabbabbaba=aabbbbbababab.

Reduce RHS:

Referenced by [187].

Overlap of [43] aabbbbbbababbbbbbbabbab=aabbbababbbbabbbbbba with [56] aabbbbbbababbbbbbba=bbbbbbbababbbbbb:

Critical pair: bbbbbbbababbbbbbbbab=aabbbababbbbabbbbbba.

Flip LHS and RHS.

Referenced by [201].

Overlap of [45] abbabbbbbbabababba=babbbbbabbbbabb with [75] bbbababab=babbbbbabbbbbbbabbbbb:

Critical pair: abbabbbbabbbbbabbbbbbbabbbbbba=babbbbbabbbbabb.

Referenced by [202].

Overlap of [50] bbababbbbbababbbbbbb=ab with [78] bbababbbbbababbbb=aabbbbbabbbbbabbbbbbbbbbbbbbb:

Critical pair: aabbbbbabbbbbabbbbbbbbbbbbbbbbbb=ab.

Referenced by [203].

Overlap of [51] abbbbbababbbbbbbabbbbbabbbbbbbabb=aababbababba with [60] abbbbbababbbbbbbabbbbb=bbab:

Critical pair: bbababbbbbbbabb=aababbababba.

Flip LHS and RHS.

Referenced by [119], [126], [204].

Overlap of [57] bbbbbabbbbbbbbbababbbbbbbbab=ababbbbbbabba with [66] bbabbbbbbbbbabab=abbbababbbbbbbbb:

Critical pair: bbbabbbababbbbbbbbbbbbbbbbab=ababbbbbbabba.

Reduce LHS:

Referenced by [205].

Overlap of [64] bbabbbbbbbababab=abbbabbbbbababbb with [75] bbbababab=babbbbbabbbbbbbabbbbb:

Critical pair: bbabbbbbabbbbbabbbbbbbabbbbb=abbbabbbbbababbb.

Referenced by [108].

Simplify [71] bbbbbababbbbbabab=babbbbbbbabababbb.

Reduce RHS:

Referenced by [108].

Overlap of [1] aaa=1 with [55] aabbbbbbababbbbbbbbbb=bbbbba:

Critical pair: abbbbba=bbbbbbababbbbbbbbbb.

Flip LHS and RHS.

Referenced by [89], [90], [91], [92], [93], [94], [95], [96], [108], [115], [122], [146], [147], [148], [149], [153], [169], [170], [177], [178], [254], [258], [264], [265], [270], [275], [280], [286].

Overlap of [5] babababbbb=aabbbba with [88] bbbbbbababbbbbbbbbb=abbbbba:

Critical pair: bababaabbbbba=aabbbbabbababbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [287].

Overlap of [5] babababbbb=aabbbba with [88] bbbbbbababbbbbbbbbb=abbbbba:

Critical pair: bababababbbbba=aabbbbabbbababbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [206].

Overlap of [8] bbbababbbbbba=ababbab with [88] bbbbbbababbbbbbbbbb=abbbbba:

Critical pair: bbbabaabbbbba=ababbabbabbbbbbbbbb.

Reduce LHS:

Referenced by [228], [329], [338], [384], [385].

Overlap of [13] bbbababbbbbababbb=ababbaba with [88] bbbbbbababbbbbbbbbb=abbbbba:

Critical pair: bbbababbbbbabababbbbba=ababbababbbbababbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [181].

Overlap of [26] bbabbbbbababbbbbb=ababa with [88] bbbbbbababbbbbbbbbb=abbbbba:

Critical pair: bbabbbbbababbbabbbbba=abababbbababbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Defines rule #9.

Referenced by [104], [118], [127], [157], [162], [165], [189], [198], [199], [212], [223], [229], [236], [245], [249], [253], [254], [260], [262], [264], [268], [269], [270], [273], [280], [281], [301], [316], [317], [319], [320], [321], [322], [326], [329], [331], [332], [335], [339], [340], [341], [342], [343], [344], [347], [349], [369], [377], [378], [379], [380], [381], [385], [389], [390], [400], [410], [413], [416], [420], [425], [455], [464], [470], [472], [473], [479], [487], [489], [490], [491], [499], [502], [504], [513], [517], [518], [520], [525], [532], [537], [540], [546], [570].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [88] bbbbbbababbbbbbbbbb=abbbbba:

Critical pair: bbbbbababbbbbbbaabbbbba=aabbabbababbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [333], [334], [335], [336], [339], [340].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [88] bbbbbbababbbbbbbbbb=abbbbba:

Critical pair: bbbbbababbbbbbbabbabbbbba=aabbabbbbababbbbbbbbbb.

Reduce LHS:

Referenced by [207].

Overlap of [88] bbbbbbababbbbbbbbbb=abbbbba with [88] bbbbbbababbbbbbbbbb=abbbbba:

Critical pair: bbbbbbababbbbbbabbbbba=abbbbbabbababbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [174], [338].

Overlap of [31] babbabbabbbbbba=aabbbbbabbab with [26] bbabbbbbababbbbbb=ababa:

Critical pair: babbabbabbbbababa=aabbbbbabbabbbbbbababbbbbb.

Referenced by [208].

Overlap of [31] babbabbabbbbbba=aabbbbbabbab with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: babbabbabaabbab=aabbbbbabbabbabbbbbbbabbbbb.

Reduce LHS:

Referenced by [209].

Overlap of [44] bbabbababba=aababbbbabb with [31] babbabbabbbbbba=aabbbbbabbab:

Critical pair: bbabbaaabbbbbabbab=aababbbbabbbbabbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [258], [329], [361].

Overlap of [1] aaa=1 with [54] aabbbbbbababbbbbbbbba=bababb:

Critical pair: abababb=bbbbbbababbbbbbbbba.

Flip LHS and RHS.

Referenced by [101], [102], [103], [104], [105], [106], [107], [108], [109], [110], [111], [112], [113], [114], [115], [116], [154], [164], [165], [171], [178].

Overlap of [5] babababbbb=aabbbba with [100] bbbbbbababbbbbbbbba=abababb:

Critical pair: bababaabababb=aabbbbabbababbbbbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [196].

Overlap of [5] babababbbb=aabbbba with [100] bbbbbbababbbbbbbbba=abababb:

Critical pair: babababbabababb=aabbbbabbbbababbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [210].

Overlap of [8] bbbababbbbbba=ababbab with [100] bbbbbbababbbbbbbbba=abababb:

Critical pair: bbbabaabababb=ababbabbabbbbbbbbba.

Reduce LHS:

Referenced by [120], [129], [290].

Overlap of [26] bbabbbbbababbbbbb=ababa with [100] bbbbbbababbbbbbbbba=abababb:

Critical pair: bbabbbbbabababababb=abababababbbbbbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [118], [122], [125], [158], [186], [203].

Overlap of [26] bbabbbbbababbbbbb=ababa with [100] bbbbbbababbbbbbbbba=abababb:

Critical pair: bbabbbbbababbbabababb=abababbbababbbbbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [120].

Overlap of [26] bbabbbbbababbbbbb=ababa with [100] bbbbbbababbbbbbbbba=abababb:

Critical pair: bbabbbbbababbbbabababb=abababbbbababbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [188].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [100] bbbbbbababbbbbbbbba=abababb:

Critical pair: bbbbbababbbbbbbabbabababb=aabbabbbbababbbbbbbbba.

Reduce LHS:

Referenced by [212].

Overlap of [88] bbbbbbababbbbbbbbbb=abbbbba with [100] bbbbbbababbbbbbbbba=abababb:

Critical pair: bbbbbbababbbbbabababb=abbbbbabababbbbbbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [213].

Overlap of [100] bbbbbbababbbbbbbbba=abababb with [3] babbba=aab:

Critical pair: bbbbbbababbbbbbbbaab=abababbbbba.

Reduce LHS:

Referenced by [113].

Overlap of [100] bbbbbbababbbbbbbbba=abababb with [21] babbbbabbab=abbabbbbbba:

Critical pair: bbbbbbababbbbbbbbabbabbbbbba=abababbbbbbabbab.

Referenced by [214].

Overlap of [100] bbbbbbababbbbbbbbba=abababb with [26] bbabbbbbababbbbbb=ababa:

Critical pair: bbbbbbababbbbbbbababa=abababbbbbbbababbbbbb.

Referenced by [215].

Overlap of [100] bbbbbbababbbbbbbbba=abababb with [27] bbbababbaba=abababab:

Critical pair: bbbbbbababbbbbbabababab=abababbbabbaba.

Reduce LHS:

Reduce RHS:

Referenced by [117], [118], [119], [120], [121], [122], [123], [155], [172], [217].

Overlap of [100] bbbbbbababbbbbbbbba=abababb with [28] babababa=aabbbbbbababbbbbb:

Critical pair: bbbbbbababbbbbbbbaabbbbbbababbbbbb=abababbbababa.

Reduce LHS:

Reduce RHS:

Referenced by [198], [218].

Overlap of [100] bbbbbbababbbbbbbbba=abababb with [63] bbbbbababbbbbbbabbbbb=aabbab:

Critical pair: bbbbbbababbbbaabbab=abababbbabbbbbbbabbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [117], [125], [162], [168], [170], [188], [197], [207], [219].

Overlap of [100] bbbbbbababbbbbbbbba=abababb with [88] bbbbbbababbbbbbbbbb=abbbbba:

Critical pair: bbbbbbababbbabbbbba=abababbbabbbbbbbbbb.

Reduce LHS:

Reduce RHS:

Defines rule #3.

Referenced 253 times.

Overlap of [100] bbbbbbababbbbbbbbba=abababb with [100] bbbbbbababbbbbbbbba=abababb:

Critical pair: bbbbbbababbbabababb=abababbbabbbbbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [118], [127], [129], [134], [151], [156], [157], [158], [159], [160], [161], [162], [163], [164], [165], [166], [167], [168], [169], [170], [171], [172], [173], [174], [181], [187], [188], [210], [220].

Overlap of [5] babababbbb=aabbbba with [112] bbbababbabbababab=abbbbaba:

Critical pair: bababababbbbaba=aabbbbaababbabbababab.

Reduce LHS:

Reduce RHS:

Referenced by [128], [129], [132], [162], [196], [197], [260], [285], [320], [330], [342], [344], [347], [349], [379], [385], [386], [389], [400].

Overlap of [5] babababbbb=aabbbba with [112] bbbababbabbababab=abbbbaba:

Critical pair: babababbabbbbaba=aabbbbabababbabbababab.

Reduce RHS:

Referenced by [125], [221].

Overlap of [6] babbababbb=aaba with [112] bbbababbabbababab=abbbbaba:

Critical pair: babbababbabbbbaba=aababbababbabbababab.

Reduce LHS:

Reduce RHS:

Referenced by [126].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [112] bbbababbabbababab=abbbbaba:

Critical pair: bbbbbababbbbbbbabbabbbbaba=aabbabababbabbababab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [222].

Overlap of [63] bbbbbababbbbbbbabbbbb=aabbab with [112] bbbababbabbababab=abbbbaba:

Critical pair: bbbbbababbbbbbbabbbabbbbaba=aabbabbababbabbababab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [223].

Overlap of [88] bbbbbbababbbbbbbbbb=abbbbba with [112] bbbababbabbababab=abbbbaba:

Critical pair: bbbbbbababbbbbbbbabbbbaba=abbbbbabababbabbababab.

Reduce RHS:

Referenced by [224].

Overlap of [112] bbbababbabbababab=abbbbaba with [3] babbba=aab:

Critical pair: bbbababbabbabaaab=abbbbababba.

Reduce LHS:

Referenced by [124], [125], [126], [127], [128], [129], [130], [131], [132], [133], [134], [174], [179], [225].

Overlap of [3] babbba=aab with [123] bbbababbabbabb=abbbbababba:

Critical pair: baabbbbababba=aabbabbabbabb.

Reduce LHS:

Referenced by [226].

Overlap of [5] babababbbb=aabbbba with [123] bbbababbabbabb=abbbbababba:

Critical pair: babababbabbbbababba=aabbbbabababbabbabb.

Reduce LHS:

Reduce RHS:

Referenced by [250].

Overlap of [6] babbababbb=aaba with [123] bbbababbabbabb=abbbbababba:

Critical pair: babbababbabbbbababba=aababbababbabbabb.

Reduce LHS:

Reduce RHS:

Referenced by [227].

Overlap of [8] bbbababbbbbba=ababbab with [123] bbbababbabbabb=abbbbababba:

Critical pair: bbbababbbabbbbababba=ababbabbabbabbabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [337], [338], [339].

Overlap of [15] babbbbbababbbbbbbabbbb=bbba with [123] bbbababbabbabb=abbbbababba:

Critical pair: babbbbbababbbbbbbababbbbababba=bbbaababbabbabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [229].

Overlap of [26] bbabbbbbababbbbbb=ababa with [123] bbbababbabbabb=abbbbababba:

Critical pair: bbabbbbbababbbbabbbbababba=abababababbabbabb.

Reduce LHS:

Reduce RHS:

Referenced by [231].

Overlap of [123] bbbababbabbabb=abbbbababba with [3] babbba=aab:

Critical pair: bbbababbabbabaab=abbbbababbaabbba.

Reduce LHS:

Reduce RHS:

Referenced by [232].

Overlap of [123] bbbababbabbabb=abbbbababba with [21] babbbbabbab=abbabbbbbba:

Critical pair: bbbababbabbababbabbbbbba=abbbbababbaabbbbabbab.

Reduce LHS:

Reduce RHS:

Referenced by [325].

Overlap of [123] bbbababbabbabb=abbbbababba with [26] bbabbbbbababbbbbb=ababa:

Critical pair: bbbababbaababa=abbbbababbabbbababbbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [233].

Overlap of [123] bbbababbabbabb=abbbbababba with [31] babbabbabbbbbba=aabbbbbabbab:

Critical pair: bbbaaabbbbbabbab=abbbbababbabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [235].

Overlap of [123] bbbababbabbabb=abbbbababba with [31] babbabbabbbbbba=aabbbbbabbab:

Critical pair: bbbababbabaabbbbbabbab=abbbbababbaabbabbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [141], [142].

Overlap of [5] babababbbb=aabbbba with [115] bbbbbbbbbbbba=abbbbbbbbbbbb:

Critical pair: bababaabbbbbbbbbbbb=aabbbbabbbbbbbba.

Reduce LHS:

Referenced by [262], [319], [329], [341], [356], [396], [420].

Overlap of [5] babababbbb=aabbbba with [115] bbbbbbbbbbbba=abbbbbbbbbbbb:

Critical pair: bababababbbbbbbbbbbb=aabbbbabbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [172].

Overlap of [5] babababbbb=aabbbba with [115] bbbbbbbbbbbba=abbbbbbbbbbbb:

Critical pair: babababbabbbbbbbbbbbb=aabbbbabbbbbbbbbba.

Referenced by [174].

Overlap of [6] babbababbb=aaba with [115] bbbbbbbbbbbba=abbbbbbbbbbbb:

Critical pair: babbabaabbbbbbbbbbbb=aababbbbbbbbba.

Reduce LHS:

Referenced by [238], [249], [274].

Overlap of [13] bbbababbbbbababbb=ababbaba with [115] bbbbbbbbbbbba=abbbbbbbbbbbb:

Critical pair: bbbababbbbbabaabbbbbbbbbbbb=ababbababbbbbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [236].

Overlap of [13] bbbababbbbbababbb=ababbaba with [115] bbbbbbbbbbbba=abbbbbbbbbbbb:

Critical pair: bbbababbbbbabababbbbbbbbbbbb=ababbababbbbbbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [222], [224], [237].

Overlap of [13] bbbababbbbbababbb=ababbaba with [115] bbbbbbbbbbbba=abbbbbbbbbbbb:

Critical pair: bbbababbbbbababbabbbbbbbbbbbb=ababbababbbbbbbbbbba.

Reduce LHS:

Reduce RHS:

Referenced by [238].

Overlap of [26] bbabbbbbababbbbbb=ababa with [115] bbbbbbbbbbbba=abbbbbbbbbbbb:

Critical pair: bbabbbbbababbabbbbbbbbbbbb=abababbbbbbbba.

Reduce LHS:

Referenced by [291].

Overlap of [26] bbabbbbbababbbbbb=ababa with [115] bbbbbbbbbbbba=abbbbbbbbbbbb:

Critical pair: bbabbbbbababbbabbbbbbbbbbbb=abababbbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [357], [358], [359].

Overlap of [26] bbabbbbbababbbbbb=ababa with [115] bbbbbbbbbbbba=abbbbbbbbbbbb: