pmGenerator doesn't filter anything? That's false. What do you mean?

[xamidi]

Possibly I am missing a problem about pmGenerator stated in ~w2.mm.

One of your comments says

pmGenerator generates basically every theorem possible but doesn't seem to
have a way to filter anything. For example, theorems like ( ph -> T )
and ( -. T -> ph ) can appear many times in disguise.

But assuming T is a unique formula (i.e. T=T), that cannot happen (such is necessarily filtered out upon proof collection since conclusions are used as unique keys, and all isomorphic formulas are represented by equal strings). If you interprete T as "any tautology", then sure it shall not be filtered, since for syntactic consequence we need to consider all kinds of tautological structures. Am I missing something, or is it just that?

My tool doesn't yet have any features that look at semantics (which is irrelevant to formal proofs, but might be useful in the future in case I add features to look for new axioms rather than formal proofs).

I also don't think it's at all fair to say that "pmGenerator doesn't filter anything". After all, filtering out redundant schemas (via -m, or -g without -u) is a major feature upon generating proof databases. And, of course, upon proof collection, all duplicates (i.e. equal conclusions for different proofs) are also filtered out, and those proofs that do not meet extraction conditions — such as set by -g -l <limit> or -g -k <limit> — are filtered out as well. And then there is --transform -z which upon morphing a proof summary filters out subproofs that are unnecessary.

Let me show you how much of an impact filtering in pmGenerator can make. Exemplary output (which was recently produced):

Fri Jul 12 07:04:39 2024: Starting to generate D-proof representatives of length 13661.
Fri Jul 12 07:05:28 2024: Iterated ≈ 10% of D-proof candidates. [ 146801029 of approximately 1468010291] (ETC: Fri Jul 12 07:12:49 2024 ; 7 min 21 s 273.60 ms remaining ; 8 min 10 s 304.00 ms total)
[...]
Fri Jul 12 07:10:54 2024: Iterated ≈100% of D-proof candidates. [1468010291 of approximately 1468010291] (ETC: Fri Jul 12 07:10:54 2024 ; 0.00 ms remaining ; 6 min 14 s 716.77 ms total)
374778.29 ms (6 min 14 s 778.29 ms) taken to collect 728415 D-proofs of length 13661. [iterated 1468180428 condensed detachment proof strings]
[...]
Fri Jul 12 07:12:18 2024: Removed ≈ 10% of redundant conclusions. [ 72548 of approximately 725489] (ETC: Fri Jul 12 07:24:49 2024 ; 12 min 30 s 887.93 ms remaining ; 13 min 54 s 318.77 ms total)
[...]
Fri Jul 12 07:24:46 2024: Removed ≈100% of redundant conclusions. [725489 of approximately 725489] (ETC: Fri Jul 12 07:24:46 2024 ; 0.00 ms remaining ; 13 min 51 s 701.26 ms total)
837509.68 ms (13 min 57 s 509.68 ms) taken to detect 727169 conclusions for which there are more general variants proven in lower or equal amounts of steps.
[...]
Found 1246 representative, 333267510 redundant, and 1134911672 invalid condensed detachment proof strings.
[...]
15.82 ms taken to print and save 17050756 bytes of representative condensed detachment proof strings to data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/extraction-4/dProofs-withConclusions/dProofs13661.txt.
[...]
Fri Jul 12 07:24:52 2024: Starting to generate D-proof representatives of length 13663.

This is from an ongoing pmGenerator -c -n -s CpCCNqCCNrsCptCCtqCrq -e 4 -g -1 -l 19 -v^✻ run.
In the example, 1468180428 (1.4… billion) D-proof candidates were filtered to those 728415 which are valid, have new conclusions, and do not prove theorems that exceed 19 symbols (in a mere 6.246305 minutes), which again were filtered to those 1246 D-proofs whose conclusions do not already have schemas in the database representing them (in a mere 13.958495 minutes).
That's filtering out ≈99.999915133% of garbage in order to create a proof file small enough so that generation can continue as quickly and as long as possible.
It does so for thousands of files, and even a single time not filtering like that would basically cripple progression to an halt.

^✻_{Probably -g -v will be -g -b soon, and current -g -b be made the default, and the current default will be -g -f for "full parsing" (which shouldn't normally be used since it tends to be slow).}

[icecream17]

Yeah my comment was really unfair/inaccurate. T is indeed "any tautology"

I think it stemmed from the feeling that the manual heuristics were automatable, but that's too vague to be useful.

Here are some ideas that may or may not be useful:

1. extended filtering: grouping/noting/ignoring conclusions that are the same as others but with extra/reordered antecedents
   ** Especially useful with axioms A1 and L3. Filters anywhere from 5% to 70% of theorems, I imagine
2. extended filter generation: generating only extended-filtered theorems. Could result in deeper searches in more useful theorems?
3. reverse-search searching for theorems that match a schema instead of vice versa (for example, searching for theorems of the form CpNq)
   ** An incidental unrelated thing I ran into, but probably easier to code

[xamidi]

I'm not sure what you mean with (1.) and (2.). Could you give examples?

3. reverse-search searching for theorems that match a schema instead of vice versa [...]

Right, potentially useful and easy to add, so I just did that: [3f44a65] --search -t: look for formulas of given schemas (typed search)

Now, when for example up to dProofs21.txt are present for the default system, the query

$ ./pmGenerator --search C0NN1,CCNNCCN0.1.2.3NN4 -t

results in

Sun Jul 14 22:00:10 2024: Process started. [pid: 21040, tid:1]
Tasks:
1. searchProofFiles("C0NN1,CCNNCCN0.1.2.3NN4", false, false, 3, null, false)

[Main] Calling searchProofFiles("C0NN1,CCNNCCN0.1.2.3NN4", false, 3, false, null, false).
Found 2 of 2 formula types. All results:
Found [0] : "C0NN1"
        in line 9539 - D3DD2DD2D13DD2D1311:C0NN0
        of 'dProofs19.txt'.
        Substitution is {(0,0), (1,0)}.
Found [0] : "C0NN1"
        in line 41136 - DD2DD211DD2D1DD23D113:CCNNC0C1.0NNNNC0C1.0NNNNC0C1.0
        of 'dProofs21.txt'.
        Substitution is {(0,CNNC0C1.0NNNNC0C1.0), (1,NNC0C1.0)}.
Found [0] : "C0NN1"
        in line 41137 - DD2DD211DD2D1DD23D123:CCNNCC0C1.2CC0.1C0.2NNNNCC0C1.2CC0.1C0.2NNNNCC0C1.2CC0.1C0.2
        of 'dProofs21.txt'.
        Substitution is {(0,CNNCC0C1.2CC0.1C0.2NNNNCC0C1.2CC0.1C0.2), (1,NNCC0C1.2CC0.1C0.2)}.
Found [0] : "C0NN1"
        in line 41138 - DD2DD211DD2D1DD23D133:CCNNCCN0N1C1.0NNNNCCN0N1C1.0NNNNCCN0N1C1.0
        of 'dProofs21.txt'.
        Substitution is {(0,CNNCCN0N1C1.0NNNNCCN0N1C1.0), (1,NNCCN0N1C1.0)}.
Found [1] : "CCNNCCN0.1.2.3NN4"
        in line 41138 - DD2DD211DD2D1DD23D133:CCNNCCN0N1C1.0NNNNCCN0N1C1.0NNNNCCN0N1C1.0
        of 'dProofs21.txt'.
        Substitution is {(0,0), (1,N1), (2,C1.0), (3,NNNNCCN0N1C1.0), (4,NNCCN0N1C1.0)}.

Prior to this, I only implemented what I needed myself, but I'd gladly consider feature requests.
These should be placed at the discussion forum, which is also a good place to ask whether pmGenerator is able to handle certain problems or which ways are intended.

[Side note: This repository doesn't have discussions enabled, otherwise I would have posted there.]

[xamidi]

As a reminder, I wrote:

I'm not sure what you mean with (1.) and (2.). Could you give examples?

I plan to release 1.2.1 around the end of this month, but I certainly cannot address your problems without understanding them.

[icecream17]

My original idea was as follows:

If we have say a>b>c>d>e, a b c d are antecedents and e is the consequent

So a new filter might be to remove conclusions with the same consequent but reordered or extra antecedents (first idea)

But, except for a very specific use case of manually searching through a list of pmGenerator proofs, I don't see a use case. Maybe if some system had A1, where 50% of statements had an extra antecedent, a search with only the non-extra antecedent versions could go deeper by a few depth; this was my second idea

Even in the manual use case, one can just look at the ending statement, so the total effect is to save a half minute of time per equivalent statement. I don't think I really looked at that many, maybe 20 at most; most of my time was spent trying to extract more usefulness out of non redundant potentially useful statements

idea 4: inference

This is probably a much better idea

com12 is an inference proof: given some hypothesis H, it makes a conclusion

Here's a random D proof that may or may not be valid:

DDDD111D1DD1111D1D11

Let's say it successfully makes some complicated theorem, and let's also say that if we replace part of it with a hypothesis and unify:

DDDD111D1DH11D1D11

we get a much simpler inference statement akin to w2-q or com12

Statements like com12 are likely to be useful in multiple places. It also probably takes longer to prove the [(A>B>C)>(B>A>C)] (closed form)

D[(A>B>C)>(B>A>C)]H

than it takes to use the inference proof (inference form: first antecedent of closed form becomes a hypothesis).

Examples where the inference form of a proof is shorter to prove than the full statement and then D definitely exist, for example id has a proof of 1 character in inference form: H

My suggestion is to generate these inference forms for a specific proof, and see if these inference forms can be applied to any step in the proof to make it shorter

edit: Future ideas/feature requests will go in the discussions page linked. Thanks for the reminder too

[xamidi]

Thanks for your suggestions.

So I understand them as basically:

1. Option for --search:
   Use input ψ,…,φ,χ,ξ to look for formulas of the form Cψ…CφCχξ, but with arbitrary swaps between "antecedents" ψ,…,φ,χ and potentially extra such antecedents (but only ψ,…,φ,χ are specified as required).
2. Feature to analyze a given partially defined D-proof by searching for its unspecified parts (which are essentially variables of subproofs/formulas). It would test which assignments of the missing parts would result in which conclusions.

Details are still unclear about (2) — would you like to be able to specify a set or schema of formulas to try, or rather use some exhaustive generation or proof files?

I'm still not sure if those are really what you meant. You need to be more precise. But:

• What I wrote above as (1.) seems simple enough and I might still implement it as part of some 1.2.* patch.
• Regarding (2.), I considered the ability to use derivations/inferences as potentially very useful for a while now, but I didn't plan to implement any of this before version 1.3. So I am definitely open for suggestions of good (and specific) ways of how inferences could be utilized in useful ways.

[icecream17]

That's pretty much what I meant

In the case of (2) I imagined the case where a proof file is used. (Very dense text follows:)

Given a proof D[1][2], its subproofs are [1], [2], and the subproofs of [1] and [2]. Subproofs are equivalent to steps.

• The "partially defined D-proof"s would come from taking each subproof of a given D-proof, and:
  1. removing one of the subproofs of that subproof, and replacing it with what is indeed essentially a variable that stands in for that subproof
• Then, taking these inference-proofs-from-subproof's-subproofs
  1. See what steps the conclusion of the inference matches
  2. If the corresponding hypothesis has been proven, and using the inference proof including the proof of the hypothesis is shorter, then use the inference proof. Tada, the proof is shorter!

This seems to be O(n^3) (n(nn-1)/6) rather than O(n^2) as I initially assumed though...

since --transform -z (presumably O(n^2) as it applies subproof to subproof) took hours for a single proof, doing O(n^3) seems to limit this idea to only apply for just a single proof

failed manual example

I ran pmGenerator --transform data/w2.txt -f -n -t . -j 1 on w2.txt (the full summary that lists all the steps) and tried to find an example, but manually searching for usages of w2-q seemed moot as it was covered by [212] (147 steps), [205] (75 steps), and other similar instances of (¬p→((¬2→3)→q))→(2→p) where p→q.

Technically, I did find that [231]'s inference version was shorter: it corresponds to w2-5g DDD11D1HDDDDD111111
However, D[231]H never happens.

output of above command

    CpCCqCprCCNrCCNstqCsr = 1
[0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
[1] CCNCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqpCCNwxCsCvpCwCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqp = D[0]1
[2] CCNCpqCCNrsCCCNtCCNuvNpCutCCwCCxCwyCCNyCCNzaxCzyqCrCpq = D[0][0]
[3] CCpCCCqCCrCCsCrtCCNtCCNuvsCutwCCNwCCNxyqCxwzCCNzCCNabpCaz = D1[0]
[4] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[3]1
[5] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = D[1]1
[6] CCNCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqpCCNzasCzCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqp = D[5]1
[7] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = D[6]1
[8] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[7]
[9] CCNCpqCCNrsCCtpCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[8][0]
[10] CCpqCCNCCNqCCNrstCrqCCNuvpCuCCNqCCNrstCrq = D[1][7]
[11] CCCpCCqCprCCNrCCNstqCsruCvu = D[2][7]
[12] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[4][7]
[13] CCNpCCNqrCCsCCtCsuCCNuCCNvwtCvupCqp = D[0][11]
[14] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][12]
[15] CCpCCCCNqrsCCNCqtCCNuvCsCCwCCxCwyCCNyCCNzaxCzytCuCqtbCCNbCCNcdpCcb = D1[12]
[16] CCNCCNCpCqrCCNstCCNquvCsCpCqrCCNwxCNCqrCCNpyCvCCzCCaCzbCCNbCCNcdaCcbrCwCCNCpCqrCCNstCCNquvCsCpCqr = D[15]1
[17] CpCCCNCqCCrCqsCCNsCCNturCtsvNpw = D[9]1
[18] CCpCCqCCCNCrCCsCrtCCNtCCNuvsCutwNqxyCCNyCCNzapCzy = D1[17]
[19] CCNCCNpCCNqrsCqpCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaNsCtCCNpCCNqrsCqp = D[18]1
[20] Cpp = D[13][7]
[21] CCNpCCNCqCCrCqsCCNsCCNturCtsvNwCwCxp = D[14][7]
[22] CCCNpqCrCCsCCtCsuCCNuCCNvwtCvuxCCNCpCyxCCNzaCCNybrCzCpCyx = D[16][7]
[23] CNpCCNqCCNrspCrq = D[19][7]
[24] CCpCCqqrCCNrCCNstpCsr = D1[20]
[25] CCNCCNpCCNqrCspCqpCCNtusCtCCNpCCNqrCspCqp = D[24]1
[26] CCNCpCqCrsCCNtuCCNqvCCCNwCCNxyNrCxwCCNpzsCtCpCqCrs = D[22]1
[27] CpCqCCCNqrsCts = D[26]1
[28] CCNCCNpCCNqrCspCqpCCNtuCNCCNpCCNqrCspCqpCCNCvCCwCvxCCNxCCNyzwCyxasCtCCNpCCNqrCspCqp = D[0][25]
[29] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNCbCCcCbdCCNdCCNefcCedgCNqCCNphtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[0][4]
[30] CCCNCpCCqCprCCNrCCNstqCsruCNvCCNwxyCCNCwvCCNzaCyCCbCCcCbdCCNdCCNefcCedvCzCwv = D[29][7]
[31] CCpCCCCNCqCCrCqsCCNsCCNturCtsvCNwCCNxyzCCNCxwCCNabCzCCcCCdCceCCNeCCNfgdCfewCaCxwhCCNhCCNijpCih = D1[30]
[32] CCNCCNCpCqrCCNstCCNCuCCvCuwCCNwCCNxyvCxwzCNrCCNqabCsCpCqrCCNcdCNCqrCCNpeCbCCfCCgCfhCCNhCCNijgCihrCcCCNCpCqrCCNstCCNCuCCvCuwCCNwCCNxyvCxwzCNrCCNqabCsCpCqr = D[31]1
[33] CCCNpqCrCCsCCtCsuCCNuCCNvwtCvuxCCNCpCyxCCNzaCCNCbCCcCbdCCNdCCNefcCedgCNxCCNyhrCzCpCyx = D[32][7]
[34] CCNCpCqCrsCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaCNCrsCCNqbCCCNcCCNdeNrCdcCCNpfsCtCpCqCrs = D[33]1
[35] CpCqCrCsCtq = D[34]1
[36] CpCqCrCsp = D[35]1
[37] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1[36]
[38] CpCqCrCNps = D[2][27]
[39] CCNCpCNqrCCNstqCsCpCNqr = D[0][38]
[40] CCpCCNqCCNrCCNstqCsruCCNuCCNvwpCvu = D1[23]
[41] CCNCCNCpqCCNrsNtCrCpqCCNuvCNqCCNpwtCuCCNCpqCCNrsNtCrCpq = D[40]1
[42] CCCNpqrCCNCpsCCNtuNrCtCps = D[41][7]
[43] CCpCCCNCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqrCCNabCNrCCNqcuCaCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqrdCCNdCCNefpCed = D1[4]     
[44] CCNCCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNbcCNqCCNpdtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNefbCeCCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNbcCNqCCNpdtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[43]1
[45] CpCCNCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqrCCNabCNCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqrCCNCCNcCCNdeNpCdcfCNrCCNqguCaCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqr = D[44]1
[46] CCpCCqCCNCCNCrsCCNtuCvCCwCCxCwyCCNyCCNzaxCzysCtCrsCCNbcCNCCNCrsCCNtuCvCCwCCxCwyCCNyCCNzaxCzysCtCrsCCNCCNdCCNefNqCedgCNsCCNrhvCbCCNCrsCCNtuCvCCwCCxCwyCCNyCCNzaxCzysCtCrsiCCNiCCNjkpCji = D1[45]
[47] CCNCCNCpCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqrCCNabcCaCpCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqrCCNdeCNCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqrCCNpfCNCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqrCCNCCNgCCNhiNcChgjCNrCCNqkuCdCCNCpCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqrCCNabcCaCpCCNCqrCCNstCuCCvCCwCvxCCNxCCNyzwCyxrCsCqr = D[46]1
[48] CCCNpqCNCCNCrsCCNtuCvCCwCCxCwyCCNyCCNzaxCzysCtCrsCCNCCNbCCNcdNeCcbfCNsCCNrgvCCNCpCCNCrsCCNtuCvCCwCCxCwyCCNyCCNzaxCzysCtCrsCCNhieChCpCCNCrsCCNtuCvCCwCCxCwyCCNyCCNzaxCzysCtCrs = D[47][7]
[49] CCNCpCqCCNCrsCCNtuCvCCwCCxCwyCCNyCCNzaxCzysCtCrsCCNbcCCNqdCNCCNCrsCCNtuCvCCwCCxCwyCCNyCCNzaxCzysCtCrsCCNCCNeCCNfgNCCNhCCNijNpCihCfekCNsCCNrlvCbCpCqCCNCrsCCNtuCvCCwCCxCwyCCNyCCNzaxCzysCtCrs = D[0][48]
[50] CpCqCCCNCCNrCCNstNCCNuCCNvwNqCvuCsrxCNyCCNzabCCNCzyCCNcdCbCCeCCfCegCCNgCCNhifChgyCcCzy = D[49]1
[51] CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq = D[9][50]
[52] CCNCpqCCNrsCCtCuNqCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[37][0]
[53] CpCqp = D[52]1
[54] CCpCCqCrqsCCNsCCNtupCts = D1[53]
[55] CCCNCpCCqCprCCNrCCNstqCsruvCCNwCCNxyCvwCxw = D[28][7]
[56] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[12][21]
[57] CpCNpq = D[56]1
[58] CCNCCNCpCCNqCCNrstCrqCCNuvwCuCpCCNqCCNrstCrqCCNxyCNCCNqCCNrstCrqCCNpzCCNCaCCbCacCCNcCCNdebCdcfNtCxCCNCpCCNqCCNrstCrqCCNuvwCuCpCCNqCCNrstCrq = D[10][19]
[59] CCCNpqCCNCrCCsCrtCCNtCCNuvsCutwNxCCNCpCCNyCCNzaxCzyCCNbcdCbCpCCNyCCNzaxCzy = D[58][7]
[60] CCNCpCqCCNrCCNstuCsrCCNvwCCNqxCCNCyCCzCyaCCNaCCNbczCbadNuCvCpCqCCNrCCNstuCsr = D[0][59]
[61] CpCqCNrCCNsCCNturCts = D[60]1
[62] CCpCCqCrCNsCCNtCCNuvsCutwCCNwCCNxypCxw = D1[61]
[63] CCNCpCqCrsCCNtuCCNqvCpCCwCCxCwyCCNyCCNzaxCzysCtCpCqCrs = D[8][22]
[64] CCpCCqCCrCqsCCNsCCNturCtsvCpCwCxv = D[63][7]
[65] CpCqCNCrps = D[39][7]
[66] CCNCNCpqrCCNstqCsCNCpqr = D[0][65]
[67] CCNCpCqrCCNstCNCpCqrCCNCuCCvCuwCCNwCCNxyvCxwzCCNqaCNrCCNCbCCcCbdCCNdCCNefcCedgNpCsCpCqr = D[0][14]
[68] CpCqCrp = D[67][35]
[69] CCNCpCqrCCNstCCNCuCCvCuwCCNwCCNxyvCxwzCNrCCNqaNpCsCpCqr = D[0][55]
[70] CCNpCCNqrNsCsCqp = D[69][7]
[71] CpCCCNpqrCsr = D[27]1
[72] CCpCCqCCCNqrsCtsuCCNuCCNvwpCvu = D1[71]
[73] CCNCCNCpqCCNrstCrCpqCCNuvCCNtwqCuCCNCpqCCNrstCrCpq = D[72]1
[74] CpCCNCqCrsCCNtusCtCqCrs = D[73]1
[75] CCpCCqCCNCrCstCCNuvtCuCrCstwCCNwCCNxypCxw = D1[74]
[76] CCNCCNCpCqCrsCCNtuvCtCpCqCrsCCNwxCNCqCrsCCNpysCwCCNCpCqCrsCCNtuvCtCpCqCrs = D[75]1
[77] CCCNpqrCCNCpCsCtrCCNuvwCuCpCsCtr = D[76][7]
[78] CCNCpCqCrCstCCNuvCCNqwtCuCpCqCrCst = D[0][77]
[79] CpCqCrCsCtp = D[78][7]
[80] CCpCCqCrCsCNqtuCCNuCCNvwpCvu = D1[38]
[81] CCNCCNCpCNqrCCNstqCsCpCNqrCCNuvwCuCCNCpCNqrCCNstqCsCpCNqr = D[80]1
[82] CpCCNCqCNrsCCNturCtCqCNrs = D[81]1
[83] CCNCpCqCNCrpsCCNtuvCtCpCqCNCrps = D[8][82]
[84] CpCqCrCNCsqt = D[83]1
[85] CpCNCqCNprs = D[13][84]
[86] CpCCNqCCNrsCpqCrq = D[28][51]
[87] CCpCCqCrCsqtCCNtCCNuvpCut = D1[68]
[88] CCNCpqCCNrsCCtNqCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[87][0]
[89] CpCqCCCNCrCCsCrtCCNtCCNuvsCutwNqx = D[14]1
[90] CpCqCNpr = D[88][89]
[91] CCNCNpqCCNrspCrCNpq = D[0][90]
[92] CCNCpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNxCrqCCNyzxCyCpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNxCrq = D[0][5]
[93] CCpCCCCqCCrCqsCCNsCCNturCtsvCwvxCCNxCCNyzpCyx = D1[11]
[94] CCNCCNpCCNqrCCsCCtCsuCCNuCCNvwtCvupCqpCCNxyzCxCCNpCCNqrCCsCCtCsuCCNuCCNvwtCvupCqp = D[93]1
[95] CpCCNqCCNrsCCtCCuCtvCCNvCCNwxuCwvqCrq = D[94]1
[96] CCpCCqCCNrCCNstCCuCCvCuwCCNwCCNxyvCxwrCsrzCCNzCCNabpCaz = D1[95]
[97] CCNCCNCpqCCNrstCrCpqCCNuvCNqCCNpwCCxCCyCxzCCNzCCNabyCazqCuCCNCpqCCNrstCrCpq = D[96]1
[98] CCCNpqCCrCCsCrtCCNtCCNuvsCutwCCNCpwCCNxyzCxCpw = D[97][7]
[99] CCNCpCqrCCNstCCNquCCvCCwCvxCCNxCCNyzwCyxrCsCpCqr = D[0][98]
[100] CpCqCrr = D[99]1
[101] CpCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyyCsr = D[92][100]
[102] CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq = D[56][101]
[103] CCpCCqCCNrCCNCCNsCCNtuNCNqvCtswNCxxryCCNyCCNzapCzy = D1[102]
[104] CCNCCNCpCqrCCNstCCNquvCsCpCqrCCNwxCNCCNCpCqrCCNstCCNquvCsCpCqrCCNCyCCzCyaCCNaCCNbczCbadCNCqrCCNpeCvCCfCCgCfhCCNhCCNijgCihrCwCCNCpCqrCCNstCCNquvCsCpCqr = D[0][16]
[105] CCCNCpCCqCprCCNrCCNstqCsruCNCvwCCNxyCzCCaCCbCacCCNcCCNdebCdcwCCNCxCvwCCNfgCCNvhzCfCxCvw = D[104][7]
[106] CCNCpCqCrsCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaCNCrsCCNqbCpCCcCCdCceCCNeCCNfgdCfesCtCpCqCrs = D[8][105]
[107] CCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCtCrCpq = D[106][7]
[108] CCNCCNCCpCqrCCNrCCNstpCsrCCNuvwCuCCpCqrCCNrCCNstpCsrCCNxyqCxCCNCCpCqrCCNrCCNstpCsrCCNuvwCuCCpCqrCCNrCCNstpCsr = D[10]1
[109] CCNCCNCCpCqrCCNrCCNstpCsrCCNuvwCuCCpCqrCCNrCCNstpCsrCCNxyCNCCNCCpCqrCCNrCCNstpCsrCCNuvwCuCCpCqrCCNrCCNstpCsrCCNCzCCaCzbCCNbCCNcdaCcbeqCxCCNCCpCqrCCNrCCNstpCsrCCNuvwCuCCpCqrCCNrCCNstpCsr = D[0][108]
[110] CCCNCpCCqCprCCNrCCNstqCsruvCCNCCwCvxCCNxCCNyzwCyxCCNabcCaCCwCvxCCNxCCNyzwCyx = D[109][7]
[111] CCNCpCCqCrsCCNsCCNtuqCtsCCNvwCCNCxCCyCxzCCNzCCNabyCazcrCvCpCCqCrsCCNsCCNtuqCts = D[0][110]
[112] CpCqCCrCpsCCNsCCNturCts = D[111][7]
[113] CCCCNpCCNqrNsCqpCNCtCsuuCvCtCsu = D[107][112]
[114] CCNCpCqrCCNstCCCNuCCNvwNqCvuCNCpCqrrCsCpCqr = D[0][113]
[115] CCNCpCqrrCpCqr = D[114][7]
[116] CCpCCCqCCrCsCtCurvCCNvCCNwxqCwvyCCNyCCNzapCzy = D1[37]
[117] CCNCCNCpqCCNrsCtCCuCvCwCxuqCrCpqCCNyzCNqCCNpatCyCCNCpqCCNrsCtCCuCvCwCxuqCrCpq = D[116]1
[118] CCCNpqrCCNCpsCCNtuCrCCvCwCxCyvsCtCps = D[117][7]
[119] CCNCpCqCrsCCNtuCCNqvNCwCxNsCtCpCqCrs = D[62][118]
[120] CNCpCqNrCsCtCur = D[119][7]
[121] CCpCCCqCCrCsrtCCNtCCNuvqCutwCCNwCCNxypCxw = D1[54]
[122] CCNCCNCpqCCNrsCtCCuCvuqCrCpqCCNwxCNqCCNpytCwCCNCpqCCNrsCtCCuCvuqCrCpq = D[121]1
[123] CCCNpqrCCNCpsCCNtuCrCCvCwvsCtCps = D[122][7]
[124] CCNCpCqCrsCCNtuCCNqvNNsCtCpCqCrs = D[62][123]
[125] CNNpCqCrCsp = D[124][7]
[126] CCpCCqCNCrCNqstuCCNuCCNvwpCvu = D1[85]
[127] CCNCCNpCCNqrsCqpCCNtuNCvCNswCtCCNpCCNqrsCqp = D[126]1
[128] CpCCNqCCNNrsrCNrq = D[127][53]
[129] CCNpCCNNqrqCNqp = D[128]1
[130] CCNCCpqqCCNrspCrCCpqq = D[103][86]
[131] CpCNCqCrsCtNs = D[91][120]
[132] CNCpCqrCsNr = D[131]1
[133] CpCCpqq = D[130][102]
[134] CCpCCqCCNrCCNstCqrCsruCCNuCCNvwpCvu = D1[86]
[135] CCNCCNCpqCCNrstCrCpqCCNuvCNqCCNpwCtqCuCCNCpqCCNrstCrCpq = D[134]1
[136] CCNpCCNqrCspCCNCqpCCNtusCtCqp = D[135][102]
[137] CCNCpCqrCCNstCNrCCNquCprCsCpCqr = D[103][136]
[138] CCpqCpCrq = D[137][51]
[139] CpCCNqCCNrsCNqqCrq = D[25][132]
[140] CCNpCCNqrCNppCqp = D[139]1
[141] CCNppp = D[140][102]
[142] CCpCCCNqqqrCCNrCCNstpCsr = D1[141]
[143] CCNCCNpCCNqrCNCspCspCqpCCNtusCtCCNpCCNqrCNCspCspCqp = D[142]1
[144] CpCCNqCCNrsCNCpqCpqCrq = D[143][102]
[145] CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq = D[103][144]
[146] CpCCNCpqCpqq = D[145][102]
[147] CCpqCrCpCsq = D[138][138]
[148] CCNCpCNqrCCNstCNCpCNqrCCNCuCCvCuwCCNwCCNxyvCxwzqCsCpCNqr = D[0][39]
[149] CCCNCpCCqCprCCNrCCNstqCsruvCwCNvx = D[148][7]
[150] CCNCNpqCCNrsCCNCtCCuCtvCCNvCCNwxuCwvypCrCNpq = D[0][149]
[151] CpCNCqrCsNr = D[150][120]
[152] CNCpqCrNq = D[151]1
[153] CpCCNCNqqCNqqq = D[145][152]
[154] CpCCNCNqCrqCNqCrqCrq = D[145][132]
[155] CCpCCqCCNCqrCqrrsCCNsCCNtupCts = D1[146]
[156] CCNpCCNqrCCsCCNCstCsttpCqp = D[155][20]
[157] CpCCNqNpq = D[156]1
[158] CCpCCqCCNrNqrsCCNsCCNtupCts = D1[157]
[159] CCNCCNpCCNqrsCqpCCNtuCNpNsCtCCNpCCNqrsCqp = D[158]1
[160] CCNpNqCCNpCCNrsqCrp = D[159][102]
[161] CCNCCpqqpCCpqq = D[130][146]
[162] CCNppCCpqq = D[130][153]
[163] CCNCpqCCNrsCpCCttqCrCpq = D[103][24]
[164] CCpCCqqrCpr = D[163][102]
[165] CCpCCCqCCrCCNsCCNtuCNsCCNCCNvCCNwxNrCwvyNCzCCaCzbCCNbCCNcdaCcbCtseCCNeCCNfgqCfehCCNhCCNijpCih = D1[8]
[166] CCNCCNCpqCCNrsCtCCuCCNvCCNwxCNvCCNCCNyCCNzaNuCzybNCcCCdCceCCNeCCNfgdCfeCwvqCrCpqCCNhiCNqCCNpjtChCCNCpqCCNrsCtCCuCCNvCCNwxCNvCCNCCNyCCNzaNuCzybNCcCCdCceCCNeCCNfgdCfeCwvqCrCpq = D[165]1
[167] CCCNpqrCCNCpsCCNtuCrCCvCCNwCCNxyCNwCCNCCNzCCNabNvCazcNCdCCeCdfCCNfCCNgheCgfCxwsCtCps = D[166][7]
[168] CCpCCCCNqrsCCNCqtCCNuvCsCCwCCNxCCNyzCNxCCNCCNaCCNbcNwCbadNCeCCfCegCCNgCCNhifChgCyxtCuCqtjCCNjCCNklpCkj = D1[167]
[169] CCNCCNCpCqrCCNstCCNquvCsCpCqrCCNwxCNCqrCCNpyCvCCzCCNaCCNbcCNaCCNCCNdCCNefNzCedgNChCCiChjCCNjCCNkliCkjCbarCwCCNCpCqrCCNstCCNquvCsCpCqr = D[168]1
[170] CCCNpqCrCCsCCNtCCNuvCNtCCNCCNwCCNxyNsCxwzNCaCCbCacCCNcCCNdebCdcCutfCCNCpCgfCCNhiCCNgjrChCpCgf = D[169][7]
[171] CCNCpCqCrsCCNtuCCNqvCCwrCCNpxsCtCpCqCrs = D[170]1
[172] CCCpqCCNrstCrCuCqt = D[171][7]
[173] CCCpqrCsCqr = D[172][146]
[174] CCCpqrCqr = D[164][173]
[175] CpCCNqqCCqrr = D[53][162]
[176] CCpCCCCNqrsCCNCqtCCNuvNsCuCqtwCCNwCCNxypCxw = D1[42]
[177] CCNCCNCpCqrCCNstCCNquvCsCpCqrCCNwxCNCqrCCNpyNvCwCCNCpCqrCCNstCCNquvCsCpCqr = D[176]1
[178] CCCNpqNrCCNCpCstCCNuvCCNswrCuCpCst = D[177][7]
[179] CCNCpCqCrsCCNtuCCNqvNCwrCtCpCqCrs = D[0][178]
[180] CNCpqCrCsCqt = D[179][7]
[181] CpCNCqCrCsts = D[66][180]
[182] CNCpCqCrsr = D[181]1
[183] CCpCqCprCqCpr = D[161][182]
[184] CCNCpqCCNrsCNqNpCrCpq = D[103][160]
[185] CCNpNqCqp = D[184][102]
[186] CCNCpCCNqCCNrstCrqCCNuvCCCNwCCNxyNpCxwqCuCpCCNqCCNrstCrq = D[0][10]
[187] CpCqCCNpCCNrstCrp = D[186][7]
[188] CCpCCqCrCCNqCCNstuCsqvCCNvCCNwxpCwv = D1[187]
[189] CCNCpqCCNrsNCtCupCrCpq = D[42][21]
[190] CCNCpqCCNrsCNCpqCCNCtCuCCNtCCNvwxCvtyNCzCapCrCpq = D[188][189]
[191] CNCpCqrCrs = D[190][51]
[192] CCCpqCrpCrp = D[161][191]
[193] CNCpCqCrNss = D[129][79]
[194] CCpCqCrNpCqCrNp = D[161][193]
[195] CNNpCqCrCsCtp = D[64][125]
[196] CNCpCqCrsNs = D[129][195]
[197] CCNpCqCrpCqCrp = D[161][196]
[198] CCpCqNpCqNp = D[194][133]
[199] CNCpCNCqrsq = D[192][85]
[200] CCpCNCpqrCNCpqr = D[161][199]
[201] CpCCCCpqqrr = D[130][175]
[202] CCCCpqqCprCpr = D[183][201]
[203] CCNpCCNqrpCqp = D[0][53]
[204] CCNpCqpCqp = D[203][154]
[205] CCNCpqCCNrsqCrCpq = D[0][68]
[206] CCNpCqpCrCqp = D[205][154]
[207] CCNCpqCCNrsNCCNtCCNuvNpCutCrCpq = D[0][23]
[208] CCNCCNCpCqrCCNstuCsCpCqrCCNvwCNCqrCCNpxNCCNyCCNzaNqCzyCvCCNCpCqrCCNstuCsCpCqr = D[10][207]
[209] CCCNpqNCCNrCCNstNuCsrCCNCpCuvCCNwxyCwCpCuv = D[208][7]
[210] CCNCpCqCrsCCNtuCCNqvNCCNwCCNxyNrCxwCtCpCqCrs = D[0][209]
[211] CpCCNCqrCCNstNqCsCqr = D[210][68]
[212] CCNCpqCCNrsNpCrCpq = D[211]1
[213] CCpCCqCrCNCsqtuCCNuCCNvwpCvu = D1[65]
[214] CCNCpqCCNrsCCNCtCCuCtvCCNvCCNwxuCwvyNCzNqCrCpq = D[213][55]
[215] CNCpNqCrq = D[214][7]
[216] CpCqNNq = D[212][215]
[217] CpCCNNCNpqrr = D[130][216]
[218] CpCCNNCNNqrqq = D[206][217]
[219] CNCNNpqCCprr = D[130][218]
[220] CCpCNNpqCNNpq = D[204][219]
[221] CCNCpqCCNrsNNqCrCpq = D[54][23]
[222] CCNCpqCCNrsCNCpqCCNCtCCuCtvCCNvCCNwxuCwvyNNqCrCpq = D[0][221]
[223] CNNpCqp = D[222][51]
[224] CCNpCCNqrNNpCqp = D[0][223]
[225] CCNNNpNNpp = D[224][153]
[226] CpCCNNNqNNqq = D[53][225]
[227] CNNpCCNCpqCpqq = D[145][226]
[228] CpCCqNpNq = D[70][227]
[229] CpCCNNpqq = D[130][228]
[230] CCNNCpqpp = D[192][229]
[231] CpCCpqCrq = D[202][147]
[232] CpCqCCprCsr = D[138][231]
[233] CpCNCqCCprrs = D[66][175]
[234] CNCpCCqrrNq = D[198][233]
[235] CCNpCCpqqCCpqq = D[161][234]
[236] CpCCNNCqrqq = D[53][230]
[237] CNCpqCCNCprCprr = D[145][236]
[238] CCpqCpCNqr = D[39][237]
[239] CNNpCCpqCrq = D[220][232]
[240] CNCpqCCprCsr = D[200][232]
[241] CCpqCNCprq = D[183][240]
[242] CpCCqNpCqr = D[70][237]
[243] CNCpqCCrNpCrs = D[241][242]
[244] CCpNqCpCqr = D[197][243]
[245] CCNCpCqCrsCCNtusCtCpCqCrs = D[0][79]
[246] CCpqCpCrCsq = D[245][237]
[247] CCNCNpqpCNpq = D[91][146]
[248] CCCNpqCrsCrCps = D[137][7]
[249] CpCNCCpqrq = D[248][230]
[250] CpCNCNCCpqrqs = D[238][249]
[251] CNCNCCpqrqCsNp = D[194][250]
[252] CNCCpqNpq = D[247][251]
[253] CNCCpqNpCrCsq = D[246][252]
[254] CCCCpqNpCrqCrq = D[235][253]
[255] CCpNqCNCpCqrs = D[238][244]
[256] CNCCpqCprq = D[254][255]
[257] CNCCpqCprCsq = D[138][256]
[258] CNCCpqCprCsCtq = D[64][257]
[259] CCCNpqrCpCCrss = D[174][130]
[260] CNNNCCpqCprCsq = D[220][258]
[261] CCNNCCpqCprqq = D[235][260]
[262] CNCCpqCprCCqss = D[259][261]
[263] CCpqCpCCqrr = D[115][262]
[264] CCNpCCNqrCspCsCqp = D[137][102]
[265] CpCCNqCpqq = D[264][146]
[266] CCNpCCqCCqrCsrpp = D[265][231]
[267] CCpqCNNpq = D[183][239]
[268] CCpCCNNqCrCsCtquCCNuCCNvwpCvu = D1[125]
[269] CCNCpNqCCNrsCCtCuqCCvCCwCvxCCNxCCNyzwCyxNqCrCpNq = D[268][0]
[270] CpCqNNp = D[269]1
[271] CCNNNpCCNqrpCqNNp = D[0][270]
[272] CCCNpqrCpNNr = D[174][271]
[273] CCpCCNppqCCNppq = D[183][162]
[274] CCNppCCpqCrq = D[273][232]
[275] CCpqCCNppq = D[183][274]
[276] CpCCCCpqqrCsr = D[202][232]
[277] CCCCpqqrCpr = D[183][276]
[278] CpCCpNqCqr = D[277][244]
[279] CCNppCCpNqCqr = D[275][278]
[280] CpNNCCpNqCqr = D[272][279]
[281] CNCCNpNqCqrp = D[185][280]
[282] CNCCNpNqCqrCCpss = D[263][281]
[283] CCNpNqCqCCprr = D[115][282]
[284] CNNCNpNqCqCCprr = D[267][283]
[285] CNpCCqpCqr = D[129][257]
[286] CCpqCpNNq = D[194][285]
[287] CNCpqCCrqCrs = D[129][258]
[288] CCpqCpNNCrq = D[194][287]
[289] CCpqNNCpNNCrq = D[286][288]
[290] CCNCpqCCNrsCNqNCtpCrCpq = D[8][160]
[291] CCNpNCqrCrp = D[290][102]
[292] CpCqCCprr = D[138][133]
[293] CNCCNpqqp = D[129][292]
[294] CpCCNNCqprr = D[291][293]
[295] CCNNCpqNqNq = D[198][294]
[296] CpCCNNCqrNrNr = D[53][295]
[297] CNCpqCCNqrr = D[130][296]
[298] CCNpCNCqprCNCqpr = D[183][297]
[299] CCpqCrCNCpsq = D[138][241]
[300] CNCCpqrCNCpsq = D[200][299]
[301] CNCpCCpqrq = D[298][300]
[302] CNCpCCpqrCsq = D[138][301]
[303] CNpCqCCqpr = D[129][302]
[304] NNCNpNNCqCrCCrps = D[289][303]
[305] CNCpCqCCqrsCCrtt = D[284][304]
[306] CCpCCqprCqCCqpr = D[266][305]
[307] CpCCpqCCqrCsr = D[306][232]
[308] CCNCpqrCCrqCpq = D[197][307]
[309] CCpCqrCCqpCqr = D[308][256]
[310] CCpCqrCpCqCsr = D[309][147]
[311] CNCCpqrCpCsq = D[200][147]
[312] CCCpCqrsCCprs = D[308][311]
[313] CCpqCCrpCrq = D[312][309]
[314] CCpqCCrpCsCrq = D[310][313]
[315] CCpqCCqrCpr = D[183][314]
[316] CCNCpqCCNrsNCtCNpuCrCpq = D[42][53]
[317] CNCpCNqrCqs = D[316][102]
[318] CCCpqCNprCNpr = D[161][317]
[319] CpCqCNCrCspt = D[39][51]
[320] CNpCNCqCrCpst = D[318][319]
[321] CNCpCqCrsNNr = D[198][320]
[322] CCNNpCqCprCqCpr = D[161][321]
[323] CNNpCCCCpqCrqss = D[263][239]
[324] CCCCpqCrqCpsCps = D[322][323]
[325] CpCCCCpqCrqsCts = D[324][232]
[326] CCCCpqCrqsCps = D[183][325]
[327] CpCCqCprCqr = D[326][309]
[328] CpCCqCprCsCqr = D[310][327]
[329] CCpCqrCqCpr = D[183][328]
[330] CCCpCqrsCCqCprs = D[315][329]
[331] CCpCqrCCpqCpr = D[330][309]

[xamidi]

I elaborated on (2) in the first comment of xamidi/pmGenerator/discussions/3.

[icecream17]

(Remaining discussion moved)