From 3dcaae430aec4ebdf50dd3aada174c23298070fe Mon Sep 17 00:00:00 2001 From: Samiro Discher Date: Tue, 2 Apr 2024 12:28:04 +0200 Subject: [PATCH] =?UTF-8?q?w3:(A2:2762055=E2=86=A6614905,A3:182879?= =?UTF-8?q?=E2=86=A651239,L1:180451=E2=86=A639253,L2:2177=E2=86=A61649)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - solution from https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-8980688 (discussions) - |22|->1401,|19|->2001,(squish & regenerate dProofs1897+),|19|->2391 - based on https://github.com/xamidi/pmGenerator/commit/8a231d7debc5ec9457481c315f546dc5262811fe --- data/w3.txt | 126 ++++++++++++++++++++++++++-------------------------- 1 file changed, 63 insertions(+), 63 deletions(-) diff --git a/data/w3.txt b/data/w3.txt index 70aebcc..a2b7dd5 100644 --- a/data/w3.txt +++ b/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]