Certificate for #22283 ⟨a, b | aaa=1, abbbab=ba⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #14.

Referenced by [3], [5], [10], [24], [30], [32], [34], [35], [37], [40], [41], [43], [44], [67], [70], [73], [75], [84], [114], [117].

Axiom: abbbab=ba.

Referenced by [3], [4], [6], [8], [15], [17], [18], [19], [26], [30], [36], [37], [47], [48], [49].

Overlap of [1] aaa=1 with [2] abbbab=ba:

Critical pair: aaba=bbbab.

Defines rule #15.

Referenced by [5], [6], [7], [11], [15], [16], [22], [27], [32], [33], [34], [38], [41], [42], [53], [61], [69], [82], [83].

Overlap of [2] abbbab=ba with [2] abbbab=ba:

Critical pair: abbbba=babbab.

Flip LHS and RHS.

Referenced by [8], [9], [16], [20], [21], [27], [30], [31], [32], [35], [50].

Overlap of [3] aaba=bbbab with [1] aaa=1:

Critical pair: aab=bbbabaa.

Flip LHS and RHS.

Referenced by [12], [25], [33].

Overlap of [3] aaba=bbbab with [2] abbbab=ba:

Critical pair: aabba=bbbabbbbab.

Defines rule #16.

Referenced by [13], [14], [15], [24], [32], [39], [68], [74], [97], [117].

Overlap of [3] aaba=bbbab with [3] aaba=bbbab:

Critical pair: aabbbbab=bbbababa.

Flip LHS and RHS.

Referenced by [29], [30], [31], [40], [55].

Overlap of [2] abbbab=ba with [4] babbab=abbbba:

Critical pair: abbabbbba=babab.

Defines rule #23.

Referenced by [9], [10], [11], [12], [13], [14], [31], [81].

Overlap of [4] babbab=abbbba with [8] abbabbbba=babab:

Critical pair: bbabab=abbbbabbba.

Flip LHS and RHS.

Referenced by [17], [18].

Overlap of [8] abbabbbba=babab with [1] aaa=1:

Critical pair: abbabbbb=bababaa.

Flip LHS and RHS.

Referenced by [15], [16].

Overlap of [8] abbabbbba=babab with [3] aaba=bbbab:

Critical pair: abbabbbbbbbab=babababa.

Flip LHS and RHS.

Referenced by [66].

Overlap of [8] abbabbbba=babab with [5] bbbabaa=aab:

Critical pair: abbabaab=bababbaa.

Flip LHS and RHS.

Referenced by [34].

Overlap of [6] aabba=bbbabbbbab with [8] abbabbbba=babab:

Critical pair: ababab=bbbabbbbabbbbba.

Flip LHS and RHS.

Defines rule #37.

Referenced by [66], [81], [82], [83], [112].

Overlap of [8] abbabbbba=babab with [6] aabba=bbbabbbbab:

Critical pair: abbabbbbbbbabbbbab=babababba.

Flip LHS and RHS.

Referenced by [56].

Overlap of [2] abbbab=ba with [10] bababaa=abbabbbb:

Critical pair: abbbaabbabbbb=baababaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [40].

Overlap of [4] babbab=abbbba with [10] bababaa=abbabbbb:

Critical pair: bababbabbbb=abbbbaabaa.

Reduce LHS:

Reduce RHS:

Referenced by [56].

Overlap of [2] abbbab=ba with [9] abbbbabbba=bbabab:

Critical pair: abbbbbabab=babbbabbba.

Reduce RHS:

Referenced by [26], [27], [28].

Overlap of [9] abbbbabbba=bbabab with [2] abbbab=ba:

Critical pair: abbbbba=bbababb.

Flip LHS and RHS.

Referenced by [19], [20], [21], [23], [30], [34], [40], [44], [51], [53].

Overlap of [2] abbbab=ba with [18] bbababb=abbbbba:

Critical pair: ababbbbba=baabb.

Defines rule #21.

Referenced by [22], [23], [24], [25], [28], [29], [30], [35], [81], [82], [90].

Overlap of [4] babbab=abbbba with [18] bbababb=abbbbba:

Critical pair: baabbbbba=abbbbaabb.

Referenced by [36], [57].

Overlap of [18] bbababb=abbbbba with [4] babbab=abbbba:

Critical pair: bbaabbbba=abbbbbaab.

Referenced by [36], [42].

Overlap of [3] aaba=bbbab with [19] ababbbbba=baabb:

Critical pair: abaabb=bbbabbbbbba.

Referenced by [31], [34].

Overlap of [18] bbababb=abbbbba with [19] ababbbbba=baabb:

Critical pair: bbbaabb=abbbbbabbba.

Flip LHS and RHS.

Referenced by [32].

Overlap of [19] ababbbbba=baabb with [1] aaa=1:

Critical pair: ababbbbb=baabbaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [19] ababbbbba=baabb with [5] bbbabaa=aab:

Critical pair: ababbaab=baabbbaa.

Flip LHS and RHS.

Referenced by [32], [33], [34], [35], [36], [42], [44].

Overlap of [2] abbbab=ba with [17] abbbbbabab=bbabba:

Critical pair: abbbbbabba=babbbbabab.

Flip LHS and RHS.

Referenced by [35].

Overlap of [4] babbab=abbbba with [17] abbbbbabab=bbabba:

Critical pair: babbbbabba=abbbbabbbbabab.

Reduce RHS:

Referenced by [39].

Overlap of [19] ababbbbba=baabb with [17] abbbbbabab=bbabba:

Critical pair: ababbbbbbbabba=baabbbbbbbabab.

Flip LHS and RHS.

Referenced by [56].

Overlap of [7] bbbababa=aabbbbab with [19] ababbbbba=baabb:

Critical pair: bbbabbaabb=aabbbbabbbbbba.

Flip LHS and RHS.

Referenced by [58].

Overlap of [7] bbbababa=aabbbbab with [19] ababbbbba=baabb:

Critical pair: bbbababbaabb=aabbbbabbabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [8] abbabbbba=babab with [7] bbbababa=aabbbbab:

Critical pair: abbabaabbbbab=bababbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [59].

Overlap of [4] babbab=abbbba with [25] baabbbaa=ababbaab:

Critical pair: babbaababbaab=abbbbaaabbbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [38].

Overlap of [5] bbbabaa=aab with [25] baabbbaa=ababbaab:

Critical pair: bbbaababbaab=aabbbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36], [59], [60].

Overlap of [18] bbababb=abbbbba with [25] baabbbaa=ababbaab:

Critical pair: bbababababbaab=abbbbbaaabbbaa.

Reduce LHS:

Reduce RHS:

Referenced by [62].

Overlap of [19] ababbbbba=baabb with [25] baabbbaa=ababbaab:

Critical pair: ababbbbababbaab=baabbabbbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #32.

Referenced by [97], [98], [99].

Overlap of [25] baabbbaa=ababbaab with [2] abbbab=ba:

Critical pair: baabbbaba=ababbaabbbbab.

Reduce LHS:

Reduce RHS:

Referenced by [37], [38], [39], [40], [41], [42], [64].

Overlap of [2] abbbab=ba with [36] babaa=bbbbbbbaab:

Critical pair: abbbbbbbbbaab=baaa.

Reduce RHS:

Referenced by [43], [44], [45], [46].

Overlap of [3] aaba=bbbab with [36] babaa=bbbbbbbaab:

Critical pair: aabbbbbbbaab=bbbabbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [58].

Overlap of [6] aabba=bbbabbbbab with [36] babaa=bbbbbbbaab:

Critical pair: aabbbbbbbbaab=bbbabbbbabbaa.

Reduce RHS:

Referenced by [65].

Overlap of [7] bbbababa=aabbbbab with [36] babaa=bbbbbbbaab:

Critical pair: bbbababbbbbbbaab=aabbbbabbaa.

Reduce LHS:

Reduce RHS:

Referenced by [66].

Overlap of [36] babaa=bbbbbbbaab with [1] aaa=1:

Critical pair: bab=bbbbbbbaaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [46], [52].

Overlap of [36] babaa=bbbbbbbaab with [25] baabbbaa=ababbaab:

Critical pair: baababbaab=bbbbbbbaabbbbaa.

Reduce LHS:

Reduce RHS:

Referenced by [59], [60].

Overlap of [1] aaa=1 with [37] abbbbbbbbbaab=b:

Critical pair: aab=bbbbbbbbbaab.

Flip LHS and RHS.

Referenced by [45].

Overlap of [37] abbbbbbbbbaab=b with [25] baabbbaa=ababbaab:

Critical pair: abbbbbbbbababbaab=bbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [57], [61], [62], [64], [65], [66], [73], [74], [76], [78], [83], [93], [96], [97], [103], [104], [116], [117].

Overlap of [37] abbbbbbbbbaab=b with [37] abbbbbbbbbaab=b:

Critical pair: abbbbbbbbbab=bbbbbbbbbaab.

Reduce RHS:

Referenced by [70].

Overlap of [41] bbbbbbbbbbab=bab with [37] abbbbbbbbbaab=b:

Critical pair: bbbbbbbbbbb=babbbbbbbbbaab.

Reduce RHS:

Referenced by [47].

Overlap of [2] abbbab=ba with [46] bbbbbbbbbbb=bb:

Critical pair: abbbabb=babbbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [48].

Overlap of [2] abbbab=ba with [47] babbbbbbbbbb=bab:

Critical pair: abbbab=babbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [49], [50], [51], [52], [53], [54], [56], [66], [68], [72], [76], [77], [78], [80], [82], [83], [84], [85], [86], [87], [88], [89], [91], [93], [95], [96], [97], [98], [99], [100], [101], [102], [103], [104], [105], [106], [108], [110], [111], [112], [113], [115], [116], [117], [118].

Overlap of [2] abbbab=ba with [48] babbbbbbbbb=ba:

Critical pair: abbba=babbbbbbbb.

Defines rule #4.

Referenced by [68], [69], [76], [77], [80], [82], [84], [85], [86], [91], [96], [98], [103], [112], [113].

Overlap of [4] babbab=abbbba with [48] babbbbbbbbb=ba:

Critical pair: babba=abbbbabbbbbbbb.

Defines rule #6.

Referenced by [56], [66], [82], [83], [87], [89], [94], [99], [100], [101], [104], [108], [116], [118].

Overlap of [18] bbababb=abbbbba with [48] babbbbbbbbb=ba:

Critical pair: bbaba=abbbbbabbbbbbb.

Defines rule #7.

Referenced by [55], [69], [78], [81], [87], [89], [101], [102], [104], [105], [106], [107], [108], [112], [113], [115].

Overlap of [41] bbbbbbbbbbab=bab with [48] babbbbbbbbb=ba:

Critical pair: bbbbbbbbbba=babbbbbbbbb.

Reduce RHS:

Referenced by [67].

Overlap of [48] babbbbbbbbb=ba with [18] bbababb=abbbbba:

Critical pair: babbbbbbbabbbbba=baababb.

Reduce RHS:

Referenced by [63].

Overlap of [48] babbbbbbbbb=ba with [48] babbbbbbbbb=ba:

Critical pair: babbbbbbbbba=baabbbbbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [108], [111].

Overlap of [7] bbbababa=aabbbbab with [51] bbaba=abbbbbabbbbbbb:

Critical pair: babbbbbabbbbbbbba=aabbbbab.

Referenced by [109].

Overlap of [14] babababba=abbabbbbbbbabbbbab with [50] babba=abbbbabbbbbbbb:

Critical pair: babaabbbbabbbbbbbb=abbabbbbbbbabbbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [78].

Simplify [20] baabbbbba=abbbbaabb.

Reduce RHS:

Defines rule #31.

Simplify [29] aabbbbabbbbbba=bbbabbaabb.

Reduce RHS:

Referenced by [81].

Overlap of [31] baabbbbaa=abbbbbabbbbbabbbba with [33] aabbbbaa=bbbbbbabbbaab:

Critical pair: bbbbbbbabbbaab=abbbbbabbbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [79].

Simplify [33] aabbbbaa=bbbbbbabbbaab.

Reduce RHS:

Referenced by [61].

Overlap of [60] aabbbbaa=bbbbbbbabbbbbbbbab with [44] bbbaa=abbbbbbabbbbbb:

Critical pair: aababbbbbbabbbbbb=bbbbbbbabbbbbbbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [79].

Simplify [34] bbbbbabbbbbbbabbbbba=abbbbbbbbaa.

Reduce RHS:

Referenced by [63].

Overlap of [62] bbbbbabbbbbbbabbbbba=abbbbbabbbbbbabbbbbb with [53] babbbbbbbabbbbba=bbbbabbb:

Critical pair: bbbbbbbbabbb=abbbbbabbbbbbabbbbbb.

Flip LHS and RHS.

Referenced by [65].

Simplify [36] babaa=bbbbbbbaab.

Reduce RHS:

Referenced by [71].

Overlap of [39] aabbbbbbbbaab=bbbbbabbbbbbba with [44] bbbaa=abbbbbbabbbbbb:

Critical pair: aabbbbbabbbbbbabbbbbbb=bbbbbabbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [80].

Overlap of [40] babbbbbabbbbbaab=bbbbbbabbbbabbbbb with [44] bbbaa=abbbbbbabbbbbb:

Critical pair: babbbbbabbabbbbbbabbbbbbb=bbbbbbabbbbabbbbb.

Reduce LHS:

Defines rule #25.

Referenced by [78].

Overlap of [52] bbbbbbbbbba=ba with [1] aaa=1:

Critical pair: bbbbbbbbbb=baaa.

Reduce RHS:

Defines rule #1.

Referenced by [71], [100], [102], [115].

Overlap of [6] aabba=bbbabbbbab with [49] abbba=babbbbbbbb:

Critical pair: aabbbabbbbbbbb=bbbabbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [87], [89], [101], [102], [103], [104], [105].

Overlap of [49] abbba=babbbbbbbb with [3] aaba=bbbab:

Critical pair: abbbbbbab=babbbbbbbbaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [81].

Overlap of [1] aaa=1 with [45] abbbbbbbbbab=aab:

Critical pair: aaaab=bbbbbbbbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [71], [72].

Overlap of [70] bbbbbbbbbab=ab with [64] babaa=bbbbabbbbbbabbbbbbb:

Critical pair: bbbbbbbbbbbbabbbbbbabbbbbbb=abaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [86], [95].

Overlap of [70] bbbbbbbbbab=ab with [48] babbbbbbbbb=ba:

Critical pair: bbbbbbbbba=abbbbbbbbb.

Defines rule #3.

Referenced by [100], [102], [115].

Overlap of [44] bbbaa=abbbbbbabbbbbb with [1] aaa=1:

Critical pair: bbb=abbbbbbabbbbbba.

Flip LHS and RHS.

Referenced by [75], [76], [77].

Overlap of [44] bbbaa=abbbbbbabbbbbb with [6] aabba=bbbabbbbab:

Critical pair: bbbbbbabbbbab=abbbbbbabbbbbbbba.

Flip LHS and RHS.

Referenced by [86].

Overlap of [1] aaa=1 with [73] abbbbbbabbbbbba=bbb:

Critical pair: aabbb=bbbbbbabbbbbba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [80], [103].

Overlap of [44] bbbaa=abbbbbbabbbbbb with [73] abbbbbbabbbbbba=bbb:

Critical pair: bbbabbb=abbbbbbabbbbbbbbbbbbabbbbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [84], [85], [86], [89].

Overlap of [49] abbba=babbbbbbbb with [73] abbbbbbabbbbbba=bbb:

Critical pair: abbbbbb=babbbbbbbbbbbbbbabbbbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [90], [91], [92].

Overlap of [56] abbabbbbbbbabbbbab=ababbbbbbabbbbabbb with [66] abbabbbbbbba=bbbbbbabbbbabbbbb:

Critical pair: bbbbbbabbbbabbbbbbbbbab=ababbbbbbabbbbabbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [99].

Simplify [59] abbbbbabbbbbabbbba=bbbbbbbbabbbbbbbbab.

Reduce RHS:

Defines rule #50.

Overlap of [75] bbbbbbabbbbbba=aabbb with [49] abbba=babbbbbbbb:

Critical pair: bbbbbbabbbbbbbabbbbbbbb=aabbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [95].

Overlap of [8] abbabbbba=babab with [13] bbbabbbbabbbbba=ababab:

Critical pair: abbabababab=bababbbbbabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #36.

Referenced by [82].

Overlap of [13] bbbabbbbabbbbba=ababab with [13] bbbabbbbabbbbba=ababab:

Critical pair: bbbabbbbabbababab=abababbbbbabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [94].

Overlap of [13] bbbabbbbabbbbba=ababab with [44] bbbaa=abbbbbbabbbbbb:

Critical pair: bbbabbbbabbabbbbbbabbbbbb=abababa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #45.

Overlap of [1] aaa=1 with [76] abbbbbbbabbbbba=bbbabbb:

Critical pair: aabbbabbb=bbbbbbbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [87], [92], [104].

Overlap of [49] abbba=babbbbbbbb with [76] abbbbbbbabbbbba=bbbabbb:

Critical pair: abbbbbbabbb=babbbbbbbbbbbbbbbabbbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [86].

Overlap of [71] abaa=bbbabbbbbbabbbbbbb with [76] abbbbbbbabbbbba=bbbabbb:

Critical pair: ababbbabbb=bbbabbbbbbabbbbbbbbbbbbbbabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [88].

Overlap of [84] bbbbbbbabbbbba=ababb with [50] babba=abbbbabbbbbbbb:

Critical pair: bbbbbbbabbbbabbbbabbbbbbbb=ababbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [89], [109].

Overlap of [86] bbbbbbbbabbbbab=abbabb with [48] babbbbbbbbb=ba:

Critical pair: bbbbbbbbabbbba=abbabbbbbbbbbb.

Reduce RHS:

Defines rule #13.

Referenced by [105].

Overlap of [87] ababbbba=bbabbbbbabbbb with [76] abbbbbbbabbbbba=bbbabbb:

Critical pair: ababbbbbbbabbb=bbabbbbbabbbbbbbbbbbabbbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [107].

Overlap of [19] ababbbbba=baabb with [77] babbbbbabbbbbba=abbbbbb:

Critical pair: aabbbbbb=baabbbbbbbba.

Flip LHS and RHS.

Referenced by [93], [94].

Overlap of [49] abbba=babbbbbbbb with [77] babbbbbabbbbbba=abbbbbb:

Critical pair: abbabbbbbb=babbbbbbbbbbbbbabbbbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [97], [100], [101].

Overlap of [84] bbbbbbbabbbbba=ababb with [77] babbbbbabbbbbba=abbbbbb:

Critical pair: bbbbbbabbbbbb=ababbbbbbbba.

Flip LHS and RHS.

Defines rule #22.

Referenced by [98], [106], [107].

Overlap of [44] bbbaa=abbbbbbabbbbbb with [90] baabbbbbbbba=aabbbbbb:

Critical pair: bbaabbbbbb=abbbbbbabbbbbbbbbbbbbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [96], [108].

Overlap of [90] baabbbbbbbba=aabbbbbb with [50] babba=abbbbabbbbbbbb:

Critical pair: baabbbbbbbabbbbabbbbbbbb=aabbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [108].

Overlap of [71] abaa=bbbabbbbbbabbbbbbb with [80] aabbbbbba=babbbbbbbbabbb:

Critical pair: abbabbbbbbbbabbb=bbbabbbbbbabbbbbbbbbbbbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #38.

Referenced by [108].

Overlap of [49] abbba=babbbbbbbb with [93] abbbbbbabbbbba=bbaabbbbbb:

Critical pair: abbbbbaabbbbbb=babbbbbbbbbbbbbbabbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #34.

Referenced by [112], [113].

Overlap of [35] bababbbbbbba=aabbbbabbbbb with [44] bbbaa=abbbbbbabbbbbb:

Critical pair: bababbbbabbbbbbabbbbbb=aabbbbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #40.

Overlap of [35] bababbbbbbba=aabbbbabbbbb with [49] abbba=babbbbbbbb:

Critical pair: bababbbbbbbbabbbbbbbb=aabbbbabbbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [114].

Overlap of [35] bababbbbbbba=aabbbbabbbbb with [50] babba=abbbbabbbbbbbb:

Critical pair: bababbbbbbabbbbabbbbbbbb=aabbbbabbbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #41.

Overlap of [72] bbbbbbbbba=abbbbbbbbb with [91] babbbbabbbbbba=abbabbbbbb:

Critical pair: bbbbbbbbabbabbbbbb=abbbbbbbbbbbbbabbbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #27.

Referenced by [115].

Overlap of [91] babbbbabbbbbba=abbabbbbbb with [91] babbbbabbbbbba=abbabbbbbb:

Critical pair: babbbbabbbbbabbabbbbbb=abbabbbbbbbbbbabbbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #42.

Overlap of [72] bbbbbbbbba=abbbbbbbbb with [68] bbbabbbbabbbba=ababbbbbbb:

Critical pair: bbbbbbababbbbbbb=abbbbbbbbbbbbbabbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #26.

Referenced by [109], [115], [116].

Overlap of [75] bbbbbbabbbbbba=aabbb with [68] bbbabbbbabbbba=ababbbbbbb:

Critical pair: bbbbbbabbbababbbbbbb=aabbbbbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #44.

Overlap of [84] bbbbbbbabbbbba=ababb with [68] bbbabbbbabbbba=ababbbbbbb:

Critical pair: bbbbbbbabbababbbbbbb=ababbbbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #47.

Overlap of [88] bbbbbbbbabbbba=abbab with [68] bbbabbbbabbbba=ababbbbbbb:

Critical pair: bbbbbababbbbbbb=abbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [51] bbaba=abbbbbabbbbbbb with [92] ababbbbbbbba=bbbbbbabbbbbb:

Critical pair: bbbbbbbbabbbbbb=abbbbbabbbbbbbbbbbbbbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #28.

Referenced by [115].

Overlap of [51] bbaba=abbbbbabbbbbbb with [92] ababbbbbbbba=bbbbbbabbbbbb:

Critical pair: bbabbbbbbbabbbbbb=abbbbbabbbbbbbbabbbbbbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [117].

Overlap of [94] aabbbbbbbba=bbbbbabbbbbbabbb with [51] bbaba=abbbbbabbbbbbb:

Critical pair: aabbbbbbabbbbbabbbbbbb=bbbbbabbbbbbabbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [111].

Overlap of [87] ababbbba=bbabbbbbabbbb with [102] abbbbabbbba=bbbbabbbbbabbbbb:

Critical pair: abbbbbabbbbbabbbbb=bbabbbbbabbbbbbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [110].

Overlap of [109] baabbbbab=abbbbbabbbbbabbbbb with [48] babbbbbbbbb=ba:

Critical pair: baabbbba=abbbbbabbbbbabbbbbbbbbbbbb.

Reduce RHS:

Defines rule #30.

Overlap of [108] babbbbabbbbbbbabbb=abbaabbbb with [48] babbbbbbbbb=ba:

Critical pair: babbbbabbbbbbba=abbaabbbbbbbbbb.

Reduce RHS:

Defines rule #33.

Overlap of [13] bbbabbbbabbbbba=ababab with [96] babbbbbabbbbba=abbabbbbbbabbb:

Critical pair: bbbabbbabbabbbbbbabbb=abababbbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #46.

Overlap of [96] babbbbbabbbbba=abbabbbbbbabbb with [51] bbaba=abbbbbabbbbbbb:

Critical pair: babbbbbabbbabbbbbabbbbbbb=abbabbbbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #48.

Referenced by [118].

Overlap of [1] aaa=1 with [98] aabbbbabbbbbbbba=bbbbbbbabbbbb:

Critical pair: abbbbbbbabbbbb=bbbbabbbbbbbba.

Flip LHS and RHS.

Defines rule #9.

Referenced by [117].

Overlap of [106] abbbbbabbbbbba=bbbbbbbbabbbbbb with [100] abbbbabbbbbba=bbbbbbbabbbbabbbbb:

Critical pair: abbbbbabbbbbbbbbbbbbabbbbabbbbb=bbbbbbbbabbbbbbbbbbabbbbbba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #39.

Referenced by [116].

Overlap of [115] bbbbbbabbbbbabbbba=aabbbbbab with [102] abbbbabbbba=bbbbabbbbbabbbbb:

Critical pair: bbbbbbabbbbbbbbbabbbbbabbbbb=aabbbbbabbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #43.

Overlap of [1] aaa=1 with [107] ababbbbbbbabbbba=bbabbbbbbbabbbbbb:

Critical pair: aabbabbbbbbbabbbbbb=babbbbbbbabbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #35.

Overlap of [50] babba=abbbbabbbbbbbb with [113] abbabbbbbbabbbba=babbbbbbabbbbabbbbbbb:

Critical pair: bbabbbbbbabbbbabbbbbbb=abbbbabbbbbbbbbbbbbbabbbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #49.