% 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 (1160 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,CCpqCCrpCrq,CCpCqNqCpCqr,CpCCpqq
% Concrete (38946 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] CCpCqrCNCqpCCNpCCNqsCrpCCqrCqp = DD[1][0]1
[4] CCNpCCNqrCspCtCNpCCNqrCsp = D[1]D[2]1
[5] CpCNCqrCCNrCCNqsCtrCCqtCqr = D[4]1
[6] CpCNCqrp = D[1][5]
[7] CNCpqCrCCNsCCNtuCvsCCtvCts = D[6]1
[8] CCpCNqCCNrsCtqCpCCrtCrq = D[0][7]
[9] CNCpqCrNCpq = D[1][7]
[10] CCpCNqCCNrsCtqCpCNpu = D[0]D[6][2]
[11] CCpqCpCCNrCCNstCurq = D[0]D[6]D[2][2]
[12] CpCCNqCCNrsCtqCCNuCCNvwCxup = D[11][2]

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

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

[15] CCNpCqpCCrqCrp = D[8][11]
[16] CCpCqCrsCpCNCqCrst = D[0]D[6]D[2]D[10][3]
[17] CCpqCpCNqr = D[0]D[6]D[2][13]
[18] CCpqCpCrq = D[0]D[6]D[2][14]
[19] CpCCNqCCNrsCtqCNpu = DD[0]D[6][12][5]
[20] CCpCqNCNqrCpCqCst = D[0]D[6]D[2]D[0]D[6][13]
[21] CCpCqrCpCqCsr = D[0]D[6]D[2][18]
[22] CCpqCCrpCrq = D[8]D[18][2]
[23] CCpCqNqCpCqr = D[0]D[6]D[2]D[0]D[8]DD[1][1][19]
[24] CNpCpq = D[23][14]
[25] CNpCqCpr = D[18][24]

% Identity principle (Cpp), i.e. 0→0 ; 465 steps
[26] Cpp = DDDDD[8]D[0]D[6]D[2]D[11][14]D[18]DD[0]D[6]D[2]D[0]DD[0]D[6]D[2][16]1[9]111

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 1703 steps
[27] CCNppp = DD[0]DD[0]DD[1][3][12][5]DD[0]DD[15]D[6][25]DD[15]D[23]DDD[0]D[11]D[8]D[20][6][1]1DDD[0]D[11]D[8]D[20][9][1]1D[15]D[23]DD[0]D[6]D[2]D[0][19][14]

[28] CCpCNqqCpq = D[22][27]
[29] CpCCpqq = DD[28][18]DD[15]D[6][24]DD[28][17]D[21]DD[0]D[11]D[17][14][26]
[30] CCpqCpCCqrr = DD[8]DD[0]D[6]D[2][6][2][29]
[31] CCpCCqqrCpr = D[22]D[29][26]

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

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 11989 steps
[33] CCpqCCqrCpr = DDD[31][15]D[30]DD[15]D[16][25][26]D[21][22]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 13819 steps
[34] CCpCqrCCpqCpr = D[8]D[18]D[33][27]