w3:(A2:2762055↦614905,A3:182879↦51239,L1:180451↦39253,L2:2177↦1649)

- solution from #2 (comment) (discussions)
- |22|->1401,|19|->2001,(squish & regenerate dProofs1897+),|19|->2391
- based on 8a231d7

data/w3.txt

@@ -7,8 +7,8 @@
 % Full summary: pmGenerator --transform data/w3.txt -f -n -t . -j 1
 % Step counting: pmGenerator --transform data/w3.txt -f -n -t . -p -2 -d
 %                pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
-% Compact (2509 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCCCpCCqrCsrtCCCqrCsrtuCvu,CCCpCqrsCCqrs,CCCCCpqrCqrsCts,CCpqCCCpqrCsr,CCCpqrCqr,CCCNpqrCpr,CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp,CCNppCqp,CCCCNpqCrqpCsp,CCCNpqCCrCsCtsqCCquCpu,CpCCpqCrq,CpCqCrp,CCCCCCpqCrqsNttCut,CCCCCNpqrCsrtCpt,CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy,CCCCCpqrCsrtCqt,CCCpCqrsCrs,CNNCpqCrCpq,CCNCCpCqpNrsCrs,CCCpqCNprCsCNpr,CpCCNCqrrCqr,CCpNpCqNp,CCpqCNNpq,CCCpqrCNpr,CCpNCNppCqNCNpp,CpCqCrNNp,CCNpqCNCrpq,CCNpqCNCrCspq,CCpqCCNppq,CNCpqCrCsp,CCpCpqCpq,CCpqCCNqpq,CpCCpqq,CCpCqrCqCpr
-% Concrete (3128030 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
+% Compact (2553 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCNpCCNqCCNrsCNptCCtqCrqCCCrqpCqpCCCCCrqpCqpuCvu,CCCpCqrsCCqrs,CCCCCpqrCqrsCts,CCpqCCCpqrCsr,CCCpqrCqr,CCCNpqrCpr,CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp,CCNppCqp,CCCCNpqCrqpCsp,CCCNpqCCrCsCtsqCCquCpu,CpCCpqCrq,CCCNCNpqrsCps,CpCqCrp,CCCCCNpqrCsrtCpt,CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy,CCCCCpqrCsrtCqt,CNNCpqCrCpq,CCNCCpCqpNrsCrs,CCCpqpCrp,CCpqCCCrrNNpq,CCCpqCNprCsCNpr,CCpNpCqNp,CCpCqNpCrCqNp,CCCpqrCNpr,CCpCqNCNppCrCqNCNpp,CCNpqCNCrpq,CNCpqCrCsp,CCNpqCNCrCspq,CCpqCCNppq,CCNCpqrCCrqCpq,CCpCpqCpq,CCpqCCNqpq,CpCCpqq,CCpCqrCqCpr
+% Concrete (707514 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
 
     CpCCNqCCNrsCptCCtqCrq = 1
 [0] CCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqp = D11
@@ -29,78 +29,78 @@
 [15] CCCCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpwCxCCqwCpwCCCxCCqwCpwyCzy = D[3]D[3]D1[7]
 [16] CCCpqCrqCCCCpqCrqsCts = D[3][11]
 [17] CCCCCpqrCqrsCts = DD[13][0]1
-[18] CCCCCCpqCrqsCtsuCqu = DD[13]DD[3]111
-[19] CCCNpqCCCCrstCstqCCquCpu = D[3]DD[17]11
-[20] CCpqCCCpqrCsr = D[13][11]
-[21] CCCpqrCqr = DDD[17]D[3][2]1[0]
-[22] CCCNpqrCpr = D[0]D[12][13]
-[23] CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp = D1D[6][19]
-[24] CpCCqpCrp = D[22][0]
-[25] CCNppCqp = D[0][24]
-[26] CpCqCrq = DD[17][17]1
-[27] CCNpCCNqrCCsCtCutvCCvpCqp = D1[26]
+[18] CCCCpqCrqsCtCCCpqCrqs = D[6][10]
+[19] CCCCCCpqCrqsCtsuCqu = DD[13]DD[3]111
+[20] CCCNpqCCCCrstCstqCCquCpu = D[3]DD[17]11
+[21] CCpqCCCpqrCsr = D[13][11]
+[22] CCCpqrCqr = DDD[17]D[3][2]1[0]
+[23] CCCNpqrCpr = D[0]D[12][13]
+[24] CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp = D1D[6][20]
+[25] CpCCqpCrp = D[23][0]
+[26] CCNppCqp = D[0][25]
+[27] CpCqCrq = DD[17][17]1
+[28] CCNpCCNqrCCsCtCutvCCvpCqp = D1[27]
 
 % Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 67 steps
-[28] CpCqp = D[26]1
+[29] CpCqp = D[27]1
 
-[29] CCNpCCNqrCCsCtsuCCupCqp = D1[28]
-[30] CCCCNpqCrqpCsp = D[0]D[18]DD[3][8][3]
-[31] CCCNpqCCrCsCtsqCCquCpu = D[3][27]
-[32] CpCCpqCrq = DD[1]DDD[3]D[3]D1[8][3][13][0]
-[33] CCCNpqCCrCsCtsuCCuvCpv = D[13][27]
-[34] CpCqCrp = D[21]D[13][10]
-[35] CCCCCCpqCrqsNttCut = D[0]D[21]DDD1[6]1D[6][10]
-[36] CCCCCNpqrCsrtCpt = DD[13]D1DDD[17]D[3]D[3]D1[11]1[0]1
-[37] CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy = D[13]D1D[13][29]
-[38] CCCCCpqrCsrtCqt = DD[13]DD[3]D[13]1[25]1
+[30] CCNpCCNqrCCsCtsuCCupCqp = D1[29]
+[31] CCCCNpqCrqpCsp = D[0]D[19]DD[3][8][3]
+[32] CCpqCpq = D[7][26]
+[33] CCCNpqCCrCsCtsqCCquCpu = D[3][28]
+[34] CpCCpqCrq = DD[1]DDD[3]D[3]D1[8][3][13][0]
+[35] CCCNCNpqrsCps = D[0]D[12]D[0]DD[14][5][13]
+[36] CCCNpqCCrCsCtsuCCuvCpv = D[13][28]
+[37] CpCqCrp = D[22]D[13][10]
+[38] CCCCCNpqrCsrtCpt = DD[13]D1DDD[17]D[3]D[3]D1[11]1[0]1
+[39] CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy = D[13]D1D[13][30]
+[40] CCCCCpqrCsrtCqt = DD[13]DD[3]D[13]1[26]1
 
 % Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 127 steps
-[39] CpCNpq = D[22]D[7][25]
-
-[40] CCCpCqrsCrs = DD1[25]DD[15][6][13]
+[41] CpCNpq = D[23][32]
 
 % Identity principle (Cpp), i.e. 0→0 ; 135 steps
-[41] Cpp = DD[22]D[0][32]1
+[42] Cpp = DD[23]D[0][34]1
 
-[42] CCNpCCNqrCCsstCCtpCqp = D1[41]
-[43] CNNCpqCrCpq = DD[30]DD[6]D[3]D1[13]D[30]D[1]DD[0]D[12]D[0]DD[14][5][13]DD[0]DDD[3]D[3]D1D[6][3][13][13][12]1
-[44] CCpNCCqCrqpCsNCCqCrqp = D[29][43]
-[45] CCNCCpCqpNrsCrs = D[19][44]
-[46] CpCqCrNCCsCtsNp = D[45][34]
-[47] CCCpqCNprCsCNpr = D[23]D[38]D[20]D[22]D[33]D[22][44]
-[48] CpCCNCqrrCqr = DD[42]D[21]D[36]D[16][45][30]
-[49] CCCpCqpNCNNCNrrsCtr = DD[31]D[42]D[22][46][25]
-[50] CCpNpCqNp = D[23]D[38]D[20]DD[22]D[42]D[45][32]1
-[51] CCpqCNNpq = DD[35]DD[31]D[42]D[22]D[13][46][32]1
-[52] CCNNpqCpq = D[31][50]
-[53] CCCpqrCNpr = DDD[42]D[38]D[20]D[22]D[33]D[13]D[22]D[42][43][20]1
-[54] CCpNCNppCqNCNpp = D[23]DD[30]D[20]D[21][49]1
-[55] CpCqCrNNp = D[22]D[42]D[21]DD[31]D[42]D[21][46][24]
-[56] CpCqCrNNCNps = D[22][55]
+[43] CCNpCCNqrCCsstCCtpCqp = D1[42]
+[44] CNNCpqCrCpq = DD[31]DD[6]D[3]D1[13]D[31]D[1]D[35]DD[0]DDD[3]D[3]D1D[6][3][13][13][12]1
+[45] CCpNCCqCrqpCsNCCqCrqp = D[30][44]
+[46] CCNCCpCqpNrsCrs = D[20][45]
+[47] CCpNCCqqpCrNCCqqp = D[43][44]
+[48] CpCqCrNCCsCtsNp = D[46][37]
+[49] CCCpqpCrp = D[43]D[22]D[38]D[16][46]
+[50] CCpqCCCrrNNpq = D[33]D[43]DD[33][47][25]
+[51] CCCpqCNprCsCNpr = D[24]D[40]D[21]D[23]D[36]D[23][45]
+[52] CCCpCqpNCNCrNCNsstCus = DD[33]D[43]D[22]D[23][48][26]
+[53] CCpNpCqNp = D[24]D[40]D[21]DD[23]D[43]D[46][34]1
+[54] CCpCqNpCrCqNp = D[43]D[22]DD[33]D[43]D[22][48][25]
+[55] CCCpqrCNpr = DDD[43]D[40]D[21]D[23]D[36]D[13]D[23][47][21]1
+[56] CpCqCrNNp = D[23][54]
+[57] CCpCqNCNppCrCqNCNpp = D[43]DD[31]D[21]D[22][52]1
 
-% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 2177 steps
-[57] CCNppp = D[52]DD[35][49]1
+% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 1649 steps
+[58] CCNppp = D[46]DDD[0]D[22]DDD1[6]1[18][52]1
 
-[58] CCNpqCNCrpq = D[37]D[23]D[51]D[21][55]
-[59] CCNpqCNCrCspq = D[37]D[23]D[51]D[40][55]
-[60] CCpqCCNppq = DD[13]D1[1]D[23]DD[37]DD[37]D[23]D[51]DD[37][54][34]D[53][54][34]
-[61] CCNCpqrCCrqCpq = DD[60][40]D[59]1
-[62] CNCpqCrCsp = DDDD[42][48][52]DD[23]DD[37]D[23]D[51][56][34]D[51]D[23]D[58][34]D[59]DD[47]DD[0]DD[14][6][13][12]1
-[63] CCpCpqCrCpq = D[23][62]
-[64] CpCCqCqrCqr = D[63][63]
-[65] CCpCpqCpq = D[64][64]
-[66] CCpqCCNqpq = D[23]DDD[13][23]D[60]D[38][65][60]
-[67] CCpCqCprCqCpr = D[65]D[23]D[58][62]
-[68] CpCCpqq = DD[67]D[18][15]DD[29][48][65]
+[59] CCNpqCNCrpq = D[39]D[24]D[22]DD[33]D[43]D[46]D[22][18]D[22][56]
+[60] CNCpqCrCsp = DD[31]D[21]DD[31]D[21]DD[49]D[43]DD[51]D[23]DD[0]DD[14][3]DD[13]D1D[17]D[9][4]1[17]1111
+[61] CCNpqCNCrCspq = D[39]D[24]D[22]D[50]D[22]D[13][56]
+[62] CCpCpqCrCpq = D[24][60]
+[63] CCpqCCNppq = DD[13]D1[1]D[24]DD[39]DD[39]D[24]D[22]D[50]D[23][57]DD[31]D[21]DD[57]D[35][32]11[37]
+[64] CpCCqCqrCqr = D[62][62]
+[65] CCNCpqrCCrqCpq = DD[63]DD1[26]DD[15][6][13]D[61]1
+[66] CCpCpqCpq = D[64][64]
+[67] CCpCqCprCqCpr = D[66]D[24]D[59][60]
+[68] CCpqCCNqpq = D[24]DDD[13][24]D[63]D[40][66][63]
+[69] CpCCpqq = DD[67]D[19][15]DD[30]D[49][31][66]
 
-% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 180451 steps
-[69] CCpqCCqrCpr = DDD1D[37]D[23]DD[65][47]D[36]D[16][50]D[28]D[60][68][61]
+% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 39253 steps
+[70] CCpqCCqrCpr = DDD1D[39]D[24]DD[51]D[38]D[16][53]1D[29]D[63][69][65]
 
-% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 182879 steps
-[70] CCNpNqCqp = D[52]D[67]DD[66]D[21]D[22][45]D[58]D[65]DD[37]D[23][56][59]
+% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 51239 steps
+[71] CCNpNqCqp = DD[33][53]D[67]DD[68]D[22]D[23][46]D[59]D[66]DD[39]D[24]D[35][54][61]
 
-[71] CCCCpqCrqsCCrps = D[69][69]
-[72] CCpCqrCqCpr = D[71]D[69][68]
+[72] CCCCpqCrqsCCrps = D[70][70]
+[73] CCpCqrCqCpr = D[72]D[70][69]
 
-% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 2762055 steps
-[73] CCpCqrCCpqCpr = D[72]D[71]D[61]DD[72]D[53][66]D[72]D[71][53]
+% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 614905 steps
+[74] CCpCqrCCpqCpr = D[73]D[72]D[65]DD[73]D[55][68]D[73]D[72][55]