% Walsh's 6th Axiom (CCCpqCCCNrNsrtCCtpCsp), i.e. ((0→1)→(((¬2→¬3)→2)→4))→((4→0)→(3→0))
% Completeness follows w.r.t. CpCqp,CCpCqrCCpqCpr,CCNpNqCqp and CCpqCCqrCpr,CCNppp,CpCNpq.
%
% Proof system configuration: pmGenerator -c -n -s CCCpqCCCNrNsrtCCtpCsp
% SHA-512/224 hash: 7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69
%
% Full summary: pmGenerator --transform data/w6.txt -f -n -t . -j 1
% Step counting: pmGenerator --transform data/w6.txt -f -n -t . -p -2 -d
%                pmGenerator --transform data/w6.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% Compact (823 bytes): pmGenerator --transform data/w6.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCCNpNqprCqr,CCCppqCrq,CCpCpqCrCpq,CCCpqrCqr,CpCqCCCrrNps,CpCCpqCrq,CCNpqCNCrpq,CCpqCCCrrpq,CCCCpqqrCpr
% Concrete (12794 bytes): pmGenerator --transform data/w6.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e

    CCCpqCCCNrNsrtCCtpCsp = 1
[0] CCCpqCqrCsCqr = D11
[1] CCCpqCrpCsCrp = D1[0]
[2] CCCCNpNqprCqr = D1D[0][0]
[3] CCCppqCrq = D1D[1]1

% Identity principle (Cpp), i.e. 0→0 ; 13 steps
[4] Cpp = DDD[1][0]11

[5] CCpCNCpqrCsCNCpqr = D1D1D[2][0]

% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 19 steps
[6] CpCqp = D[2][3]

[7] CCpCpqCrCpq = D1D1[6]
[8] CCCNpqrCpr = D1D[7][0]
[9] CCCpqrCqr = D1D[6][3]
[10] CCCCNpNqprCCrsCqs = D[9]1

% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 37 steps
[11] CpCNpq = DD[1][8]1

[12] CpCqCrp = D[9][6]
[13] CpCqCCCrrNps = D[2]D1D[6]D[5][3]
[14] CCpCCCqqNCprsCtCCCqqNCprs = D1D1[13]
[15] CpCCpqCrq = D[9][10]
[16] CCCpqNqCrNq = D1[15]
[17] CpCqNNp = D[2][16]
[18] CCNppCqp = D1D1DD[7]D1[16]1

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 125 steps
[19] CCNppp = DD[7][18]1

[20] CCNpqCNCrpq = D1DD1D1DD1D[6]D1DD1D[6]1[8][13][3]
[21] CCpqCCCrrpq = D1D[18]DD1D[14][3][3]

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 297 steps
[22] CCNpNqCqp = D[2]D1D[7]D1D[6]D[7]DD1D[7]D1D[6]D[0][17]D1D[14][6]

[23] CCCCpqqrCpr = D[10]D[21]DD[10]D[21][15]DD[7][7]1

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 1821 steps
[24] CCpqCCqrCpr = DD[10]D[21]DDD[7]D1D1[12]1DDDDD1[10][12]1DD[10]D[21]DD[5][20]1DD[1]D1D[7][16]1D[20]DD[5]D1D[7]D1D[6]D[0]D[9][17]1D[23][10]

[25] CCCCpqCrqsCCrps = D[24][24]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 10343 steps
[26] CCpCqrCCpqCpr = DD[25][23]D[25]DDD[7]D1D1D[9][12]1D[23][24]