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 (811 bytes): pmGenerator --transform data/w4.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCpCqrCpCqp,CpCCNqCCNrsCtqp,CpCNCqrp,CCpqCpCCNrCCNstCurq,CCpqCpCrq,CCpqCCrpCrq,CCpCqCrCqsCpCrCqs
% Concrete (3866 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]
[11] CpCNpCCNqrCsp = DD[0]D[5][3]1
[12] CpCCNqCCNrsCtqCCNuCCNvwCxup = D[10][2]

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

% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 59 steps
[14] CpCqp = D[1]DD[0]D[11]11

[15] CNCpqCCNrCCNstCurCvCwv = D[5]D[2][14]
[16] CCpqCpCrq = D[0][15]
[17] CCpCqrCpCqCsr = D[0]D[5]D[2][16]
[18] CCpqCCrpCrq = D[7]D[16][2]

% Identity principle (Cpp), i.e. 0→0 ; 361 steps
[19] Cpp = DDDD[0]D[10]D[7]DD[0]D[5]D[2][11]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][0]11

[20] CCpCqCrCqsCpCrCqs = D[0]D[10]DD[0]D[5]D[2]D[17][18]DD[0]D[5]D[2]D[0]D[7]DD[1][1]DD[0]D[5][12][4][8]

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 697 steps
[21] CCNppp = DDD[20][7]D[0]D[5]D[2][12][4]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 731 steps
[22] CCpCqrCCpqCpr = D[20]D[0]D[5]D[2][18]

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 827 steps
[23] CCpqCCqrCpr = DD[20][17][18]

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 999 steps
[24] CCNpNqCqp = DD[0]D[5]D[2]D[0]D[10]DD[20][0][15]DD[0]D[5]D[2]D[0]D[5][18][14]