Proof summary of https://us.metamath.org/mmsolitaire/pmproofs.txt (version 26-Feb-2025) for use with https://github.com/xamidi/pmGenerator.

pm.txt

% Full summary:      pmGenerator --transform data/pm.txt -f -n -t . -j 1
%  - infix formulas: pmGenerator --transform data/pm.txt -f -n -t . -j 1 -u
%    - to file:      pmGenerator --transform data/pm.txt -f -n -t . -j 1 -u -o data/tmp.txt
% Same steps:
%  - step counting:  pmGenerator --transform data/pm.txt -f -n -t . -j -1 -p -2 -d
%  - infix formulas: pmGenerator --transform data/pm.txt -f -n -t . -j -1 -u
% Summary containing intermediate theorems with use counts of at least two:
%  - to file:        pmGenerator --transform data/pm.txt -f -n -t . -o data/tmp.txt -d
%                    (14702 bytes, in contrast to 14059 bytes here)

% List of theorems: CCNppp,CCNpqCNqp,CCpCqrCqCpr,CCpqCCrpCrq,CCpNpNp,CCpNqCqNp,CCpqCCqrCpr,Cpp,CNNpp,CpNNp,CCpqCNqNp,CpCNpq,CNpCpq,CpCCpqq,CNNpCCpqq,CCpCNqrCpCNrq,CCpCNqrCNCpqr,CCNCpqrCpCNqr,CCpqCCNrpCNqr,CCpqCCNprCNrq,CCpqCCNprCNqr,CCpCpqCpq,CCNpCqpCqp,CCNNpCpqCpq,CNCpqp,CNCpqNq,CNCpqCNpr,CNCpqCrNq,CNCpqCqr,CNpCCNqpq,CCNpqCCpqq,CCpqCCNpqq,CCNpqCCNpNqp,CCpqCCpNqNp,CCCNpqrCpr,CCCpqrCNpr,CCCpqrCCrpp,CCpqCCNCNpqrCNqr,CCpqCCNCNqprCNqr,CCpqCCpCqrCpr,CCpqCCNNqrCpr,CCpCqrCCspCCsqCsr,CCNCpqrCCNCpNrsCNCpqs,CCpCqrCCpCrsCpCqs,CCCpqCrsCrCqs,CNCpqNCNNpq,CNCNNpqNCpq,CNNCpqCNNpq,CCNNpqNNCpq,CpCqNCpNq,CpCqNCqNp,CNCpNqNCqNp,NNCpNNp,CNCpNqq,CCNCpNqrCpCqr,CCpCqrCNCpNqr,CNCCpqNCqrCpr,CNCCpqNCrpCrq,CNCpNCpqq,CCNCpNqrCNCpNNrNq,CNCpNqCrq,CCpqCNCprq,CCpqCNCrNpq,CNCCpqNCprCpNCqNr,CNCCpqNCrqCCNprq,CCpqCNCprNCqr,CNCCpqNCrsCNCpNrNCqNs,CNCCpqNCrsCCNprCNqs,NCCCpqCNqNpNCCNrNsCsr,NCCNCCpqNCrsNCCNsNrNCNqNpNCNCCNtNuNCNvNwNCCwvNCut,NCCNCCpNqNCNrsNCCqNpNCNsrNCNCCtNuNCNvwNCCuNtNCNwv,NCCpNNpNCNNqq,NCCCNCpNqrCNCpNNrNqNCCNCsNNtuCNCsut,NCCCNCpNqrCNCqrNpNCCNCstNuCNCuNst,NCCppNCqq,NCCNCpNqNCqNpNCNCrNsNCsNr,CNCNCCpqNCrsNNCCqtNCurNCCptNCus,NCCpNCpNpNCNCqNrr,NCCpCqpNCCNrrr,NCCCNpqCNqpNCCNrsCNsr,NCCNCNCpNqrNCpNNCqrNCNCsNNCtuNCNCsNtu,NCCCNCpqrCpCNqrNCCsCNtuCNCstu,CNCCpqNCrsNCCNCptNCqtNCNCruNCsu,CNCCpqNCrsNCCCNptCNqtNCCNruCNsu,CNCNCCpqNCrsNNCCtuNCvwNCCNCpNtNCqNuNCNCrNvNCsNw,CNCNCCpqNCrsNNCCtuNCvwNCCCNptCNquNCCNrvCNsw,NCCNCpNCqrCNNCpqNCpNrNCCNNCstNCsNuNCsNCtu,NCCCpNCqNrNCCpqNCprNCNCCstNCsuCsNCtNu,NCCpCNNCpqNCpNqNCCNNCrsNCrtr,NCCpNCCNpqNCNprNCNCCNstNCNsNts,NCCpCNpqNCCNrNCrsr,NCCpNCpNCNpqNCNCrsr,NCCNCpqNCNNpqNCNCNNrsNCrs,NCCNNCpqCNNpqNCCNNrsNNCrs,NCCNCpNNqNCNNpqNCNCNNrsNCrNNs,NCCNNCpNNqCNNpqNCCNNrsNNCrNNs,NCCNNppNCqNNq,NCCNCpNNqNCpqNCNCrsNCrNNs,NCCNNCpNNqCpqNCCrsNNCrNNs,NCCCpqCNNpqNCCNNrsCrs,NCCNCpqNCpNNqNCNCrNNsNCrs,NCCCpqCpNCpNqNCCrNCsNtCrt,NCCCpqNCCpNCpNqNCNCrsrNCNCCtNCuNvwCtv,NCCCpqNCCrCsrNCCNpqqNCNCtNCCNuvwCuw,CpNCCqNCqNpNCNCrsr,CpNCCqCrqNCCpss,NCCNCCpqNCprCpNCqNrNCCsNCtNuNCCstNCsu,NCCNCCpqNCrqCCNprqNCCCNstuNCCsuNCtu,NCCCNCpqCprCpCNqrNCCsCNtuCNCvtCsu,NCCCNCpqCrqCNCpNrqNCCNCsNtuCNCsvCtu,NCCCpNpNpNCqCrq,NCCCNpppNCqCrq,NCCNCCpqNCpNqNpNCNrNCCrsNCrt,NCCNCCpqNCNpqqNCrNCCsrNCtr,CNCCpqNCrsNCCCstCrtNCCquCpu,CNCCpqNCrsNCCCtpCtqNCCurCus,CNCCpqNCrsNCCNCCstNCupNCCrtNCuqNCNCCqvNCwrNCCpvNCws,NCNCNCCCNCpNqrCpCqrNCCsCtuCNCsNtuNNCCCvCwxCwCvxNCCyCzaCzCyaNNCCCbCcdCNCbNcdNCCNCeNfgCeCfg,CNCpNqNCCrqNCsp,CNNCCpqNCrsNCCsNqNCNrp,NNCNCCpqNCqpNNCCpNqNCNqp,NCCNCCNpqNNNrNCrNCNqpNCNCsNCNtuNCCNutNNNs,NCCNCCpqNCqpNNCCpNqNCNqpNCNNCCrNsNCNtuNCCusNCtr,NNCCpNpNCNpp,CNCNpNNqNCCprNCqs,NCCNNCCpqNCrsCNNCpNNqNCrNNsNCCNNCtNNuNCvNNwNNCCtuNCvw,NCCNCCpqNCqpCNNCpNqNCNpNNqNCCNNCrNsNCNtNNuNCCtsNCur,NCCNCNNCpNqNCNpNNqCNNCpNNqNCqNNpNCCNNCrNsNCtNNuNCNNCusNCNrNNt,NCCCNpqCCpqqNCCCrstCNrt,NCCCNCpqrCNCpqNCpNrNCCsNCtNuCsu,CNCpNCqrCqNCrNp,NCCCpNCCqrNCstNCCNCpNqNCpNrNCNCpNsNCpNtNCNCCNCuNvNCwNxNCNCuNyNCzNaCuNCCvxNCya,NCCNCpNCqrNCpNCNCsNqrNCNCtNCNCtNuvNCtNCuv,CNCCpqNCprCpNCCsrNCtq,NCCNCpNNCCpqrNCqNNCCpqrNCNCsNNCtNCsuNCuNNCtNCsu,NCCCpCpqCpqNCrCsr,NCCCCpqCrsCrCqsNCCtCuvCCtuCtv,NCCCpCqrCpCqNCpNrNCCsCtNCuNvCsCtv,CCpqNCCCprCpNCqNrNCCsNCtNuCsu,CpNCCCpqqNCrCsr,CpNCCqNCCrqNCspNCNCCptut,NCCCCNCNpqrsNCNCCpsNCqsNCrsNCNCNCCtuNCvuNCwuCCNCNtvwu,CNNCCpqNCrNCrNsNCCNCtNuuNCsp,CNNCCCNpqpNCrCNrsNCCtqNCuCvu,NCCCNCpNqrCpCqrNCCsCtuCNCsNtu,NCCNCCNpqNNqNCpNNqNCNCrsNCCNrts,NCCCNNCpqrCNprNCCNstCNNCstt,NCCNCCCNpqCNrsNCCNtuCNvsCNsNCCprNCtvNCCNwNCCxyNCzaNCCCNxwCNywNCCNzwCNaw,CCpNqNCCNCCNrpNqNCrNqNCNCstNCCNsut,NCCCpNCCqrNCstNCCCpqCprNCCpsCptNCNCCCuvCwxNCCyzCwaCwNCCvxNCza,CNCCpqNNCCrCstNCCupvNCCNCrNstNCpNCvNq,CCCCCpqCNrNsrtCCtpCsp,CCCpqpp,NCCNCCNCCpqNCrstNCuNCCsvNCrpNCCsNCCqtNCuvNCNCCruNCtrpNCNCCwNCCxyNCzaNCNCCxzNCybcNCCNCCcxNCxwyNCzNCCwaNCbc
%  - generated from 'data/pmproofs.txt' (https://us.metamath.org/mmsolitaire/pmproofs.txt, version 26-Feb-2025) via
%    $ ./dProofsFromDB data/pmproofs.txt data/pmproofs_dproofs.txt 1 1
%    $ ./pmGenerator --parse data/pmproofs_dProofs.txt -f -n -b -o data/tmp.txt
%    $ sed -i 's/[0-9]+\. //g' -r data/tmp.txt && tr '\n' ',' < data/tmp.txt > data/pmproofs_theorems.txt && sed -i 's/,$//g' -r data/pmproofs_theorems.txt

% File generated from 'data/pmproofs.txt' via
% $ ./dProofsFromDB data/pmproofs.txt data/pmproofs_dproofs.txt 1 1
% $ ./pmGenerator --parse data/pmproofs_dProofs.txt -f -n -s -o data/tmp.txt
% $ ./pmGenerator --transform data/tmp.txt -f -n -j -1 -o data/pm.txt -t <list of theorems>

% Compacting list: CCpCqCrsCpCCqrCqs,CCpCNqNrCpCrq,CNNpCqp,CCpCqCCrqsCpCqs,CCpqCpCrq,CCpCNqCCqrsCpCNqs,CCpCqrCpCCrsCqs,CNpCqCpr,CCpqCpNNq,CCNNCpqpCNNCpqq,CCpCNNCqrqCpCNNCqrr,CCpCNNqCqrCpCNNqr,CpCNCqNrr,CCNNpqCpq,CCpCqCNrrCpCqr,CCpCCNqrsCpCCNrqs,CCCpqCrCspCCpqCrCsq,CCpqCpCrNCqNr,CCNNCpqCrpCNNCpqCrq,CCpqCNNCqrCpr,CNCpNCqrCCsqCsr,CNCpqCrp,CNCCpqrCCspCsq,CpCNqNCpq,CNNCCpqNCrsCsNq,CCpCqrCpCCqsCqNCrNs,CCpCqNNrCpCqr,CpCqNCCrqNCsp,CNNCpNqCqNNNp,CCpqCpNNNNq,CNCpNNqNCpq,CNCpNNCqrq,CNCpNNCqNrr,CNCNCpqrp,CNCNCpNqrCsq,CNCCpqNCqpNNCCpNqNCNqp
%  - generated from 'data/pm.txt' via
%    $ ./findCompactSummary data/pm.txt <list of theorems>
%  - usage:
%    $ ./pmGenerator --transform data/pm.txt -f -n -j -1 -o data/pm-compact.txt -t <list of theorems> -s <compacting list> -d
%     - examplary output: 24.43 ms taken to obtain 1039 helper proof candidates, i.e. the minimal set of referenced proofs such that each proof contains only a single rule with inputs.
%                         76.86 ms taken to morph and parse 1194 abstract proofs.
%                         0.32 ms taken to validate 155 conclusions.
%                         4.99 ms taken to find 155 occurrences of 154 theorems.
%                         0.36 ms taken to obtain 1194 referenced indices.
%                         2.14 ms taken to obtain 191 dedicated indices.
%                         0.92 ms taken to build transformed proof.
%                         2.12 ms taken to print and save 11850 bytes to data/pm-compact.txt.
% NOTE: There are two proofs for CCpqCNCrNpq at [34] and [36] — only [36] is referenced by other proofs.

    CpCqp = 1
    CCpCqrCCpqCpr = 2
    CCNpNqCqp = 3
[0] Cpp = DD211
[1] CCpCpqCpq = DD22D21
[2] CCpqCCrpCrq = DD2D121
[3] CNpCpq = DD2D131
[4] CCpqCCpCqrCpr = DD2D1D221
[5] CpCCpqq = DD2D1D2[0]1
[6] CCpqCCqrCpr = DD2D1D2[2]1
[7] CpCNpq = DD2D1D2[3]1
[8] CCpCqrCCspCCsqCsr = DD2D1D2D12[2]
[9] CNNpp = DD2DD2D13[3]1
[10] CpNNp = D3[9]
[11] CCpCqrCqCpr = DD2D1DD22D11DD2D112
[12] CCCpqrCNpr = DD2D1DD22D1[3]1
[13] CCNppp = DD2DD2D13D2[3]1
[14] CCpCqrCCpCrsCpCqs = DD2D12D2D1[6]
[15] CNNpCCpqq = DD2D1D2[0]DD2D13[3]
[16] CNCpqCqr = DD2D1DD22D11DD2D11[3]
[17] CNCpNqq = D3DD2D1[10]1
[18] CCCNpqrCpr = DD2D1DD22D1[7]1
[19] CCNpqCNqp = DD2D13D2D1[10]
[20] CpCqNCpNq = DD2D13DD2D1D2[9]1
[21] CNCpNqCrq = DD2D13[16]
[22] CCpNqCqNp = DD2D13DD2D1DD22D2DD2D13[3]1
[23] CNCpqCNpr = DD2D1DD22D1[3]DD2D11[3]
[24] CCpCNqrCpCNrq = D2D1[19]
[25] CNCpqp = D3DD2D1[10][3]
[26] NCCCpCpqCpqNCrCsr = DD3DD2[9]D1[1]1
[27] CNpCCNqpq = DD2D1D2D1DD23D11DD2D12DD2D11[3]
[28] NCCppNCqq = DD3DD2[9]D1[0][0]
[29] CCCpqCrsCrCqs = DD2D1DD22D11DD2D11DD2D12DD2D1DD22D111
[30] CNNCpqCNNpq = DD2D1DD22D2DD2D13[3]DD2D13[3]
[31] CNCpqNq = D3DD2D1[10]DD2D13[3]
[32] CCNpqCCNpNqp = DD2D13D2[20]
[33] CpCqNCqNp = DD2D1D2[20]1
[34] CCpqCNCrNpq = DD2[2]D1[17]
[35] NNCpNNp = D[10][10]
[36] CCpqCNCrNpq = DD2D1DD22D1[17]1
[37] CpNCCqCrqNCCpss = DD2D1D3DD2[9]D11[5]
[38] CCNNpCpqCpq = DD2D1[1]DD2D1DD22D1[10]1
[39] CNCpqCrNq = DD2D1DD2D13DD2D1DD22D1DD2D13[3]1[3]
[40] CCpqCCNNqrCpr = DD2D1[6]D2D1[10]
[41] CCCpqpp = DD2D1[13][12]
[42] CCpqCCNrpCNqr = DD2D1[24][2]
[43] CCpqCNCprq = DD2[2]D1[25]
[44] NCCpCqpNCCNrrr = DD3DD2[9]D11[13]
[45] NCCCNpppNCqCrq = DD3DD2[9]D1[13]1
[46] CCNpCqpCqp = DD2D1D2D1[13][11]
[47] CCpNpNp = DD2D1[13]DD2D1DD22D2DD2D13[3]1
[48] CCpqCCNprCNrq = DD2D1DD2[2]D1[19][2]
[49] CCNNpqNNCpq = DD2D1[10]DD2D1DD22D1[10]1
[50] CCNCpNqrCpCqr = DD2DD2D12DD2D11[2]D1[20]
[51] CpNCCCpqqNCrCsr = DD2DD2D1[20][5]D11
[52] CCpqCNqNp = DD2D1[22]D2D1[10]
[53] CCpqCNCprNCqr = D[24]DD2D1D2DD2D12DD2D13[3]1
[54] NCCpNNpNCNNqq = DD3DD2[9]D1[10][9]
[55] NCCNNppNCqNNq = DD3DD2[9]D1[9][10]
[56] CNCNNpqNCpq = D3DD2D1[10][30]
[57] CNCpNCpqq = DD2[17][25]
[58] NCCCCpqCrsCrCqsNCCtCuvCCtuCtv = DD3DD2[9]D1[29]2
[59] CCCpqrCCrpp = DD2D1DD2D1D2D1[13][6][12]
[60] CNCpNqNCqNp = D3DD2D1[10]DD2D13[30]
[61] CNCpqNCNNpq = D3DD2D1[10]DD2DD2D12DD2D13[3]D1[10]
[62] CCpqCCpNqNp = DD2D1[22]D2[20]
[63] CNCCpqNCqrCpr = DD2DD2D12[21][25]
[64] CNCCpqNCrpCrq = DD2DD2D12DD2D13[23][17]
[65] NCCCpNpNpNCqCrq = DD3DD2[9]D1[47]1
[66] CCNpqCCpqq = DD2D1DD2D1DD2D1D2D1[13][6]3D2D1[10]
[67] CCpqCCNprCNqr = DD2D1[6][52]
[68] NCCpCNpqNCCNrNCrsr = DD3DD2[9]D1[7]DD2DD2D13D2DD2D1D2[3]DD2D11[3]3
[69] CCpqCCNpqq = DD2D1D2D1[13][48]
[70] NCCCpqCNNpqNCCNNrsCrs = DD3DD2[9]D1DD2D1DD22D2DD2D13[3]1DD2D1DD22D1[10]1
[71] CCNCpqrCpCNqr = DD2DD2D12DD2D11[2]D1DD2D13DD2D1D2D1[10]DD2D1D2[9]1
[72] CCpCqrCNCpNqr = DD2DD2D12[43]D1[17]
[73] NCCCNpqCNqpNCCNrsCNsr = DD3DD2[9]D1[19][19]
[74] NCCCpqCNqNpNCCNrNsCsr = DD3DD2[9]D1[52]3
[75] CNCpNqNCCrqNCsp = D3DD2D1[10]DD2D1DD2D1DD22D111DD2D13DD2D1DD22D1DD2D13[3]DD2D13[3]
[76] CCNCpqrCCNCpNrsCNCpqs = DD2D1[6]D2DD2D13DD2D1D2[9]DD2D13[23]
[77] NCCCpqCpNCpNqNCCrNCsNtCrt = DD3DD2[9]D1D2[20]D2D1[17]
[78] NCCpNCpNpNCNCqNrr = DD3DD2[9]D1DD2DD2D1D231DD2D1D2[9]1[17]
[79] CCpCNqrCNCpqr = D[24]DD2D1[11][24]
[80] CNCpNCqrCqNCrNp = DD2D1D2DD2D13DD2D1D2D1DD2D1[10]3DD2D1DD2D1D2DD2D12DD2D13[3]1DD2D1D2[9]11
[81] NNCCpNpNCNpp = D[10]D3DDD22D2DD2D13[3]D1DD2D1DD2DD2D1D231DD2D1D2[9]1[13]
[82] NCCCpCqrCpCqNCpNrNCCsCtNCuNvCsCtv = DD3DD2[9]D1D2DD2D1[2][20]D2D1D2D1[17]
[83] NCCpNCpNCNpqNCNCrsr = DD3DD2[9]D1DD2[20][7][25]
[84] CNCCpqNCprCpNCqNr = DD2DD2D1DD2D12D2D1[20][25][17]
[85] CNCNpNNqNCCprNCqs = D3DD2D1[10]DD2D1D2D1D3DD2D1[10]DD2D13DD2D13[3]DD2D1DD22D1[3]DD2D13[3]
[86] CCpqNCCCprCpNCqNrNCCsNCtNuCsu = DD2DD2D1[20]DD2D12D2D1[20]D1D2D1[17]
[87] CpNCCqNCqNpNCNCrsr = DD2DD2D1[20][33]D1[25]
[88] NCCNNCpNNqCpqNCCrsNNCrNNs = DD3DD2[9]D1DD2D1D2D1[9][9]DD2D1[10]D2D1[10]
[89] NCCNNCpqCNNpqNCCNNrsNNCrs = DD3DD2[9]D1[30][49]
[90] CCpqCCNCNqprCNqr = DD2D1[6]DD2D1[52]DD2D1D2D1[13][2]
[91] CNCCpqNCrsNCCCtpCtqNCCurCus = DD2DD2D1[20]DD2D12DD2D13[23]DD2D12[21]
[92] NCCCNpqCCpqqNCCCrstCNrt = DD3DD2[9]D1[66][12]
[93] NCCCNCpqrCNCpqNCpNrNCCsNCtNuCsu = DD3DD2[9]D1D2DD2D13DD2D1D2[9]DD2D13[23]D2D1[17]
[94] CNCCpqNCprCpNCCsrNCtq = DD2DD2D1DD2D12D2D1DD2D1D2DD2D13DD2D1D2[9]DD2D111DD2D111[25][17]
[95] CpNCCqNCCrqNCspNCNCCptut = DD2DD2D1[20]DD2D1D2DD2D13DD2D1D2[9]DD2D111DD2D111DD2D1D2[25]1
[96] CNCCpqNCrsNCCCstCrtNCCquCpu = DD2DD2D1[20]DD2D1D2[2][21]DD2D1D2[2]DD2D13[23]
[97] CCCCCpqCNrNsrtCCtpCsp = DD2D1D2DD2D1DD2D1D2D3DD2[3]DD2D1DD2D111D3DD2D1[10]DD2D1[6]DD2D1[11]DD2D1D2D2D13DD2D11[3]211
[98] CCNCpNqrCNCpNNrNq = DD2D1DD2D13D2DD2D1DD2D1D2D1DD2D1[10]D2D1[10]DD2D1[6]D2[20]DD2D13[3]1
[99] CNNCCpqNCrNCrNsNCCNCtNuuNCsp = DD2D1D3DD2[9]D1[17]DD2D1DD2[2]D1[33]DD2D13DD2D1DD22D1[3]DD2D13[3]
[100] CCpqCCNCNpqrCNqr = DD2D1[6]DD2D1D2DD2D1D2DD2D13DD2D1D2D1[10]DD2D1D2[9]11[52]
[101] NCCNCCpqNCpNqNpNCNrNCCrsNCrt = DD3DD2[9]D1D3DD2D1[10]DD2D1D2D2[20]DD2D13[3]DD2DD2D1[20][3][3]
[102] NCCNCpqNCNNpqNCNCNNrsNCrs = DD3DD2[9]D1[61][56]
[103] NCCNNCpNNqCNNpqNCCNNrsNNCrNNs = DD3DD2[9]D1DD2D13DD2D13DD2D1DD22D2DD2D13DD2D13DD2D13[3]DD2D13[3]DD2D1[10]DD2D13DD2D13D2D1D3DD2DD2D13DD2D13DD2D13[3]1
[104] NCCpCNNCpqNCpNqNCCNNCrsNCrtr = DD3DD2[9]D1DD2D1DD2D1DD22D2DD2D13[3]1DD2D1D2D2[20]1D3DD2DD2D13DD2D1D2DD2D13[9]DD2D11[3][3]
[105] NCCCNNCpqrCNprNCCNstCNNCstt = DD3DD2[9]D1DD2[2]D1DD2D1[10][3]DD2D1DD2D1DD2D1D2D1[13]DD2D1D2DD2D12DD2D13[3]13D2D1[10]
[106] CNCCpqNCrqCCNprq = DD2D1D2D1[13]DD2DD2D12DD2D11DD2D12DD2D13[23]DD2D1[24]DD2D12[21]
[107] CNNCCpqNCrsNCCsNqNCNrp = DD2DD2D1[20]DD2D1DD2D1DD22D111DD2D13DD2D1DD22D1DD2D13[3]DD2D13[3]DD2D1DD22D1[3]DD2D11DD2D13DD2D1DD22D1[3]DD2D13[3]
[108] NCCpNCCNpqNCNprNCNCCNstNCNsNts = DD3DD2[9]D1DD2DD2D1[20][7][7]D3DD2D1[10]DD2D1D2D2[20]1
[109] NCCNCpNqNCqNpNCNCrNsNCsNr = DD3DD2[9]D1[60][60]
[110] NCCCNCpNqrCpCqrNCCsCtuCNCsNtu = DD3DD2[9]D1[50][72]
[111] CNNCCCNpqpNCrCNrsNCCtqNCuCvu = DD2DD2D1[20]DDD22D2DD2D13[3]D1D3DD2DD2D1[20]DD2D1D2DD2D13D2D1DD2D1[10]11D1[7]D11
[112] NCCNCpNNqNCpqNCNCrsNCrNNs = DD3DD2[9]D1D3DD2D1[10]DD2D1D2D1[10][9]D3DD2D1[10]DD2D1D2D1[9][9]
[113] NCCNCpqNCpNNqNCNCrNNsNCrs = DD3DD2[9]D1D3DD2D1[10]DD2D1D2D1[9][9]D3DD2D1[10]DD2D1D2D1[10][9]
[114] CNCCpqNCrsCCNprCNqs = DD2DD2D12DD2D11DD2D12[21]DD2D1[6]D[24]DD2D1DD22D2DD2D13[3]DD2D13[23]
[115] NCCCNCpqCprCpCNqrNCCsCNtuCNCvtCsu = DD3DD2[9]D1DD2D1DD22D11DD2D1D2D12[71]DD2D1DD2[2]D1[39]2
[116] NCCCpqNCCrCsrNCCNpqqNCNCtNCCNuvwCuw = DD3DD2[9]D1DD2D1D3DD2[9]D11[69]DD2DD2D12[21]D1[7]
[117] NCCNCCpqNCNpqqNCrNCCsrNCtr = DD3DD2[9]D1DD2D1[13]DD2DD2D12DD2D13[23]D[24][17]DD2DD2D13DD2D1D2[9]DD2D1111
[118] CNCCpqNCrsCNCpNrNCqNs = DD2DD2D1DD2D12D2D1[20]DD2DD2D12DD2D13[23]D1[25]DD2DD2D12[21]D1[17]
[119] NCCCNCpqrCpCNqrNCCsCNtuCNCstu = DD3DD2[9]D1[71][79]
[120] NCCCpqNCCpNCpNqNCNCrsrNCNCCtNCuNvwCtv = DD3DD2[9]D1DD2D1DD2[20]D1[25]D2[20]DD2D1D2D1[17][25]
[121] NCCCNCpNqrCNCqrNpNCCNCstNuCNCuNst = DD3DD2[9]D1D[24]DD2DD2D12DD2D11[2]D1DD2D13DD2D1D2[9]DD2D13[3]DD2D1DD22D1[17]DD2D13D2D1DD2D1[10][3]
[122] NCCNCpNNqNCNNpqNCNCNNrsNCrNNs = DD3DD2[9]D1D3DD2D1[10]DD2D1DD2D13DD2D13D2D1D3DD2DD2D13DD2D13DD2D13[3]1[9]D3DD2D1DD2D1[10]3DD2D13DD2D1DD22D2DD2D13DD2D13DD2D13[3]DD2D13[3]
[123] CNCCpqNCrsNCCNCptNCqtNCNCruNCsu = D3DD2D1[10]DD2D1D2D1D3DD2D1[10]D[24]DD2D1D2DD2D12DD2D13[3]DD2D13[3]DD2DD2D12DD2D13[3]D1[53]
[124] NCCNCCNpqNNqNCpNNqNCNCrsNCCNrts = DD3DD2[9]D1D3DD2D1[10]DD2D1DD2D1D2D1[13]DD2DD2D12DD2D11[2]D1DD2D13D2D1D3DD2DD2D13DD2D13DD2D13[3]1[9]D3DD2D1[10]DD2D1DD22D1[7]DD2D13[3]
[125] NCCNCCpqNCprCpNCqNrNCCsNCtNuNCCstNCsu = DD3DD2[9]D1[84]DD2DD2D1[20]D2D1[25]D2D1[17]
[126] NCCCpNCqNrNCCpqNCprNCNCCstNCsuCsNCtNu = DD3DD2[9]D1DD2DD2D1[20]D2D1[25]D2D1[17][84]
[127] CCpNqNCCNCCNrpNqNCrNqNCNCstNCCNsut = DD2DD2D1[20]DD2DD2D1DD2D12D2D1[20]D[24]DD2D1DD22D11DD2D11DD2D12[2]D1[17]D1D3DD2D1[10]DD2DD2D12DD2D13[3]D1[7]
[128] CNCCpqNCrsNCCCNptCNqtNCCNruCNsu = D3DD2D1[10]DD2D1D2D1D3DD2D1[10]DD2D1[6]D[24][30]DD2DD2D12DD2D13[3]D1[67]
[129] NCCNCpNNCCpqrNCqNNCCpqrNCNCsNNCtNCsuNCuNNCtNCsu = DD3DD2[9]D1DD2DD2D13DD2DD2D12DD2D11[3]DD2D1DD2D1D2DD2D12DD2D13[3]1D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]11[3]1DD2DD2D13DD2DD2D12DD2D11[3]DD2D1DD2D1D2DD2D12DD2D13[3]1D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]1111
[130] NCCCNCpqCrqCNCpNrqNCCNCsNtuCNCsvCtu = DD3DD2[9]D3DD2[3]DD2D11DD2D1[43]D3DD2D1[10]DD2D1D2D2D1[36]1DD2DD2D12DD2D11[2]D1DD2D13DD2D1D2[9]DD2D13[23]
[131] NCCCNCpNqrCNCpNNrNqNCCNCsNNtuCNCsut = DD3DD2[9]D1[98]D[24]DD2DD2D12DD2D11[2]D1[33]
[132] NCCNCCpqNCrqCCNprqNCCCNstuNCCsuNCtu = DD3DD2[9]D1[106]DD2DD2D1[20][18]DD2D1DD22D111
[133] CNCNCCpqNCrsNNCCqtNCurNCCptNCus = DD2DD2D1[20]DD2DD2D1[2]D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]11[3]D3DD2D1DD2D1[10][7][3]DD2DD2D12DD2D13DD2DD2D12DD2D11[3]D1DD2D1D2[3]DD2D111D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]111
[134] NCCNCCNpqNNNrNCrNCNqpNCNCsNCNtuNCCNutNNNs = DD3DD2[9]D1D3DD2D1[10]DD2D1DD2[2]D1[19]DD2D13DD2D1DD22D2DD2D13DD2D13DD2D13[3]DD2D13[3]D3DD2D1DD2D1[10]3DD2D1D2D1[9]DD2DD2D12DD2D13[3]D1DD2D13DD2D1D2D1[10][9]
[135] NCCNCpNCqrNCpNCNCsNqrNCNCtNCNCtNuvNCtNCuv = DD3DD2[9]D1DD2DD2D13DD2D1D2[9]DD2D13[23]DD2DD2D12[21]D1[17]D3DD2D1[10]DDD22D2DD2D13[3]D1D2D[24]DD2D1DD2D1D2DD2D12DD2D13[3]1[20]
[136] NCCNCNCpNqrNCpNNCqrNCNCsNNCtuNCNCsNtu = DD3DD2[9]D1D3DD2D1[10]DD2D1DD2D1[72]D2D1[9][9]D3DD2D1[10]DD2D1DD2D1D2D1[10][50][9]
[137] CNCCpqNNCCrCstNCCupvNCCNCrNstNCpNCvNq = DD2DD2D1[20]DD2D1[72]D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]11[3]DD2DD2D1DD2D12D2D1[20]DD2D1DD2D1DD22D111D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]111[25]
[138] NNCNCCpqNCqpNNCCpNqNCNqp = D[10]DD2D1[10]DD2DD2D1DD2D12D2D1DD2D13DD2D1D2D1[10]DD2D1D2[9]1DD2D1D2D1[47]DD2D1D2[2][21]DD2D1[62][25]
[139] NCCNNCCpqNCrsCNNCpNNqNCrNNsNCCNNCtNNuNCvNNwNNCCtuNCvw = DD3DD2[9]D1DD2D1D2D1D3DD2D1[10]DD2D1D2D1[9][9]DD2DD2D12DD2D13[3]D1DD2D1D2D1[9][9]DD2D1[10]DD2D1D2D1D3DD2D1[10]DD2D1D2D1[10][9]DD2[2]D1DD2D1[10]D2D1[10]
[140] NCCCpNCCqrNCstNCCCpqCprNCCpsCptNCNCCCuvCwxNCCyzCwaCwNCCvxNCza = DD3DD2[9]D1DD2DD2D1[20]DD2D12D2D1[25]DD2D12D2D1[17]DD2DD2D1DD2D12D2D1[20]DD2D1[11]DD2D1DD22D11DD2D13[23]DD2D1[11]DD2DD2D12[21]D11
[141] NCCNCpNCqrCNNCpqNCpNrNCCNNCstNCsNuNCsNCtu = DD3DD2[9]D1DD2D1D2DD2D1[52]DD2D1DD2D12D2D1DD2D13DD2D1D2D1[10]DD2D1D2[9]1[9]1D3DD2D1DD2DD2D1DD2D1D2DD2D13DD2D1D2DD2D13[9]11D2D1[25]D2D1[31][9]
[142] NCCNCCpNqNCNrsNCCqNpNCNsrNCNCCtNuNCNvwNCCuNtNCNwv = DD3DD2[9]D1DD2DD2D1[20]DD2D13DD2D1DD22D2DD2D13[3]DD2D13[23]D[24][17]DD2DD2D1[20]DD2D13DD2D1DD22D2DD2D13[3]DD2D13[23]D[24][17]
[143] NCCNCCpqNCrsNCCNsNrNCNqNpNCNCCNtNuNCNvNwNCCwvNCut = DD3DD2[9]D1DD2DD2D1[20]D[24]DD2D1DD22D2DD2D13[3][21]D[24]DD2D1DD22D2DD2D13[3]DD2D13[23]DD2DD2D1[20]DD2D13[17]DD2D13[25]
[144] NCNCNCCCNCpNqrCpCqrNCCsCtuCNCsNtuNNCCCvCwxCwCvxNCCyCzaCzCyaNNCCCbCcdCNCbNcdNCCNCeNfgCeCfg = DD3DD2[9]D1DD3DD2[9]D1[110]DD3DD2[9]D1[11][11]DD3DD2[9]D1[72][50]
[145] CNCNCCpqNCrsNNCCtuNCvwNCCCNptCNquNCCNrvCNsw = DD2DD2D13DD2D1D2[9]DD2D11DD2DD2D12DD2D11DD2D1[2]D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]11[3]DD2D1D2[2]DD2D11DD2D1[52]D3DD2D1DD2D1[10][7][3]DD2DD2D12DD2D11DD2D1[2]D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]111DD2D1[6]D[24]DD2D1DD22D2DD2D13[3]DD2D13DD2DD2D12DD2D11[3]D1DD2D1D2[3]DD2D111
[146] CNCCpqNCrsNCCNCCstNCupNCCrtNCuqNCNCCqvNCwrNCCpvNCws = DD2DD2D1[20]DD2DD2D1DD2D12D2D1[20]DD2D1D2DD2D12DD2D13[23][21]DD2DD2D12DD2D11DD2D12DD2D13[23]D1[17]DD2DD2D1DD2D12D2D1[20]DD2D1D2DD2D12DD2D13[23]DD2D13[23]DD2DD2D12DD2D11DD2D12[21]D1[17]
[147] NCCNCCpqNCqpNNCCpNqNCNqpNCNNCCrNsNCNtuNCCusNCtr = DD3DD2[9]D1DD2D1[10]DD2DD2D1DD2D12D2D1DD2D13DD2D1D2D1[10]DD2D1D2[9]1DD2D1D2D1[47]DD2D1D2[2][21]DD2D1[62][25]DD2D1DD2DD2D1[20]DD2D1DD22D11DD2D11DD2D13DD2D1DD22D111DD2D1[18]DD2D13[12][9]
[148] NCCNCCpqNCqpCNNCpNqNCNpNNqNCCNNCrNsNCNtNNuNCCtsNCur = DD3DD2[9]D1DD2D1DD2D1DD22D2DD2D13[3]1DD2DD2D1DD2D12D2D1[20]DD2D1[62][25]DD2D1D2D1[47]DD2D1D2[2][21]DD2D1DD2DD2D1[20]DD2D1[18]DD2D13DD2D1DD22D111DD2D1DD2D13[12]D2D1[17]DD2D1DD22D1[10]1
[149] CNCNCCpqNCrsNNCCtuNCvwNCCNCpNtNCqNuNCNCrNvNCsNw = DD2DD2D1[20]DD2DD2D1DD2D12D2D1[20]DD2D1[43]D3DD2D1DD2D1[10][7][3]DD2DD2D1[2]D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]11[3]D1[17]DD2DD2D1DD2D12D2D1[20]DD2DD2D12DD2D13DD2DD2D12DD2D11[3]D1DD2D1D2[3]DD2D111D1[25]DD2D1[36]D3DD2D1D3D3DD2D1D3DD2DD2D13DD2D13DD2D13[3]111
[150] NCCNCNNCpNqNCNpNNqCNNCpNNqNCqNNpNCCNNCrNsNCtNNuNCNNCusNCNrNNt = DD3DD2[9]D1DD2DD2D1[2]DD2DD2D1DD2D12D2D1[20]DD2D1DD2D1DD2D1D2D1[13][6]3[17]DD2D1DD2D1D2D1DD23D11DD2D1D2D1DD2D1DD22D2DD2D13[3]1DD2D12D2D1[3]D3DD2D1[10][7]D1DD2D1D2D1[9][9]DD2D1DD2DD2D1DD2D1D2DD2D13DD2D1D2DD2D13[9]11DD2D13DD2D1D2D1[17]DD2D1DD22D111DD2D1D2D1D3DD2D1[10]DD2D13DD2D13[3][12]DD2D1DD22D1[10]1
[151] NCCCCNCNpqrsNCNCCpsNCqsNCrsNCNCNCCtuNCvuNCwuCCNCNtvwu = DD3DD2[9]D1DD2DD2D1[20]DD2D1DD2DD2D1[20][18]DD2D1DD22D111[18]DD2D1DD22D111DD2D1D2D1[13]DD2DD2D12DD2D11DD2D12[21]DD2D1[6]DD2D1DD2D1[52][106][25]
[152] NCCNCCCNpqCNrsNCCNtuCNvsCNsNCCprNCtvNCCNwNCCxyNCzaNCCCNxwCNywNCCNzwCNaw = DD3DD2[9]D1DD2DD2D1DD2D12D2D1[20]DD2D1[11]DD2D1[24]DD2D1DD22D1[7]DD2D13[23]DD2D1[11]DD2D1[24]DD2DD2D12[21]D1[7]DD2DD2D1[20]DD2D1DD2D1DD2D1DD2[2]D1[19][24]2D2D1[25]DD2D1DD2D1DD2D1DD2[2]D1[19][24]2D2D1[17]
[153] NCCCpNCCqrNCstNCCNCpNqNCpNrNCNCpNsNCpNtNCNCCNCuNvNCwNxNCNCuNyNCzNaCuNCCvxNCya = DD3DD2[9]D1DD2DD2D1[20]DD2D1[52]DD2D12D2D1D[24]DD2D1DD22D2DD2D13[3]DD2D13[23]DD2D1[52]DD2D12D2D1D[24]DD2D1DD22D2DD2D13[3][21]DD2DD2D1DD2D12D2D1[20]DD2D1D2D13DD2D1[29]DD2D13[25]DD2D1D2D13DD2D1[29]DD2D13[17]
[154] NCCNCCNCCpqNCrstNCuNCCsvNCrpNCCsNCCqtNCuvNCNCCruNCtrpNCNCCwNCCxyNCzaNCNCCxzNCybcNCCNCCcxNCxwyNCzNCCwaNCbc = DD3DD2[9]D1DD2DD2D1[20]DD2DD2D12DD2D1D2D1[20]DD2DD2D12DD2D11DD2D12DD2D13[23]D1DD2D1D2DD2D13DD2D1D2[9]DD2D111DD2D111DD2DD2D12DD2D11DD2D12DD2D1D2D1[25][17]D11DD2D1D2D1DD2DD2D1[66]DD2D1DD22D1[3]DD2D1D2D1DD2D13[12]D[24][17]DD2D1[1]DD2D1D2D1[17][25]DD2DD2D12DD2D1D2D1[20]DD2DD2D12DD2D11DD2D12[21]D1[25]DD2D1D2DD2D12[21]DD2D13[23]DD2DD2D1[20]DD2D1D2D1DD2DD2D1[59]DD2D13DD2D1DD22D1[3]D[24][25]DD2D1D2DD2D1D2[25]1[17]DD2DD2D1DD2D12D2D1[20]DD2D1D2DD2D12DD2D13[23][21]DD2DD2D12DD2D11DD2D12DD2D13[23]D1[17]DD2DD2D1DD2D12D2D1[20]DD2DD2D12DD2D11DD2D12DD2D1D2D1[17][25]D11DD2DD2D12DD2D11DD2D12[21]D1DD2D1DD2D1DD22D111DD2D13DD2D1D2[9]DD2D111