Skip to content

Commit

Permalink
improvements via '--extract -l' script
Browse files Browse the repository at this point in the history 
Used formula length limits (|·|) and proof lengths (->·) as follows.
m: |20|->133,|15|->203 (steps of 10)
w1: |30|->211[,|15|->491+],|25|->265->275,|20|->327->337,|16|->413->425->433
    (steps of 20)
w2: |50|-|100|->139,|50|->177,|25|->277,|20|->313,|19|->339
    (steps of 10, but irregular for a few beginning |100|-steps)
w3: |40|->159[,|20|->309],|30|->225->231,|25|->249->257,|24|->265->271->277
    (steps of 10)
w4: |25|->261,|15|->495
    (steps of 20, steps of 10 since 419, steps of 8 since 479)
w5: |70|->111[,|30|->161],|50|->149,|40|->159 (steps of 10)
w6: |25|->149,|15|->327 (steps of 10)
s5: |15|->45,|12|->85 (steps of 5, steps of 4 since 69)
  • Loading branch information
@xamidi
xamidi committed Jan 29, 2024
1 parent d054305 commit a848c40
Show file tree
Hide file tree
Showing 8 changed files with 213 additions and 213 deletions.
42 changes: 22 additions & 20 deletions data/m.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@
% 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

CCCCCpqCNrNsrtCCtpCsp = 1
[0] CCCCpqCrqCqsCtCqs = D11
Expand All @@ -23,32 +25,32 @@
% Identity principle (Cpp), i.e. 0→0 ; 19 steps
[7] Cpp = DD[5]11

[8] CCCCNpNqprCqr = D1[6]
[9] CpCCpqCrq = D[6]1
[10] CCCpCNNqqrCsr = D1DD1DD1D1D[2]1[4][0]
[8] CpCCpqCrq = D[6]1
[9] CCCpqCrCNNqsCtCrCNNqs = D1D1D[4][1]
[10] CCpqCCCNCCCCCrsCNtNutvCCvrCurwCNqNNpq = DDD1D1DD1[3]111
[11] CpCCCCqrsCNCqrNCCtqCuqCqr = DD1D1[8][0]

% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 41 steps
[11] CpCNpq = D[8][6]
[12] CpCNpq = DD1[6][6]

[12] CpCCCqprCsr = D[6][9]
[13] CCpCpqCrCpq = DDD1D1DDDD1D1[12][9]1[12]11
[14] CCpCpqCpq = DD[13][13]1
[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]

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 315 steps
[15] CCNppp = D[14]DDD1D1DD1D1D[4][1][12]11
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 163 steps
[16] CCNppp = DD[14]DDD1D1D[9]D[6][8]111

[16] CCpqCCCrCNNssNNpq = D1D[14]D[12]DD1D1D[2]D1D[0]DDDD1D1DD1[3]111[10]D[14][10]
% 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

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 1287 steps
[17] CCpqCCqrCpr = DD1D[16][16]1
[18] CCpCpqCpq = DD[14][14]1
[19] CCpqCCCrCNNssNNpq = D1D[18][15]

[18] CCCCpqCrqsCCrps = D[17][17]
[19] CCCCpqqrCpr = D[17]DD[17][9][14]
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 619 steps
[20] CCpqCCqrCpr = DD1D[19][19]1

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 2861 steps
[20] CCNpNqCqp = D[19][8]
[21] CCCCpqCrqsCCrps = D[20][20]
[22] CCpqCCrpCrq = DD[20]DD1DD1[15]1[18][21]

[21] CCpqCCrpCrq = D[19][18]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 16225 steps
[22] CCpCqrCCpqCpr = DD[21][18]D[18]D[21][14]
% 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]
2 changes: 2 additions & 0 deletions data/s5.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@
% Full summary: pmGenerator --transform data/s5.txt -f -n -t . -j 1
% Step counting: pmGenerator --transform data/s5.txt -f -n -t . -p -2 -d
% pmGenerator --transform data/s5.txt -f -n -t CpLNLNp,CLpLLp,CLpNLNp,CpNLNp,CNLNNLpNLp -p -2 -d
% Compact (466 bytes): pmGenerator --transform data/s5.txt -f -n -t CpLNLNp,CLpLLp,CLpNLNp,CpNLNp,CNLNNLpNLp -j -1 -s CNNpCqp,CNNpp,CCpqCNqNp
% Concrete (971 bytes): pmGenerator --transform data/s5.txt -f -n -t CpLNLNp,CLpLLp,CLpNLNp,CpNLNp,CNLNNLpNLp -j -1 -e

% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0)
CpCqp = 1
Expand Down
74 changes: 38 additions & 36 deletions data/w1.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,58 +7,60 @@
% 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 (1074 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 (3166 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] 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] CCNpCCqCCNrCsrCNtrpCtp = DD[8]11
[10] CpCCNqCrqCCNrCCCNsCCCNtCutCvtsCCvCCNvwusrq = D1DD[7][0]1
[11] CCpCCNpqrCCrsCps = D[4][6]
[12] CpCCNqCrqCrq = D1D[6][4]
[13] CpCCNqCCNrsqCrq = D1D[9][2]
[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]

% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 33 steps
[14] CpCqp = D[6][5]
[15] CpCqp = D[7][6]

[15] CCNpCqpCqp = D[12]1
[16] CCpqCCNpCCCNrCCCNsCtsCusrCCuCCNuvtrpq = D[3][10]
[17] CCCNpqrCpr = D[3][13]
[18] CCCCNpCqpCrpsCqs = D[3]D1D[5][8]
[19] CCCNpqrCCrsCps = D[6][11]
[20] CpCCpqCrq = D[5][19]
[16] CCNpCqpCqp = D[12]1
[17] CCNpCCNqrpCqp = D[13]1
[18] CCpqCCNpCCCNrCCCNsCtsCusrCCuCCNuvtrpq = D[4][10]
[19] CpCqCCNrCprCsr = D[6][9]
[20] CCpqCpq = D[4][12]
[21] CCCNpqrCpr = D[4][13]
[22] CpCqCCNrCsrCNpr = D[21]1
[23] CCCCNpCqpCrpsCqs = D[4]D1[19]

% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 87 steps
[21] CpCNpq = D[17]D[3][12]
[24] CpCNpq = D[21][20]

[22] CCCCNNpCpNpqrCpr = D[3]D1D[5]D[5]D[4][11]
[25] CCCCNNpCpNpqrCpr = D[4]D1D[6]D[6]D[5]D[5][7]
[26] CCNpCqpCrCCNsCpsCqs = DD[4]D[9]DD[10]1[10][9]
[27] CpCCpNpq = D[25][7]

% Identity principle (Cpp), i.e. 0→0 ; 143 steps
[23] Cpp = DD[13]1D[22][6]
[28] Cpp = D[17][27]

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 151 steps
[24] CCpqCCqrCpr = D[6]DD[3]D1DD[3]D[8]DD[10]1[10][8][6]
[29] CCpqCCqrCpr = D[7]DD[4]D1[26][7]

[25] CpCCqrCCpqr = D[5]D[5]DD[3]D1DD[3]D[7]DD[3]D1D[16]1[6]1[6]
[26] CCCCpqCrqsCCrps = D[24][24]
[27] CCCpqrCNCspr = D[19]D[11]D[6]DD[19]D[3]D[8]D[15]D[17][16][9]
[28] CpCCpqq = DD[11]D[18]D[4]D[20]D[22]D[3]D[8][14][6]
[30] CNpCpq = D[25]D[4]D[9][15]
[31] CCCCpqCrqsCCrps = D[4]D[9]DD[4][11][29]
[32] CCCCNpCqpprCqr = D[4]D1DD[4]D1[14]D[5]D[4]D[14][30]

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 475 steps
[29] CCNppp = D[3]D[18]D[4]DD[11]DD[6][20][23][23]
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 323 steps
[33] CCNppp = D[4]D[32][20]

[30] CNCpqCrNq = D[15]DD[11]D[27][9]D[6][21]
[31] CCpCqrCqCpr = D[26]D[11]D[18]D[28]D[14][28]
[32] CCNpCqCrpCqCrp = D[15]DD[11]DD[11][30][30][28]
% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 363 steps
[34] CCNpNqCqp = DD[7]DD1DD[4]D1D[7][26]D[4]DD[7][19][27]1[17]

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 2753 steps
[33] CCNpNqCqp = D[31]D[17]D[32][25]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 3489 steps
[34] CCpCqrCCpqCpr = D[31]D[26]D[32]DD[11]D[15]D[27][21][25]
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 1927 steps
[35] CCpCqrCCpqCpr = DD[31]D[4]D1D[23]DD[4]D[9]D[18][7]D[5]D[4]D[19][30]D[31]DD[16]DD[4]D[3]DD[4]D1DDD[19]D[6]D[7]D[5][24]1[11]D[7]D[7][22]D[32][7]DD[4]D[3]DD[4]D[9]D[4]D1D[23]DDD[9]D[4]D[9]D[16]D[21][18]1[0][22]D[6]D[6]DD[4]D1DD[4]D[8]DD[4]D1D[18]1[7]1[7]
24 changes: 8 additions & 16 deletions data/w2.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,27 +7,19 @@
% 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,Cpp,CpCNpq -p -2 -d
% Compact & concrete (213 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CpCNpq -j -1

CpCCqCprCCNrCCNstqCsr = 1
[0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
[1] CCNCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqpCCNwxCsCvpCwCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqp = D[0]1
[2] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDD[1]111
[3] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][2]
[4] CpCqCCNpCCNrstCrp = DD[0]D[1][2][2]
[1] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDD[0]1111

% Identity principle (Cpp), i.e. 0→0 ; 35 steps
[5] Cpp = DD[0][3][2]
[2] Cpp = DD[0]DD[0][0][1][1]

[6] CpCqCCrCqsCCNsCCNturCts = DDD[4]111
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 53 steps
[3] CpCqp = DDD1DDDDDD1DD[0]DD1[0]1[1]1[1]111[0]1

% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 69 steps
[7] CpCqp = DD[0]DD[0]D[0][4][2][2]
[4] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = DDD1[0]1[1]

[8] CpCCNqCCNrsCCNptqCrq = DDD1[5][5][6]
[9] CCNCpCqrCCNstrCsCpCqr = D[0][8]
[10] CCNpCCNqrCCNCsstpCqp = D[8][5]
[11] CpCqCrCsp = D[9]D[10][6]
[12] CpCqCrCsCtCuCvs = D[11][11]

% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 2011 steps
[13] CpCNpq = D[10]DD[0]DDD1[0]1D[12][12]D[10]D[11]D[9]DDD1[2]DDD1[3]111
% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 57 steps
[5] CpCNpq = DD[4]DD[0][4][1]1
129 changes: 65 additions & 64 deletions data/w3.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +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 (2135 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCpCqrsCCqrs,CCCpqrCqr,CCCNpqrCpr,CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp,CCNppCqp,CpCCpqCrq,CpCqCrp,CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy,CCCCCpqrCsrtCqt,CCCpCqrsCrs,CpCNNCqrCsCqr,CCNCCppNqrCqr,CCNNpqCpq,CpCqCrNNp,CCpqCNNpq,CCNpqCNCrpq,CCNpqCNCrCspq,CCCpqCNprCsCNpr,CCpNCNppCqNCNpp,CNCpqCrCsp,CCpCpqCpq,CCpqCNCprq,CCCpqrCNpr,CCpqCCNppq,CpCCpqq,CCpqCCNqpq,CCpCqrCqCpr
% Concrete (20789800 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e

CpCCNqCCNrsCptCCtqCrq = 1
[0] CCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqp = D11
Expand All @@ -19,81 +21,80 @@
[7] CCCNpqCCCNrCCNstCCuCCNvCCNwxCuyCCyvCwvzCCzrCsrqCCqaCpa = D[3][1]
[8] CCCNpCCNqCCNrsCNptCCtqCrqCCCrqpCqpCCCCCrqpCqpuCvu = D[2][6]
[9] CCCCCpCCNqCCNrsCtuCCuqCrqvCCCNqCCNrsCtuCCuqCrqvwCxw = D[8][0]
[10] CCCpCqrsCCqrs = DD1[9]1
[11] CCCCCpCCqrCsrtCCCqrCsrtuCCuvCwv = D[5]D[3][4]
[12] CCCCCpqrCqrsCts = DD[10][0]1
[13] CCCCCCpqCrqsCtsuCqu = DD[10]DD[3]111
[14] CCpqCrCpq = D[10][9]
[15] CCCpqrCqr = DDD[12]D[3][2]1[0]
[16] CCCNpqrCpr = D[0]DD[8][1][10]
[17] CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp = D1D[5]D[3]DD[12]11
[18] CCNppCqp = D[0]D[16][0]
[10] CCCCCpCCqrCsrtCCCqrCsrtuCvu = D[8][1]
[11] CCCpCqrsCCqrs = DD1[9]1
[12] CCCCCpCCqrCsrtCCCqrCsrtCuCCCqrCsrtCCCuCCCqrCsrtvCwv = D[3]D[3][4]
[13] CCCCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpwCxCCqwCpwCCCxCCqwCpwyCzy = D[3]D[3]D1[6]
[14] CCCCCpqrCqrsCts = DD[11][0]1
[15] CCCCCCpqCrqsCtsuCqu = DD[11]DD[3]111
[16] CCpqCrCpq = D[11][9]
[17] CCCpqrCqr = DDD[14]D[3][2]1[0]
[18] CCCNpqrCpr = D[0]D[10][11]
[19] CCNpCCNqrCCCCCCstuCtuvCCvwCxwyCCypCqp = D1D[5]D[3]DD[14]11
[20] CCNppCqp = D[0]D[18][0]

% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 67 steps
[19] CpCqp = DDD[12][12]11
[21] CpCqp = DDD[14][14]11

[20] CCNpCCNqrCCsCtsuCCupCqp = D1[19]
[21] CCCCNpqCrqpCsp = D[0]D[13]DD[3][7][3]
[22] CCpqCrCsCpq = D[10][14]
[23] CpCCpqCrq = D[15][11]
[24] CpCqCNpr = D[16][14]
[25] CpCqCrp = D[15][19]
[26] CCNpCCNqrCCCCNstCCuCvuwCCwxCsxyCCypCqp = D1D[15][20]
[22] CCNpCCNqrCCsCtsuCCupCqp = D1[21]
[23] CCCCNpqCrqpCsp = D[0]D[15]DD[3][7][3]
[24] CpCCpqCrq = DD[1]DDD[3]D[3]D1[7][3][11][0]
[25] CCNpCCNqrCCCCNstCCuCvuwCCwxCsxyCCypCqp = D1D[11][22]
[26] CpCqCrp = D[17][16]
[27] CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy = D[11][25]
[28] CCCCCpqrCsrtCqt = DD[11]DD[3]D[11]1[20]1

% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 127 steps
[27] CpCNpq = D[16]D[6][18]
[29] CpCNpq = D[18]D[6][20]

[28] CpCqq = D[16]D[1][23]
[29] CCCpCqrsCrs = DD1[18]DD[11]1D[1]DDD[3]D[3]D1[7][3][10]
[30] CCCCCpqrCsrtCqt = DD1DD[3][14][18]D[14]1
[31] CCCNpqCCCCNrsCCtCutvCCvwCrwxCCxyCpy = D[15][26]
[30] CCCpCqrsCrs = DD1[20]DD[13][5][11]

% Identity principle (Cpp), i.e. 0→0 ; 283 steps
[32] Cpp = D[28][28]
% Identity principle (Cpp), i.e. 0→0 ; 135 steps
[31] Cpp = DD[18]D[0][24]1

[33] CCNpCCNqrCCsstCCtpCqp = D1[32]
[34] CpCNNCqrCsCqr = D[21]DD[29][26]D[21]D[1]DD[1]D[14][24]D[16][22]
[35] CCNCCppNqrCqr = D[31]D[33]D[34][34]
[36] CCCppNqCqr = D[16][35]
[37] CCNNpqCpq = D[31]D[17]D[15]DD[31]D[17]D[35][25][25]
[38] CpCqCrNNp = D[37][25]
[39] CpCqCrNNCNps = D[16][38]
[40] CCpqCNNpq = D[31]D[17][38]
[41] CCpqCNCNNprq = D[31]D[17][39]
[42] CpCNNCNqqq = D[18]D[41][18]
[43] CCNpqCNCrpq = D[31]D[17]D[40]D[15][38]
[44] CCNpqCNCNprq = D[31]D[17]D[40][39]
[45] CCNpqCNCrCspq = D[31]D[17]D[40]D[29][38]
[46] CCNpCqpCrCqp = D[17]D[43][25]
[47] CpCCNCqrrCqr = D[46][23]
[48] CCpqCCCrrpq = D[33][47]
[49] CCCpqCNprCsCNpr = D[17]D[44]D[30]D[23][36]
[32] CCNpCCNqrCCsstCCtpCqp = D1[31]
[33] CpCNNCqrCsCqr = D[23]DD[11]D[3][25]D[23]D[1]DD[0]D[10]D[0]DD[12]DD1[2]1[11]DD[0]DDD[3]D[3]D1D[5][3][11][11][10]
[34] CCNCCppNqrCqr = D[27]D[32]D[33][33]
[35] CCCppNqCqr = D[18][34]
[36] CCNNpqCpq = D[27]D[19]D[17]DD[27]D[19]D[34][26][26]
[37] CpCqCrNNp = D[36][26]
[38] CpCqCrNNCNps = D[18][37]
[39] CCpqCNNpq = D[27]D[19][37]
[40] CCpqCNCNNprq = D[27]D[19][38]
[41] CpCNNCNqqq = D[20]D[40][20]
[42] CCNpqCNCrpq = D[27]D[19]D[39]D[17][37]
[43] CCNpqCNCNprq = D[27]D[19]D[39][38]
[44] CCNpqCNCrCspq = D[27]D[19]D[39]D[30][37]
[45] CCNpCqpCrCqp = D[19]D[42][26]
[46] CpCCNCqrrCqr = D[45][24]
[47] CCpqCCCrrpq = D[32][46]
[48] CCCpqCNprCsCNpr = D[19]D[43]D[28]D[24][35]

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 9109 steps
[50] CCNppp = D[37]D[42][42]
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 6541 steps
[49] CCNppp = D[36]D[41][41]

[51] CpCNCqrCNqs = D[49][49]
[52] CCpNCNppCqNCNpp = D[17]D[40]D[30]D[23]D[48][50]
[53] CNCpqCrCsp = DDD[48][37]DD[17]D[44][25]D[40][46]D[45]DD[49][24]D[51][51]
[54] CCpCpqCrCpq = D[17][53]
[55] CpCCqCqrCqr = D[54][54]
[56] CCpCpqCpq = D[55][55]
[57] CCpqCNCprq = D[31]D[17]DD[56][49]D[37]D[15][22]
[58] CCCpqrCNpr = D[31]D[17]D[57][38]
[59] CCpqCCNppq = DD[10]D1[1]D[17]DD[31]DD[31]D[17]D[40]DD[31][52][25]D[58][52][25]
[60] CCNCpqrCCrqCpq = DD[59][29]D[45]1
[61] CCpCqCprCqCpr = D[56]D[17]D[43][53]
[62] CpCCpqq = DD[61]D[13]D[3]D[3]D1[6]DD[20][47][56]
[63] CCpqCCNqpq = D[17]DDD[15][17]D[59]D[30][56][59]
[50] CpCNCqrCNqs = D[48][48]
[51] CCpNCNppCqNCNpp = D[19]D[39]D[28]D[24]D[47][49]
[52] CNCpqCrCsp = DDD[47][36]DD[19]D[43][26]D[39][45]D[44]DD[48]DD[0]DD[12][5][11][10]D[50][50]
[53] CCpCpqCrCpq = D[19][52]
[54] CpCCqCqrCqr = D[53][53]
[55] CCpCpqCpq = D[54][54]
[56] CCpqCNCprq = D[27]D[19]DD[55][48]D[36]D[17]D[11][16]
[57] CCCpqrCNpr = D[27]D[19]D[56][37]
[58] CCpqCCNppq = DD[11]D1[1]D[19]DD[27]DD[27]D[19]D[39]DD[27][51][26]D[57][51][26]
[59] CCNCpqrCCrqCpq = DD[58][30]D[44]1
[60] CCpCqCprCqCpr = D[55]D[19]D[42][52]
[61] CpCCpqq = DD[60]D[15][13]DD[22][46][55]
[62] CCpqCCNqpq = D[19]DDD[11][19]D[58]D[28][55][58]

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 1682551 steps
[64] CCNpNqCqp = D[37]D[61]DD[63]D[15][36]D[43]D[56]D[41][45]
% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 1193987 steps
[63] CCNpNqCqp = D[36]D[60]DD[62]D[17][35]D[42]D[55]D[40][44]

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 1686507 steps
[65] CCpqCCqrCpr = DDD1[57]D[19]D[59][62][60]
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 1196969 steps
[64] CCpqCCqrCpr = DDD1[56]D[21]D[58][61][59]

[66] CCCCpqCrqsCCrps = D[65][65]
[67] CCpCqrCqCpr = D[66]D[65][62]
[65] CCCCpqCrqsCCrps = D[64][64]
[66] CCpCqrCqCpr = D[65]D[64][61]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 25914517 steps
[68] CCpCqrCCpqCpr = D[67]D[66]D[60]DD[67]D[58][63]D[67]D[66][58]
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 18391835 steps
[67] CCpCqrCCpqCpr = D[66]D[65]D[59]DD[66]D[57][62]D[66]D[65][57]
Loading

0 comments on commit a848c40

Please sign in to comment.