-
-
Notifications
You must be signed in to change notification settings - Fork 3
Expand file tree
/
Copy pathw2.txt
More file actions
121 lines (100 loc) · 10.7 KB
/
w2.txt
File metadata and controls
121 lines (100 loc) · 10.7 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
% 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 _
% Step counting: pmGenerator --transform data/w2.txt -f -n -t . -p -2 -d
% - all: pmGenerator --transform data/w2.txt -f -n -t _ -p -2 -d
% - targets: pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq,CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCNqCCNrsCptCCtqCrq,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -p -2 -d
% - 1st PMC: pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% - 2nd PMC: pmGenerator --transform data/w2.txt -f -n -t CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCNqCCNrsCptCCtqCrq,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -p -2 -d
% Compact (3090 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq,CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCNqCCNrsCptCCtqCrq,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CCpqCCNCCNqCCNrstCrqCCNuvpCuCCNqCCNrstCrq,CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps,CNpCCNqCCNrspCrq,CCCpqCCrCCsCrtCCNtCCNuvsCutwCxCyCqw,CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq,CpCCNCpqCCNCrCCsCrtCCNtCCNuvsCutwCCxpCCyCCzCyaCCNaCCNbczCbaqq,CCpCCqCCNrCCNCCNsCCNtuNCNqvCtswNCxCCyCxzCCNzCCNabyCazrcCCNcCCNdepCdc,CCpqCpCrq,CCCNpqCrsCCNCpsCCNturCtCps,CpCCpqq,CNpCqCrCCNsps,CCNCCNppqCCNrsCCtpCCuCCvCuwCCNwCCNxyvCxwqCrCCNppq,CpCCNqqCCrCqsCCNsCCNturCts,CpCCNCqCrsCqCrsCrCCNsCCNtuqCts,CCpCCNCqrCCNCqsCCNCtCCuCtvCCNvCCNwxuCwvyCCzqCCaCCbCacCCNcCCNdebCdcssfCCNfCCNghpCgf,CNCpCqrCCNCqsCCNCtCCuCtvCCNvCCNwxuCwvyCCzqCCaCCbCacCCNcCCNdebCdcss,CNCpCqCrsCCNCrtCCNCuCCvCuwCCNwCCNxyvCxwzCCarCCbCCcCbdCCNdCCNefcCedtt,CCNCCpqCrqCCNstCrCNqpCsCCpqCrq
% - 1st PMC (1043 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCCNCpqCCNCrCCsCrtCCNtCCNuvsCutwCCxpCCyCCzCyaCCNaCCNbczCbaqq,CCpCCqCCNrCCNCCNsCCNtuNCNqvCtswNCxCCyCxzCCNzCCNabyCazrcCCNcCCNdepCdc,CCCNpqCrsCCNCpsCCNturCtCps,CCpCCNCqrCCNCqsCCNCtCCuCtvCCNvCCNwxuCwvyCCzqCCaCCbCacCCNcCCNdebCdcssfCCNfCCNghpCgf
% - 2nd PMC (2902 bytes): pmGenerator --transform data/w2.txt -f -n -t CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCNqCCNrsCptCCtqCrq,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -j -1 -s CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CCpqCCNCCNqCCNrstCrqCCNuvpCuCCNqCCNrstCrq,CCCpCCqCprCCNrCCNstqCsruCvu,CCCNpqrCCNCpsCCNtuCrCCvCCwCvxCCNxCCNyzwCyxsCtCps,CNpCCNqCCNrspCrq,CCCpqCCrCCsCrtCCNtCCNuvsCutwCxCyCqw,CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq,CpCqp,CpCCNCpqCCNCrCCsCrtCCNtCCNuvsCutwCCxpCCyCCzCyaCCNaCCNbczCbaqq,CCpCCqCCNrCCNCCNsCCNtuNCNqvCtswNCxCCyCxzCCNzCCNabyCazrcCCNcCCNdepCdc,CCpqCpCrq,CCCNpqCrsCCNCpsCCNturCtCps,CpCCpqq,CNpCqCrCCNsps,CCNCCNppqCCNrsCCtpCCuCCvCuwCCNwCCNxyvCxwqCrCCNppq,CpCCNqqCCrCqsCCNsCCNturCts,CCpCCNCqrCCNCqsCCNCtCCuCtvCCNvCCNwxuCwvyCCzqCCaCCbCacCCNcCCNdebCdcssfCCNfCCNghpCgf,CNCpCqrCCNCqsCCNCtCCuCtvCCNvCCNwxuCwvyCCzqCCaCCbCacCCNcCCNdebCdcss,CNCpCqCrsCCNCrtCCNCuCCvCuwCCNwCCNxyvCxwzCCarCCbCCcCbdCCNdCCNefcCedtt,CCNCCpqCrqCCNstCrCNqpCsCCpqCrq
% Concrete (13763 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq,CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCNqCCNrsCptCCtqCrq,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -j -1 -e
% - 1st PMC (2198 bytes): pmGenerator --transform data/w2.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
% - 2nd PMC (11592 bytes): pmGenerator --transform data/w2.txt -f -n -t CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCNqCCNrsCptCCtqCrq,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -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] CCNCpCqrCCNstCCNquCNrCCNCvCCwCvxCCNxCCNyzwCyxaNpCsCpCqr = D[0][9]
[11] CCNCCNpCCNqrsCqpCCNtuCCNCvCCwCvxCCNxCCNyzwCyxaNsCtCCNpCCNqrsCqp = DD1D[6]11
[12] CpCqCCCNCrCCsCrtCCNtCCNuvsCutwNqx = D[10]1
[13] CCpCCqCrCCCNCsCCtCsuCCNuCCNvwtCvuxNryzCCNzCCNabpCaz = D1[12]
[14] CCNCCNCpCqrCCNstCCNCuCCvCuwCCNwCCNxyvCxwzCNrCCNqabCsCpCqrCCNcdCNCqrCCNpeCbCCfCCgCfhCCNhCCNijgCihrCcCCNCpCqrCCNstCCNCuCCvCuwCCNwCCNxyvCxwzCNrCCNqabCsCpCqr = DD1DD[0][2][4]1
[15] CCCpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrqcCdc = DD[0][5][4]
% Identity principle (Cpp), i.e. 0→0 ; 35 steps
[16] Cpp = DD[0][8][4]
[17] CNpCCNqCCNrspCrq = D[11][4]
[18] CCCNCpCCqCprCCNrCCNstqCsruCNCvwCCNCxCCyCxzCCNzCCNabyCazcCCdvCCeCCfCegCCNgCCNhifChgwCvw = DD[0]D[0][6][4]
[19] CCNCpCCqCrsCCNsCCNtuqCtsCCNvwCCNCxCCyCxzCCNzCCNabyCazcrCvCpCCqCrsCCNsCCNtuqCts = D[0]DD[0]D[7]1[4]
[20] CCNCCNpCCNqrCspCqpCCNtusCtCCNpCCNqrCspCqp = DD1[16]1
[21] CCNCCNpCCNqrCspCqpCCNtuCNCCNpCCNqrCspCqpCCNCvCCwCvxCCNxCCNyzwCyxasCtCCNpCCNqrCspCqp = D[0][20]
[22] CpCqCrCsp = DDDD[14][4]111
[23] CpCqCrCsCtCur = DD[0]DD[0][14][4]1
[24] CCCpqCCrCCsCrtCCNtCCNuvsCutwCxCyCqw = DD[0]DDD1[9]1[4][4]
[25] CCpCCqCrCCsCqtCCNtCCNuvsCutwCCNwCCNxypCxw = D1D[19][4]
[26] CpCCNqCCNrsCNqCCNCtCCuCtvCCNvCCNwxuCwvyNzCzCrq = D[6]DD[0]DDD1DDD1[2]111[4]1
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 53 steps
[27] CpCqp = DDD1[22][0]1
[28] CCNCpqCCNrsCCtCupCCvCCwCvxCCNxCCNyzwCyxqCrCpq = D[9]D[10][4]
[29] CCCNCpCCqCprCCNrCCNstqCsruvCCNwCCNxyCCNCzCCaCzbCCNbCCNcdaCcbeCNCvwCCNCfCCgCfhCCNhCCNijgCihkCClvCCmCCnCmoCCNoCCN<26><27>nC<26>owCxw = DD[0]DD1[18]1[4]
% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 57 steps
[30] CpCNpq = D[28]1
[31] CCCNpqNrCCNCpCstCCNuvCCNswrCuCpCst = DDD1DDD1[17]1[4]1[4]
[32] CCNCCNCpqCCNCrCCsCrtCCNtCCNuvsCutwCCxpCCyCCzCyaCCNaCCNbczCbaqqCCNdeCCNCfCCgCfhCCNhCCNijgCihkpCdCCNCpqCCNCrCCsCrtCCNtCCNuvsCutwCCxpCCyCCzCyaCCNaCCNbczCbaqq = D[5][29]
[33] CNCpqCrCsCqt = DD[0][31][4]
[34] CpCCNCpqCCNCrCCsCrtCCNtCCNuvsCutwCCxpCCyCCzCyaCCNaCCNbczCbaqq = D[32][4]
[35] CCpCCqCCNCqrCCNCsCCtCsuCCNuCCNvwtCvuxCCyqCCzCCaCzbCCNbCCNcdaCcbrreCCNeCCNfgpCfe = D1[34]
[36] CCpCCqCCNrCCNCCNsCCNtuNCNqvCtswNCxCCyCxzCCNzCCNabyCazrcCCNcCCNdepCdc = D1D[28]D[8][3]
[37] CCNCCNpCCNqrsCqpCCNtuCNCspCCNCvCCwCvxCCNxCCNyzwCyxaCCbsCCcCCdCceCCNeCCNfgdCfepCtCCNpCCNqrsCqp = D[35]1
[38] CCNCpqCCNrsCCCNtCCNuvNpCutCCwCCNCwxCCNCyCCzCyaCCNaCCNbczCbadCCewCCfCCgCfhCCNhCCNijgCihxxqCrCpq = D[0][35]
[39] CCpqCpCrq = DD[5]DDD1D[21][4]1[4][4]
[40] CCNCCNCpqCCNrstCrCpqCCNuvCNqCCNpwCtqCuCCNCpqCCNrstCrCpq = DD1D[21][26]1
[41] CCNpCCNqrCCsCCNCstCCNCuCCvCuwCCNwCCNxyvCxwzCCasCCbCCcCbdCCNdCCNefcCedttpCqp = D[0]D[38][4]
[42] CCCNpqCrsCCNCpsCCNturCtCps = D[40][4]
[43] CpCCpqq = DDD1DD[0]D[2][23]1[29][4]
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 141 steps
[44] CCNppp = DD[0][27][34]
[45] CNpCqCrCCNsps = DD[0]DD[7]D[35][17][4][4]
[46] CpCCNCNqqCCNCrCCsCrtCCNtCCNuvsCutwCCxNqCCyCCzCyaCCNaCCNbczCbaqCdq = DD[5]D1[27]D[24][37]
[47] CCpCCqCCNCNrrCCNCsCCtCsuCCNuCCNvwtCvuxCCyNrCCzCCaCzbCCNbCCNcdaCcbrCerfCCNfCCNghpCgf = D1[46]
[48] CCNCCNppqCCNrsCCtpCCuCCvCuwCCNwCCNxyvCxwqCrCCNppq = D[47][0]
% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 227 steps
[49] CCNpNqCqp = DD[36]DD[0]DD1D[41]11[4][4]
[50] CCpCCqCCNCNrrCCNCsCCtCsuCCNuCCNvwtCvuxCCyNrCCzCCaCzbCCNbCCNcdaCcbrreCCNeCCNfgpCfe = D1D[38][45]
[51] CCCpCCNCNqqCCNCrCCsCrtCCNtCCNuvsCutwCCxNqCCyCCzCyaCCNaCCNbczCbaqqdCed = DD[0][50][4]
[52] CpCCNqqCCrCqsCCNsCCNturCts = DD[50]DD[25]111
[53] CpCCNCqCrsCqCrsCrCCNsCCNtuqCts = DD[47][36]DD[0]DDD1DDD1[1]111[4]1
[54] CCpCCNCqrCCNCqsCCNCtCCuCtvCCNvCCNwxuCwvyCCzqCCaCCbCacCCNcCCNdebCdcssfCCNfCCNghpCgf = D1DDDDD1DDD1DDDD[0]DD[7][10][4][33]11DD[0]DD1D[6][12]1[4][4][42][4][34]1
[55] CNCpCqrCCNCqsCCNCtCCuCtvCCNvCCNwxuCwvyCCzqCCaCCbCacCCNcCCNdebCdcss = D[32]D[48]D[24]DD1[33][17]
[56] CNCpCqCrsCCNCrtCCNCuCCvCuwCCNwCCNxyvCxwzCCarCCbCCcCbdCCNdCCNefcCedtt = D[32]D[51]DD1DD[0]DDD1DD[7]D[0][17][22]1[4][4][17]
[57] CCNCCNCpqCCNrsCtqCrCpqCCNuvCptCuCCNCpqCCNrsCtqCrCpq = DD1DD[54][42][4]1
% Walsh's 4th Axiom (CpCCNqCCNrsCtqCCrtCrq), i.e. 0→((¬1→((¬2→3)→(4→1)))→((2→4)→(2→1))) ; 587 steps
[58] CpCCNqCCNrsCtqCCrtCrq = D[15]D[54]DD[0][40][4]
[59] CCNCCNCpCqrCCNstCquCsCpCqrCCNvwCNCqrCCNpxCurCvCCNCpCqrCCNstCquCsCpCqr = DD1DDD1[39]1[56]1
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 685 steps
[60] CCpqCCqrCpr = DD[36]DD[0][57][4][4]
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 861 steps
[61] CCpCqrCCpqCpr = DD[54][36][53]
% Walsh's 1st Axiom (CCpCCNpqrCsCCNtCrtCpt), i.e. (0→((¬0→1)→2))→(3→((¬4→(2→4))→(0→4))) ; 1015 steps
[62] CCpCCNpqrCsCCNtCrtCpt = D[39]DDD1DD[0]DD[7][41][4][45]DDD1D[37]DD[5]DDD1[8]1111[4][55]
[63] CCNCCpqCrqCCNstCrCNqpCsCCpqCrq = DD[59][4]DD[35]DD[0]DD1[43]1[4][46]
% Walsh's 3rd Axiom (CpCCNqCCNrsCptCCtqCrq), i.e. 0→((¬1→((¬2→3)→(0→4)))→((4→1)→(2→1))) ; 1469 steps
[64] CpCCNqCCNrsCptCCtqCrq = DD[36]D1D[15]D[54]DDD1DD[0]DD1[44]1[26]1[4]D[51]D[36]D[1][52]
% Walsh's 5th Axiom (CCpqCCCrCstCqCNsNpCps), i.e. (0→1)→(((2→(3→4))→(1→(¬3→¬0)))→(0→3)) ; 2227 steps
[65] CCpqCCCrCstCqCNsNpCps = DD[0]DDD1[49]DD[5]DDD1[42]1[4][56]D[51]D[0]DD[0]DD[0]D[7]DD[36]D1DD[0]DD[7]D[13]D[20][4][4][4][52][4][4][55]
% Walsh's 6th Axiom (CCCpqCCCNrNsrtCCtpCsp), i.e. ((0→1)→(((¬2→¬3)→2)→4))→((4→0)→(3→0)) ; 2359 steps
[66] CCCpqCCCNrNsrtCCtpCsp = D[63]D[48]D[24]D[0]DD[7]DDD1DDD[0]D1D[15][10][4]D[0]D[35][0][36][53]D[48]D[19]DDD1[23][31][4]
% Meredith's Axiom (CCCCCpqCNrNsrtCCtpCsp), i.e. ((((0→1)→(¬2→¬3))→2)→4)→((4→0)→(3→0)) ; 3731 steps
[67] CCCCCpqCNrNsrtCCtpCsp = D[63]D[48]D[24]DDDD1DDD1D[57][55]1[26]1[4]D[8]D[0]DDD1DDDD[25][9][4]DD[0]DD[0]D[7][43][4]DDD1DD[0]DD[7][11][4]1DDD1D1DD[13][9]11[4][4]1D[59][26]D[15]D[35][18]