I finally found the first proofs of A2 and L1 based on only w2
<https://xamidi.github.io/pmGenerator/svg/walsh2nd.svg> and modus ponens,
and thereby the first constructive completeness proof for w2!
Using all hints encoded in the current version of w2.txt
<https://github.com/xamidi/pmGenerator/blob/f06cb6eff0f4248fd6c7d8492301eb4716d725f4/data/w2.txt>,
Prover9 (version 2017-11A (CIIRC) <https://github.com/ai4reason/Prover9>)
was able to complete the proofs after only 1 day 7 hours and 44 minutes on
my old i7-3610QM laptop.
I used this input file <https://pastebin.com/JfZKgLXb> (hints generated via
./prover9HintsFromProofs on a comma-separated sequence of concrete D-proofs
from w2.txt) which produced this output file <https://pastebin.com/Ct3gwVEU>
.
The generated proofs of L1 and A2 are — as converted via 1.
./prover9OutputConverter, 2. ./findCompactSummary, 3. ./pmGenerator
--transform — [109] and [110] of:
CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] CCCpCCqCprCCNrCCNstqCsruCvu = DDD11D11[0]
[2] Cpp = DDD1D11[1][0]
[3] CpCCNqCCNrsCCtCCuCtvCCNvCCNwxuCwvqCrq = DDD1[1]1D[1]DD1[0]D11
[4] CpCqCrr = DDD1[3]DDD1[3]1[3]D[1]DD1[1]1
[5] CCNpCCNCqCCrCqsCCNsCCNturCtsvNwCwCxp = DDD11DDD1D111[3][3]
[6] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = DDDD1D111[3][5]
[7] CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq = D[6]DDD11DDD1111[4]
[8] CpCqCrCsCtq = DDDDD1DDD11DD1D111[3]1[3]1DDD11DDD1111[4]
[9] CpCqCrp = DDD11DD11DDD1D111[3][8]
[10] CCNCpqCCNrsqCrCpq = DD1DDD11DD1D111[3][9]
[11] CCNCpCqrCCNstrCsCpCqr = DD1DDD11DD1D111[3]D[8][8]
[12] CCNCNpqCCNrspCrCNpq = DD1D[8][8]DDD1[9]D11D[1]DD1[0]D11
[13] CpCqp = DDDDD11DD1D111[3][8]1
[14] CNCpCqNrCsCtCur =
DDD1DDDD11D1DD1DDD1[0]D1111[3]DDD11D1[0][3]DDD1D1D[8][8]1[3][3]
[15] CNCpCqrCsNr = DD[12][14]D[12][14]
[16] CCNpCCNqrCNppCqp = DDDD1[2]1[15]DDD1[2]1[15]
[17] CpCCNqqq = D[13]D[16][7]
[18] CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq = DD1[17]DDD1D[16][7]1[17]
[19] CCNCCpqqCCNrspCrCCpqq = DD1[3]DDD1D[16][7]1[17]
[20] CpCCNCpqCpqq = D[18][17]
[21] CCNCNpqpCNpq = D[12][20]
[22] CpCCNqNpq = DDD1[20][2]1
[23] CCNCpqCCNrsCNqNpCrCpq = DD1[22]DDD1[22]1[22]
[24] CCNpNqCqp = D[23][22]
[25] CNNpCqp = DD[12][15]DD[6]1D[4][4]
[26] CpCqNNCNpr = D[23]D[13]D[24]D[24]DDD1[20][2]D[13]D[5][25]
[27] CpNNp = D[24]DD[16][7]D[5][26]
[28] CCCpqCCrrsCqs = DDD1[0]D1[2]D[13]D[22][2]
[29] CpCqCNCrps = D[28]D[6]DDDD11D1[0][3]DD1[2]1
[30] CpCqNNCrCsp =
DD[6]D[9]D[24]D[24]DD[6]D[9]D[5][25]DD[6]1D[24]DDDD1[0]D11D[9]D[5][25]DDD1[0]D11D[9]D[5][25]D[27]DD[12]D[21][14]D[21]D[21]D[21][14]
[31] CpCCNCNqqCNqqq = D[18]D[21]D[5][30]
[32] CCCNpqNrCrCps = DDDD1[0]D11[7]DDD1[2]1[7]
[33] CCNpCCNqrNsCsCqp = DDDDD1DDD11DD1D111[3]1[3][2]DDDDD11111[8]
[34] CCNCpCqrrCpCqr = D[11][20]
[35] CpCCNqNNqq = D[13]DDD1[22][25][20]
[36] CpCCNNNqNNqq = D[13]DDD1[22][25][31]
[37] CpCCqCCrrsCqs = DDD1[17]D1[17]D[9]D1[2]
[38] CpCCpqq = D[19][35]
[39] CCNCCpqqpCCpqq = D[19][20]
[40] CCNpCqpCqp = DDD1D1D[8][8][13]D[18][15]
[41] CpCCNqqCCqrr = D[25]D[27]D[19][31]
[42] CNCpqCrCqs = DDD1DDDD11D1DD1DDD1[0]D1111[3]DDD11D1[0][3]D1[3][41]
[43] CpCCNNCqprr =
DDDD1[3]DDD1[22]1[22]D[13]DD[37][37]DDD1[9]DDD1[22]1[22][35]D[40]D[12][41]
[44] CCpCqNpCqNp = D[40]D[19]DD[10]D[18][15][43]
[45] CCpCNNpqCNNpq = D[40]D[19]D[13]D[40]D[19]D[13][27]
[46] CCCpqCrpCrp = D[39]DDDDD1D1D[8][8]1[3][5]D[13]D[32]D[44]D[19][31]
[47] CCNpCqCrpCqCrp = D[39]DD[37][37]D[21][14]
[48] CCCpqCNprCNpr = D[39]DDDD11DDD1D111[3][7]D[28]D[5]D[5][30]
[49] CCpCqCrNpCqCrNp = D[39]D[24]D[28][30]
[50] CpCCNNCqrqq = D[13]D[46]D[19]D[13]DDD1[2][2]D[18][36]
[51] CCpCqCprCqCpr =
D[39]D[46]DD[6]D[9]DDD1[9]D11D[1]DD1[0]D11D[24]D[24]DDD1[20][2]D[13][26]
[52] CCpCNCpqrCNCpqr = D[39]D[46]D[12]D[6][4]
[53] CCCpqCrCqsCrCqs =
D[39]D[34]D[46]D[28]D[28]DDD1[3]DDD1[3]1[3]D[13]D[6][8]
[54] CCCCpqqCprCpr = D[51]D[19][41]
[55] CCCpqCrCspCrCsp = D[39]D[51]D[28]D[28]D[28]DDD1[3]DDD1[3]1[3][8]
[56] CCpCCNppqCCNppq = D[39]D[16]D[13]D[46][43]
[57] CCNNpCqCprCqCpr = D[39]D[44]D[48]D[28]D[28]DDD1[3]DDD1[3]1[3][8]
[58] CCNpCCpqqCCpqq = D[39]D[44]D[54][29]
[59] CCNpCNCqprCNCqpr = DD[38]D[19]D[13]D[44][43][51]
[60] CCpqCpCrq = D[11]D[18][50]
[61] CCpqCrCpCsq = D[60][60]
[62] CpCqCCprCsr = D[60]D[54][61]
[63] CpCCCqprCsr =
DD[39]D[34]D[46]D[28]D[23]D[13]DDD1[0]D11D[1]DD1[0]D11[62]
[64] CCNNpqCpq = D[51]DD[39]D[44]D[48][29][62]
[65] CCCNpqrCpNNr = DD[51][63]DD1[22]D[5][25]
[66] CCCNpqrCpCCrss = DD[51][63][19]
[67] CCCNpqrCpCNrs = DD[51][63][12]
[68] CCpqCNNpq = D[51]D[45][62]
[69] CCNCpNpCpqCpq = D[58]D[60]D[51]D[24]D[52]D[45]D[11]D[18]D[21][15]
[70] CCpqCNCprq = D[51]D[52][62]
[71] CCCCpqqrCpr = D[51]D[54][62]
[72] CCpqCCNppq = D[51]D[56][62]
[73] CpCCqNpCqr = D[33]D[18][50]
[74] CpCCpNqCqr = D[47]D[70]D[33]D[70][72]
[75] CCpNqCpCqr = D[47]D[70][73]
[76] CCpNqCqCpr = D[47]D[70][74]
[77] CNCCNpqpq = D[21]D[60]D[24]D[65]D[56]D[60]D[51]D[52][61]
[78] CCNNCCNpqpqq = D[58]D[60]D[68][77]
[79] CCNCpNNqqCpNNq = D[34]D[65][78]
[80] CCCCNpqpCrqCrq = D[58]D[60]D[60][77]
[81] CCCCpqNpCrqCrq = D[58]D[60]D[60]D[21]D[49]D[67]D[56]D[60]D[51]D[52][61]
[82] CCpNqCNCpCqrs = D[75]D[79]D[70][75]
[83] CNCCNpqCrpq = D[80]D[67]D[56][61]
[84] CNCCCpqrpr = D[81]D[75]D[79]D[70]D[55][73]
[85] CNCCpqCprq = D[81][82]
[86] CNCpCCpqrq = D[81]D[75]D[79]D[70][76]
[87] CNCpNCpqNNq = D[79]D[70]D[81]D[75]D[79]D[70]D[49][74]
[88] CNCCpqCprNNq = D[79]D[70][85]
[89] CCpqCpNNq = D[34][88]
[90] CCpqCpCNqr = D[34]D[75][88]
[91] CpCCpqCNqr = D[71][90]
[92] CCNpqCNqp = D[47][91]
[93] CCpqCpCCqrr = D[34]D[66]D[58]D[60]D[68][85]
[94] CCNpqCCqpp = D[47]D[71][93]
[95] CCpCCqpNpNNNp =
DD[49]D[68][74]DD[58]D[60]D[68]D[51]D[24]D[52]D[60]DD[19]D[21]D[21][14]D[40]D[19]D[13]D[11][31]D[24][87]
[96] CCpCCNqpqCCNqpq = DD[47]DD[53]D[54][62][93]DD[38]D[32]D[20]D[4][4][80]
[97] CCNNCNpNNNNNCCNNqqprCNrs =
DD[64][91]DD[38]D[45]D[60]D[38]DD[16][7]D[5][26]D[49]D[68][91]
[98] CCCpqrCNNNrp = D[55]D[47]DD[51]D[70]D[48][62]D[72]D[24]D[89][86]
[99] CCpNNqCNNNNpq =
D[47]DDD[47]D[52]D[60][22]D[81]D[12][41]D[60]D[47]DD[51]D[70]D[48][62]D[72]D[24][88]
[100] CpCCpqCNCrqs = D[71]D[47]DD[56]D[60][70]DD[60][92]D[60][85]
[101] CNNCpNqCCCqNprr = DD[99]D[89][93]D[95]DD[67]D[56]D[60][68]D[49][74]
[102] CCCCpNNqqCprCpr =
D[57]DD[51]D[45]D[54]D[60][62]D[66]D[58]D[60]D[68]D[47][73]
[103] CCCNpqrCpNCrNr =
D[33]D[68]DD[96]D[60]D[38]D[32]D[40]D[18][36]DDD[66]DDDD1[17]D1[9][35]D[10][20]D[13]D[92]DD[34]D[60]D[24]D[65]D[72][74][87][93]
[104] CCCCpqCrqsCps = D[51]DD[57]DD[38]D[45][62][93][62]
[105] CpCCpqCCNNqrr = DD[57]DD[51]D[45]D[54]D[60][62]D[66]D[72][89]D[60][93]
[106] CNNCNpqCCqNCrrp =
D[68]D[51]DD[51]DD[96]D[60]DDD1[22]DD[6]1[2]D[18][50]DD[51]D[92]D[60][83]D[92][83]DD[99]D[89][93]D[95]DD[6]1[83]
[107] CCNCCpCCpqCrqsss =
DD[106]DD[89]D[49][91]D[34]D[81]D[90][93]D[97]DD[10][41]D[54][61]
[108] CCNCpqrCCrqCpq =
D[47]DDDDD[106]DD[65]D[56][61][84]DDDD[99]D[89][93]DDD[49]D[68]D[47]DD[56]D[60][70]DD[60]D[51]DD[51]D[69]D[60]D[24]D[65][78]D[24]D[65]D[56]D[60][62]D[24]D[89][86]D[76]D[89]D[58]D[60][84]DD[60]D[38]D[21]DD[37][37][42]D[33]D[18][36]DD[49][91]DD[47]D[52]D[60][22]DDDD1[17]D1[2]D[13]DD[37][37]D[47][22]D[13][83]DD[51]D[45][61]D[54][61]D[106]DD[65]D[56]D[60][68]D[104][96]DD[68]D[34]DD[68]D[47]DDDDDD[47]D[52]D[60][22]D[103]D[94]D[65]D[56][62]D[71][93]DD[49]DD[56]D[60][70]DD[60]D[51][63][91]DD[106]DD[89]D[49][91][90]D[97]DD[60][51]DD[53]DD[51]D[19]D[19]D[5]D[5]D[5]D[28]D[24]D[24]D[24]D[24]DD[6][7]D[5]D[34]D[24]D[24]D[24]DDD1D1D[8][8][13]D[13]D[24]DDD1[22][25][36][62]D[98]D[94]D[92]D[80]D[90]D[34]D[60]D[24]D[65]D[72][73]D[13]DDDD[106]DD[89]D[49][91][94]D[97]DD[60][44]D[67]D[60]D[58]D[34]DDD1[2][24]D[13]D[40]D[19]D[13][27]D[70][100]DD[47]D[70][91]DDDD[55][105]DDD[55]D[64]D[102]D[60][93]DD[68]D[22]D[23]DDD1D[16][7]1[17]DD[89]D[47]D[64][91]D[98]D[94]D[92]D[81]D[90]D[49]D[68][91]DD[55][100]D[94]D[49]D[71]D[47]D[70][90]D[68]D[60]D[45][61]D[92]DDD[47]D[59]D[60]D[71][93]D[24]D[89][86]D[90][90]D[51]D[92]DD[99]D[89][93]D[95]DD[6]1[83]DD[89]D[53]D[102]D[60]D[34]D[60]D[60][85]DDDDD[64][105]DDD[47]DD[56]D[60][70]DD[60][92]D[80][82]DD[51]D[92]DD[49]DD[58]D[60]D[68]D[24]D[70]D[69]D[49]D[67]D[58]D[60]D[45]D[60]D[39]D[21][42]DD[34]D[60]D[24]D[65]D[72][74][88]D[60]D[81]D[67]D[56][61]D[76]D[44]D[66]D[72]D[23]D[13]D[56]D[60]D[51]D[45][61]DD[49]DDD1[17]D1[2][41]DD[6]1D[51]D[64]D[34]D[60]D[24]D[65]D[72]D[71][76]D[13]D[107]DD[34]D[60]D[80][82]D[98]D[66]D[58]D[60]D[68]D[58]D[60][77]D[68]D[107]DD[51]DD[68]D[51]DD[51]D[92]DD[34]DD[34]DDD[51][63][16][78]D[70][85][83]D[59]D[59]DD[51]DD[51]D[48][62]DD[39]D[44]D[48][29][62]D[60]D[68]D[51]D[52][61]DD[89]D[47]D[24]D[80]D[90][93]D[92]D[98]D[94]D[92]D[80]D[90]D[34]D[60]D[60][85]DD[106]DD[79]D[70]D[49][74]D[79]D[70][70]D[97]D[61]D[19]D[13]D[58]D[60]D[45]D[60]DD[19][42]D[27]D[21]DD[37][37][42]D[101]D[27]D[65]D[72][74]DD[79]D[52]D[60]D[51][63]DD[99]D[89]D[49]D[92]D[60][85]DDD[101]D[27]D[44]D[67]D[58]D[68]D[60]D[40]D[19][41]D[49]D[92]D[81]D[90][90]DDDD[92]D[60][84]DD[38]D[44]D[12]D[18]D[1]DD1[3]DDD1[3]1[3]DD[19]D[13]DDD1[2][2]D[18][36]D[44]D[12]D[13]D[32]D[44]D[19][31]DD[47]D[64]D[71][93]DD[51]DD[68]D[51]D[68]D[45][62]D[27][63]D[72]D[49]D[92]D[60][86]DD[34]D[23][50]D[103]D[58]D[60]D[68][86][62]
[109] CCpqCCqrCpr = D[51]DDD[108][85][61]DD[108]D[52][61]D[108][85]
[110] CCpCqrCCpqCpr = DD[109]D[51]DDD[108][85][61]D[104]D[108][85]D[108][85]
More details in appended file 'w2-A2,L1.txt'. But those proofs of A2 and L1
have 661949665229 (661.9… billion) and 330556198971 (330.5… billion) steps,
respectively, which via searching exhaustive proof files and some of my
extractions, I could reduce to 1515183111 (1.5… billion) and 756629451
(756.6… million) steps, respectively.
I am now running proof compression on those results, which seems will take
a while (the proof summary contains 1034 different proofs).
But I am going to add today's results to the 1-base proof minimization
challenge <https://github.com/xamidi/pmGenerator/discussions/2> also today
(and compression results possibly later).
It surprised me that now Prover9 found the remaining target theorems in
just a little more than a day, since before Steven's contribution
<https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-10014766>
it would run for months without further results.
So finding that manual proof for A3 clearly was a major milestone in
progressing from w2.
Needless to say, the results (also when compressed) still have massive
potential for proof minimization.
[email protected] schrieb am Mittwoch, 10. Juli 2024 um 19:44:42
UTC+2:
> By the way, proof compression further improves it to 1877 steps:
>
> $ ./pmGenerator --transform data/w2.txt -f -n -t
> CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq -p -2 -d -z -o data/w2-z.txt
> Wed Jul 10 18:28:49 2024: Process started. [pid: 26064, tid:1]
> Tasks:
> 1. recombineProofSummary("data/w2.txt", true, null, 2,
> 18446744073709551614, true, false, "CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq",
> true, 18446744073709551615, 134217728, true, "data/w2-z.txt", true)
>
> [Main] Calling recombineProofSummary("data/w2.txt", true, null, 2,
> 18446744073709551614, true, false, "CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq",
> true, 18446744073709551615, 134217728, true, "data/w2-z.txt", true).
> 0.14 ms taken to obtain 67 helper proof candidates, i.e. the minimal set
> of referenced proofs such that each proof contains only a single rule with
> inputs.
> 19.61 ms taken to morph and parse 84 abstract proofs.
> 0.04 ms taken to validate 17 conclusions.
> 0.03 ms taken to find 5 occurrences of 5 theorems.
> [Proof compression (rule search), round 1] Started. There are 27816 proof
> steps in total.
> [Proof compression (rule search), round 1] D-step [16] improved from
> D[79][15] (1+2829+471 = 3301 steps) to D[79][74] (1+2829+115 = 2945 steps).
> [CCNpNqCqp]
> [Proof compression (rule search), round 1] D-step [77] improved from
> D[75][15] (1+1883+471 = 2355 steps) to D[75][74] (1+1883+115 = 1999 steps).
> [CCNpNqCCNpCCNrsqCrp]
> [Proof compression (rule search), round 1] D-step [57] improved from
> D[51][15] (1+1367+471 = 1839 steps) to D[51][74] (1+1367+115 = 1483 steps).
> [CpCCNCpqCpqq]
> [Proof compression (rule search), round 1] D-step [48] improved from
> D[37][15] (1+421+471 = 893 steps) to D[37][74] (1+421+115 = 537 steps).
> [CpCCNqCCNrsCNCpqCpqCrq]
> [Proof compression (rule search), round 1] Complete. Applied 4 shortening
> replacements.
> [Proof compression (rule search), round 2] Started. There are 19272 proof
> steps in total.
> [Proof compression (rule search), round 2] Complete. Applied 0 shortening
> replacements.
>
> There are 35 steps towards Cpp / C0.0 (index 8).
> There are 53 steps towards CpCqp / C0C1.0 (index 11).
> There are 57 steps towards CpCNpq / C0CN0.1 (index 13).
> There are 417 steps towards CCNppp / CCN0.0.0 (index 14).
> There are 1877 steps towards CCNpNqCqp / CCN0N1C1.0 (index 16).
> 0.01 ms taken to count 2439 relevant proof steps in total.
> 0.02 ms taken to obtain 84 referenced indices.
> 0.03 ms taken to obtain 18 dedicated indices.
> 0.05 ms taken to build transformed proof.
> 0.63 ms taken to print and save 1129 bytes to data/w2-z.txt.
> Wed Jul 10 18:29:05 2024: Process terminated. [pid: 26064, tid:1]
>
> $ ./pmGenerator --transform data/w2-z.txt -f -n -t
> CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq -j -1 -s
> CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq
>
> -d -p -2
> Wed Jul 10 18:29:08 2024: Process started. [pid: 23984, tid:1]
> Tasks:
> 1. recombineProofSummary("data/w2-z.txt", true,
> "CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq",
>
> 4294967295, 18446744073709551614, true, false,
> "CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq", true, 18446744073709551615, 134217728,
> false, null, true)
>
> [Main] Calling recombineProofSummary("data/w2-z.txt", true,
> "CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq",
>
> 4294967295, 18446744073709551614, true, false,
> "CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq", true, 18446744073709551615, 134217728,
> false, null, true).
> 0.15 ms taken to obtain 66 helper proof candidates, i.e. the minimal set
> of referenced proofs such that each proof contains only a single rule with
> inputs.
> 20.83 ms taken to morph and parse 84 abstract proofs.
> 0.04 ms taken to validate 18 conclusions.
> 0.03 ms taken to find 5 occurrences of 5 theorems.
>
> There are 35 steps towards Cpp / C0.0 (index 8).
> There are 53 steps towards CpCqp / C0C1.0 (index 11).
> There are 57 steps towards CpCNpq / C0CN0.1 (index 13).
> There are 417 steps towards CCNppp / CCN0.0.0 (index 15).
> There are 1877 steps towards CCNpNqCqp / CCN0N1C1.0 (index 17).
> 0.01 ms taken to count 2439 relevant proof steps in total.
> 0.03 ms taken to obtain 84 referenced indices.
> 0.03 ms taken to obtain 8 dedicated indices.
> 0.05 ms taken to build transformed proof.
>
> CpCCqCprCCNrCCNstqCsr = 1
> [0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
> [1] Cpp = DDD11DDD11D11[0][0]
> [2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
> [3] CpCqp = DDD1D[2]1D111
> [4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
> [5] CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq =
> DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1
> [6] CCNppp =
> DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11[5]
> [7] CCNpNqCqp = DDD1D[3][6]DDD1DDD1DDD1D[3][6]DDD1[6]1[5][5][1]11[5][5]
> 0.05 ms taken to print 585 bytes.
> Wed Jul 10 18:29:08 2024: Process terminated. [pid: 23984, tid:1]
>
> You may add a short remark about this in your solution (in comment) or
> under your solution (as reply), then I will credit you for this as well.
>
> ------------------------------
> *Von:* Discher, Samiro
> *Gesendet:* Mittwoch, 10. Juli 2024 18:46:16
> *An:* [email protected]
> *Betreff:* AW: [Metamath] Re: Shortest possible axiom for propositional
> calculus
>
>
> > I managed to prove ax3 from w2 manually!
>
> Indeed, nice.
> Compactly written, that is
>
> CpCCqCprCCNrCCNstqCsr = 1
> [0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
> [1] Cpp = DDD11DDD11D11[0][0]
> [2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
> [3] CpCqp = DDD1D[2]1D111
> [4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
> [5] CCNppp =
> DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1
> [6] CpCCNqqq = D[3][5]
> [7] CCNpNqCqp = DDD1[6]DDD1DDD1DDD1[6]DDD1[5]1[6][6][1]11[6][6]
>
> and
> ./pmGenerator --transform data/w2.txt -f -n -t
> CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq -p -2 -d
> now prints
>
> There are 35 steps towards Cpp / C0.0 (index 8).
> There are 53 steps towards CpCqp / C0C1.0 (index 11).
> There are 57 steps towards CpCNpq / C0CN0.1 (index 13).
> There are 417 steps towards CCNppp / CCN0.0.0 (index 14).
> There are 3301 steps towards CCNpNqCqp / CCN0N1C1.0 (index 16).
>
> i.e. this is a "w2: A3: ω↦3301" improvement, the biggest so far 😃.
> Congratulations!
>
> Could you also post your solution and procedure/details at
> https://github.com/xamidi/pmGenerator/discussions/2?
>
>
> ------------------------------
> *Von:* [email protected] <[email protected]> im Auftrag von
> Steven Nguyen <[email protected]>
> *Gesendet:* Mittwoch, 10. Juli 2024 18:24:46
> *An:* [email protected]
> *Betreff:* Re: [Metamath] Re: Shortest possible axiom for propositional
> calculus
>
>
> I managed to prove ax3 from w2 manually!
>
> (append this to ./data/w2.txt to verify)
>
> [15] CpCCNqqq = D[11][14]
> % Axiom 3
> [16] CCNpNqCqp = DDD1[15]DDD1DDD1DDD1[15]DDD1[14]1[15][15][8]11[15][15]
>
> Based on how procedural/repetitive this manual proof looks compared to the
> more brute force proofs, there’s probably a shorter proof of this.
>
>
> I found this manually-ish by looking at random pmGenerator proofs and only
> filling in steps that require lots of syntax to match. Doing this
> generalizes a pmGenerator proof to an inference proof. Unfortunately due to
> inane reasons my desktop computer doesn't have internet but I took relevant
> photos
>
> Details:
> Letting w2 be 1, a1dt (frege24) be 2, luk2 be 3, partially proving
> DDD1DD2DD1D233321 in metamath.exe resulted in w2-q, which I then repurposed
> for ax3
>
> I think proofs with hypotheses are more intuitive for humans, but I’m not
> sure how much this can help computers.
>
> I tried to send photos of my metamath proofs but for some reason each
> photo is like 8 mb and gmail refuses to send that long of an email. I
> posted them to
> https://github.com/icecream17/Stuff/blob/main/math/
> <https://github.com/icecream17/Stuff/blob/main/math/IMG_0057.jpeg> and
> the files are in the format “IMG_00xx.JPEG”
>
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/CAAfCLnhtUBBz7i9V0QMj8NJidzOMrhUTa4CLe7%2BSS9FynSGMwA%40mail.gmail.com
>
> <https://groups.google.com/d/msgid/metamath/CAAfCLnhtUBBz7i9V0QMj8NJidzOMrhUTa4CLe7%2BSS9FynSGMwA%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/430751c7-82ec-4037-af74-6b45f1cc1952n%40googlegroups.com.
% Step counting: pmGenerator --transform data/w2-A2,L1.txt -f -n -t
CCpCqrCCpqCpr,CCpqCCqrCpr -p -2 -d
% Compact (8345 bytes): pmGenerator --transform data/w2-A2,L1.txt -f -n -t
CCpCqrCCpqCpr,CCpqCCqrCpr -j -1 -s
CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CCCpCCqCprCCNrCCNstqCsruCvu,Cpp,CpCCNqCCNrsCCtCCuCtvCCNvCCNwxuCwvqCrq,CpCqCrr,CCNpCCNCqCCrCqsCCNsCCNturCtsvNwCwCxp,CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq,CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq,CpCqCrCsCtq,CpCqCrp,CCNCpqCCNrsqCrCpq,CCNCpCqrCCNstrCsCpCqr,CCNCNpqCCNrspCrCNpq,CpCqp,CNCpCqNrCsCtCur,CNCpCqrCsNr,CCNpCCNqrCNppCqp,CpCCNqqq,CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq,CCNCCpqqCCNrspCrCCpqq,CpCCNCpqCpqq,CCNCNpqpCNpq,CpCCNqNpq,CCNCpqCCNrsCNqNpCrCpq,CCNpNqCqp,CNNpCqp,CpCqNNCNpr,CpNNp,CCCpqCCrrsCqs,CpCqCNCrps,CpCqNNCrCsp,CpCCNCNqqCNqqq,CCCNpqNrCrCps,CCNpCCNqrNsCsCqp,CCNCpCqrrCpCqr,CpCCNqNNqq,CpCCNNNqNNqq,CpCCqCCrrsCqs,CpCCpqq,CCNCCpqqpCCpqq,CCNpCqpCqp,CpCCNqqCCqrr,CNCpqCrCqs,CpCCNNCqprr,CCpCqNpCqNp,CCpCNNpqCNNpq,CCCpqCrpCrp,CCNpCqCrpCqCrp,CCCpqCNprCNpr,CCpCqCrNpCqCrNp,CpCCNNCqrqq,CCpCqCprCqCpr,CCpCNCpqrCNCpqr,CCCpqCrCqsCrCqs,CCCCpqqCprCpr,CCCpqCrCspCrCsp,CCpCCNppqCCNppq,CCNNpCqCprCqCpr,CCNpCCpqqCCpqq,CCNpCNCqprCNCqpr,CCpqCpCrq,CCpqCrCpCsq,CpCqCCprCsr,CpCCCqprCsr,CCNNpqCpq,CCCNpqrCpNNr,CCCNpqrCpCCrss,CCCNpqrCpCNrs,CCpqCNNpq,CCNCpNpCpqCpq,CCpqCNCprq,CCCCpqqrCpr,CCpqCCNppq,CpCCqNpCqr,CpCCpNqCqr,CCpNqCpCqr,CCpNqCqCpr,CNCCNpqpq,CCNNCCNpqpqq,CCNCpNNqqCpNNq,CCCCNpqpCrqCrq,CCCCpqNpCrqCrq,CCpNqCNCpCqrs,CNCCNpqCrpq,CNCCCpqrpr,CNCCpqCprq,CNCpCCpqrq,CNCpNCpqNNq,CNCCpqCprNNq,CCpqCpNNq,CCpqCpCNqr,CpCCpqCNqr,CCNpqCNqp,CCpqCpCCqrr,CCNpqCCqpp,CCpCCqpNpNNNp,CCpCCNqpqCCNqpq,CCNNCNpNNNNNCCNNqqprCNrs,CCCpqrCNNNrp,CCpNNqCNNNNpq,CpCCpqCNCrqs,CNNCpNqCCCqNprr,CCCCpNNqqCprCpr,CCCNpqrCpNCrNr,CCCCpqCrqsCps,CpCCpqCCNNqrr,CNNCNpqCCqNCrrp,CCNCCpCCpqCrqsss,CCNCpqrCCrqCpq
% There are 330556198971 steps towards CCpqCCqrCpr / CC0.1CC1.2C0.2 (index 214).
% There are 661949665229 steps towards CCpCqrCCpqCpr / CC0C1.2CC0.1C0.2 (index
215).
CpCCqCprCCNrCCNstqCsr = 1
[0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
[1] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = DD[0]11
[2]
CCNCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqpCCNzasCzCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqp
= D[1]1
[3] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = D[2]1
[4] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][3]
[5] CCpCCCqCCrCCsCrtCCNtCCNuvsCutwCCNwCCNxyqCxwzCCNzCCNabpCaz = D1[0]
[6] Cpp = DD[5][4][3]
[7]
CCNCCNpCCNqrCCsCCtCsuCCNuCCNvwtCvupCqpCCNxyzCxCCNpCCNqrCCsCCtCsuCCNuCCNvwtCvupCqp
= DD1[4]1
[8] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed
= D1[3]
[9] CCNCpqCCNrsCCtpCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[8][0]
[10] CpCqCCCNCrCCsCrtCCNtCCNuvsCutwNqx = D[4][9]
[11] CpCCNqCCNrsCCtCCuCtvCCNvCCNwxuCwvqCrq = D[7][10]
[12] CCpCCqCCNrCCNstCCuCCvCuwCCNwCCNxyvCxwrCsrzCCNzCCNabpCaz = D1[11]
[13] CCNCpCqrCCNstCCNquCCvCCwCvxCCNxCCNyzwCyxrCsCpCqr = D[12]DD[12]1[11]
[14] CpCqCrr = D[13]D[4][7]
[15]
CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq
= D[5]1
[16] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[15][11]
[17] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][16]
[18] CCNpCCNCqCCrCqsCCNsCCNturCtsvNwCwCxp = D[17][11]
[19] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[16][18]
[20] CpCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyyCsr = DD[0][1][14]
[21] CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq = D[19][20]
[22]
CCCNCpCCqCprCCNrCCNstqCsruCNvCCNwxyCCNCwvCCNzaCyCCbCCcCbdCCNdCCNefcCedvCzCwv =
DD[0][15][11]
[23]
CCpCCCCNCqCCrCqsCCNsCCNturCtsvCNwCCNxyzCCNCxwCCNabCzCCcCCdCceCCNeCCNfgdCfewCaCxwhCCNhCCNijpCih
= D1[22]
[24]
CCCNpqCrCCsCCtCsuCCNuCCNvwtCvuxCCNCpCyxCCNzaCCNCbCCcCbdCCNdCCNefcCedgCNxCCNyhrCzCpCyx
= DD[23]1[11]
[25] CpCqCrCsCtq = DD[24]1[20]
[26] CpCqCrp = DD[0][17][25]
[27] CCNCpqCCNrsqCrCpq = D[23][26]
[28] CpCqCrCsp = D[25][25]
[29] CCNCpCqrCCNstrCsCpCqr = D[23][28]
[30] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1[28]
[31] CCpCCqCrCsqtCCNtCCNuvpCut = D1[26]
[32] CpCqCNpr = DD[31][0][10]
[33] CCNCNpqCCNrspCrCNpq = D[30][32]
[34] CpCqp = DD[22][25]1
[35] CCCpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrqcCdc =
DD[0][8][11]
[36] CCpCCqCrCNsCCNtCCNuvsCutwCCNwCCNxypCxw = D1DDD[0]D1DD1D[9]11[11][35]
[37] CCpCCCqCCrCsCtCurvCCNvCCNwxqCwvyCCNyCCNzapCzy = D1[30]
[38] CCCNpqrCCNCpsCCNtuCrCCvCwCxCyvsCtCps = DD[37]1[11]
[39] CNCpCqNrCsCtCur = DD[36][38][11]
[40] CpCNCqCrsCtNs = D[33][39]
[41] CNCpCqrCsNr = D[40][40]
[42] CCpCCqqrCCNrCCNstpCsr = D1[6]
[43] CCNCCNpCCNqrCspCqpCCNtusCtCCNpCCNqrCspCqp = D[42]1
[44] CpCCNqCCNrsCNqqCrq = D[43][41]
[45] CCNpCCNqrCNppCqp = D[44][44]
[46] CCNppp = D[45][21]
[47] CpCCNqqq = D[34][46]
[48] CCpCCqCCNrrrsCCNsCCNtupCts = D1[47]
[49] CpCCNqCCNrsCNCpqCpqCrq = DDD1[46]1[47]
[50] CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq = D[48][49]
[51] CCNCCpqqCCNrspCrCCpqq = D[12][49]
[52] CpCCNCpqCpqq = D[50][47]
[53] CCNCNpqpCNpq = D[33][52]
[54] CCNpCCNqrCCsCCNCstCsttpCqp = DD1[52][6]
[55] CpCCNqNpq = D[54]1
[56] CCpCCqCCNrNqrsCCNsCCNtupCts = D1[55]
[57] CCNpNqCCNpCCNrsqCrp = DD[56]1[55]
[58] CCNCpqCCNrsCNqNpCrCpq = D[56][57]
[59] CCNpNqCqp = D[58][55]
[60] CpCNpq = D[19]1
[61] CpCqq = D[14][14]
[62] CNNpCqp = DD[33][41]D[60][61]
[63] CpCqNNp = D[18][62]
[64] CpCqNNCNpr = D[58]D[34]D[59]D[59]D[54]D[34][63]
[65] CNNpp = D[46]D[18][64]
[66] CpNNp = D[59][65]
[67] CCCpqCCrrsCqs = DD[8][42]D[34]D[55][6]
[68] CpCqCNCrps = D[67]D[19]D[35][43]
[69] CpCqCrCsNNr = D[26][63]
[70] CpCqNNCrq = D[9][69]
[71] CNCpCqCrsCtNs = D[53][39]
[72] CNCpNqCrCsq = D[53][71]
[73] CpCqNNCrCsp =
DD[19]D[26]D[59]D[59]DD[19][69]D[60]D[59]D[70][70]D[66]DD[33][71]D[53][72]
[74] CNCpCqNrCsr = D[18][73]
[75] CpCCNCNqqCNqqq = D[50]D[53][74]
[76] CCCNpqNrCrCps = DD[9][21]D[43][21]
[77] CCNpCCNqrNsCsCqp = DD[24][6]D[2][25]
[78] CCNCpCqrrCpCqr = D[29][52]
[79] CCNpCCNqrNNpCqp = D[56][62]
[80] CpCCNqNNqq = D[34]D[79][52]
[81] CpCCNNNqNNqq = D[34]D[79][75]
[82] CpCCqCCrrsCqs = DD[48][48]D[26][42]
[83] CpCCpqq = D[51][80]
[84] CCNCCpqqpCCpqq = D[51][52]
[85] CCNpCCNqrpCqp = D[37][34]
[86] CpCCNCNqCrqCNqCrqCrq = D[50][41]
[87] CCNpCqpCqp = D[85][86]
[88] CCNppCCpqq = D[51][75]
[89] CpCCNqqCCqrr = D[62]D[66][88]
[90] CNCpqCrCqs = DD[36][12][89]
[91] CCpCCqqrCpr = D[82][82]
[92] CpCNCCpqqr = D[33][89]
[93] CpCCNNCqprr = DDD[12][57]D[34]D[91]DD[31][57][80]D[87][92]
[94] CCpCqNpCqNp = D[87]D[51]DD[27][86][93]
[95] CpCCNNCNNqrqq = D[34]D[87]D[51]D[34][66]
[96] CCpCNNpqCNNpq = D[87]D[51][95]
[97] CpCCNNqNqCqr = D[34]D[76]D[94][88]
[98] CCCpqCrpCrp = D[84]DD[38][18][97]
[99] CCNpCqCrpCqCrp = D[84]D[91][71]
[100] CCCpqCNprCNpr = D[84]DD[17][21]D[67]D[18][74]
[101] CCpCqCrNpCqCrNp = D[84]D[59]D[67][73]
[102] CNNpCCNCpqCpqq = D[50][81]
[103] CpCCNNpqq = D[51]D[34]DD[42][6][102]
[104] CpCCNNCqrqq = D[34]D[98][103]
[105] CCpCqCprCqCpr = D[84]D[98]DD[19]D[26][32]D[59]D[59]D[54]D[34][64]
[106] CCpCNCpqrCNCpqr = D[84]D[98]D[33]D[19][14]
[107] CCCpqCrCqsCrCqs = D[84]D[78]D[98]D[67]D[67]D[13]D[34]D[19][25]
[108] CpCCCCpqqrr = D[51][89]
[109] CCCCpqqCprCpr = D[105][108]
[110] CpCqCNCrCspt = D[67]D[67]D[13][25]
[111] CCCpqCrCspCrCsp = D[84]D[105]D[67][110]
[112] CCpCCNppqCCNppq = D[84]D[45]D[34]D[98][93]
[113] CCNNpCqCprCqCpr = D[84]D[94]D[100][110]
[114] CCNpCCpqqCCpqq = D[84]D[94]D[109][68]
[115] CCNpCNCqprCNCqpr = DD[83]D[51]D[34]D[94][93][105]
[116] CNCpqCCNCprCprr = D[50][104]
[117] CCpqCpCrq = D[29][116]
[118] CCpqCrCpCsq = D[117][117]
[119] CpCCpqCrq = D[109][118]
[120] CpCqCCprCsr = D[117][119]
[121] CpCCCqprCsr = DD[84]D[78]D[98]D[67]D[58]D[34]D[9][10][120]
[122] CpCCNNpqCrq = DD[84]D[94]D[100][68][120]
[123] CCNNpqCpq = D[105][122]
[124] CCCpqrCqr = D[105][121]
[125] CCCNpqrCpNNr = D[124]D[56][63]
[126] CCCNpqrCpCCrss = D[124][51]
[127] CCCNpqrCpCNrs = D[124][33]
[128] CNNpCCpqCrq = D[96][120]
[129] CCpqCNNpq = D[105][128]
[130] CCNCpNpCpqCpq = D[114]D[117]D[105]D[59]D[106]D[96]D[29]D[50]D[53][41]
[131] CCpqCNCprq = D[105]D[106][120]
[132] CpCCCCpqqrCsr = D[109][120]
[133] CCCCpqqrCpr = D[105][132]
[134] CCNppCCpqCrq = D[112][120]
[135] CCpqCCNppq = D[105][134]
[136] CpCCqNpCqr = D[77][116]
[137] CpCCpNqCqr = D[99]D[131]D[77]D[131][135]
[138] CCpNqCpCqr = D[99]D[131][136]
[139] CCpNqCqCpr = D[99]D[131][137]
[140] CNCCpqrCpCsq = D[106][118]
[141] CpCNCCpqrq = D[105][140]
[142] CCNppCNCCpqrq = D[112]D[117][141]
[143] CNCCNpqpq = D[53]D[117]D[59]D[125][142]
[144] CCNNCCNpqpqq = D[114]D[117]D[129][143]
[145] CNCCNpqpNNq = D[125][144]
[146] CCNCpNNqqCpNNq = D[78][145]
[147] CNCCNpqpCrq = D[117][143]
[148] CCCCNpqpCrqCrq = D[114]D[117][147]
[149] CCCCpqNpCrqCrq = D[114]D[117]D[117]D[53]D[101]D[127][142]
[150] CCpNqCNCpCqrs = D[138]D[146]D[131][138]
[151] CCNCpqCpqCpCrq = D[112][118]
[152] CCpqCNCpCrqs = D[127][151]
[153] CNCCNpqCrpq = D[148][152]
[154] CNCCCpqrpr = D[149]D[138]D[146]D[131]D[111][136]
[155] CNCCpqCprq = D[149][150]
[156] CNCpCCpqrq = D[149]D[138]D[146]D[131][139]
[157] CCpNqCqNp = D[101][137]
[158] CCpNqNNCqNp = D[146]D[131][157]
[159] CNCpNCpqNNq = D[146]D[131]D[149]D[138][158]
[160] CNCNCCpqCprsq = D[131][155]
[161] CNCCpqCprNNq = D[146][160]
[162] CCpqCpNNq = D[78][161]
[163] CCpqCpCNqr = D[78]D[138][161]
[164] CpCCpqCNqr = D[133][163]
[165] CCNpqCNqp = D[99][164]
[166] CCpqCpCCqrr = D[78]D[126]D[114]D[117]D[129][155]
[167] CpCCpqCCqrr = D[133][166]
[168] CCNpqCCqpp = D[99][167]
[169] CCpCCqpNpNNNp =
DD[101]D[129][137]DD[114]D[117]D[129]D[105]D[59]D[106]D[117]DD[51][72]D[87]D[51]D[34]D[29][75]D[59][159]
[170] CCpCCNqpqCCNqpq = DD[99]DD[107][132][166]DD[83]D[76]D[52][61][148]
[171] CpCCNNpqCNqr = D[123][164]
[172] CCpqCNqNNNp = D[101]D[129][164]
[173] CCNNCNpNNNNNCCNNqqprCNrs = D[171]DD[83]D[96]D[117]D[83][65][172]
[174] CNpCCCpqrCsr = D[100][120]
[175] CCCpqrCNCNpsr = D[105]D[131][174]
[176] CNpCqCCqpr = D[59]D[162][156]
[177] CCCpqrCNNNrp = D[111]D[99]D[175]D[135][176]
[178] CCNCpCqrNqCpCqr = D[99]D[106]D[117][55]
[179] CCpNNqCNNNNpq = D[99]DD[178]D[149][92]D[117]D[99]D[175]D[135]D[59][161]
[180] CCNCpqCpqCNCprq = D[112]D[117][131]
[181] CCNpqCrCNqp = D[117][165]
[182] CNCCpqCprCsq = D[117][155]
[183] CpCCpqCNCrqs = D[133]D[99]D[180]D[181][182]
[184] CNNNNCpqCpCCqrr = D[179]D[162][166]
[185] CCNCpqCpqCNNpq = D[112]D[117][129]
[186] CNNCpNqCCCqNprr = D[184]D[169]DD[127][185][157]
[187] CpCqCrCCpsCts = D[117][120]
[188] CCCCpqqrCNNpr = D[105]D[96]D[109][187]
[189] CCCCpNNqqCprCpr = D[113]D[188]D[126]D[114]D[117]D[129]D[99][136]
[190] CpNNCCpNqCqr = D[125]D[135][137]
[191] CCNpNqCqCrp = D[78]D[117]D[59][190]
[192] CCCNpqrCpNCrNr =
D[77]D[129]DD[170]D[117]D[83]D[76]D[87][102]DDD[126]DDD[48][31][80]D[27][52]D[34]D[165]D[191][159][166]
[193] CCCCpqCrqsCps = D[105]DD[113]DD[83][128][166][120]
[194] CCpqCrCpCCqss = D[117][166]
[195] CpCCpqCCNNqrr = DD[113]D[188]D[126]D[135][162][194]
[196] CNCCNpqCrpCCqss = D[184]D[169]D[60][153]
[197] CNNCNpqCCqNCrrp =
D[129]D[105]DD[105]DD[170]D[117]DD[56]D[60][6][116]DD[105]D[165]D[117][153]D[165][153][196]
[198] CCpqCNqNp = D[101][164]
[199] CCpqNNCNqNp = D[162][198]
[200] CCpqCNCpCCqrrs = D[163][166]
[201] CCNCCpCCpqCrqsss = DD[197]D[199]D[78]D[149][200]D[173]DD[27][89][119]
[202] CNCCCpqrpCsr = D[117][154]
[203] CNCpqp = D[53]D[91][90]
[204] CCNCpqCCNrsCpCCttqCrCpq = D[48][42]
[205] CNNCpqCpCrq = D[96][118]
[206] CpCNNCpqq = D[105][205]
[207] CCCpqrCsCqr = D[117][124]
[208] CCpqCNCpCNqrs = D[163][163]
[209] CCpqCpCrCsq = D[78]D[117][182]
[210] CNCCNNpqCprq = D[148][150]
[211] CCNCpqrCCrqCpq =
D[99]DDDDD[197]DD[125][151][154]DDD[184]DDD[101]D[129]D[99]D[180]DD[117]D[105]DD[105]D[130]D[117]D[59][145]D[59]D[125]D[112][187][176]D[139]D[162]D[114][202]DD[117]D[83][203]D[77][102]D[198]D[178]DD[204]D[34]D[91]D[99][55]D[34][153]D[206][119]D[197]DD[125][185]D[193][170]DD[129]D[78]DD[129]D[99]DDDDD[178]D[192]D[168]D[125][134][167]DD[101]D[180]D[207][164]DD[197]D[199][163]D[173]DD[117][105]DD[107]DD[105]D[51]D[51]D[18]D[18]D[18]D[67]D[59]D[59]D[59]D[59]DD[19][21]D[18]D[78]D[59]D[59]D[59]D[85]D[34]D[59]D[79][81][120]D[177]D[168]D[165]D[148]D[163]D[78]D[117]D[59]D[125]D[135][136]D[34]DDDD[197]D[199][168]D[173]DD[117][94]D[127]D[117]D[114]D[78]DD[42][59][95]D[131][183]DD[99]D[131][164]DDDD[111][195]DDD[111]D[123]D[189][194]DD[129]D[55]D[58][49]DD[162]D[99][171]D[177]D[168]D[165]D[149]D[163][172]DD[111][183]D[168]D[101]D[133]D[99]D[131][163]D[129]D[117][205]D[165]DDD[99]D[115]D[117][167][176][208]D[105]D[165][196]DD[162]D[107]D[189]D[117][209]DDDDD[123][195]DDD[99]D[180]D[181][210]DD[105]D[165]DD[101]DD[114]D[117]D[129]D[59]D[131]D[130]D[101]D[127]D[114]D[117]D[96]D[117]D[84]D[53][90]D[191][161]D[117]D[149][152]D[139]D[94]D[126]D[135]D[58]D[34]D[112]D[117][206]DD[101]D[204][89]D[60]D[105]D[123]D[78]D[117]D[59]D[125]D[135]D[133][139]D[34]D[201]DD[78]D[117][210]D[177]D[126]D[114]D[117]D[129]D[114][147]D[129]D[201]DD[105]DD[129]D[105]DD[105]D[165]DD[78]DD[78]DD[124][45][144][160][153]D[115]D[115]DD[105]DD[105][174][122]D[117]D[129][141]DD[162]D[99]D[59]D[148][200]D[165]D[177]D[168]D[165]D[148]D[163][209]DD[197]D[158]D[146]D[131][131]D[173]D[118]D[51]D[34]D[114]D[117]D[96]D[117]DD[51][90]D[66][203]D[186]D[66][190]DD[146]D[106][207]DD[179]D[162]D[101]D[165][182]DDD[186]D[66]D[94]D[127]D[114]D[129]D[117]D[87][108]D[101]D[165]D[149][208]DDDD[165][202]DD[83]D[94]D[33]D[50]D[4][13]D[103]D[94]D[33][97]DD[99]D[123][167]DD[105]DD[129]D[105]D[129][128]D[66][121]D[135]D[101]D[165]D[117][156]DD[78]D[58][104]D[192]D[114]D[117]D[129][156][120]
[212] CCpCqrCCqpCqr = D[211][155]
[213] CCpCqrCpCqCsr = D[212][118]
[214] CCpqCCqrCpr = D[105]D[213]DD[211][140][212]
[215] CCpCqrCCpqCpr = DD[214]D[105]D[213]D[193][212][212]
