s5.txt

% S5 (CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp)
%
% Proof system configuration: pmGenerator -c -n -N -1 -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp    (or "-N 1" for faster – but incomplete – generation via outruling consecutive necessitation steps)
% SHA-512/224 hash: d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f    (or 360ceff28c45b2d8ea630fc79a7dad68b04acdceaf41521e9f6ecd95)
%
% Full summary: pmGenerator --transform data/s5.txt -f -n -t . -j 1
% Step counting: pmGenerator --transform data/s5.txt -f -n -t . -p -2 -d
%                pmGenerator --transform data/s5.txt -f -n -t CpLNLNp,CLpLLp,CLpNLNp,CpNLNp,CNLNNLpNLp,CNLpLNLp -p -2 -d
% Compact (544 bytes): pmGenerator --transform data/s5.txt -f -n -t CpLNLNp,CLpLLp,CLpNLNp,CpNLNp,CNLNNLpNLp,CNLpLNLp -j -1 -s CNNpCqp,CNNpp,CCpqCNqNp,CNLNLpLp
% Concrete (1360 bytes): pmGenerator --transform data/s5.txt -f -n -t CpLNLNp,CLpLLp,CLpNLNp,CpNLNp,CNLNNLpNLp,CNLpLNLp -j -1 -e

% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0)
    CpCqp = 1

% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2))
    CCpCqrCCpqCpr = 2

% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0)
    CCNpNqCqp = 3

% Axiom T (CLpp), i.e. □0→0
    CLpp = 4

% Axiom K by Kripke (CLCpqCLpLq), i.e. □(0→1)→(□0→□1)
    CLCpqCLpLq = 5

% Axiom 5 by Lewis (CMpLMp, i.e. CNLNpLNLNp), i.e. ¬□¬0→□¬□¬0, alias ◇0→□◇0
    CNLNpLNLNp = 6

[0] CCpCNqNrCpCrq = D2D13
[1] CCpqCCrpCrq = DD2D121
[2] CNNpCqp = D[0]D[0]1
[3] CCNNpqCNNpp = D2[2]
[4] CNNpp = D[3]1
[5] CpCNNqq = D1[4]
[6] CpNNp = D3[4]
[7] CLpLNNp = D5N[6]
[8] CCpqCpNNq = D2D1[6]

% Alternative to axiom T (CpMp, i.e. CpNLNp), i.e 0→¬□¬0, alias 0→◇0 ; 25 steps
[9] CpNLNp = D3DD2D14[4]

[10] CCpCqrCpCqNNr = D2D1[8]

% Axiom B by Brouwer (CpLMp, i.e. CpLNLNp), i.e. 0→□¬□¬0, alias 0→□◇0 ; 31 steps
[11] CpLNLNp = DD2D16[9]

% Axiom D (CLpMp, i.e. CLpNLNp), i.e. 0→□¬□¬0, alias 0→◇0 ; 31 steps
[12] CLpNLNp = DD2D1[9]4

[13] CCpqCNqNp = D[0]D[10]DD2D1DD22[3]1
[14] CNLNLpLp = DD2D1DD2D1D5N[4][4]DD2D[0]DD2D1D2D1D[8]6[5]DD[0]D[10]DD2D1D2DD2D1D2DD2D15D5N[13][2]1N[7]

% Axiom 4 by Lewis (CLpLLp), i.e. □0→□□0 ; 302 steps
[15] CLpLLp = DD2D1D5N[14][11]

% Alternative to axiom 5 (CNLpLNLp), i.e. ¬□0→□¬□0 ; 373 steps
[16] CNLpLNLp = DD[0]D[0]DD[1]D[1]D[13][14][5]1

% Alternative to axiom 4 (CMMpMp, i.e. CNLNNLNpNLNp of CNLNNLpNLp), i.e. ¬□¬¬□0→¬□0, schema of ¬□¬¬□¬0→¬□¬0, alias ◇◇0→◇0 ; 401 steps
[17] CNLNNLpNLp = D[13]DDDD2D1D2[1]1[15][7]