-
Notifications
You must be signed in to change notification settings - Fork 3
/
dProofs30-unfiltered25+_64cpu.log
168 lines (167 loc) · 24 KB
/
dProofs30-unfiltered25+_64cpu.log
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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
( This log file was generated by 'pmGenerator 1.2' (master branch), compiled by 'Intel(R) oneAPI DPC++/C++ Compiler 2022.1.0 (2022.1.0.20220316)'.
The run was executed on a CLAIX-2018-OPTANE MPI node
— 2-socket Intel Xeon Gold 6338, 32 cores each (64 cores total per node), 2.0 GHz, 3.20 GHz turbo mode, 512 GiB DDR4-3200 caching for 2 TiB non-volatile memory (NVM) (Intel Optane DC Persistent Memory DIMMs) —
running Linux, Rocky 8.9.
Wall-clock time: 74.6030555… h
CPU utilization: 4774.59555… core-h )
Mon Dec 11 19:13:27 2023: Process started. [pid: 235800, tid:23414160705408]
Tasks:
1. resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true)
2. generateDProofRepresentativeFiles(30, false, true, 50)
[Main] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true).
Loaded 6 custom axioms. [SHA-512/224 hash: d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f]
(1) C0C1.0 - CpCqp - 0\imply(1\imply0)
(2) CC0C1.2CC0.1C0.2 - CCpCqrCCpqCpr - (0\imply(1\imply2))\imply((0\imply1)\imply(0\imply2))
(3) CCN0N1C1.0 - CCNpNqCqp - (\not0\imply\not1)\imply(1\imply0)
(4) CL0.0 - CLpp - \nece0\imply0
(5) CLC0.1CL0L1 - CLCpqCLpLq - \nece(0\imply1)\imply(\nece0\imply\nece1)
(6) CNLN0LNLN0 - CNLNpLNLNp - \not\nece\not0\imply\nece\not\nece\not0
Supports necessitation steps.
[Main] Calling generateDProofRepresentativeFiles(30, false, true, 50).
Mon Dec 11 19:13:27 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 30, unfiltered, candidate queue capacities: 50]
0.01 ms taken to load initial representatives.
7.64 ms taken to read 6 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs2.txt. [tid:23414083688192]
11.58 ms taken to read 17 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs3.txt. [tid:23413980624640]
7.35 ms taken to read 28 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs4.txt. [tid:23413978523392]
6.42 ms taken to read 56 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs5.txt. [tid:23413976422144]
8.09 ms taken to read 89 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs6.txt. [tid:23413974320896]
9.93 ms taken to read 203 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs7.txt. [tid:23413972219648]
25.62 ms taken to read 325 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs8.txt. [tid:23413970118400]
18.16 ms taken to read 666 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs9.txt. [tid:23413968017152]
9.13 ms taken to read 1174 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs10.txt. [tid:23413965915904]
31.21 ms taken to read 2340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs11.txt. [tid:23413963814656]
53.44 ms taken to read 4106 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs12.txt. [tid:23413961713408]
25.92 ms taken to read 8396 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs13.txt. [tid:23413959612160]
40.58 ms taken to read 15153 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs14.txt. [tid:23413957510912]
41.31 ms taken to read 30340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs15.txt. [tid:23413955409664]
56.20 ms taken to read 56725 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs16.txt. [tid:23413953308416]
121.58 ms taken to read 113539 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs17.txt. [tid:23413951207168]
287.89 ms taken to read 214468 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs18.txt. [tid:23412940470016]
1934.20 ms (1 s 934.20 ms) taken to read 431896 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs19.txt. [tid:23412938368768]
4515.82 ms (4 s 515.82 ms) taken to read 829754 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs20.txt. [tid:23412936267520]
1971.10 ms (1 s 971.10 ms) taken to read 1666562 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs21.txt. [tid:23412934166272]
3157.43 ms (3 s 157.43 ms) taken to read 3250922 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs22.txt. [tid:23412932065024]
4318.74 ms (4 s 318.74 ms) taken to read 6547739 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs23.txt. [tid:23412929963776]
5931.94 ms (5 s 931.94 ms) taken to read 12887201 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs24.txt. [tid:23412927862528]
5983.16 ms (5 s 983.16 ms) total read duration.
Loaded 24 representative collections of sizes:
1 : 6
2 : 6
3 : 17
4 : 28
5 : 56
6 : 89
7 : 203
8 : 325
9 : 666
10 : 1174
11 : 2340
12 : 4106
13 : 8396
14 : 15153
15 : 30340
16 : 56725
17 : 113539
18 : 214468
19 : 431896
20 : 829754
21 : 1666562
22 : 3250922
23 : 6547739
24 : 12887201
26061711 representatives in total.
24250.96 ms (24 s 250.96 ms) taken to read 28743307 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs25-unfiltered25+.txt. [tid:23412927862528]
40288.68 ms (40 s 288.68 ms) taken to read 59305631 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs26-unfiltered25+.txt. [tid:23412929963776]
103964.26 ms (1 min 43 s 964.26 ms) taken to read 128588180 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs27-unfiltered25+.txt. [tid:23412932065024]
146587.71 ms (2 min 26 s 587.71 ms) taken to read 268614600 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs28-unfiltered25+.txt. [tid:23412934166272]
230428.90 ms (3 min 50 s 428.91 ms) taken to read 568393543 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs29-unfiltered25+.txt. [tid:23412936267520]
230439.97 ms (3 min 50 s 439.97 ms) additional read duration.
Loaded 5 more representative collections of sizes:
25 : 28743307
26 : 59305631
27 : 128588180
28 : 268614600
29 : 568393543
1079706972 representatives in total.
Mon Dec 11 19:18:12 2023: Inserted ≈ 5% of D-proof conclusions. [ 53985348 of 1079706972] (ETC: Mon Dec 11 19:33:31 2023 ; 15 min 18 s 521.42 ms remaining ; 16 min 6 s 864.65 ms total)
Mon Dec 11 19:19:03 2023: Inserted ≈10% of D-proof conclusions. [ 107970697 of 1079706972] (ETC: Mon Dec 11 19:33:56 2023 ; 14 min 52 s 879.33 ms remaining ; 16 min 32 s 88.14 ms total)
Mon Dec 11 19:19:56 2023: Inserted ≈15% of D-proof conclusions. [ 161956045 of 1079706972] (ETC: Mon Dec 11 19:34:17 2023 ; 14 min 21 s 543.75 ms remaining ; 16 min 53 s 580.88 ms total)
Mon Dec 11 19:20:51 2023: Inserted ≈20% of D-proof conclusions. [ 215941394 of 1079706972] (ETC: Mon Dec 11 19:34:40 2023 ; 13 min 48 s 696.45 ms remaining ; 17 min 15 s 870.56 ms total)
Mon Dec 11 19:21:47 2023: Inserted ≈25% of D-proof conclusions. [ 269926743 of 1079706972] (ETC: Mon Dec 11 19:34:58 2023 ; 13 min 10 s 701.56 ms remaining ; 17 min 34 s 268.75 ms total)
Mon Dec 11 19:22:42 2023: Inserted ≈30% of D-proof conclusions. [ 323912091 of 1079706972] (ETC: Mon Dec 11 19:35:06 2023 ; 12 min 23 s 611.03 ms remaining ; 17 min 42 s 301.47 ms total)
Mon Dec 11 19:23:38 2023: Inserted ≈35% of D-proof conclusions. [ 377897440 of 1079706972] (ETC: Mon Dec 11 19:35:14 2023 ; 11 min 35 s 429.39 ms remaining ; 17 min 49 s 891.37 ms total)
Mon Dec 11 19:24:32 2023: Inserted ≈40% of D-proof conclusions. [ 431882788 of 1079706972] (ETC: Mon Dec 11 19:35:14 2023 ; 10 min 42 s 112.06 ms remaining ; 17 min 50 s 186.77 ms total)
Mon Dec 11 19:25:25 2023: Inserted ≈45% of D-proof conclusions. [ 485868137 of 1079706972] (ETC: Mon Dec 11 19:35:13 2023 ; 9 min 48 s 214.71 ms remaining ; 17 min 49 s 481.29 ms total)
Mon Dec 11 19:26:19 2023: Inserted ≈50% of D-proof conclusions. [ 539853486 of 1079706972] (ETC: Mon Dec 11 19:35:15 2023 ; 8 min 55 s 633.88 ms remaining ; 17 min 51 s 267.76 ms total)
Mon Dec 11 19:27:08 2023: Inserted ≈55% of D-proof conclusions. [ 593838834 of 1079706972] (ETC: Mon Dec 11 19:35:06 2023 ; 7 min 57 s 859.10 ms remaining ; 17 min 41 s 909.10 ms total)
Mon Dec 11 19:27:57 2023: Inserted ≈60% of D-proof conclusions. [ 647824183 of 1079706972] (ETC: Mon Dec 11 19:35:00 2023 ; 7 min 2 s 432.06 ms remaining ; 17 min 36 s 80.15 ms total)
Mon Dec 11 19:28:50 2023: Inserted ≈65% of D-proof conclusions. [ 701809531 of 1079706972] (ETC: Mon Dec 11 19:34:59 2023 ; 6 min 9 s 344.05 ms remaining ; 17 min 35 s 268.72 ms total)
Mon Dec 11 19:29:42 2023: Inserted ≈70% of D-proof conclusions. [ 755794880 of 1079706972] (ETC: Mon Dec 11 19:34:58 2023 ; 5 min 16 s 440.72 ms remaining ; 17 min 34 s 802.39 ms total)
Mon Dec 11 19:30:36 2023: Inserted ≈75% of D-proof conclusions. [ 809780229 of 1079706972] (ETC: Mon Dec 11 19:35:00 2023 ; 4 min 23 s 987.03 ms remaining ; 17 min 35 s 948.13 ms total)
Mon Dec 11 19:31:32 2023: Inserted ≈80% of D-proof conclusions. [ 863765577 of 1079706972] (ETC: Mon Dec 11 19:35:03 2023 ; 3 min 31 s 966.12 ms remaining ; 17 min 39 s 830.60 ms total)
Mon Dec 11 19:32:27 2023: Inserted ≈85% of D-proof conclusions. [ 917750926 of 1079706972] (ETC: Mon Dec 11 19:35:07 2023 ; 2 min 39 s 453.94 ms remaining ; 17 min 43 s 26.26 ms total)
Mon Dec 11 19:33:25 2023: Inserted ≈90% of D-proof conclusions. [ 971736274 of 1079706972] (ETC: Mon Dec 11 19:35:12 2023 ; 1 min 46 s 853.95 ms remaining ; 17 min 48 s 539.52 ms total)
Mon Dec 11 19:34:25 2023: Inserted ≈95% of D-proof conclusions. [1025721623 of 1079706972] (ETC: Mon Dec 11 19:35:18 2023 ; 53 s 738.51 ms remaining ; 17 min 54 s 770.27 ms total)
Mon Dec 11 19:35:27 2023: Inserted 100% of D-proof conclusions. [1079706972 of 1079706972] (ETC: Mon Dec 11 19:35:27 2023 ; 0.00 ms remaining ; 18 min 3 s 1.63 ms total)
1083002.22 ms (18 min 3 s 2.22 ms) total insertion duration.
Known iteration count loaded from 30:19900274119.
Mon Dec 11 19:35:27 2023: Starting to generate D-proof representatives of length 30.
Mon Dec 11 21:06:14 2023: Iterated ≈ 2% of D-proof candidates. [ 398005482 of 19900274119] (ETC: Thu Dec 14 23:14:28 2023 ; 3 d 2 h 8 min 14 s 553.39 ms remaining ; 3 d 3 h 39 min 1 s 381.01 ms total)
Mon Dec 11 22:35:49 2023: Iterated ≈ 4% of D-proof candidates. [ 796010964 of 19900274119] (ETC: Thu Dec 14 22:44:39 2023 ; 3 d 8 min 50 s 315.37 ms remaining ; 3 d 3 h 9 min 12 s 411.83 ms total)
Tue Dec 12 00:04:28 2023: Iterated ≈ 6% of D-proof candidates. [ 1194016447 of 19900274119] (ETC: Thu Dec 14 22:19:02 2023 ; 2 d 22 h 14 min 34 s 799.01 ms remaining ; 3 d 2 h 43 min 35 s 743.63 ms total)
Tue Dec 12 01:27:29 2023: Iterated ≈ 8% of D-proof candidates. [ 1592021929 of 19900274119] (ETC: Thu Dec 14 20:55:57 2023 ; 2 d 19 h 28 min 27 s 999.51 ms remaining ; 3 d 1 h 20 min 30 s 434.25 ms total)
Tue Dec 12 02:52:23 2023: Iterated ≈10% of D-proof candidates. [ 1990027411 of 19900274119] (ETC: Thu Dec 14 20:24:45 2023 ; 2 d 17 h 32 min 22 s 664.77 ms remaining ; 3 d 49 min 18 s 516.40 ms total)
Tue Dec 12 04:16:44 2023: Iterated ≈12% of D-proof candidates. [ 2388032894 of 19900274119] (ETC: Thu Dec 14 19:59:32 2023 ; 2 d 15 h 42 min 47 s 787.64 ms remaining ; 3 d 24 min 5 s 213.22 ms total)
Tue Dec 12 05:45:04 2023: Iterated ≈14% of D-proof candidates. [ 2786038376 of 19900274119] (ETC: Thu Dec 14 20:09:50 2023 ; 2 d 14 h 24 min 46 s 141.20 ms remaining ; 3 d 34 min 22 s 954.88 ms total)
Tue Dec 12 07:08:37 2023: Iterated ≈16% of D-proof candidates. [ 3184043859 of 19900274119] (ETC: Thu Dec 14 19:47:49 2023 ; 2 d 12 h 39 min 11 s 230.72 ms remaining ; 3 d 12 min 21 s 941.33 ms total)
Tue Dec 12 08:31:07 2023: Iterated ≈18% of D-proof candidates. [ 3582049341 of 19900274119] (ETC: Thu Dec 14 19:24:42 2023 ; 2 d 10 h 53 min 35 s 417.14 ms remaining ; 2 d 23 h 49 min 15 s 386.75 ms total)
Tue Dec 12 09:49:20 2023: Iterated ≈20% of D-proof candidates. [ 3980054823 of 19900274119] (ETC: Thu Dec 14 18:44:51 2023 ; 2 d 8 h 55 min 31 s 682.96 ms remaining ; 2 d 23 h 9 min 24 s 603.69 ms total)
Tue Dec 12 11:08:12 2023: Iterated ≈22% of D-proof candidates. [ 4378060306 of 19900274119] (ETC: Thu Dec 14 18:15:14 2023 ; 2 d 7 h 7 min 1 s 957.55 ms remaining ; 2 d 22 h 39 min 47 s 125.06 ms total)
Tue Dec 12 12:30:18 2023: Iterated ≈24% of D-proof candidates. [ 4776065788 of 19900274119] (ETC: Thu Dec 14 18:04:03 2023 ; 2 d 5 h 33 min 44 s 163.61 ms remaining ; 2 d 22 h 28 min 36 s 4.74 ms total)
Tue Dec 12 13:51:59 2023: Iterated ≈26% of D-proof candidates. [ 5174071270 of 19900274119] (ETC: Thu Dec 14 17:52:54 2023 ; 2 d 4 h 55 s 311.86 ms remaining ; 2 d 22 h 17 min 27 s 718.72 ms total)
Tue Dec 12 15:12:57 2023: Iterated ≈28% of D-proof candidates. [ 5572076753 of 19900274119] (ETC: Thu Dec 14 17:40:51 2023 ; 2 d 2 h 27 min 53 s 212.25 ms remaining ; 2 d 22 h 5 min 23 s 905.90 ms total)
Tue Dec 12 16:37:43 2023: Iterated ≈30% of D-proof candidates. [ 5970082235 of 19900274119] (ETC: Thu Dec 14 17:43:02 2023 ; 2 d 1 h 5 min 18 s 979.73 ms remaining ; 2 d 22 h 7 min 35 s 685.32 ms total)
Tue Dec 12 17:57:16 2023: Iterated ≈32% of D-proof candidates. [ 6368087718 of 19900274119] (ETC: Thu Dec 14 17:28:38 2023 ; 1 d 23 h 31 min 22 s 19.75 ms remaining ; 2 d 21 h 53 min 11 s 205.52 ms total)
Tue Dec 12 19:23:29 2023: Iterated ≈34% of D-proof candidates. [ 6766093200 of 19900274119] (ETC: Thu Dec 14 17:35:34 2023 ; 1 d 22 h 12 min 4 s 819.16 ms remaining ; 2 d 22 h 7 s 301.75 ms total)
Tue Dec 12 20:49:01 2023: Iterated ≈36% of D-proof candidates. [ 7164098682 of 19900274119] (ETC: Thu Dec 14 17:39:47 2023 ; 1 d 20 h 50 min 46 s 799.59 ms remaining ; 2 d 22 h 4 min 20 s 624.34 ms total)
Tue Dec 12 22:14:51 2023: Iterated ≈38% of D-proof candidates. [ 7562104165 of 19900274119] (ETC: Thu Dec 14 17:44:23 2023 ; 1 d 19 h 29 min 32 s 769.86 ms remaining ; 2 d 22 h 8 min 56 s 725.58 ms total)
Tue Dec 12 23:40:30 2023: Iterated ≈40% of D-proof candidates. [ 7960109647 of 19900274119] (ETC: Thu Dec 14 17:48:04 2023 ; 1 d 18 h 7 min 34 s 712.40 ms remaining ; 2 d 22 h 12 min 37 s 853.99 ms total)
Wed Dec 13 01:07:37 2023: Iterated ≈42% of D-proof candidates. [ 8358115129 of 19900274119] (ETC: Thu Dec 14 17:54:55 2023 ; 1 d 16 h 47 min 17 s 656.38 ms remaining ; 2 d 22 h 19 min 28 s 373.04 ms total)
Wed Dec 13 02:33:56 2023: Iterated ≈44% of D-proof candidates. [ 8756120612 of 19900274119] (ETC: Thu Dec 14 17:59:17 2023 ; 1 d 15 h 25 min 21 s 251.38 ms remaining ; 2 d 22 h 23 min 50 s 806.02 ms total)
Wed Dec 13 03:58:17 2023: Iterated ≈46% of D-proof candidates. [ 9154126094 of 19900274119] (ETC: Thu Dec 14 17:59:00 2023 ; 1 d 14 h 42 s 976.11 ms remaining ; 2 d 22 h 23 min 32 s 918.70 ms total)
Wed Dec 13 05:21:01 2023: Iterated ≈48% of D-proof candidates. [ 9552131577 of 19900274119] (ETC: Thu Dec 14 17:55:22 2023 ; 1 d 12 h 34 min 21 s 684.55 ms remaining ; 2 d 22 h 19 min 55 s 547.21 ms total)
Wed Dec 13 06:45:09 2023: Iterated ≈50% of D-proof candidates. [ 9950137059 of 19900274119] (ETC: Thu Dec 14 17:54:52 2023 ; 1 d 11 h 9 min 42 s 660.87 ms remaining ; 2 d 22 h 19 min 25 s 321.73 ms total)
Wed Dec 13 08:08:52 2023: Iterated ≈52% of D-proof candidates. [10348142541 of 19900274119] (ETC: Thu Dec 14 17:53:33 2023 ; 1 d 9 h 44 min 41 s 515.03 ms remaining ; 2 d 22 h 18 min 6 s 489.62 ms total)
Wed Dec 13 09:33:29 2023: Iterated ≈54% of D-proof candidates. [10746148024 of 19900274119] (ETC: Thu Dec 14 17:54:03 2023 ; 1 d 8 h 20 min 33 s 397.22 ms remaining ; 2 d 22 h 18 min 36 s 80.92 ms total)
Wed Dec 13 10:57:31 2023: Iterated ≈56% of D-proof candidates. [11144153506 of 19900274119] (ETC: Thu Dec 14 17:53:25 2023 ; 1 d 6 h 55 min 54 s 506.76 ms remaining ; 2 d 22 h 17 min 58 s 424.43 ms total)
Wed Dec 13 12:21:04 2023: Iterated ≈58% of D-proof candidates. [11542158989 of 19900274119] (ETC: Thu Dec 14 17:52:02 2023 ; 1 d 5 h 30 min 58 s 49.62 ms remaining ; 2 d 22 h 16 min 35 s 356.24 ms total)
Wed Dec 13 13:47:47 2023: Iterated ≈60% of D-proof candidates. [11940164471 of 19900274119] (ETC: Thu Dec 14 17:56:00 2023 ; 1 d 4 h 8 min 13 s 241.10 ms remaining ; 2 d 22 h 20 min 33 s 102.75 ms total)
Wed Dec 13 15:10:52 2023: Iterated ≈62% of D-proof candidates. [12338169953 of 19900274119] (ETC: Thu Dec 14 17:53:51 2023 ; 1 d 2 h 42 min 59 s 809.12 ms remaining ; 2 d 22 h 18 min 24 s 760.80 ms total)
Wed Dec 13 16:35:51 2023: Iterated ≈64% of D-proof candidates. [12736175436 of 19900274119] (ETC: Thu Dec 14 17:54:50 2023 ; 1 d 1 h 18 min 58 s 784.96 ms remaining ; 2 d 22 h 19 min 23 s 291.55 ms total)
Wed Dec 13 17:58:42 2023: Iterated ≈66% of D-proof candidates. [13134180918 of 19900274119] (ETC: Thu Dec 14 17:52:30 2023 ; 23 h 53 min 47 s 931.10 ms remaining ; 2 d 22 h 17 min 3 s 326.75 ms total)
Wed Dec 13 19:20:44 2023: Iterated ≈68% of D-proof candidates. [13532186400 of 19900274119] (ETC: Thu Dec 14 17:49:06 2023 ; 22 h 28 min 22 s 334.23 ms remaining ; 2 d 22 h 13 min 39 s 794.42 ms total)
Wed Dec 13 20:43:16 2023: Iterated ≈70% of D-proof candidates. [13930191883 of 19900274119] (ETC: Thu Dec 14 17:46:37 2023 ; 21 h 3 min 20 s 985.82 ms remaining ; 2 d 22 h 11 min 9 s 952.73 ms total)
Wed Dec 13 22:07:08 2023: Iterated ≈72% of D-proof candidates. [14328197365 of 19900274119] (ETC: Thu Dec 14 17:46:08 2023 ; 19 h 38 min 59 s 453.41 ms remaining ; 2 d 22 h 10 min 40 s 905.00 ms total)
Wed Dec 13 23:29:55 2023: Iterated ≈74% of D-proof candidates. [14726202848 of 19900274119] (ETC: Thu Dec 14 17:44:12 2023 ; 18 h 14 min 16 s 496.04 ms remaining ; 2 d 22 h 8 min 44 s 984.76 ms total)
Thu Dec 14 00:50:47 2023: Iterated ≈76% of D-proof candidates. [15124208330 of 19900274119] (ETC: Thu Dec 14 17:39:50 2023 ; 16 h 49 min 3 s 167.58 ms remaining ; 2 d 22 h 4 min 23 s 198.22 ms total)
Thu Dec 14 02:12:41 2023: Iterated ≈78% of D-proof candidates. [15522213812 of 19900274119] (ETC: Thu Dec 14 17:37:02 2023 ; 15 h 24 min 21 s 13.61 ms remaining ; 2 d 22 h 1 min 35 s 516.36 ms total)
Thu Dec 14 03:35:17 2023: Iterated ≈80% of D-proof candidates. [15920219295 of 19900274119] (ETC: Thu Dec 14 17:35:15 2023 ; 13 h 59 min 57 s 593.97 ms remaining ; 2 d 21 h 59 min 47 s 969.82 ms total)
Thu Dec 14 04:56:53 2023: Iterated ≈82% of D-proof candidates. [16318224777 of 19900274119] (ETC: Thu Dec 14 17:32:20 2023 ; 12 h 35 min 26 s 363.64 ms remaining ; 2 d 21 h 56 min 53 s 131.32 ms total)
Thu Dec 14 06:16:49 2023: Iterated ≈84% of D-proof candidates. [16716230259 of 19900274119] (ETC: Thu Dec 14 17:27:33 2023 ; 11 h 10 min 44 s 234.04 ms remaining ; 2 d 21 h 52 min 6 s 462.68 ms total)
Thu Dec 14 07:37:18 2023: Iterated ≈86% of D-proof candidates. [17114235742 of 19900274119] (ETC: Thu Dec 14 17:23:38 2023 ; 9 h 46 min 20 s 819.42 ms remaining ; 2 d 21 h 48 min 11 s 567.26 ms total)
Thu Dec 14 08:58:30 2023: Iterated ≈88% of D-proof candidates. [17512241224 of 19900274119] (ETC: Thu Dec 14 17:20:44 2023 ; 8 h 22 min 14 s 99.54 ms remaining ; 2 d 21 h 45 min 17 s 496.12 ms total)
Thu Dec 14 10:19:38 2023: Iterated ≈90% of D-proof candidates. [17910246707 of 19900274119] (ETC: Thu Dec 14 17:17:53 2023 ; 6 h 58 min 14 s 587.18 ms remaining ; 2 d 21 h 42 min 25 s 871.82 ms total)
Thu Dec 14 11:40:36 2023: Iterated ≈92% of D-proof candidates. [18308252189 of 19900274119] (ETC: Thu Dec 14 17:14:58 2023 ; 5 h 34 min 21 s 701.54 ms remaining ; 2 d 21 h 39 min 31 s 269.18 ms total)
Thu Dec 14 13:00:31 2023: Iterated ≈94% of D-proof candidates. [18706257671 of 19900274119] (ETC: Thu Dec 14 17:11:04 2023 ; 4 h 10 min 32 s 212.39 ms remaining ; 2 d 21 h 35 min 36 s 872.97 ms total)
Thu Dec 14 14:19:47 2023: Iterated ≈96% of D-proof candidates. [19104263154 of 19900274119] (ETC: Thu Dec 14 17:06:37 2023 ; 2 h 46 min 50 s 831.69 ms remaining ; 2 d 21 h 31 min 10 s 792.27 ms total)
Thu Dec 14 15:39:49 2023: Iterated ≈98% of D-proof candidates. [19502268636 of 19900274119] (ETC: Thu Dec 14 17:03:10 2023 ; 1 h 23 min 21 s 266.00 ms remaining ; 2 d 21 h 27 min 43 s 299.87 ms total)
Thu Dec 14 16:59:26 2023: Iterated 100% of D-proof candidates. [19900274119 of 19900274119] (ETC: Thu Dec 14 16:59:26 2023 ; 0.00 ms remaining ; 2 d 21 h 23 min 59 s 196.82 ms total)
249905810.87 ms (2 d 21 h 25 min 5 s 810.87 ms) taken to collect 1186223457 D-proofs of length 30. [iterated 19900274119 condensed detachment proof strings]
[Copy] Custom iteration counts: { { 1, 6 }, { 2, 6 }, { 3, 42 }, { 4, 89 }, { 5, 268 }, { 6, 596 }, { 7, 1386 }, { 8, 2895 }, { 9, 6517 }, { 10, 13164 }, { 11, 28088 }, { 12, 56806 }, { 13, 117775 }, { 14, 235494 }, { 15, 484132 }, { 16, 965558 }, { 17, 1965114 }, { 18, 3929633 }, { 19, 7965680 }, { 20, 15939098 }, { 21, 32291194 }, { 22, 64783208 }, { 23, 131182254 }, { 24, 264050751 }, { 25, 535260845 }, { 26, 1083165713 }, { 27, 2233996317 }, { 28, 4589712682 }, { 29, 9565398427 }, { 30, 19900274119 }, { 31, 41704865935 } }
7016739.70 ms (1 h 56 min 56 s 739.70 ms) taken to filter and order new representative proofs.
Found 1186223457 representative, 4926229547 redundant, and 13787821115 invalid condensed detachment proof strings.
lengths up to 30 ; amounts per length: {(1,6), (2,6), (3,17), (4,28), (5,56), (6,89), (7,203), (8,325), (9,666), (10,1174), (11,2340), (12,4106), (13,8396), (14,15153), (15,30340), (16,56725), (17,113539), (18,214468), (19,431896), (20,829754), (21,1666562), (22,3250922), (23,6547739), (24,12887201), (25,28743307), (26,59305631), (27,128588180), (28,268614600), (29,568393543), (30,1186223457)} ; 1186223457 new representative proofs (4926229547 redundant, 13787821115 invalid)
Thu Dec 14 19:34:03 2023: Starting to write 1186223457 entries to data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs30-unfiltered25+.txt.
1071447.34 ms (17 min 51 s 447.34 ms) taken to print and save 118130673527 bytes of representative condensed detachment proof strings to data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs30-unfiltered25+.txt.
Thu Dec 14 20:05:20 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 30, unfiltered, candidate queue capacities: 50]
Thu Dec 14 21:49:38 2023: Process terminated. [pid: 235800, tid:23414160705408]