-
-
Notifications
You must be signed in to change notification settings - Fork 3
Expand file tree
/
Copy pathw3.txt
More file actions
129 lines (110 loc) · 8.88 KB
/
Copy pathw3.txt
File metadata and controls
129 lines (110 loc) · 8.88 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
122
123
124
125
126
127
128
129
% Walsh's 3rd Axiom (CpCCNqCCNrsCptCCtqCrq), i.e. 0→((¬1→((¬2→3)→(0→4)))→((4→1)→(2→1)))
% Completeness follows w.r.t. CpCqp,CCpCqrCCpqCpr,CCNpNqCqp and CCpqCCqrCpr,CCNppp,CpCNpq.
%
% Proof system configuration: pmGenerator -c -n -s CpCCNqCCNrsCptCCtqCrq
% SHA-512/224 hash: 0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314
%
% Full summary: pmGenerator --transform data/w3.txt -f -n -t _
% Step counting: pmGenerator --transform data/w3.txt -f -n -t . -p -2 -d
% - all: pmGenerator --transform data/w3.txt -f -n -t _ -p -2 -d
% - targets: pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq,CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCqCprCCNrCCNstqCsr,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -p -2 -d
% - 1st PMC: pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% - 2nd PMC: pmGenerator --transform data/w3.txt -f -n -t CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCqCprCCNrCCNstqCsr,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -p -2 -d
% Compact (2837 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq,CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCqCprCCNrCCNstqCsr,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw,CCCNpqCCCNrCCNstCCuCCNvCCNwxCuyCCyvCwvzCCzrCsrqCCqaCpa,CCCCCpCCNqCCNrsCtuCCuqCrqvCCCNqCCNrsCtuCCuqCrqvwCxw,CCCpCqrsCCqrs,CCCCCCpqCrqsCtsuCqu,CCpqCrCpq,CCCpqrCqr,CCCNpqrCpr,CpCCqpCrp,CCCCNpqCrqpCsp,CpCCqrCrr,CCCCCNpCCNqrCstCCtpCqpCNCNuvwxCux,CCCCCpqrCsrtCqt,CpCNNCqrCsCqr,CCCCCpqrCsrtCCCuCCNvCCNwxCuyCCyvCwvNpt,CNpCqCCCprsCts,CpCCNCqrrCqr,CCCpCCCCqrstCutrCqr,CCCpCqrCsCCNrtCutCvCsCCNrtCut,CCCpCqrCstCCqtCst,CCCpqCCrsCtsCCNsCCNtuCprCCrsCts,CCCCpqCrqCstCCCqutCst,CCCNpqCpqCCqrCpr,CCNCpCqCrsCCNtuCrvCCvCpCqCrsCtCpCqCrs,CCCCNpqCrqCstCCNCpCrqtCst
% - 1st PMC (1101 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCpCqrsCCqrs,CCCNpqrCpr,CCCCNpqCrqpCsp,CpCNNCqrCsCqr,CCCpCCCCqrstCutrCqr,CCCpCqrCstCCqtCst,CCCNpqCpqCCqrCpr,CCCCpqCrqsCCsCCrqtCuCCrqt
% - 2nd PMC (2505 bytes): pmGenerator --transform data/w3.txt -f -n -t CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCqCprCCNrCCNstqCsr,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw,CCCNpqCCCNrCCNstCCuCCNvCCNwxCuyCCyvCwvzCCzrCsrqCCqaCpa,CCCCCpCCNqCCNrsCtuCCuqCrqvCCCNqCCNrsCtuCCuqCrqvwCxw,CCCpCqrsCCqrs,CCCCCCpqCrqsCtsuCqu,CCCpqrCqr,CpCCqpCrp,CCCCNpqCrqpCsp,CpCCqrCrr,CCCCCNpCCNqrCstCCtpCqpCNCNuvwxCux,CpCNNCqrCsCqr,CCCCCpqrCsrtCCCuCCNvCCNwxCuyCCyvCwvNpt,CNpCqCCCprsCts,CpCCNCqrrCqr,CCCpCCCCqrstCutrCqr,CCCpCqrCsCCNrtCutCvCsCCNrtCut,CCCpCqrCstCCqtCst,CCCpqCCrsCtsCCNsCCNtuCprCCrsCts,CCCCpqCrqCstCCCqutCst,CCCNpqCpqCCqrCpr,CCNCpCqCrsCCNtuCrvCCvCpCqCrsCtCpCqCrs,CCCCNpqCrqCstCCNCpCrqtCst
% Concrete (34479 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq,CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCqCprCCNrCCNstqCsr,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -j -1 -e
% - 1st PMC (6080 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -e
% - 2nd PMC (28426 bytes): pmGenerator --transform data/w3.txt -f -n -t CCCCCpqCNrNsrtCCtpCsp,CCpCCNpqrCsCCNtCrtCpt,CpCCqCprCCNrCCNstqCsr,CpCCNqCCNrsCtqCCrtCrq,CCpqCCCrCstCqCNsNpCps,CCCpqCCCNrNsrtCCtpCsp -j -1 -e
CpCCNqCCNrsCptCCtqCrq = 1
[0] CCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqp = D11
[1] CCNpCCNqrCCCNsCCNtuCCvCCNwCCNxyCvzCCzwCxwaCCasCtsbCCbpCqp = D1[0]
[2] CCCpCCNqCCNrsCtuCCuqCrqvCCCNqCCNrsCtuCCuqCrqv = D[0]1
[3] CCCpCCqrCsrtCCCqrCsrt = D[1]1
[4] CCNpCCNqrCCCCsCCtuCvuwCCCtuCvuwxCCxpCqp = D1[3]
[5] CCCpCCCNqCCNrsCtuCCuqCrqvwCCCCNqCCNrsCtuCCuqCrqvw = DD1[2]1
[6] CCCpqCrqCCNsCCNtuCCvCCpqCrqwCCwsCts = D[3]1
[7] CCCpCCCqrCsrtuCCCCqrCsrtu = D[4]1
[8] CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw = D[3][0]
[9] CCNpCCNqrCCCCNstCCuCCNvCCNwxCuyCCyvCwvtCCtzCszaCCapCqp = D1[8]
[10] CCCNpqCCCNrCCNstCCuCCNvCCNwxCuyCCyvCwvzCCzrCsrqCCqaCpa = D[3][1]
[11] CCCNpCCNqCCNrsCNptCCtqCrqCCCrqpCqpCCCCCrqpCqpuCvu = D[2][8]
[12] CCCpqCrqCCNsCCNtuCCvCCwCrqCCpqCrqxCCxsCts = D[3][6]
[13] CCCCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqpCyCCxpCqpCCCyCCxpCqpzCaz = D[3][10]
[14] CCCCCpCCNqCCNrsCtuCCuqCrqvCCCNqCCNrsCtuCCuqCrqvwCxw = D[11][0]
[15] CCCCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqpyCCyzCaz = D[5][10]
[16] CCCCCpCCqrCsrtCCCqrCsrtuCvu = D[11][1]
[17] CCCpCqrsCCqrs = DD1[14]1
[18] CCCCCpCCqrCsrtCCCqrCsrtCuCCCqrCsrtCCCuCCCqrCsrtvCwv = D[3]D[3][4]
[19] CCCpqCrqCsCCpqCrq = D[3][14]
[20] CCCNpqCCrCCNsCCNtuCrvCCvsCtswCCwxCpx = D[17][0]
[21] CCCpqCrqCCCCpqCrqsCts = D[3][15]
[22] CCCCCpqrCqrsCts = D[20]1
[23] CCCCCCNpCCNqrCstCCtpCqpuCCCvwCxwCCCNpCCNqrCstCCtpCqpuyCzy = D[18][5]
[24] CCCCCCpqCrqsCtsuCqu = DD[17]D[6]11
[25] CCpqCrCpq = D[17][14]
[26] CCCpqrCqr = DDD[22]D[3][2]1[0]
[27] CCCNpqrCpr = D[0]D[16][17]
[28] CCCpqCrqCsCtCCpqCrq = D[3][25]
[29] CpCCqpCrp = D[27][0]
[30] CCNppCqp = D[0][29]
[31] CCCpqCrqCCsCtCCpqCrqCuCtCCpqCrq = D[3][29]
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 67 steps
[32] CpCqp = DDD[22][22]11
[33] CpCCCqCCprCsrtCut = D[24]D[3]D[3][9]
[34] CpCqCrCCpsCts = D[24]D[13][3]
[35] CCCCNpqCrqpCsp = D[0][34]
[36] CpCCqrCrr = DDD[22]D[3]D[3]D1[15]1[0]
[37] CCpqCrCsCtCuCpq = D[24]DD[2]D[3]DD[17]11[0]
[38] CCCCCNpCCNqrCstCCtpCqpCNCNuvwxCux = D[0]D[23]D[0]D[23][17]
[39] CCCCCpqrCsrtCqt = DD[17]D[12][30]1
[40] CCNpCCNqrCCCCCCstuCvuwCtwxCCxpCqp = D1[39]
% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 127 steps
[41] CpCNpq = D[27]D[8][30]
% Identity principle (Cpp), i.e. 0→0 ; 135 steps
[42] Cpp = DD[27]D[0]DD[1]DDD[3]D[3]D1[10][3][17][0]1
[43] CpCNNCqrCsCqr = D[35]D[15]D[35]D[0]DD[0]D[16]D[0]D[23][38][0]
[44] CCCCCpqrCsrtCCCuCCNvCCNwxCuyCCyvCwvNpt = DD[17]D[12]D[8]D[0]D[43]11
[45] CCCpCCNqCCNrsCptCCtqCrqNCCNuvCwvCxCyCzu = D[44]DD[3]D1[34]1
[46] CNpCqCCCprsCts = D[26]D[44][19]
[47] CCCpCqrCCNrsCtsCuCCNrsCts = DD1[35][46]
[48] CpCCNCqrrCqr = DD[0]D[26][45][14]
[49] CCCpCCCCqrstCutrCqr = DDD[0]D[26]D[44][22][33]1
[50] CCCpCqrCsCCNrtCutCvCsCCNrtCut = DD1D[9]D[24][19][46]
[51] CpCCqCrsCCNqsCrs = D[50][8]
[52] CCpCqrCCNprCqr = D[51]1
[53] CCCCpqCrqCstCCCuCqvtCst = D[49]D[3]D1[24]
[54] CCCpCqrCstCCqtCst = D[53][8]
[55] CCCpqCCrsCtsCCNsCCNtuCprCCrsCts = DD[54][15]1
[56] CCCCpqCrqCstCCCqutCst = DD[53][21][15]
[57] CCCCpqCrqCpsCtCps = DD[3]DD[53][6][25]1
[58] CpCCNqCCNrsCrtCCtqCrq = DD[54][28]1
[59] CCCpCqrCCstCutCCNtCCNuvCCNqwsCCstCut = DD[49]D[3]D1DD[17]D1[36]11
[60] CCNpCCNqrCqsCCspCqp = D[58]1
[61] CCCNpqCCNprqCCqsCps = D[3]D[55][20]
[62] CCCNpqCpqCCqrCpr = D[3][60]
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 711 steps
[63] CCNppp = DDD[54][2][30][0]
[64] CCCNpqCrqCCqCrsCpCrs = D[3]D[55][29]
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 733 steps
[65] CCpqCCqrCpr = D[17][62]
[66] CCNCpCqCrsCCNtuCrvCCvCpCqCrsCtCpCqCrs = D[55][37]
[67] CCCCpqCrqsCCsCCrqtCuCCrqt = D[7]D[3]DDD[49]D[3][40]1[25]
% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 1195 steps
[68] CCNpNqCqp = D[27]D[0]DDDD[17][64]1D[13][43]1
[69] CCCCNpqCrqCstCCNCpCrqtCst = DD[3]DDDDDD[50][21]1[8][33]1[7][51]
[70] CCpCqCrCstCCspCqCrCst = D[66][48]
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 2973 steps
[71] CCpCqrCCpqCpr = DDD[67][64]D[67][62]1
% Walsh's 4th Axiom (CpCCNqCCNrsCtqCCrtCrq), i.e. 0→((¬1→((¬2→3)→(4→1)))→((2→4)→(2→1))) ; 3497 steps
[72] CpCCNqCCNrsCtqCCrtCrq = DDD[17]D[6][36]1DD[70]D[2][62]D[70]1
% Walsh's 6th Axiom (CCCpqCCCNrNsrtCCtpCsp), i.e. ((0→1)→(((¬2→¬3)→2)→4))→((4→0)→(3→0)) ; 4011 steps
[73] CCCpqCCCNrNsrtCCtpCsp = DDDDD[56][8]1D[24]DD[2]D[3]D1D[14][17][1][48]D[17]D[3]DDDD[59][31][48]1DDDD[54][13]1[0][48]
% Meredith's Axiom (CCCCCpqCNrNsrtCCtpCsp), i.e. ((((0→1)→(¬2→¬3))→2)→4)→((4→0)→(3→0)) ; 4187 steps
[74] CCCCCpqCNrNsrtCCtpCsp = D[17]D[3]D[55]DD[57]DD[3]D1DDD[3][66][51]D[3]DDDD[47][37]111DD[56][28]11
% Walsh's 1st Axiom (CCpCCNpqrCsCCNtCrtCpt), i.e. (0→((¬0→1)→2))→(3→((¬4→(2→4))→(0→4))) ; 4659 steps
[75] CCpCCNpqrCsCCNtCrtCpt = DDD[3][61]D[69][61]DD[57]DD[3]D[6]D[52]DDD[0]D[26]D[7]D[7][14][45]111
% Walsh's 5th Axiom (CCpqCCCrCstCqCNsNpCps), i.e. (0→1)→(((2→(3→4))→(1→(¬3→¬0)))→(0→3)) ; 5851 steps
[76] CCpqCCCrCstCqCNsNpCps = DDD[3]DDDDD[40][46][31]1[6]1[58]DDD[3]D1[68]D[69][64]D[8]D[52]DD1D[0]DD[18][17][17][46]
% Walsh's 2nd Axiom (CpCCqCprCCNrCCNstqCsr), i.e. 0→((1→(0→2))→((¬2→((¬3→4)→1))→(3→2))) ; 6017 steps
[77] CpCCqCprCCNrCCNstqCsr = DDD[3]D1[25]DDD[50]D[39][13]1[62]DDDD[66]D[22]DD[3]D[3]D1[60][3]D[3][62]1DD[59][29]DD[35]DD[3]D[55]DD[0]DD[18][7][17][14]D[47]D[38]D[13]11