forked from xamidi/pmGenerator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathw3.txt
89 lines (77 loc) · 4.46 KB
/
w3.txt
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
% 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 . -j 1
% Step counting: pmGenerator --transform data/w3.txt -f -n -t . -p -2 -d
% pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -p -2 -d
% Compact (1951 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -j -1 -s CCCpCCqrCsrtCCCqrCsrt,CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw,CCCCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqpyCCyzCaz,CCCpCqrsCCqrs,CCCpqrCqr,CCCNpqrCpr,CCNppCqp,CCCCNpqCrqpCsp,CpCCpqCrq,CCCNCNpqrsCps,CpCqCrp,CCCCCpqrCsrtCqt,CNNCpqCrCpq,CCNCCpCqpNrsCrs,CCpNpCqNp,CCpCqNpCrCqNp,CCCpqrCNpr,CCNpqCNCrpq,CCpqCNCprq,CCNpqCNCrCspq,CCpqCCNppq,CCNCpqrCCrqCpq,CCpCpqCpq,CCCCpqCrqsCps,CCpCqrCqCpr
% Concrete (296514 bytes): pmGenerator --transform data/w3.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -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] CCCpCCCqrCsrtuCCCCqrCsrtu = D[4]1
[7] CCCNpqCCrCCNsCCNtuCrvCCvsCtsqCCqwCpw = D[3][0]
[8] CCCNpqCCCNrCCNstCCuCCNvCCNwxCuyCCyvCwvzCCzrCsrqCCqaCpa = D[3][1]
[9] CCCNpCCNqCCNrsCNptCCtqCrqCCCrqpCqpCCCCCrqpCqpuCvu = D[2][7]
[10] CCCCCpCCNqCCNrsCtuCCuqCrqvCCCNqCCNrsCtuCCuqCrqvwCxw = D[9][0]
[11] CCCCNpCCNqrCCsCCNtCCNuvCswCCwtCutxCCxpCqpyCCyzCaz = D[5][8]
[12] CCCCCpCCqrCsrtCCCqrCsrtuCvu = D[9][1]
[13] CCCpCqrsCCqrs = DD1[10]1
[14] CCCNpqCCrCCNsCCNtuCrvCCvsCtswCCwxCpx = D[13][0]
[15] CCCCCpqrCqrsCts = D[14]1
[16] CCCCpqCrqsCtCCCpqCrqs = D[6][10]
[17] CCpqCCCpqrCsr = D[13][11]
[18] CCCpqrCqr = DDD[15]D[3][2]1[0]
[19] CCCNpqrCpr = D[0]D[12][13]
[20] CpCCqpCrp = D[19][0]
[21] CCNppCqp = D[0][20]
% Axiom 1 by Frege (CpCqp), i.e. 0→(1→0) ; 67 steps
[22] CpCqp = DDD[15][15]11
[23] CCCCNpqCrqpCsp = D[0]DDD[13]DD[3]111DD[3][8][3]
[24] CpCCpqCrq = DD[1]DDD[3]D[3]D1[8][3][13][0]
[25] CCCNCNpqrsCps = D[0]D[12]D[0]DDD[3]D[3][4][5][13]
[26] CCpqCrCpq = D[13][10]
[27] CpCqCrp = D[18][26]
[28] CCCCCpqrCsrtCqt = DD[13]DD[3]D[13]1[21]1
% Axiom 3 by Łukasiewicz (CpCNpq), i.e. 0→(¬0→1) ; 127 steps
[29] CpCNpq = D[19]D[7][21]
% Identity principle (Cpp), i.e. 0→0 ; 135 steps
[30] Cpp = DD[19]D[0][24]1
[31] CNNCpqCrCpq = DD[23]D[11]D[23]D[0]D[25]DD[0]DDD[3]D[3]D1D[6][3][13][13][10]1
[32] CCpNCCqCrqpCsNCCqCrqp = DD1[22][31]
[33] CCNCCpCqpNrsCrs = D[7][32]
[34] CCpNCCqqpCrNCCqqp = DD1[30][31]
[35] CpCqCrNCCsCtsNp = D[33][27]
[36] CCCpCqpNCNCrNCNsstCus = DD[7]D[0]D[18]D[19][35][21]
[37] CCpNpCqNp = D[0]D[28]D[11]D[19]D[0]D[33][24]
[38] CCpCqNpCrCqNp = D[0]D[18]DD[7]D[0]D[18][35][20]
[39] CCCpqrCNpr = DDD[0]D[28]D[17]D[19]D[14]D[13]D[19][34][17]1
[40] CpCqCrNNp = D[19][38]
% Axiom 2 by Łukasiewicz (CCNppp), i.e. (¬0→0)→0 ; 1331 steps
[41] CCNppp = D[33]DDD[0]D[18]DDD1[6]1[16][36]1
[42] CCNpqCNCrpq = D[7]D[0]D[18]DD[7]D[0]D[33]D[18][16]D[18][40]
[43] CCpqCNCprq = D[7]D[0]DDD[0]D[28]D[17]D[19]D[14]D[19][32]DDD[13]D1DDD[15]D[3]D[3]D1[11]1[0]1DD[3][11][37]1
[44] CNCpqCrCsp = D[43][27]
[45] CCNpqCNCrCspq = D[7]D[0]D[18]DD[7]D[0]DD[7][34][20]D[18]D[13][40]
[46] CCpCpqCrCpq = D[0][44]
[47] CCpqCCNppq = D[7]D[0]D[39]D[0]DD[23]D[17]D[18][36]1
[48] CCNCpqrCCrqCpq = DD[47]DD1[21]DDD[3]D[3]D1[7][6][13]D[45]1
[49] CCpCpqCpq = DD[46][46]1
[50] CCCCpqCrqsCps = DD[13]D1D[6]D[3]DD[15]11D[47]D[28][49]
[51] CCpqCCNqpq = D[0]D[50][47]
[52] CpCCpqq = D[50][49]
% Axiom 1 by Łukasiewicz (CCpqCCqrCpr), i.e. (0→1)→((1→2)→(0→2)) ; 16469 steps
[53] CCpqCCqrCpr = DDD1[43]D[26]D[47][52][48]
% Axiom 3 for Frege by Łukasiewicz (CCNpNqCqp), i.e. (¬0→¬1)→(1→0) ; 23321 steps
[54] CCNpNqCqp = DD[7][37]DD[49]D[0]D[42][44]DD[51]D[18]D[19][33]D[42]D[49]DD[7]D[0]D[25][38][45]
[55] CCCCpqCrqsCCrps = D[53][53]
[56] CCpCqrCqCpr = D[55]D[53][52]
% Axiom 2 by Frege (CCpCqrCCpqCpr), i.e. (0→(1→2))→((0→1)→(0→2)) ; 254925 steps
[57] CCpCqrCCpqCpr = D[56]D[55]D[48]DD[56]D[39][51]D[56]D[55][39]