I have just released pmGenerator 1.2
<https://github.com/xamidi/pmGenerator/releases/tag/1.2.0>, which is
capable of building and iterating condensed detachment proofs for
user-definable sets of axioms. The only rules of inference currently
supported, however, are *modus ponens* and *necessitation*. The latter
allows to explore proof systems in modal logic, such as S5.
Consequently, the tool can now assist in research exploring any Hilbert
systems with modus ponens and/or necessitation, not limited to classical
logic.
Metamath's propositional axioms
<https://us.metamath.org/mpeuni/mmset.html#scaxioms> are still the default.
Different systems (e.g. Łukasiewicz' first system: {L1:(p→q)→((q→r)→(p→r)),
L2:(¬p→p)→p, L3:p→(¬p→q)}) can now be addressed as simple as
$ ./pmGenerator -c -n -s CCpqCCqrCpr,CCNppp,CpCNpq [do whatever with L1-L3
as axioms]
using formulas in Polish notation (here: "normal" Polish notation via '-n').
Necessitation can be enabled by '-N <consequtive limit>', e.g.
$ ./pmGenerator -c -n -N -1 -s
CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp
addresses a full axiomatization of S5 in terms of {¬,→,□}, which extends on
our default axioms.
But what I mostly worked on are quality of life features to find, display
and handle these proofs, for example to convert them into formula-based or
abstract summary representations, and to actually find meaningful proofs,
such as these: s5proofs.txt
<https://xamidi.github.io/pmGenerator/data/s5proofs.txt> (abstract proof
summary: s5.txt <https://xamidi.github.io/pmGenerator/data/s5.txt>)
For illustration, I created an abstract proof summary of the whole
pmproofs.txt <https://us.metamath.org/mmsolitaire/pmproofs.txt> database of
Metamath's mmsolitaire <https://us.metamath.org/mmsolitaire/mms.html>
project, and documented on how this can be done: pmproofs-summary.txt (online
version <https://pastebin.com/NjTx1E7c>)
Comments excluded it is only 12059 bytes in size, and with pmGenerator's
new features it could probably be used as a resource to further tackle
Metamath's "shortest known proofs" challenge.
I left that challenge behind for almost a year now. Instead I created a new
proof minimization challenge that concerns minimal single axioms and
includes even some proofs that are yet to be found!
You may have a look <https://github.com/xamidi/pmGenerator/discussions/2>.
As usual, if you find any bugs, please report them to my issue tracker
<https://github.com/xamidi/pmGenerator/issues>. (Not a single bug has been
reported so far!)
I would be happy to receive some feedback.
— Samiro Discher
--
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/c65b0722-bf5f-46ec-9c9c-c978513b90b0n%40googlegroups.com.
% Full summary: pmGenerator --transform data/pmproofs-summary.txt -f -n -t
. -j 1
% - infix formulas: pmGenerator --transform data/pmproofs-summary.txt -f -n -t
. -j 1 -u
% - to file: pmGenerator --transform data/pmproofs-summary.txt -f -n -t
. -j 1 -u -o data/tmp.txt
% Current summary:
% - step counting: pmGenerator --transform data/pmproofs-summary.txt -f -n -t
. -j -1 -p -2 -d
% - infix formulas: pmGenerator --transform data/pmproofs-summary.txt -f -n -t
. -j -1 -u
% Steps to generate this file in Bash via pmGenerator 1.2 and its released
(quick'n'dirty) helper tools:
% 1. Write all D-proofs from 'data/pmproofs.txt' (version 17-Apr-2023) to
'data/tmp.txt', but without duplicates and trivial proofs (i.e. of length 1):
% $ ./dProofsFromDB data/pmproofs.txt data/tmp.txt 1 1
% 2. Combine proofs in 'data/tmp.txt' to an abstract proof summary (based on
default axioms, which are CpCqp,CCpCqrCCpqCpr,CCNpNqCqp).
% $ ./pmGenerator --parse data/tmp.txt -f -n -s -o data/pmproofs-summary.txt
%
% The below steps are optional, but used to reduce the abstract proof summary
size from 14569 bytes to 12059 bytes,
% while still containing all 154 (non-trivial) proof results from pmproofs.txt
of its current 196 theorems.
%
% 3. Obtain conclusions for all proofs in 'data/tmp.txt' via 'pmGenerator
--parse data/tmp.txt -f -n -b',
% and reformat them to be in a single comma-separated line, e.g. via:
% $ ./pmGenerator --parse data/tmp.txt -f -n -b | sed -E 's/[0-9]+\. /,/g' |
sed -E 's/^[^,].+//g' | sed -E 's/,printProofs.+//g' | tr -d '\r' | tr -d '\n'
% Output: ",<L>", for <L> being the list of all 154 proof results from
pmproofs.txt in normal Polish notation
% (Not to be confused with ' ./formulasFromProofs
CpCqp,CCpCqrCCpqCpr,CCNpNqCqp data/tmp.txt <output file>', which would generate
a line with all used formulas, not only final conclusions.)
% 4. Find extra conclusions necessary to reach a compact abstract proof summary:
% $ ./findCompactSummary data/pmproofs-summary.txt <L>
% Output mentions "<E>" as 'bestDedicatedConclusions' in the final iteration
after a few minutes.
% 5. Transform abstract proof summary to compact variant.
% $ ./pmGenerator --transform data/pmproofs-summary.txt -f -n -t <L> -j -1
-s <E> -d -o data/pmproofs-summary.txt
% (total command length: 4153 bytes)
%
% NOTE: <L> =
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,NCCCNCpNqrCNCqrNpNCCNCsNtNuCNCuNsNt,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
% <E> =
CCpqCpCrq,CCpCqCrsCpCCqrCqs,CCpCNqNrCpCrq,CCpCqCCrqsCpCqs,CNNpCqp,CCpCqrCpCCrsCqs,CCNNCpqpCNNCpqq,CpCCqNNrCqr,CCpqCpNNq,CCpCqCrsCpCrCqs,CCpqCNNpq,CCpCqrCpCqNNr,CCpCqCNrrCpCqr,CCpNCqNrCpr,CCNNpqCpq,CCpqCpNNNNq,CCpqCpCrNCqNr,CCpNCqrCpq,CCCNpqrCCNqpr,CCpCqrCpCCqsCqNCrNs,CNCCpqrCCspCsq,CpCqNCCrqNCsp,CCpCqrCpCNrNq,CNCpqNCpNNq,CCpCqrCpCCqNsCqNCrs,CNCCpqNCrsCNCCstNCupNCCrtNCuq,CNCCpqNCqpNNCCpNqNCNqp
CpCqp = 1
CCpCqrCCpqCpr = 2
CCNpNqCqp = 3
[0] CCpqCpCrq = D2D11
[1] CCpCqCrsCpCCqrCqs = D2D12
[2] CCpCNqNrCpCrq = D2D13
[3] Cpp = DD211
[4] CCpCpqCpq = DD22D21
[5] CCpqCCrpCrq = D[1]1
[6] CNpCpq = D[2]1
[7] CCpqCCpCqrCpr = DD2D1D221
[8] CCpCqCCrqsCpCqs = D2D1DD22D11
[9] CNNpCqp = D[2][6]
[10] CpCCpqq = DD2D1D2[3]1
[11] CCpqCCqrCpr = DD2D1D2[5]1
[12] CpCNpq = DD2D1D2[6]1
[13] CCpCqrCCspCCsqCsr = DD2D1[1][5]
[14] CNNpp = DD2[9]1
[15] CCpCqrCpCCrsCqs = D2D1[11]
[16] CCNNCpqpCNNCpqq = D2[14]
[17] CpNNp = D3[14]
[18] CCpCqrCqCpr = D[8]D[0]2
[19] CCCpqrCNpr = DD2D1DD22D1[6]1
[20] CCNppp = DD2D[2]D2[6]1
[21] CpCCqNNrCqr = D1D2D1[14]
[22] CCpqCpNNq = D2D1[17]
[23] CCpCqCrsCpCrCqs = D2D1[18]
[24] CCpCqrCCpCrsCpCqs = D[1][15]
[25] CNNpCCpqq = DD2D1D2[3][9]
[26] CNCpqCqr = D[8]D[0][6]
[27] CCpqCNNpq = DD2D1DD22D2[9]1
[28] CCpCqrCpCqNNr = D2D1[22]
[29] CCpCqCNrrCpCqr = D2D1D2D1[20]
[30] CNCpNqq = D3D[22]1
[31] CCCNpqrCpr = DD2D1DD22D1[12]1
[32] CCNpqCNqp = D[2][22]
[33] CCpNCqNrCpr = D2D1[30]
[34] CpCqNCpNq = D[2]DD2D1[16]1
[35] CNCpNqCrq = D[2][26]
[36] CCpNqCqNp = D[2][27]
[37] CCNNpqCpq = DD2D1DD22D1[17]1
[38] CNCpqCNpr = DD2D1DD22D1[6]D[0][6]
[39] CCpCNqrCpCNrq = D2D1[32]
[40] CNCpqp = D3D[22][6]
[41] NCCCpCpqCpqNCrCsr = DD3D[16]D1[4]1
[42] CCpqCpNNNNq = D2D1D3DD2D[2]D[2][9]1
[43] CCpqCpCrNCqNr = D2D1[34]
[44] CNpCCNqpq = DD2D1D2D1DD23D11D[1]D[0][6]
[45] NCCppNCqq = DD3D[16]D1[3][3]
[46] CCpNCqrCpq = D2D1[40]
[47] CCCpqCrsCrCqs = D[8]D[0]D[1]D[8]1
[48] CNNCpqCNNpq = DD2D1DD22D2[9][9]
[49] CNCpqNq = D3D[22][9]
[50] CCNpqCCNpNqp = D[2]D2[34]
[51] CpCqNCqNp = DD2D1D2[34]1
[52] CCpqCNCrNpq = DD2[5]D1[30]
[53] NNCpNNp = D[17][17]
[54] CCCNpqrCCNqpr = DD2[5]D1[32]
[55] CpNCCqCrqNCCpss = DD2D1D3D[16]D11[10]
[56] CCNNpCpqCpq = DD2D1[4][37]
[57] CNCpqCrNq = DD2D1D[2]DD2D1DD22D1[9]1[6]
[58] CCpqCCNNqrCpr = D[15][22]
[59] CCCpqpp = DD2D1[20][19]
[60] CCpCqrCpCCqsCqNCrNs = D2D1D[1][43]
[61] CCpqCCNrpCNqr = DD2D1[39][5]
[62] CNCCpqrCCspCsq = DD2D1[5][40]
[63] CCpqCNCprq = DD2[5]D1[40]
[64] NCCpCqpNCCNrrr = DD3D[16]D11[20]
[65] NCCCNpppNCqCrq = DD3D[16]D1[20]1
[66] CCNpCqpCqp = D[29][18]
[67] CCpNpNp = DD2D1[20][27]
[68] CpCqNCCrqNCsp = DD2D1D2D[2]DD2D1[16]D[0]1D[0]1
[69] CCpqCCNprCNrq = DD2D1[54][5]
[70] CCNNpqNNCpq = D[22][37]
[71] CpNCCCpqqNCrCsr = DD2D[43][10]D11
[72] CCNCpNqrCpCqr = DD2D1D2D[15][34]1
[73] CCpqCNqNp = DD2D1[36][22]
[74] CCpqCNCprNCqr = D[39]DD2D1D2D[1][9]1
[75] NCCpNNpNCNNqq = DD3D[16]D1[17][14]
[76] NCCNNppNCqNNq = DD3D[16]D1[14][17]
[77] CCpCqrCpCNrNq = D2D1[73]
[78] CNCNNpqNCpq = D3D[22][48]
[79] CNCpNCpqq = DD2[30][40]
[80] NCCCCpqCrsCrCqsNCCtCuvCCtuCtv = DD3D[16]D1[47]2
[81] CCCpqrCCrpp = DD2D1D[29][11][19]
[82] CNCpNqNCqNp = D3D[22]D[2][48]
[83] CNCpqNCpNNq = D3D[22]DD2[21][14]
[84] CNCpqNCNNpq = D3D[22]DD2D[1][9]D1[17]
[85] CCpqCCpNqNp = DD2D1[36]D2[34]
[86] CCpCqrCpCCqNsCqNCrs = D2D1D[1]D2D1D[2]D[28]DD2D1[16]1
[87] NCCCpNpNpNCqCrq = DD3D[16]D1[67]1
[88] CCNpqCCpqq = DD2D1DD2D1D[29][11]3[22]
[89] CCpqCCNprCNqr = D[15][73]
[90] NCCpCNpqNCCNrNCrsr = DD3D[16]D1[12]DD2D[2]D2DD2D1D2[6]D[0][6]3
[91] CCpqCCNpqq = D[29][69]
[92] NCCCpqCNNpqNCCNNrsCrs = DD3D[16]D1[27][37]
[93] CCpCqrCNCpNqr = DD2D[1][63]D1[30]
[94] NCCCNpqCNqpNCCNrsCNsr = DD3D[16]D1[32][32]
[95] NCCCpqCNqNpNCCNrNsCsr = DD3D[16]D1[73]3
[96] NCCCpqCpNCpNqNCCrNCsNtCrt = DD3D[16]D1D2[34][33]
[97] NCCpNCpNpNCNCqNrr = DD3D[16]D1DD2DD2D1D231DD2D1[16]1[30]
[98] CCNCpqrCpCNqr = DD2D1[39]D[23][32]
[99] CCpCNqrCNCpqr = D[39]D[23][39]
[100] CCNCpqrCCNCpNrsCNCpqs = D[15]D2D[43][40]
[101] CNCCpqNCqrCpr = D3D[22]DD2D1D2[74]1
[102] CNCCpqNCrpCrq = D3D[22]DD2D1D2D[77][5]1
[103] NCCCpCqrCpCqNCpNrNCCsCtNCuNvCsCtv = DD3D[16]D1D2DD2D1[5][34]D2D1[33]
[104] CNCpNqNCCrqNCsp = DD2D[43][35]D[2][38]
[105] NCCpNCpNCNpqNCNCrsr = DD3D[16]D1DD2[34][12][40]
[106] CNCpNCqrCqNCrNp = DD2D1D2D[2]D[28]DD2D1[2]DD2D1DD2D1D2D[1][9]1DD2D1[16]11
[107] CCpqNCCCprCpNCqNrNCCsNCtNuCsu = DD2D[43]D[1][43]D1[33]
[108] CpNCCqNCqNpNCNCrsr = DD2D[43][51]D1[40]
[109] CNCNpNNqNCCprNCqs = DD2D[43]DD2D[1]D[0][6]D1[12]D[2][35]
[110] NCCNNCpNNqCpqNCCrsNNCrNNs = DD3D[16]D1DD2[21][14]D[22][22]
[111] CNCCpqNCprCpNCqNr = DD2D[1]DD2D1[2]DD2D1D2D1[16]DD2D1[0][40][30]
[112] NCCNNCpqCNNpqNCCNNrsNNCrs = DD3D[16]D1[48][70]
[113] CCpqCCNCNqprCNqr = D[15]D[77]D[29][5]
[114] CNCCpqNCrsNCCCtpCtqNCCurCus = DD2D[43][62]D[1][35]
[115] NCCCNpqCCpqqNCCCrstCNrt = DD3D[16]D1[88][19]
[116] NNCCpNpNCNpp = D[17]DD2D1DD2DD2D1D[2]D2DD2D1D2[6][14]11[67]
[117] NCCCNCpqrCNCpqNCpNrNCCsNCtNuCsu = DD3D[16]D1D2D[43][40][33]
[118] CpNCCqNCCrqNCspNCNCCptut = DD2D[43][68]DD2D1D2[40]1
[119] CNCCpqNCrsNCCCstCrtNCCquCpu = DD2D[43]DD2D1D2[5][35]DD2D1D2[5]D[2][38]
[120] CCCCCpqCNrNsrtCCtpCsp =
DD2D1D2DD2D1DD2D1D2D3DD2[6]DD2D1D[0]1D3D[22]D[15]D[23]DD2D1D2[2]D[0][6]211
[121] CCNCpNqrCNCpNNrNq = DD2D1D[2]D2DD2D1DD2D1D2D1D[22][22]D[15]D2[34][9]1
[122] NCCNCpqNCNNpqNCNCNNrsNCrs = DD3D[16]D1[84][78]
[123] CNCCpqNCprCpNCCsrNCtq = D3D[22]DD2D1D2D[77]D[1]D2D1[68]1
[124] NCCpNCCNpqNCNprNCNCCNstNCNsNts =
DD3D[16]D1DD2D[43][12][12]D3D[22]DD2D1D2D2[34]1
[125] NCCNCpNqNCqNpNCNCrNsNCsNr = DD3D[16]D1[82][82]
[126] CCpqCCNCNpqrCNqr = D[15]D[77][91]
[127] NCCNCpNNqNCpqNCNCrsNCrNNs = DD3D[16]D1D3D[22]D[28][14][83]
[128] NCCNCpqNCpNNqNCNCrNNsNCrs = DD3D[16]D1[83]D3D[22]D[28][14]
[129] NCCpCNNCpqNCpNqNCCNNCrsNCrtr =
DD3D[16]D1DD2D1[27]DD2D1D2D2[34]1D3DD2DD2D1DD2D1D2D[2]DD2D1D2D[2][14]11[6][6]
[130] CNNCCCNpqpNCrCNrsNCCtqNCuCvu =
DD2D[43]D3D[22]DD2D[43]DD2D1D2D[2]D2D1D[22]11D1[12]D11
[131] NCCCNCpNqrCpCqrNCCsCtuCNCsNtu = DD3D[16]D1[72][93]
[132] NCCCNNCpqrCNprNCCNstCNNCstt =
DD3D[16]D1DD2[5]D1D[22][6]DD2D1DD2D1DD2D1D2DD2D1D[29][5][14]13[22]
[133] NCCNNCpNNqCNNpqNCCNNrsNNCrNNs =
DD3D[16]D1DD2D1DD2[21][27][14]D[22]D[2]D[2][42]
[134] NCCNCCpqNCpNqNpNCNrNCCrsNCrt =
DD3D[16]D1D3D[22]DD2D1D2DD2D1[27]D2[34]1DD2D[43][6][6]
[135] CNCCpqNCrqCCNprq =
DD2D[1]DD2D1[2]DD2D1D2D1D2[6]DD2D[1]D[0][62]DD2D1[2]DD2D1[28]D[1][35]D1D11
[136] NCCCpqNCCrCsrNCCNpqqNCNCtNCCNuvwCuw =
DD3D[16]D1DD2D1D3D[16]D11[91]DD2D1[31][30]
[137] NCCCpqNCCpNCpNqNCNCrsrNCNCCtNCuNvwCtv =
DD3D[16]D1DD2D1DD2[34]D1[40]D2[34]DD2D1[33][40]
[138] CNCCpqNCrsCNCpNrNCqNs = DD2D[60]DD2D1[63][40]DD2D1[52][30]
[139] NCCCNCpqrCpCNqrNCCsCNtuCNCstu = DD3D[16]D1[98][99]
[140] NCCNCpNNqNCNNpqNCNCNNrsNCrNNs =
DD3D[16]D1D3D[22]DD2D1D[2]D[2][42][14]D3D[22]DD2D1DD2[21][27][14]
[141] CNCCpqNCrsCNCCstNCupNCCrtNCuq =
DD2D[1]DD2D1D2D1[51]DD2D[1]D[0][62]D1[30]DD2D1D2[62][35]
[142] CNNCCpqNCrNCrNsNCCNCtNuuNCsp =
DD2D[43]D1[30]D3D[22]DD2D[43][26]DD2D1DD2D1D2[34][46]1
[143] CNCCpqNCrsCCNprCNqs =
DD2D1D2D[39]D[23]DD2D1[77]DD2D1DD2[5]D1[73]DD2D1[15][5]1
[144] NCCNCCpqNCNpqqNCrNCCsrNCtr =
DD3D[16]D1D3D[22]DD2D1D2D[77][91]1DD2D[2]DD2D1[16]D[0]11
[145] CCpNqNCCNCCNrpNqNCrNqNCNCstNCCNsut =
DD2D[43]DD2D[60]D[39]D[8]D[0]D[1][5]D1[30]D1D3D[22]DD2D[1][9]D1[12]
[146] NCCNCCpqNCprCpNCqNrNCCsNCtNuNCCstNCsu = DD3D[16]D1[111]DD2D[43][46][33]
[147] NCCCpNCqNrNCCpqNCprNCNCCstNCsuCsNCtNu = DD3D[16]D1DD2D[43][46][33][111]
[148] NCCNCCNpqNNqNCpNNqNCNCrsNCCNrts =
DD3D[16]D1D3D[22]DD2D1DD2D1DD2D1DD22D1[22]1[91][14]D3D[22]DD2D[1][9]D1[12]
[149] CNNCCpqNCrsNCCsNqNCNrp =
DD2D[43]DD2D1D2D[77][68]1DD2D1D2D[39]DD2D1DD2D1D2D[43][6]1[6]1
[150] CNCCpqNCrsNCCNCptNCqtNCNCruNCsu =
D3DDD22D2[9]D1D[22]DDDD2D[1]D[0]D[1]D[0][5]D1[11]D3DDD22D2[9]D1D[22][74][74]
[151] CNCNCCpqNCrsNNCCqtNCurNCCptNCus =
DD2D[43]DD2DD2D1[5]D3DD2D1D3D3D[42]1[6]D3DD2D1D[22][12][6]DD2DD2D1[5]D3DD2D1D[22][12]1D3DD2D1D3D3D[42]11
[152] NCCCNCpNqrCNCqrNpNCCNCsNtNuCNCuNsNt =
DD3D[16]D1D[77][72]D[77]D[23]DD2D1D2D1[36]3
[153] NCCCNCpNqrCNCpNNrNqNCCNCsNNtuCNCsut = DD3D[16]D1[121]D[39]D[23][72]
[154] NCCNCCpqNCrqCCNprqNCCCNstuNCCsuNCtu = DD3D[16]D1[135]DD2D[43][31]D[8]1
[155] CNCCpqNCrsNCCCNptCNqtNCCNruCNsu =
D3DDD22D2[9]D1D[22]DDDD2D[1]D[0]D[1]D[0][5]D1[11]D3DDD22D2[9]D1D[22][89][89]
[156] CNCCpqNCqpNNCCpNqNCNqp =
D[22]DD2D[86]DD2D1DD2D1D2D1[67][11][30]DD2D1[85][40]
[157] NCCNCNCpNqrNCpNNCqrNCNCsNNCtuNCNCsNtu =
DD3D[16]D1D3D[22]DD2D1DD2D1[93]D2D1[14][14]D3D[22]DD2D1D[28][72][14]
[158] NCCCNCpqCprCpCNqrNCCsCNtuCNCvtCsu =
DD3D[16]D1DD2D1[47]D[23]DD2D1DD2D1DD2D1[2]D[23]DD2D1D2D1D2DD2D1D2D2[34]1[18][39][18]DD2D1DD2[5]D1[57]2
[159] NCCNCCNpqNNNrNCrNCNqpNCNCsNCNtuNCCNutNNNs =
DD3D[16]D1D3D[22]DD2D1D[28]DD2D1[54][36][14]D3D[22]DD2D1DD2D1DD2D1[36][54]D2D1[14][14]
[160] NNCNCCpqNCqpNNCCpNqNCNqp = D[17][156]
[161] NCCCpNCCqrNCstNCCCpqCprNCCpsCptNCNCCCuvCwxNCCyzCwaCwNCCvxNCza =
DD3D[16]D1DD2D[43]D[1][46]D[1][33]DD2D[60]DD2D1[47][40]DD2D1[47][30]
[162] CNCCpqNNCCrCstNCCupvNCCNCrNstNCpNCvNq =
DD2D[43]DD2D1DD2D1[93][40][30]DD2D[60]DD2D1DD2D1D[8]1[30][30][40]
[163] NCCNCpNCqrCNNCpqNCpNrNCCNNCstNCsNuNCsNCtu =
DD3D[16]D1DD2D1D2D[77]D[86][14]1D3DD2D1DD2D[43]D[22][46]D2D1[49][14]
[164] NCCNNCCpqNCrsCNNCpNNqNCrNNsNCCNNCtNNuNCvNNwNNCCtuNCvw =
DD3D[16]D1DD2D1DD2D1[27]DD2D1DD2D1DD22[21]1D2D1[83][14]D[22]DD2D1DD2D1D2D1D3D[22]D[28][14]DD2D1DD22D1[22]1[37]
[165] NCCNCCpNqNCNrsNCCqNpNCNsrNCNCCtNuNCNvwNCCuNtNCNwv =
DD3D[16]D1DD2D[43]DD2D1[36][40]D[39][30]DD2D[43]DD2D1[36][40]D[39][30]
[166] NCCNCCpqNCrsNCCNsNrNCNqNpNCNCCNtNuNCNvNwNCCwvNCut =
DD3D[16]D1DD2D[43]D[77][30]D[77][40]DD2D[43]D[2][30]D[2][40]
[167] NCCNCpNNCCpqrNCqNNCCpqrNCNCsNNCtNCsuNCuNNCtNCsu =
DD3D[16]D1DD2D[43]D3D[22]D[28]D[23]D[1]D[0][6][30]DD2D[43]D3D[22]DD2D1D2D1D[22]1DD2D1D2D[2]D[28]DD2D1[16]11[30]
[168] NCCCNCpqCrqCNCpNrqNCCNCsNtuCNCsvCtu =
DD3D[16]D1D[39]DD2D1[47]DD2D1[77]D[23]DD2D1DD2D1D2D1D[29]2D2D1D[2]DD2D1D2[6][0][18]DD2D1DD2D1DD2D1DD2[5]D1D[2][38][2]2[32]
[169] NCCNCpNCqrNCpNCNCsNqrNCNCtNCNCtNuvNCtNCuv =
DD3D[16]D1DD2D[43][40]DD2D1[52][30]DD2D[43][40]D3D[22]DD2D1D2D[77]D[15][34]1
[170]
NCNCNCCCNCpNqrCpCqrNCCsCtuCNCsNtuNNCCCvCwxCwCvxNCCyCzaCzCyaNNCCCbCcdCNCbNcdNCCNCeNfgCeCfg
= DD3D[16]D1DD3D[16]D1[131]DD3D[16]D1[18][18]DD3D[16]D1[93][72]
[171] CNCNCCpqNCrsNNCCtuNCvwNCCCNptCNquNCCNrvCNsw =
DD2D[2]DD2D1[16]D[0]DD2D[1]D[0]DD2D1[5]D3DD2D1D3D3D[42]1[6]DD2D1D2[5]D[0]D[2]DD2D[1]D[0]D[28]D3DD2D1D[22][12][6]D1[14]DD2D[1]D[0]D[1]D[2]DD2D[1]D[0]D[2][35]D11DD2D1D2[5]D[0]D[2]DD2D[1]D[0]D[28]D3DD2D1D[22][12]1D1[14]
[172] NCCNCCpqNCqpNNCCpNqNCNqpNCNNCCrNsNCNtuNCCusNCtr =
DD3D[16]D1[156]DD2D1DD2D[43]D[8]D[0]D[2]D[8]1DD2D1D[2][19][46][14]
[173] NCCNCCpqNCqpCNNCpNqNCNpNNqNCCNNCrNsNCNtNNuNCCtsNCur =
DD3D[16]D1DD2D1[27]DD2D[60]DD2D1[85][40]DD2D1DD2D1D2D1[67][11][30]DD2D1DD2D[43]DD2D1D[2]D[8]1[46]DD2D1D[2][19][33][37]
[174] CNCCpqNCrsNCCNCCstNCupNCCrtNCuqNCNCCqvNCwrNCCpvNCws =
DD2D[43][141]DD2DD2D1DD2D1[77]DD2D1DD2[5]D1[73]DD2D1D2D[1]D[0][5]D[0][11]DD2D1D2[5]D[2][38]D[1][35]
[175] CNCNCCpqNCrsNNCCtuNCvwNCCNCpNtNCqNuNCNCrNvNCsNw =
DD2D[43]DD2D[60]DD2D1DD2D1[63][40][40]DD2D1DD2D1[52][40][30]DD2D[60]DD2D1DD2D1[63][30][40]DD2D1DD2D1[52][30][30]
[176] NCCNCNNCpNqNCNpNNqCNNCpNNqNCqNNpNCCNNCrNsNCtNNuNCNNCusNCNrNNt =
DD3D[16]D1DD2D1[27]DD2D1DD2D1DD22[21]1DD2D[60]DD2D1DD2D1D[29][11]3[30]DD2D1DD2D1DD2D1D2D1[67]D[1]D2D1[6][14][40]DD2D1DD2D[43]DD2D1DD2D1D[22]3[33]D[8]1DD2D1D2D1D3D[22]D[2][9][19][37]
[177]
NCCCpNCCqrNCstNCCNCpNqNCpNrNCNCpNsNCpNtNCNCCNCuNvNCwNxNCNCuNyNCzNaCuNCCvxNCya =
DD3D[16]D1DD2D[43]D[77]D[1]D2D1D[77][40]D[77]D[1]D2D1D[77][30]DD2D[60]DD2D1[2]DD2D1[47]D[2][40]DD2D1[2]DD2D1[47]D[2][30]
[178] NCCNCCCNpqCNrsNCCNtuCNvsCNsNCCprNCtvNCCNwNCCxyNCzaNCCCNxwCNywNCCNzwCNaw =
DD3D[16]D1DD2D[60]DD2D1DD2D1DD2D1[47][39][54][40]DD2D1DD2D1DD2D1[47][39][54][30]DD2D[43]DD2D1DD2D1DD2D1[54][39]2[46]DD2D1DD2D1DD2D1[54][39]2[33]
[179] NCCCCNCNpqrsNCNCCpsNCqsNCrsNCNCNCCtuNCvuNCwuCCNCNtvwu =
DD3D[16]D1DD2D[43]DD2D[43]DD2[5]D1DD2D1D2[6]D[0][12]DD2D1DD22D1DD2D1D2[6]D[0]11D[8]1D[2]DD2D[86]DD2D1DD2D[86]D[77][40]D[77][30][40]D[77][30]
[180]
NCCNCCNCCpqNCrstNCuNCCsvNCrpNCCsNCCqtNCuvNCNCCruNCtrpNCNCCwNCCxyNCzaNCNCCxzNCybcNCCNCCcxNCxwyNCzNCCwaNCbc
=
DD3D[16]D1DD2D[43]DD2D[1]DD2D1[43]DD2D[1]D[0][62]D1[68]DD2D[1]D[0]D[1]DD2D1[46][30]D11DD2D1D2D1DD2DD2D1[88]DD2D1DD2D1D2D[39]DD2D1DD2D1D2D[43][6]1[6][73][30]DD2D[1]DD2D1[33][40]D1[3]DD2D[1]DD2D1[43]DD2D[1]D[0]D[1][35]D1[40]DD2D1D2D[1][35]D[2][38]DD2DD2D1[51]DD2D[1]DD2D1D2D1[51]DD2D[1]D[0]D[1][35]D1DD2D1D2DD2D1[51]1D[0]1DD2D[1]D[0]D[1]DD2D1[33][40]D11DD2D1D2D1DD2DD2D1[88]DD2D1DD2D1D2DD2D1D2D3D[22]DD2DD2D1[51][26]DD2D[1]D[0][6]D1[12]1[73][40]DD2D[1]DD2D1[46][30]D1[3][141]
