Certificate for #21749 ⟨a, b | aaa=1, abbbbba=b⟩

Back:⟨a, b | aaa=1, abbbbba=b⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #28.

Referenced by [7], [8], [15], [66], [73].

[2] abbbbba=b

Axiom: abbbbba=b.

Referenced by [5].

[3] bbb=c

Axiom: bbb=c.

Defines rule #5.

Referenced by [5], [6], [9], [11], [12], [13], [19], [21], [23], [26], [27], [29], [33], [42], [57], [59], [63], [64], [66], [70], [74], [75], [79], [80], [82], [84].

[4] acbacba=d

Axiom: acbacba=d.

Referenced by [15], [16], [17], [18], [19], [20], [21].

[5] acbba=b

Overlap of [2] abbbbba=b with [3] bbb=c:

a bbbbba bbb

Critical pair: acbba=b.

Referenced by [7], [8], [9], [11], [14], [17], [20], [21], [23], [36].

[6] bc=cb

Overlap of [3] bbb=c with [3] bbb=c:

b bb bbb

Critical pair: bc=cb.

Defines rule #1.

Referenced by [9], [10], [11], [19], [20], [21], [22], [28], [42], [43], [44], [46], [51], [53], [54], [56], [63], [64], [67], [68], [70], [76], [79].

[7] aab=cbba

Overlap of [1] aaa=1 with [5] acbba=b:

aa a acbba

Critical pair: aab=cbba.

Referenced by [11], [12], [37].

[8] baa=acbb

Overlap of [5] acbba=b with [1] aaa=1:

acbb a aaa

Critical pair: acbb=baa.

Flip LHS and RHS.

Defines rule #23.

Referenced by [13], [14], [18], [19], [32], [47], [49], [63], [64], [68].

[9] cca=acc

Overlap of [5] acbba=b with [5] acbba=b:

acbb a acbba

Critical pair: acbbb=bcbba.

Reduce LHS:

[3]ac(bbb)
⇒ acc

Reduce RHS:

[6](bc)bba
[3]⇒ c(bbb)a
⇒ cca

Flip LHS and RHS.

Defines rule #12.

Referenced by [10], [19], [20], [24], [44], [63], [66], [67], [78], [79].

[10] ccba=bacc

Overlap of [6] bc=cb with [9] cca=acc:

b c cca

Critical pair: bacc=cbca.

Reduce RHS:

[6]c(bc)a
⇒ ccba

Flip LHS and RHS.

Defines rule #16.

Referenced by [11], [19], [20], [21], [78], [79].

[11] acbacc=bab

Overlap of [5] acbba=b with [7] aab=cbba:

acbb a aab

Critical pair: acbbcbba=bab.

Reduce LHS:

[6]acb(bc)bba
[6]⇒ ac(bc)bbba
[3]⇒ acc(bbb)ba
[10]⇒ ac(ccba)
⇒ acbacc

Referenced by [19], [20], [21], [44].

[12] aac=cbbabb

Overlap of [7] aab=cbba with [3] bbb=c:

aa b bbb

Critical pair: aac=cbbabb.

Referenced by [38].

[13] caa=bbacbb

Overlap of [3] bbb=c with [8] baa=acbb:

bb b baa

Critical pair: bbacbb=caa.

Flip LHS and RHS.

Referenced by [39].

[14] acbacbb=ba

Overlap of [5] acbba=b with [8] baa=acbb:

acb ba baa

Critical pair: acbacbb=ba.

Referenced by [17].

[15] cbacba=aad

Overlap of [1] aaa=1 with [4] acbacba=d:

aa a acbacba

Critical pair: aad=cbacba.

Flip LHS and RHS.

Referenced by [69].

[16] dcba=acbd

Overlap of [4] acbacba=d with [4] acbacba=d:

acb acba acbacba

Critical pair: acbd=dcba.

Flip LHS and RHS.

Referenced by [40].

[17] dcbba=ba

Overlap of [4] acbacba=d with [5] acbba=b:

acbacb a acbba

Critical pair: acbacbb=dcbba.

Reduce LHS:

[14](acbacbb)
⇒ ba

Flip LHS and RHS.

Referenced by [23], [41].

[18] acbacacbb=da

Overlap of [4] acbacba=d with [8] baa=acbb:

acbac ba baa

Critical pair: acbacacbb=da.

Referenced by [70].

[19] acbab=bad

Overlap of [8] baa=acbb with [4] acbacba=d:

ba a acbacba

Critical pair: bad=acbbcbacba.

Reduce RHS:

[6]acb(bc)bacba
[6]⇒ ac(bc)bbacba
[3]⇒ acc(bbb)acba
[9]⇒ ac(cca)cba
[10]⇒ acac(ccba)
[11]⇒ ac(acbacc)
⇒ acbab

Flip LHS and RHS.

Referenced by [63], [64].

[20] ccd=bb

Overlap of [9] cca=acc with [4] acbacba=d:

cc a acbacba

Critical pair: ccd=acccbacba.

Reduce RHS:

[10]ac(ccba)cba
[11]⇒ (acbacc)cba
[6]⇒ ba(bc)ba
[5]⇒ b(acbba)
⇒ bb

Defines rule #4.

Referenced by [25], [29], [52], [54], [66], [69], [70], [74], [77], [78], [79], [82].

[21] ccbd=c

Overlap of [10] ccba=bacc with [4] acbacba=d:

ccb a acbacba

Critical pair: ccbd=bacccbacba.

Reduce RHS:

[10]bac(ccba)cba
[11]⇒ b(acbacc)cba
[6]⇒ bba(bc)ba
[5]⇒ bb(acbba)
[3]⇒ (bbb)
⇒ c

Defines rule #6.

Referenced by [22], [26], [35], [45], [52], [67], [77], [83].

[22] ccbbd=cb

Overlap of [6] bc=cb with [21] ccbd=c:

b c ccbd

Critical pair: bc=cbcbd.

Reduce LHS:

[6](bc)
⇒ cb

Reduce RHS:

[6]c(bc)bd
⇒ ccbbd

Flip LHS and RHS.

Referenced by [27], [54], [66], [67], [68], [70].

[23] dcc=bb

Overlap of [17] dcbba=ba with [5] acbba=b:

dcbb a acbba

Critical pair: dcbbb=bacbba.

Reduce LHS:

[3]dc(bbb)
⇒ dcc

Reduce RHS:

[5]b(acbba)
⇒ bb

Referenced by [24], [25], [26], [27], [29].

[24] bba=dacc

Overlap of [23] dcc=bb with [9] cca=acc:

d cc cca

Critical pair: dacc=bba.

Flip LHS and RHS.

Defines rule #13.

Referenced by [33], [34], [36], [37], [38], [39], [52], [54], [69], [70], [77], [78], [79].

[25] dbb=bbd

Overlap of [23] dcc=bb with [20] ccd=bb:

d cc ccd

Critical pair: dbb=bbd.

Referenced by [31], [34], [42], [46], [51].

[26] dc=cd

Overlap of [23] dcc=bb with [21] ccbd=c:

d cc ccbd

Critical pair: dc=bbbd.

Reduce RHS:

[3](bbb)d
⇒ cd

Defines rule #2.

Referenced by [27], [29], [30], [31], [40], [41], [43], [44], [51], [52], [53], [54], [56], [61], [66], [67], [70], [74], [75], [79].

[27] cdb=cbd

Overlap of [23] dcc=bb with [22] ccbbd=cb:

d cc ccbbd

Critical pair: dcb=bbbbd.

Reduce LHS:

[26](dc)b
⇒ cdb

Reduce RHS:

[3](bbb)bd
⇒ cbd

Referenced by [28], [29], [30], [40], [41], [51], [52], [61], [67].

[28] cbdb=cbbd

Overlap of [6] bc=cb with [27] cdb=cbd:

b c cdb

Critical pair: bcbd=cbdb.

Reduce LHS:

[6](bc)bd
⇒ cbbd

Flip LHS and RHS.

Referenced by [41], [51].

[29] bbdb=cd

Overlap of [23] dcc=bb with [27] cdb=cbd:

dc c cdb

Critical pair: dccbd=bbdb.

Reduce LHS:

[26](dc)cbd
[26]⇒ c(dc)bd
[20]⇒ (ccd)bd
[3]⇒ (bbb)d
⇒ cd

Flip LHS and RHS.

Referenced by [31], [32], [53], [54].

[30] cddb=cbdd

Overlap of [26] dc=cd with [27] cdb=cbd:

d c cdb

Critical pair: dcbd=cddb.

Reduce LHS:

[26](dc)bd
[27]⇒ (cdb)d
⇒ cbdd

Flip LHS and RHS.

Referenced by [47], [48].

[31] bbddb=cdd

Overlap of [25] dbb=bbd with [29] bbdb=cd:

d bb bbdb

Critical pair: dcd=bbddb.

Reduce LHS:

[26](dc)d
⇒ cdd

Flip LHS and RHS.

Referenced by [49], [50].

[32] cdaa=bbdacbb

Overlap of [29] bbdb=cd with [8] baa=acbb:

bbd b baa

Critical pair: bbdacbb=cdaa.

Flip LHS and RHS.

Referenced by [42].

[33] bdacc=ca

Overlap of [3] bbb=c with [24] bba=dacc:

b bb bba

Critical pair: bdacc=ca.

Referenced by [35], [43].

[34] bbda=ddacc

Overlap of [25] dbb=bbd with [24] bba=dacc:

d bb bba

Critical pair: ddacc=bbda.

Flip LHS and RHS.

Referenced by [41], [46], [53], [55].

[35] bdac=cabd

Overlap of [33] bdacc=ca with [21] ccbd=c:

bda cc ccbd

Critical pair: bdac=cabd.

Referenced by [42], [43], [46], [51], [52], [53], [54], [62].

[36] acdacc=b

Overlap of [5] acbba=b with [24] bba=dacc:

ac bba bba

Critical pair: acdacc=b.

Referenced by [44], [45], [54], [56].

[37] aab=cdacc

Simplify [7] aab=cbba.

Reduce RHS:

[24]c(bba)
⇒ cdacc

Defines rule #18.

Referenced by [66].

[38] aac=cdaccbb

Simplify [12] aac=cbbabb.

Reduce RHS:

[24]c(bba)bb
⇒ cdaccbb

Defines rule #17.

[39] caa=dacccbb

Simplify [13] caa=bbacbb.

Reduce RHS:

[24](bba)cbb
⇒ dacccbb

Defines rule #22.

[40] cbda=acbd

Overlap of [16] dcba=acbd with [26] dc=cd:

dcba dc

Critical pair: cdba=acbd.

Reduce LHS:

[27](cdb)a
⇒ cbda

Referenced by [51].

[41] cddacc=ba

Overlap of [17] dcbba=ba with [26] dc=cd:

dcbba dc

Critical pair: cdbba=ba.

Reduce LHS:

[27](cdb)ba
[28]⇒ (cbdb)a
[34]⇒ c(bbda)
⇒ cddacc

Referenced by [53].

[42] cdaa=cbacd

Simplify [32] cdaa=bbdacbb.

Reduce RHS:

[35]b(bdac)bb
[6]⇒ (bc)abdbb
[25]⇒ cbab(dbb)
[3]⇒ cba(bbb)d
⇒ cbacd

Referenced by [44], [66].

[43] cacbd=ca

Overlap of [33] bdacc=ca with [35] bdac=cabd:

bdacc bdac

Critical pair: cabdc=ca.

Reduce LHS:

[26]cab(dc)
[6]⇒ ca(bc)d
⇒ cacbd

Defines rule #9.

Referenced by [75], [84].

[44] bacbd=ba

Overlap of [36] acdacc=b with [9] cca=acc:

acda cc cca

Critical pair: acdaacc=ba.

Reduce LHS:

[42]a(cdaa)cc
[26]⇒ acbac(dc)c
[11]⇒ (acbacc)dc
[26]⇒ bab(dc)
[6]⇒ ba(bc)d
⇒ bacbd

Defines rule #10.

Referenced by [46], [48], [50], [62], [81], [82].

[45] acdac=bbd

Overlap of [36] acdacc=b with [21] ccbd=c:

acda cc ccbd

Critical pair: acdac=bbd.

Referenced by [54], [56].

[46] ddacc=cbabdbd

Overlap of [25] dbb=bbd with [44] bacbd=ba:

db b bacbd

Critical pair: dbba=bbdacbd.

Reduce LHS:

[25](dbb)a
[34]⇒ (bbda)
⇒ ddacc

Reduce RHS:

[35]b(bdac)bd
[6]⇒ (bc)abdbd
⇒ cbabdbd

Referenced by [54], [55].

[47] cbddaa=cddacbb

Overlap of [30] cddb=cbdd with [8] baa=acbb:

cdd b baa

Critical pair: cddacbb=cbddaa.

Flip LHS and RHS.

Referenced by [57].

[48] cbddacbd=cbdda

Overlap of [30] cddb=cbdd with [44] bacbd=ba:

cdd b bacbd

Critical pair: cddba=cbddacbd.

Reduce LHS:

[30](cddb)a
⇒ cbdda

Flip LHS and RHS.

Referenced by [58].

[49] cddaa=bbddacbb

Overlap of [31] bbddb=cdd with [8] baa=acbb:

bbdd b baa

Critical pair: bbddacbb=cddaa.

Flip LHS and RHS.

Referenced by [59].

[50] cddacbd=cdda

Overlap of [31] bbddb=cdd with [44] bacbd=ba:

bbdd b bacbd

Critical pair: bbddba=cddacbd.

Reduce LHS:

[31](bbddb)a
⇒ cdda

Flip LHS and RHS.

Referenced by [60].

[51] bbddac=acbbdd

Overlap of [25] dbb=bbd with [35] bdac=cabd:

db b bdac

Critical pair: dbcabd=bbddac.

Reduce LHS:

[6]d(bc)abd
[26]⇒ (dc)babd
[27]⇒ (cdb)abd
[40]⇒ (cbda)bd
[28]⇒ a(cbdb)d
⇒ acbbdd

Flip LHS and RHS.

Referenced by [59].

[52] cbddac=dac

Overlap of [27] cdb=cbd with [35] bdac=cabd:

cd b bdac

Critical pair: cdcabd=cbddac.

Reduce LHS:

[26]c(dc)abd
[20]⇒ (ccd)abd
[24]⇒ (bba)bd
[21]⇒ da(ccbd)
⇒ dac

Flip LHS and RHS.

Referenced by [58].

[53] cddac=babd

Overlap of [29] bbdb=cd with [35] bdac=cabd:

bbd b bdac

Critical pair: bbdcabd=cddac.

Reduce LHS:

[26]bb(dc)abd
[6]⇒ b(bc)dabd
[6]⇒ (bc)bdabd
[34]⇒ c(bbda)bd
[41]⇒ (cddacc)bd
⇒ babd

Flip LHS and RHS.

Referenced by [57], [60].

[54] bdb=bbd

Overlap of [35] bdac=cabd with [36] acdacc=b:

bd ac acdacc

Critical pair: bdb=cabddacc.

Reduce RHS:

[46]cab(ddacc)
[6]⇒ ca(bc)babdbd
[24]⇒ cac(bba)bdbd
[45]⇒ c(acdac)cbdbd
[26]⇒ cbb(dc)bdbd
[6]⇒ cb(bc)dbdbd
[6]⇒ c(bc)bdbdbd
[22]⇒ (ccbbd)bdbd
[29]⇒ c(bbdb)d
[20]⇒ (ccd)d
⇒ bbd

Referenced by [55], [57], [59], [60], [61], [62], [70].

[55] bbda=cbabbdd

Simplify [34] bbda=ddacc.

Reduce RHS:

[46](ddacc)
[54]⇒ cba(bdb)d
⇒ cbabbdd

Referenced by [70].

[56] cbbd=b

Overlap of [36] acdacc=b with [45] acdac=bbd:

acdacc acdac

Critical pair: bbdc=b.

Reduce LHS:

[26]bb(dc)
[6]⇒ b(bc)d
[6]⇒ (bc)bd
⇒ cbbd

Defines rule #7.

Referenced by [59], [61], [69], [70], [77], [78], [79].

[57] cbddaa=bacd

Simplify [47] cbddaa=cddacbb.

Reduce RHS:

[53](cddac)bb
[54]⇒ ba(bdb)b
[54]⇒ bab(bdb)
[3]⇒ ba(bbb)d
⇒ bacd

Referenced by [71].

[58] cbdda=dacbd

Overlap of [48] cbddacbd=cbdda with [52] cbddac=dac:

cbddacbd cbddac

Critical pair: dacbd=cbdda.

Flip LHS and RHS.

Referenced by [71].

[59] cddaa=acd

Simplify [49] cddaa=bbddacbb.

Reduce RHS:

[51](bbddac)bb
[56]⇒ a(cbbd)dbb
[54]⇒ a(bdb)b
[54]⇒ ab(bdb)
[3]⇒ a(bbb)d
⇒ acd

Referenced by [65].

[60] cdda=babbdd

Overlap of [50] cddacbd=cdda with [53] cddac=babd:

cddacbd cddac

Critical pair: babdbd=cdda.

Reduce LHS:

[54]ba(bdb)d
⇒ babbdd

Flip LHS and RHS.

Referenced by [65], [75].

[61] db=bd

Overlap of [26] dc=cd with [56] cbbd=b:

d c cbbd

Critical pair: db=cdbbd.

Reduce RHS:

[27](cdb)bd
[54]⇒ c(bdb)d
[56]⇒ (cbbd)d
⇒ bd

Defines rule #3.

Referenced by [62], [73], [75], [79], [81], [83], [84].

[62] bda=cabbdd

Overlap of [61] db=bd with [44] bacbd=ba:

d b bacbd

Critical pair: dba=bdacbd.

Reduce LHS:

[61](db)a
⇒ bda

Reduce RHS:

[35](bdac)bd
[54]⇒ ca(bdb)d
⇒ cabbdd

Defines rule #14.

Referenced by [67], [75], [79].

[63] babad=acaccb

Overlap of [8] baa=acbb with [19] acbab=bad:

ba a acbab

Critical pair: babad=acbbcbab.

Reduce RHS:

[6]acb(bc)bab
[6]⇒ ac(bc)bbab
[3]⇒ acc(bbb)ab
[9]⇒ ac(cca)b
⇒ acaccb

Referenced by [77].

[64] badaa=acacccb

Overlap of [19] acbab=bad with [8] baa=acbb:

acba b baa

Critical pair: acbaacbb=badaa.

Reduce LHS:

[8]ac(baa)cbb
[6]⇒ acacb(bc)bb
[6]⇒ acac(bc)bbb
[3]⇒ acacc(bbb)b
⇒ acacccb

Flip LHS and RHS.

Referenced by [72].

[65] babbdda=acd

Simplify [59] cddaa=acd.

Reduce LHS:

[60](cdda)a
⇒ babbdda

Referenced by [66].

[66] cbacda=cd

Overlap of [37] aab=cdacc with [65] babbdda=acd:

aa b babbdda

Critical pair: aaacd=cdaccabbdda.

Reduce LHS:

[1](aaa)cd
⇒ cd

Reduce RHS:

[9]cda(cca)bbdda
[22]⇒ cdaa(ccbbd)da
[42]⇒ (cdaa)cbda
[26]⇒ cbac(dc)bda
[20]⇒ cba(ccd)bda
[3]⇒ cba(bbb)da
⇒ cbacda

Flip LHS and RHS.

Referenced by [67].

[67] acda=cdd

Overlap of [26] dc=cd with [66] cbacda=cd:

d c cbacda

Critical pair: dcd=cdbacda.

Reduce LHS:

[26](dc)d
⇒ cdd

Reduce RHS:

[27](cdb)acda
[62]⇒ c(bda)cda
[9]⇒ (cca)bbddcda
[22]⇒ a(ccbbd)dcda
[26]⇒ acb(dc)da
[6]⇒ ac(bc)dda
[21]⇒ a(ccbd)da
⇒ acda

Flip LHS and RHS.

Defines rule #21.

Referenced by [68], [73].

[68] acba=bacdd

Overlap of [8] baa=acbb with [67] acda=cdd:

ba a acda

Critical pair: bacdd=acbbcda.

Reduce RHS:

[6]acb(bc)da
[6]⇒ ac(bc)bda
[22]⇒ a(ccbbd)a
⇒ acba

Flip LHS and RHS.

Defines rule #20.

Referenced by [69], [70], [74], [77].

[69] aad=cdab

Overlap of [15] cbacba=aad with [68] acba=bacdd:

cb acba acba

Critical pair: cbbacdd=aad.

Reduce LHS:

[24]c(bba)cdd
[20]⇒ cdac(ccd)d
[56]⇒ cda(cbbd)
⇒ cdab

Flip LHS and RHS.

Defines rule #19.

Referenced by [73].

[70] dacbd=da

Overlap of [18] acbacacbb=da with [68] acba=bacdd:

acbacacbb acba

Critical pair: bacddcacbb=da.

Reduce LHS:

[26]bacd(dc)acbb
[26]⇒ bac(dc)dacbb
[20]⇒ ba(ccd)dacbb
[55]⇒ ba(bbda)cbb
[26]⇒ bacbabbd(dc)bb
[26]⇒ bacbabb(dc)dbb
[6]⇒ bacbab(bc)ddbb
[6]⇒ bacba(bc)bddbb
[56]⇒ bacba(cbbd)dbb
[54]⇒ bacba(bdb)b
[54]⇒ bacbab(bdb)
[3]⇒ bacba(bbb)d
[68]⇒ b(acba)cd
[26]⇒ bbacd(dc)d
[26]⇒ bbac(dc)dd
[20]⇒ bba(ccd)dd
[24]⇒ (bba)bbdd
[22]⇒ da(ccbbd)d
⇒ dacbd

Defines rule #11.

Referenced by [71].

[71] daa=bacd

Overlap of [57] cbddaa=bacd with [58] cbdda=dacbd:

cbddaa cbdda

Critical pair: dacbda=bacd.

Reduce LHS:

[70](dacbd)a
⇒ daa

Defines rule #25.

Referenced by [72], [74].

[72] babacd=acacccb

Overlap of [64] badaa=acacccb with [71] daa=bacd:

ba daa daa

Critical pair: babacd=acacccb.

Referenced by [81].

[73] cbdd=d

Overlap of [1] aaa=1 with [69] aad=cdab:

a aa aad

Critical pair: acdab=d.

Reduce LHS:

[67](acda)b
[61]⇒ cd(db)
[61]⇒ c(db)d
⇒ cbdd

Defines rule #8.

Referenced by [76].

[74] dabacdd=baca

Overlap of [71] daa=bacd with [68] acba=bacdd:

da a acba

Critical pair: dabacdd=bacdcba.

Reduce RHS:

[26]bac(dc)ba
[20]⇒ ba(ccd)ba
[3]⇒ ba(bbb)a
⇒ baca

Referenced by [78], [79].

[75] cddda=caddd

Overlap of [26] dc=cd with [60] cdda=babbdd:

d c cdda

Critical pair: dbabbdd=cddda.

Reduce LHS:

[61](db)abbdd
[62]⇒ (bda)bbdd
[61]⇒ cabbd(db)bdd
[61]⇒ cabb(db)dbdd
[3]⇒ ca(bbb)ddbdd
[61]⇒ cacd(db)dd
[61]⇒ cac(db)ddd
[43]⇒ (cacbd)ddd
⇒ caddd

Flip LHS and RHS.

Referenced by [76].

[76] dda=cbaddd

Overlap of [6] bc=cb with [75] cddda=caddd:

b c cddda

Critical pair: bcaddd=cbddda.

Reduce LHS:

[6](bc)addd
⇒ cbaddd

Reduce RHS:

[73](cbdd)da
⇒ dda

Flip LHS and RHS.

Defines rule #15.

Referenced by [77], [79].

[77] acaca=badabddd

Overlap of [63] babad=acaccb with [76] dda=cbaddd:

baba d dda

Critical pair: babacbaddd=acaccbda.

Reduce LHS:

[68]bab(acba)ddd
[24]⇒ ba(bba)cddddd
[20]⇒ badac(ccd)dddd
[56]⇒ bada(cbbd)ddd
⇒ badabddd

Reduce RHS:

[21]aca(ccbd)a
⇒ acaca

Flip LHS and RHS.

Defines rule #29.

[78] dabab=bacacc

Overlap of [20] ccd=bb with [74] dabacdd=baca:

cc d dabacdd

Critical pair: ccbaca=bbabacdd.

Reduce LHS:

[10](ccba)ca
[9]⇒ bac(cca)
⇒ bacacc

Reduce RHS:

[24](bba)bacdd
[10]⇒ da(ccba)cdd
[20]⇒ dabac(ccd)d
[56]⇒ daba(cbbd)
⇒ dabab

Flip LHS and RHS.

Referenced by [80].

[79] dacacc=cababddd

Overlap of [62] bda=cabbdd with [74] dabacdd=baca:

b da dabacdd

Critical pair: bbaca=cabbddbacdd.

Reduce LHS:

[24](bba)ca
[9]⇒ dac(cca)
⇒ dacacc

Reduce RHS:

[61]cabbd(db)acdd
[61]⇒ cabb(db)dacdd
[3]⇒ ca(bbb)ddacdd
[76]⇒ cac(dda)cdd
[10]⇒ ca(ccba)dddcdd
[20]⇒ caba(ccd)ddcdd
[26]⇒ cababbd(dc)dd
[26]⇒ cababb(dc)ddd
[6]⇒ cabab(bc)dddd
[6]⇒ caba(bc)bdddd
[56]⇒ caba(cbbd)ddd
⇒ cababddd

Referenced by [83].

[80] dabac=bacaccbb

Overlap of [78] dabab=bacacc with [3] bbb=c:

daba b bbb

Critical pair: dabac=bacaccbb.

Referenced by [82].

[81] baba=acacccbb

Overlap of [72] babacd=acacccb with [61] db=bd:

babac d db

Critical pair: babacbd=acacccbb.

Reduce LHS:

[44]ba(bacbd)
⇒ baba

Defines rule #24.

[82] daba=bacacbb

Overlap of [80] dabac=bacaccbb with [44] bacbd=ba:

da bac bacbd

Critical pair: daba=bacaccbbbd.

Reduce RHS:

[3]bacacc(bbb)d
[20]⇒ bacac(ccd)
⇒ bacacbb

Defines rule #27.

[83] dacac=cababbdddd

Overlap of [79] dacacc=cababddd with [21] ccbd=c:

daca cc ccbd

Critical pair: dacac=cababdddbd.

Reduce RHS:

[61]cababdd(db)d
[61]⇒ cababd(db)dd
[61]⇒ cabab(db)ddd
⇒ cababbdddd

Referenced by [84].

[84] daca=cabacddddd

Overlap of [83] dacac=cababbdddd with [43] cacbd=ca:

da cac cacbd

Critical pair: daca=cababbddddbd.

Reduce RHS:

[61]cababbddd(db)d
[61]⇒ cababbdd(db)dd
[61]⇒ cababbd(db)ddd
[61]⇒ cababb(db)dddd
[3]⇒ caba(bbb)ddddd
⇒ cabacddddd

Defines rule #26.