m.txt

% Meredith's Axiom (CCCCCpqCNrNsrtCCtpCsp), 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 CCCCCpqCNrNsrtCCtpCsp
% SHA-512/224 hash: 478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed
%
% Full summary: pmGenerator --transform data/m.txt -f -n -t . -j 1
% Step counting: pmGenerator --transform data/m.txt -f -n -t . -p -2 -d
%                pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% Compact (672 bytes): pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCppqCrq,CCCpqrCqr,CCCpNCCCqrCNNqrNstCst,CCpCpqCrCpq,CCCpCqNCCrCNNssNqtCut,CCpqCCrpCrq
% Concrete (8170 bytes): pmGenerator --transform data/m.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e

    CCCCCpqCNrNsrtCCtpCsp = 1
[0] CCCCpqCrqCqsCtCqs = D11
[1] CCCpCNqrsCqs = D1[0]
[2] CCCppqCrq = D1[1]
[3] CpCqCrq = D[0][2]

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

[5] CpCqCrr = D[2][2]
[6] CCCpqrCqr = D1D1[5]

% Identity principle (Cpp), i.e. 0→0 ; 19 steps
[7] Cpp = DD[5]11

[8] CpCCpqCrq = D[6]1
[9] CCCpqCrCNNqsCtCrCNNqs = D1D1D[4][1]
[10] CCpqCCCNCCCCCrsCNtNutvCCvrCurwCNqNNpq = DDD1D1DD1[3]111
[11] CpCCCCqrsCNCqrNCCtqCuqCqr = DD1D1[8][0]

% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 41 steps
[12] CpCNpq = DD1[6][6]

[13] CCCpNCCCqrCNNqrNstCst = D1D1D[2]D1D[0]D[10]D1D[9]1
[14] CCpCpqCrCpq = DDD1D1D1D[2][13]11
[15] CCCpCqNCCrCNNssNqtCut = D1D1DD1DD1D[11]1D1D1D[2]D1D[0]D[10]D1DD1DD1D1D[2]1[4][0]D[1][0]

% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 163 steps
[16] CCNppp = DD[14]DDD1D1D[9]D[6][8]111

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 175 steps
[17] CCNpNqCqp = DDDDD1D1D[8]D[6]D[13][1]11DD1D1[11][4]1

[18] CCpCpqCpq = DD[14][14]1
[19] CCpqCCCrCNNssNNpq = D1D[18][15]

% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 619 steps
[20] CCpqCCqrCpr = DD1D[19][19]1

[21] CCCCpqCrqsCCrps = D[20][20]
[22] CCpqCCrpCrq = DD[20]DD1DD1[15]1[18][21]

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 7001 steps
[23] CCpCqrCCpqCpr = DD[22][21]D[21]D[22][18]