w6.txt

% 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 (622 bytes): pmGenerator --transform data/w6.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCppqCrq,CCCpqrCqr,CCpCCCqqNCprsCtCCCqqNCprs,CCNppCqp,CCpqCCCrrpq
% Concrete (2560 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

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

[6] CCCpqpCrp = D1[5]
[7] CCpCpqCrCpq = D1[6]
[8] CCCNpqrCpr = D1D[7][0]
[9] CCCpqrCqr = D1D[5][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] CCpCCCqqNCprsCtCCCqqNCprs = D1D1D[2]D1D[5]DD1D1D[2][0][3]
[13] CpCCpqCrq = D[9][10]
[14] CCpqCNCCCrrpsq = D1D[12][3]
[15] CCpCqCrCpsCtCqCrCps = D1D1D[9]D[9][5]
[16] CCNppCqp = D1D1DD[7]D1D1[13]1

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

[18] CCpqCCCrrpq = D1D[16]D[14][3]

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 243 steps
[19] CCNpNqCqp = D[2]D1D[7]D1D[5]D[0]DD1D[7]D1D[5]D[0]D[8]DD[2]11D1D[12][5]

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 431 steps
[20] CCpqCCqrCpr = DD1D[5]D[18][18][10]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 1553 steps
[21] CCpCqrCCpqCpr = DD[15]DD1DD1D[16]D[14][6][18]DD1D[5]D[18][13]DD[15]DD1D[5]D[18][20][13]11