found 19 shorter proofs for minimal 1-base proof minimization challenge

- solution from #2 (comment) (discussions)
- m:(A2:7001↦5401,L1:619↦459)
- w1:A2:1925↦1763
- w2:(A2:1264633↦27599,A3:1153↦1007,L1:588991↦11703,L2:405↦367)
- w3:(A2:254925↦14557,A3:23321↦4821,L1:16469↦3227,L2:1331↦1283)
- w4:(A2:13917↦13819,A3:10779↦10719,L1:12081↦11989,L2:1709↦1703)
- w5:(A1:83↦75,A2:157↦153)
- w6:(A2:18339↦10343,L1:2743↦1821)

data/m.txt

@@ -7,50 +7,52 @@
 % Full summary: pmGenerator --transform data/m.txt -f -n -t . -j 1
 % Step counting: pmGenerator --transform data/m.txt -f -n -t . -p -2 -d
 %                pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
-% Compact (672 bytes): pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCppqCrq,CCCpqrCqr,CCCpNCCCqrCNNqrNstCst,CCpCpqCrCpq,CCCpCqNCCrCNNssNqtCut,CCpqCCrpCrq
-% Concrete (8170 bytes): pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
+% Compact (785 bytes): pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCppqCrq,CCCpqrCqr,CpCNNCCqCNNrrss,CCCpNCCCqrCNNqrNstCst,CCpCpqCrCpq,CCpqCCCrCNNssNNpq,CCpqCCrpCrq
+% Concrete (6410 bytes): pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
 
     CCCCCpqCNrNsrtCCtpCsp = 1
 [0] CCCCpqCrqCqsCtCqs = D11
 [1] CCCpCNqrsCqs = D1[0]
 [2] CCCppqCrq = D1[1]
 [3] CpCqCrq = D[0][2]
+[4] CCCpCqprCsr = D1[3]
 
 % Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 13 steps
-[4] CpCqp = D[3]1
+[5] CpCqp = D[3]1
 
-[5] CpCqCrr = D[2][2]
-[6] CCCpqrCqr = D1D1[5]
+[6] CpCqCrr = D[2][2]
+[7] CCCpqrCqr = D1D1[6]
 
 % Identity principle (Cpp), i.e. 0→0 ; 19 steps
-[7] Cpp = DD[5]11
+[8] Cpp = DD[6]11
 
-[8] CpCCpqCrq = D[6]1
-[9] CCCpqCrCNNqsCtCrCNNqs = D1D1D[4][1]
-[10] CCpqCCCNCCCCCrsCNtNutvCCvrCurwCNqNNpq = DDD1D1DD1[3]111
-[11] CpCCCCqrsCNCqrNCCtqCuqCqr = DD1D1[8][0]
+[9] CCCCNpNqprCqr = D1[7]
+[10] CpCCpqCrq = D[7]1
+[11] CCCpqCrCNNqsCtCrCNNqs = D1D1D[5][1]
+[12] CCpqCCCNCCCCCrsCNtNutvCCvrCurwCNqNNpq = DDD1D1D[4]111
+[13] CpCCCCqrsCNCqrNCCtqCuqCqr = DD1D1[10][0]
 
 % Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 41 steps
-[12] CpCNpq = DD1[6][6]
+[14] CpCNpq = D[9][7]
 
-[13] CCCpNCCCqrCNNqrNstCst = D1D1D[2]D1D[0]D[10]D1D[9]1
-[14] CCpCpqCrCpq = DDD1D1D1D[2][13]11
-[15] CCCpCqNCCrCNNssNqtCut = D1D1DD1DD1D[11]1D1D1D[2]D1D[0]D[10]D1DD1DD1D1D[2]1[4][0]D[1][0]
+[15] CpCNNCCqCNNrrss = D[0]D[12]D1DD1DD1D1D[2]1[5][0]
+[16] CCCpNCCCqrCNNqrNstCst = D1D1D[2]D1D[0]D[12]D1D[11]1
+[17] CCpCpqCrCpq = DDD1D1D1D[2][16]11
 
 % Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 163 steps
-[16] CCNppp = DD[14]DDD1D1D[9]D[6][8]111
+[18] CCNppp = DD[17]DDD1D1D[11]D[7][10]111
 
 % Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 175 steps
-[17] CCNpNqCqp = DDDDD1D1D[8]D[6]D[13][1]11DD1D1[11][4]1
+[19] CCNpNqCqp = DDDDD1D1D[10]D[7]D[16][1]11DD1D1[13][5]1
 
-[18] CCpCpqCpq = DD[14][14]1
-[19] CCpqCCCrCNNssNNpq = D1D[18][15]
+[20] CCpCpqCpq = DD[17][17]1
+[21] CCpqCCCrCNNssNNpq = DDD1D1DD1DD1D[2][9]111DDDD1D1DD1D1D1D[2]D1D[0]DDDD1D1DD1DD1D[4]D1DD1D1D[1]1D1[2]1111[2]D[1][10]11D[15]1
 
-% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 619 steps
-[20] CCpqCCqrCpr = DD1D[19][19]1
+% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 459 steps
+[22] CCpqCCqrCpr = DD1D[21][21]1
 
-[21] CCCCpqCrqsCCrps = D[20][20]
-[22] CCpqCCrpCrq = DD[20]DD1DD1[15]1[18][21]
+[23] CCCCpqCrqsCCrps = D[22][22]
+[24] CCpqCCrpCrq = DD[22]DD1DD1D1D1DD1DD1D[13]1D1D1D[2]D1[15]D[1][0]1[20][23]
 
-% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 7001 steps
-[23] CCpCqrCCpqCpr = DD[22][21]D[21]D[22][18]
+% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 5401 steps
+[25] CCpCqrCCpqCpr = DD[24][23]D[23]D[24][20]

data/w1.txt

@@ -7,59 +7,56 @@
 % Full summary: pmGenerator --transform data/w1.txt -f -n -t . -j 1
 % Step counting: pmGenerator --transform data/w1.txt -f -n -t . -p -2 -d
 %                pmGenerator --transform data/w1.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
-% Compact (1068 bytes): pmGenerator --transform data/w1.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCNpCCqrpCrp,CCCCpCCNpqrstCst,CCCpqrCqr,CpCCNqCrqCrq,CpCCNqCCNrsqCrq,CCCCNNpCpNpqrCpr,CCNpCqpCrCCNsCpsCqs,CCCCpqCrqsCCrps,CCCCNpCqpprCqr
-% Concrete (3144 bytes): pmGenerator --transform data/w1.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
+% Compact (1008 bytes): pmGenerator --transform data/w1.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCNpCCqrpCrp,CCCCpCCNpqrstCst,CCCpqrCqr,CpCCNqCCNrsqCrq,CCpqCpq,CCCCNNpCpNpqrCpr,CCNpCqpCrCCNsCpsCqs,CCCCNpCqpprCqr
+% Concrete (2982 bytes): pmGenerator --transform data/w1.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
 
     CCpCCNpqrCsCCNtCrtCpt = 1
 [0] CpCCNqCCCNrCsrCtrqCCtCCNtusq = D11
 [1] CpCCNqCCCrCCNrstuqCuq = D1[0]
 [2] CpCCNqCCrsqCsq = D1[1]
-[3] CCNpCCCqCCNqrstpCtp = D[1]1
-[4] CCNpCCqrpCrp = D[2]1
-[5] CCCCNpCqpCrpsCCrCCNrtqs = D[4][0]
-[6] CCCCpCCNpqrstCst = D[4][1]
-[7] CCCpqrCqr = D[4][2]
-[8] CCCNCpCCNpqrstCuCCNvCtvCCpCCNpqrv = D[6]1
-[9] CCCNpqrCsCCNtCrtCpt = D[7]1
-[10] CpCCNqCrqCCNrCCCNsCCCNtCutCvtsCCvCCNvwusrq = D1DD[8][0]1
-[11] CpCCNqCrqCCNrCCCNsCCtusCusrq = D1DD[8][2]1
-[12] CpCCNqCrqCrq = D1D[7][5]
-[13] CpCCNqCCNrsqCrq = D1DDD[9]11[2]
-[14] CpCqCCNrCprCCsCCNstur = D[6][8]
+[3] CCNpCCqrpCrp = D[2]1
+[4] CCCCNpCqpCrpsCCrCCNrtqs = D[3][0]
+[5] CCCCpCCNpqrstCst = D[3][1]
+[6] CCCpqrCqr = D[3][2]
+[7] CCCNCpCCNpqrstCuCCNvCtvCCpCCNpqrv = D[5]1
+[8] CCCNpqrCsCCNtCrtCpt = D[6]1
+[9] CpCCNqCrqCCNrCCCNsCCCNtCutCvtsCCvCCNvwusrq = D1DD[7][0]1
+[10] CpCCNqCrqCrq = D1D[6][4]
+[11] CpCCNqCCNrsqCrq = D1DDD[8]11[2]
+[12] CpCqCCNrCprCCsCCNstur = D[5][7]
 
 % Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 33 steps
-[15] CpCqp = D[7][6]
+[13] CpCqp = D[6][5]
 
-[16] CCNpCqpCqp = D[12]1
-[17] CCpqCCNpCCCNrCCCNsCtsCusrCCuCCNuvtrpq = D[4][10]
-[18] CpCqCCNrCprCsr = D[6][9]
-[19] CCpqCpq = D[4][12]
-[20] CCCNpqrCpr = D[4][13]
-[21] CpCqCCNrCsrCNpr = D[20]1
+[14] CCpqCCNpCCCNrCCCNsCtsCusrCCuCCNuvtrpq = D[3][9]
+[15] CpCqCCNrCprCsr = D[5][8]
+[16] CCpqCpq = D[3][10]
+[17] CCCNpqrCpr = D[3][11]
+[18] CCCCNpCqpCCrCCNrstpuCqu = D[3]D1[12]
+[19] CpCqCCNrCCsprCtr = D[6][15]
 
 % Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 87 steps
-[22] CpCNpq = D[20][19]
+[20] CpCNpq = D[17][16]
 
-[23] CCCCNNpCpNpqrCpr = D[4]D1D[6]D[6]D[5]D[5][7]
-[24] CCNpCqpCrCCNsCpsCqs = DD[4]D[9]DD[10]1[10][9]
-[25] CpCCpNpq = D[23][7]
+[21] CCCCNNpCpNpqrCpr = D[3]D1D[5]D[5]D[4]D[4][6]
+[22] CCNpCqpCrCCNsCpsCqs = DD[3]D[8]DD[9]1[9][8]
+[23] CpCCpNpq = D[21][6]
+[24] CCCCNpCqpCrpsCCNqCrqs = D[3]D1[22]
+[25] CCCCNpCqpCrpsCCrqs = D[3]D1D[6][22]
 
 % Identity principle (Cpp), i.e. 0→0 ; 143 steps
-[26] Cpp = DD[13]1[25]
+[26] Cpp = DD[11]1[23]
 
 % Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 151 steps
-[27] CCpqCCqrCpr = D[7]DD[4]D1[24][7]
+[27] CCpqCCqrCpr = D[6]D[24][6]
 
-[28] CNpCpq = D[23]D[4]D[9][15]
-[29] CCCCpqCrqsCCrps = D[4]D[9]DD[4][11][27]
-[30] CCCCNpCqpCCrCCNrstpuCqu = D[4]D1[14]
-[31] CCCCNpCqpprCqr = D[4]D1D[30]D[5]D[4]D[14][28]
+[28] CCCCNpCqpprCqr = D[3]D1D[18]D[4]D[3]D[12]D[21]D[3]D[8][13]
 
 % Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 323 steps
-[32] CCNppp = D[4]D[31][19]
+[29] CCNppp = D[3]D[28][16]
 
 % Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 343 steps
-[33] CCNpNqCqp = DDD1DD[4]D1D[7][24]D[4]DD[7][18][25]1[13]
+[30] CCNpNqCqp = DDD1D[25]D[3]D[19][23]1[11]
 
-% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 1925 steps
-[34] CCpCqrCCpqCpr = DD[29]D[4]D1D[30]DD[4]D[9]D[17][7]D[5]D[4]D[18][28]D[29]DD[16]DD[4]D[3]DD[4]D1DDD[18]D[6]D[7]D[5][22]1[11]D[7]D[7][21]D[31][7]DD[4]D[3]DD[4]D[9]D[4]D1DD[4]D1[18]DDD[9]D[4]D[9]D[16]D[20][17]1[0][21]D[6]D[6]DD[4]D1DD[4]D[8]DD[4]D1D[17]1[7]1[7]
+% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 1763 steps
+[31] CCpCqrCCpqCpr = DD[25]D[3]D1D[28]D[6]D[5]D[6]D[4]D[3]D[15][2]DD[3]D[8]DD[3]D1DD[7][2]1[27]DDDD1D[6]D[24]D[3]D[19][20]1D[18]D[4]DD[3]D1D[3]DD[6][12]D[6][13][16]DD[3]DD[1]1DD[3]D[8]D[3]D1DD[3]D1[15]DDD[8]D[3]D[8]DD[10]1D[17][14]1[0]D[17]1D[5]D[5]DD[3]D1DD[3]D[7]DD[3]D1D[14]1[6]1[6]

data/w2.txt

@@ -7,119 +7,73 @@
 % Full summary: pmGenerator --transform data/w2.txt -f -n -t . -j 1
 % Step counting: pmGenerator --transform data/w2.txt -f -n -t . -p -2 -d
 %                pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
-% Compact (3083 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps,CpCqCrCsCtq,CpCqCrCNps,CCCNpqrCCNCpsCCNtuNrCtCps,CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq,CpCqCrp,CpCqCrCsCtp,CpCNCqCNprs,CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq,CCNCpCqrrCpCqr,CNCpCqNrCsCtCur,CNNpCqCrCsp,CCNpCCNNqrqCNqp,CCNCCpqqCCNrspCrCCpqq,CNCpCqrCsNr,CCNCpCqrCCNstCNrCCNquCprCsCpCqr,CCpqCpCrq,CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq,CCNCCpqqpCCpqq,CCNppCCpqq,CCCpqrCqr,CCpCqCprCqCpr,CCCpqCrpCrp,CCpCqCrNpCqCrNp,CCNpCqCrpCqCrp,CCpCNCpqrCNCpqr,CCpCNNpqCNNpq,CCNNCpqpp,CpCCpqCrq,CpCqCCprCsr,CCNpCCpqqCCpqq,CCpNqCpCqr,CNCCpqCprq,CCpqCpCCqrr,CCNCpqrCCrqCpq
-% Concrete (1855466 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
+% Compact (1620 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps,CCpCCqCrCsCtquCCNuCCNvwpCvu,CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq,CpCCNqCCNCrCNpstNCuCCvCuwCCNwCCNxyvCxwq,CpCCNqCCNrsCpqCrq,CCpCCqCCNrCCNCsCNqtuNCvCwCCxCwyCCNyCCNzaxCzyrbCCNbCCNcdpCcb,CNCpCqNrCsCtCur,CCNCCpqCrqCCNstCNqCCNrupCsCCpqCrq,CCNCCpqqpCCpqq,CCpCqCprCqCpr,CCpqCCNppq,CCpCqrCCqpCqr,CCpCqrCpCqCsr
+% Concrete (40960 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
 
     CpCCqCprCCNrCCNstqCsr = 1
 [0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
 [1] CCNCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqpCCNwxCsCvpCwCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqp = D[0]1
 [2] CCNCpqCCNrsCCCNtCCNuvNpCutCCwCCxCwyCCNyCCNzaxCzyqCrCpq = D[0][0]
 [3] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = DD1[0]1
 [4] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = D[1]1
-[5] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DD[4]11
-[6] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[5]
-[7] CCNCpqCCNrsCCtpCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[6][0]
-[8] CCpqCCNCCNqCCNrstCrqCCNuvpCuCCNqCCNrstCrq = D[1][5]
-[9] CCCpCCqCprCCNrCCNstqCsruCvu = D[2][5]
-[10] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[3][5]
-[11] CCNpCCNqrCCsCCtCsuCCNuCCNvwtCvupCqp = D[0][9]
-[12] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][10]
-[13] CCNCCNCpCqrCCNstCCNquvCsCpCqrCCNwxCNCqrCCNpyCvCCzCCaCzbCCNbCCNcdaCcbrCwCCNCpCqrCCNstCCNquvCsCpCqr = DD1[10]1
-[14] CCNCCNpCCNqrsCqpCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaNsCtCCNpCCNqrsCqp = DD1D[7]11
+[5] CCNCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqpCCNzasCzCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqp = D[4]1
+[6] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = D[5]1
+[7] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[6]
+[8] CCNCpqCCNrsCCtpCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[7][0]
+[9] CCpqCCNCCNqCCNrstCrqCCNuvpCuCCNqCCNrstCrq = D[1][6]
+[10] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[3][6]
+[11] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][10]
+[12] CCNCCNpCCNqrsCqpCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaNsCtCCNpCCNqrsCqp = DD1D[8]11
 
 % Identity principle (Cpp), i.e. 0→0 ; 35 steps
-[15] Cpp = D[11][5]
+[13] Cpp = DD[0]D[2][6][6]
 
-[16] CCNpCCNCqCCrCqsCCNsCCNturCtsvNwCwCxp = D[12][5]
-[17] CCCNpqCrCCsCCtCsuCCNuCCNvwtCvuxCCNCpCyxCCNzaCCNybrCzCpCyx = D[13][5]
-[18] CNpCCNqCCNrspCrq = D[14][5]
-[19] CCpCCqqrCCNrCCNstpCsr = D1[15]
-[20] CCNCCNpCCNqrCspCqpCCNtusCtCCNpCCNqrCspCqp = D[19]1
-[21] CpCqCCCNqrsCts = DD[17]11
-[22] CCNCCNpCCNqrCspCqpCCNtuCNCCNpCCNqrCspCqpCCNCvCCwCvxCCNxCCNyzwCyxasCtCCNpCCNqrCspCqp = D[0][20]
-[23] CpCqCrCsCtq = DDDDD1DD[0][3][5]1[5]11
-[24] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[23]1
-[25] CpCqCrCNps = D[2][21]
-[26] CCNCpCNqrCCNstqCsCpCNqr = D[0][25]
-[27] CCCNpqrCCNCpsCCNtuNrCtCps = DDD1[18]1[5]
-[28] CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq = D[7]DD[0]DDD1DDD1[3]111[5]1
+[14] CCNpCCNCqCCrCqsCCNsCCNturCtsvNwCwCxp = D[11][6]
+[15] CCCNpqCrCCsCCtCsuCCNuCCNvwtCvuxCCNCpCyxCCNzaCCNybrCzCpCyx = DDD1[10]1[6]
+[16] CNpCCNqCCNrspCrq = D[12][6]
+[17] CCpCCqqrCCNrCCNstpCsr = D1[13]
+[18] CCNCCNpCCNqrCspCqpCCNtusCtCCNpCCNqrCspCqp = D[17]1
+[19] CpCqCrCsCtq = DDDDD1DD[0][3][6]1[6]11
+[20] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[19]1
+[21] CCNCpCNqrCCNstqCsCpCNqr = D[0]D[2]DD[15]11
+[22] CCCNpqrCCNCpsCCNtuNrCtCps = DDD1[16]1[6]
+[23] CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq = D[8]DD[0]DDD1DDD1[3]111[6]1
 
 % Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 53 steps
-[29] CpCqp = DD[24][0]1
+[24] CpCqp = DD[20][0]1
 
-[30] CCpCCqCrqsCCNsCCNtupCts = D1[29]
-[31] CCCNCpCCqCprCCNrCCNstqCsruvCCNwCCNxyCvwCxw = D[22][5]
-[32] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[10][16]
+[25] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[10][14]
 
 % Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 57 steps
-[33] CpCNpq = D[32]1
+[26] CpCNpq = D[25]1
 
-[34] CCpCCqCrCNsCCNtCCNuvsCutwCCNwCCNxypCxw = D1DD[0]DD[8][14][5]1
-[35] CCpCCqCCrCqsCCNsCCNturCtsvCpCwCxv = DD[6][17][5]
-[36] CpCqCNCrps = D[26][5]
-[37] CCNCNCpqrCCNstqCsCNCpqr = D[0][36]
-[38] CpCqCrp = DD[0][12][23]
-[39] CCNpCCNqrNsCsCqp = DD[0][31][5]
-[40] CpCqCrCsCtp = DD[0]DDD1DDD1D[21]1111[5][5]
-[41] CpCNCqCNprs = D[11]DD[6]DDD1[25]111
-[42] CpCCNqCCNrsCpqCrq = D[22][28]
-[43] CCNCNpqCCNrspCrCNpq = D[0]DDD1[38][0]D[12]1
-[44] CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq = D[32]DD[0][4]DD[0]DDD1DDD1[9]111[5]1
-[45] CCpCCqCCNrCCNCCNsCCNtuNCNqvCtswNCxxryCCNyCCNzapCzy = D1[44]
-[46] CCNCpCqrrCpCqr = DD[0]DDD[6]DD[0][13][5][5]DD[0]DD[0]D[8]1[5][5][5]
-[47] CNCpCqNrCsCtCur = DD[34]DDD1[24]1[5][5]
-[48] CNNpCqCrCsp = DD[34]DDD1[30]1[5][5]
-[49] CCNpCCNNqrqCNqp = DDDD1[41]1[29]1
-[50] CCNCCpqqCCNrspCrCCpqq = D[45][42]
-[51] CNCpCqrCsNr = DD[43][47]1
-[52] CpCCpqq = D[50][44]
-[53] CCNCpCqrCCNstCNrCCNquCprCsCpCqr = D[45]DDD1[42]1[44]
-[54] CCpqCpCrq = D[53][28]
+[27] CpCCNqCCNCrCNpstNCuCCvCuwCCNwCCNxyvCxwq = D[25]DDD[0][7][6][5]
+[28] CpCCNqCCNrsCpqCrq = DD[0][18][23]
+[29] CCpCCqCCNrCCNCsCNqtuNCvCwCCxCwyCCNyCCNzaxCzyrbCCNbCCNcdpCcb = D1D[25]DD[0]DD[7]DDD1[4]1[6]11
+[30] CNCpCqNrCsCtCur = DDD1DD[0]DD[9][12][6]1DDD1[20]1[6][6]
+[31] CCNCCpqqCCNrspCrCCpqq = D[29][28]
+[32] CCNCpCqrCCNstCNrCCNquCprCsCpCqr = D[29]DDD1[28]1[27]
 
-% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 405 steps
-[55] CCNppp = DDD[20][51]1[44]
+% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 367 steps
+[33] CCNppp = DDD[18]DDD[0]D[2]DDD1[19]DDD1[11]111[30]11[27]
 
-[56] CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq = D[45]DDD1[55]1[44]
-[57] CpCCNCpqCpqq = D[56][44]
-[58] CCpqCrCpCsq = D[54][54]
-[59] CpCCNCNqqCNqqq = D[56]DDD[0]DD[0][26][5][47]1
-[60] CpCCNCNqCrqCNqCrqCrq = D[56][51]
-[61] CCNpNqCCNpCCNrsqCrp = DDD1DDD1[57][15]11[44]
-[62] CCNCCpqqpCCpqq = D[50][57]
-[63] CCNppCCpqq = D[50][59]
-[64] CCCpqrCqr = DDD[45][19][44]DDDDDD1DDD1[6]1[5]1[5]1[5][57]
-[65] CpCCNqqCCqrr = D[29][63]
-[66] CCpCqCprCqCpr = D[62]DD[37]DD[0]DDD1[27]1[5][5]1
+[34] CCNCCNCpqCpqqCCNrspCrCCNCpqCpqq = D[29]DDD1[33]1[27]
+[35] CCNCCpqCrqCCNstCNqCCNrupCsCCpqCrq = D[29]DDD1DDD1D[31][27]1[27]1[27]
+[36] CCCNpqrCCrsCps = D[35][6]
+[37] CpCCNCpqCpqq = D[34][27]
+[38] CCNpCCNqrsCCspCqp = D[35][27]
+[39] CCNCCpqqpCCpqq = D[31][37]
 
-% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 1153 steps
-[67] CCNpNqCqp = DD[45][61][44]
+% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 1007 steps
+[40] CCNpNqCqp = DD[29]DDD1DDD1[37][13]11[27][27]
 
-[68] CCCpqCrpCrp = D[62]DDD1DD[0][8][5]D[27][16][28]
-[69] CCpCqCrNpCqCrNp = D[62]D[49][40]
-[70] CCNpCqCrpCqCrp = D[62]D[49]D[35][48]
-[71] CCpCqNpCqNp = D[69][52]
-[72] CCpCNCpqrCNCpqr = D[62]D[68][41]
-[73] CCCCpqqCprCpr = D[66]D[50][65]
-[74] CCpCNNpqCNNpq = DDD[0][29][60]D[50]DDD[0][38][60]D[50]DDDD[0]DD[8]D[0][18][5][38]1DDD1[36][31][5]
-[75] CCNNCpqpp = D[68]D[50]D[39]D[56]D[29]DD[0]DD[0]D[30][18][28][59]
-[76] CpCCpqCrq = D[73][58]
-[77] CpCqCCprCsr = D[54][76]
-[78] CCNpCCpqqCCpqq = D[62]D[71]D[37][65]
-[79] CNCpqCCNCprCprr = D[56]D[29][75]
-[80] CCpqCpCNqr = D[26][79]
-[81] CNNpCCpqCrq = D[74][77]
-[82] CCpqCNCprq = D[66]D[72][77]
-[83] CCpNqCpCqr = D[70]D[82]D[39][79]
-[84] CNCCpqCprq = DD[78]DDD[0][40][79]DD[43][57]D[69]D[80]DD[53][5][75]D[80][83]
-[85] CNCCpqCprCsq = D[54][84]
-[86] CNCCpqCprCsCtq = D[35][85]
-[87] CCpqCpCCqrr = D[46]DD[64][50]D[78]D[74][86]
-[88] CCNCpqrCCrqCpq = D[70]DDDDD[53][44][57][76]DDD[66][81]D[46]D[87]D[67]DD[64]D[0]DDD1[48][0]1DD[66]DD[66][63][77]DD[66]D[73][77][83]DDD[69]D[49][85]D[69]D[49][86]D[49]D[54]DD[66]D[50]D[29]D[71]DDD[6][61][44]D[49]D[54][52]D[72]D[54][82][77]
-[89] CCpCqrCCqpCqr = D[88][84]
-[90] CCpCqrCpCqCsr = D[89][58]
+[41] CCpCqCprCqCpr = D[39]DDD[0]D[21][6]DD[0]DDD1[22]1[6][6]1
+[42] CCpqCCNppq = D[38]D[34]DDD[0]DD[0][21][6][30]1
+[43] CCpCqrCCqpCqr = D[38]D[34]D[24]DD[39]DDD1DD[0][9][6]D[22][14][23]D[31]D[24]DDD[29][17][27]D[39]DD[8]DDD[0][15][6]D[20][16]1
+[44] CCpCqrCpCqCsr = D[43]DD[0]DD[9]D[32][27][6][6]
 
-% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 588991 steps
-[91] CCpqCCqrCpr = D[66]D[90]DD[88]D[72][58][89]
+% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 11703 steps
+[45] CCpqCCqrCpr = D[41]D[44]DD[36]D[42]D[32][23][43]
 
-% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 1264633 steps
-[92] CCpCqrCCpqCpr = DD[91]D[66]D[90]DD[66]DDD[62]D[71]DD[62]DD[27][29][44]D[26][28]D[87][81][77][89][89]
+% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 27599 steps
+[46] CCpCqrCCpqCpr = DD[45]D[41]D[44]DD[36]D[42]D[35][23][43][43]