w4.txt

% Walsh's 4th Axiom (CpCCNqCCNrsCtqCCrtCrq), i.e. 0→((¬1→((¬2→3)→(4→1)))→((2→4)→(2→1)))
% Completeness follows w.r.t. CpCqp,CCpCqrCCpqCpr,CCNpNqCqp and CCpqCCqrCpr,CCNppp,CpCNpq.
%
% Proof system configuration: pmGenerator -c -n -s CpCCNqCCNrsCtqCCrtCrq
% SHA-512/224 hash: fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9
%
% Full summary: pmGenerator --transform data/w4.txt -f -n -t . -j 1
% Step counting: pmGenerator --transform data/w4.txt -f -n -t . -p -2 -d
%                pmGenerator --transform data/w4.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% Compact (1110 bytes): pmGenerator --transform data/w4.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCpCqrCpCqp,CpCCNqCCNrsCtqp,CpCNCqrp,CCpCNqCCNrsCtqCpCCrtCrq,CCpqCpCCNrCCNstCurq,CCpqCpCrq,CCpNNqCpq,CCpqCCrpCrq,CCpCqNqCpCqr,CpCCpqq
% Concrete (39202 bytes): pmGenerator --transform data/w4.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e

    CpCCNqCCNrsCtqCCrtCrq = 1
[0] CCNpCCNqrCspCCqsCqp = D11
[1] CCpCqrCpCqp = D[0]1
[2] CpCCNqCCNrsCtqp = D[1]1
[3] CCNpCCNqrCspCtCNpCCNqrCsp = D[1]D[2]1
[4] CpCNCqrCCNrCCNqsCtrCCqtCqr = D[3]1
[5] CpCNCqrp = D[1][4]
[6] CNCpqCrCCNsCCNtuCvsCCtvCts = D[5]1
[7] CCpCNqCCNrsCtqCpCCrtCrq = D[0][6]
[8] CNCpqCrNCpq = D[1][6]
[9] CCpCNqCCNrsCtqCpCNpu = D[0]D[5][2]
[10] CCpqCpCCNrCCNstCurq = D[0]D[5]D[2][2]

% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 53 steps
[11] CpCNpq = D[9][4]

% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 59 steps
[12] CpCqp = D[1]DD[0]DDD[0]D[5][3]111

[13] CCNpCqpCCrqCrp = D[7][10]
[14] CCpqCpCNqr = D[0]D[5]D[2][11]
[15] CCpqCpCrq = D[0]D[5]D[2][12]
[16] CpCCNqCCNrsCtqCNpu = DD[0]D[5]D[10][2][4]
[17] CCpNNqCpq = D[0][16]
[18] CpCCNqCCNrsCtqCup = D[10][12]
[19] CCpCqNCNqrCpCqCst = D[0]D[5]D[2]D[0]D[5][11]
[20] CCpCqrCpCqCsr = D[0]D[5]D[2][15]
[21] CCpqCCrpCrq = D[7]D[15][2]
[22] CCpCqNqCpCqr = D[0]D[5]D[2]D[0]D[7]DD[1][1][16]
[23] CNpCpq = D[22][12]
[24] CNpCqCpr = D[15][23]

% Identity principle (Cpp), i.e. 0→0 ; 465 steps
[25] Cpp = DDDDD[7]D[0]D[5]D[2][18]D[15]DD[0]D[5]D[2]D[0]DD[0]D[5]D[2]D[0]D[5]D[2]D[9]DD[1][0]11[8]111

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 1709 steps
[26] CCNppp = D[17]DD[0]DD[13]D[5][24]DD[13]D[22]DDD[0]D[10]D[7]D[19][5][1]1DDD[0]D[10]D[7]D[19][8][1]1D[13]D[22]DD[0]D[5]D[2][17][12]

[27] CCpCNqqCpq = D[21][26]
[28] CpCCpqq = DD[27][15]DD[13]D[5][23]DD[27][14]D[20]DD[0]D[10]D[14][12][25]
[29] CCpqCpCCqrr = D[21][28]
[30] CCpCCqqrCpr = D[21]D[28][25]

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 10779 steps
[31] CCNpNqCqp = D[30]D[7][29]

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 12081 steps
[32] CCpqCCqrCpr = DDD[30][13]D[29]DD[0]DD[0]D[5]D[2]DD[0]D[5][18][4][24][25]D[20][21]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 13917 steps
[33] CCpCqrCCpqCpr = D[7]D[15]D[32][26]