w2.txt

% Walsh's 2nd Axiom (CpCCqCprCCNrCCNstqCsr), i.e. 0→((1→(0→2))→((¬2→((¬3→4)→1))→(3→2)))
% TODO: Completeness 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,Cpp,CCNppp,CpCNpq -p -2 -d
% Compact (470 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CCNppp,CpCNpq -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq
% Concrete (644 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,Cpp,CCNppp,CpCNpq -j -1 -e

    CpCCqCprCCNrCCNstqCsr = 1
[0] CCpCCqCCrCqsCCNsCCNturCtsvCCNvCCNwxpCwv = D11
[1] CCNCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpqCCNzaCNqCCNpbtCzCCNCpqCCNrsCtCCuCCvCuwCCNwCCNxyvCxwqCrCpq = DD1[0]1
[2] CpCCNCCNqCCNrsCNqCCNtuNpCrqCCNvwtCvCCNqCCNrsCNqCCNtuNpCrq = DD[0]11
[3] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DD[2]11
[4] CCpCCqCCNrCCNstCNrCCNCCNuCCNvwNqCvuxNCyCCzCyaCCNaCCNbczCbaCsrdCCNdCCNefpCed = D1[3]
[5] CCCpCCqCprCCNrCCNstqCsruCvu = DD[0][0][3]
[6] CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps = D[1][3]
[7] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][6]

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

[9] CpCqCrCsCtq = DDDDD1DD[0][1][3]1[3]11
[10] CCpCCqCrCsCtquCCNuCCNvwpCvu = D1D[9]1

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

[12] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[6]D[7][3]

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

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 417 steps
[14] CCNppp = DDDDD1[8]1DDD[0]DDD1DD[0][7][9][0]D[7]1DDD1DDD[0]D1DD1DD[4][0]11[3]DD[0][4][3]DDD1[10]1[3][3]11D[12]DD[0][2]DD[0]DDD1DDD1[5]111[3]1