w2.txt

% Walsh's 2nd Axiom (CpCCqCprCCNrCCNstqCsr), i.e. 0→((1→(0→2))→((¬2→((¬3→4)→1))→(3→2)))
% Completeness follows w.r.t. CpCqp,CCpCqrCCpqCpr,CCNpNqCqp and CCpqCCqrCpr,CCNppp,CpCNpq.
%
% Proof system configuration: pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr
% SHA-512/224 hash: db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff
%
% Full summary: pmGenerator --transform data/w2.txt -f -n -t . -j 1
% Step counting: pmGenerator --transform data/w2.txt -f -n -t . -p -2 -d
%                pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% Compact (1119 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CNpCCNqCCNrspCrq,CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq,CCpCCqCCNrCCNCCNsCCNtuNCNqvCtswNCxCCyCxzCCNzCCNabyCazrcCCNcCCNdepCdc,CpCCpqq,CNCCNpqqCrp
% Concrete (2466 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e

    CpCCqCprCCNrCCNstqCsr = 1
[0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
[1] CCNCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqpCCNwxCsCvpCwCCNCCNpCCNqrsCqpCCNtuvCtCCNpCCNqrsCqp = D[0]1
[2] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = DD1[0]1
[3] CCNCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqpCCNzasCzCCNpCCNqrCNpCCNstNCuCCvCuwCCNwCCNxyvCxwCqp = DD[1]11
[4] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = D[3]1
[5] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[4]
[6] CCNCpqCCNrsCCtpCCuCCvCuwCCNwCCNxyvCxwqCrCpq = D[5][0]
[7] CCpqCCNCCNqCCNrstCrqCCNuvpCuCCNqCCNrstCrq = D[1][4]
[8] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][4]
[9] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[2][4]
[10] CCNCCNCpCqrCCNstCCNCuCCvCuwCCNwCCNxyvCxwzCNrCCNqabCsCpCqrCCNcdCNCqrCCNpeCbCCfCCgCfhCCNhCCNijgCihrCcCCNCpCqrCCNstCCNCuCCvCuwCCNwCCNxyvCxwzCNrCCNqabCsCpCqr = DD1DD[0][2][4]1

% Identity principle (Cpp), i.e. 0→0 ; 35 steps
[11] Cpp = DD[0][8][4]

[12] CNpCCNqCCNrspCrq = DDD1D[6]11[4]
[13] CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq = D[6]DD[0]DDD1DDD1[2]111[4]1

% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 53 steps
[14] CpCqp = DDD1DDDD[10][4]111[0]1

[15] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[9]DD[0][9][4]
[16] CCCNCpCCqCprCCNrCCNstqCsruvCCNwCCNxyCCNCzCCaCzbCCNbCCNcdaCcbeCNCvwCCNCfCCgCfhCCNhCCNijgCihkCClvCCmCCnCmoCCNoCCN<26><27>nC<26>owCxw = DD[0]DD1DD[0]D[0][6][4]1[4]

% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 57 steps
[17] CpCNpq = D[15]1

[18] CCNCCNCpqCCNCrCCsCrtCCNtCCNuvsCutwCCxpCCyCCzCyaCCNaCCNbczCbaqqCCNdeCCNCfCCgCfhCCNhCCNijgCihkpCdCCNCpqCCNCrCCsCrtCCNtCCNuvsCutwCCxpCCyCCzCyaCCNaCCNbczCbaqq = D[5][16]
[19] CNCpqCrCsCqt = DD[0]DDD1DDD1[12]1[4]1[4][4]
[20] CpCCNCpqCCNCrCCsCrtCCNtCCNuvsCutwCCxpCCyCCzCyaCCNaCCNbczCbaqq = D[18][4]
[21] CCpCCqCCNrCCNCCNsCCNtuNCNqvCtswNCxCCyCxzCCNzCCNabyCazrcCCNcCCNdepCdc = D1D[15]D[8][3]
[22] CpCCpqq = DDD1DD[0]D[2]DD[0]DD[0][10][4]11[16][4]

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 141 steps
[23] CCNppp = DD[0][14][20]

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 227 steps
[24] CCNpNqCqp = DD[21]DD[0]DD1DD[0]DD[0]D1[20][4]11[4][4]

[25] CNCCNpqqCrp = DD[0]DD1DD[0]DD[0]D[7][22][4][4][12][13]

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 703 steps
[26] CCpqCCqrCpr = DD[5]DDD1DD[0]DD1[22]1[4]1[13]D[18]DDD1[19][12][25]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 1111 steps
[27] CCpCqrCCpqCpr = DDD1D[18]DDD1DD[0]D[0][19][13][12][25]DD[0]DD1DD[21][21]DD[0]DD[0]D[7]1[13][25]1[4][4]