forked from xamidi/pmGenerator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
dProofs163-unfiltered153+_64cpu.log
266 lines (265 loc) · 35.3 KB
/
dProofs163-unfiltered153+_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
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
( 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.8.
Wall-clock time: 14.43444… h
CPU utilization: 923.80444… core-h )
Thu Nov 9 19:47:45 2023: Process started. [pid: 254588, tid:23141686105984]
Tasks:
1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true)
2. generateDProofRepresentativeFiles(163, false, true)
[Main] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9]
(1) C0CCN1CCN2.3C4.1CC2.4C2.1 - CpCCNqCCNrsCtqCCrtCrq - 0\imply((\not1\imply((\not2\imply3)\imply(4\imply1)))\imply((2\imply4)\imply(2\imply1)))
[Main] Calling generateDProofRepresentativeFiles(163, false, true).
Thu Nov 9 19:47:45 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 163, unfiltered]
0.03 ms taken to load initial representatives.
0.04 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:23141621655296]
1.44 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:23141590136576]
1.30 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:23141623756544]
2.38 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:23141613250304]
0.42 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:23141571225344]
1.26 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:23141609047808]
0.01 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:23141611149056]
0.46 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:23141602744064]
0.86 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:23141598541568]
0.47 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:23141588035328]
0.73 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:23141579630336]
10.63 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:23141625857792]
7614.46 ms (7 s 614.46 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:23141623756544]
6336.09 ms (6 s 336.09 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:23141621655296]
2.75 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:23141619554048]
6.68 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:23141617452800]
0.04 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:23141615351552]
11058.82 ms (11 s 58.82 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:23141613250304]
14915.59 ms (14 s 915.59 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:23141611149056]
13787.43 ms (13 s 787.43 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:23141609047808]
5.52 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:23141606946560]
6.18 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:23141604845312]
15718.03 ms (15 s 718.03 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:23141602744064]
0.14 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:23141600642816]
15950.87 ms (15 s 950.87 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:23141598541568]
0.72 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:23141596440320]
3.08 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:23141594339072]
7.77 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:23141592237824]
8540.79 ms (8 s 540.79 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:23141590136576]
16673.54 ms (16 s 673.54 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:23141588035328]
1.80 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:23141585934080]
9.91 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:23141583832832]
0.74 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:23141581731584]
17517.22 ms (17 s 517.22 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:23141579630336]
0.22 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:23141577529088]
13.63 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:23141575427840]
6.14 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:23141573326592]
12891.36 ms (12 s 891.36 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:23141571225344]
13.09 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:23141569124096]
6.38 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:23141567022848]
10.15 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:23141564921600]
19.07 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:23141562820352]
3.06 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:23141560719104]
11.17 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:23141558617856]
37.13 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:23141556516608]
44.01 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:23141554415360]
13.94 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:23139337631488]
360.88 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:23139335530240]
471.89 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:23139333428992]
54.96 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:23139331327744]
11.68 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:23139329226496]
53.60 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:23139327125248]
57.65 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:23139325024000]
47.91 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:23139322922752]
304.18 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:23139320821504]
315.30 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:23139318720256]
61.20 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:23139316619008]
498.24 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:23139314517760]
822.13 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:23139312416512]
494.66 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:23139310315264]
922.14 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:23139308214016]
1247.09 ms (1 s 247.09 ms) taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:23139306112768]
224.87 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:23139304011520]
1379.85 ms (1 s 379.85 ms) taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:23139301910272]
1549.51 ms (1 s 549.51 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:23139299809024]
1525.96 ms (1 s 525.96 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:23139297707776]
1916.37 ms (1 s 916.37 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:23139295606528]
2445.16 ms (2 s 445.17 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:23139293505280]
8269.04 ms (8 s 269.04 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:23139291404032]
9255.88 ms (9 s 255.88 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:23139289302784]
4571.39 ms (4 s 571.39 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:23139287201536]
1787.38 ms (1 s 787.38 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:23139285100288]
3473.21 ms (3 s 473.21 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:23139282999040]
2339.27 ms (2 s 339.27 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:23139280897792]
5718.05 ms (5 s 718.06 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:23139278796544]
17673.38 ms (17 s 673.38 ms) total read duration.
Loaded 76 representative collections of sizes:
1 : 1
3 : 1
5 : 1
7 : 1
9 : 2
11 : 2
13 : 2
15 : 2
17 : 5
19 : 5
21 : 3
23 : 6
25 : 10
27 : 7
29 : 12
31 : 14
33 : 17
35 : 21
37 : 30
39 : 28
41 : 44
43 : 56
45 : 66
47 : 80
49 : 108
51 : 123
53 : 168
55 : 197
57 : 241
59 : 303
61 : 390
63 : 444
65 : 570
67 : 707
69 : 863
71 : 1052
73 : 1340
75 : 1586
77 : 1990
79 : 2467
81 : 3018
83 : 3679
85 : 4661
87 : 5632
89 : 6994
91 : 8637
93 : 10677
95 : 13008
97 : 16295
99 : 19833
101 : 24567
103 : 30296
105 : 37377
107 : 45724
109 : 56922
111 : 69661
113 : 85894
115 : 105871
117 : 130737
119 : 160270
121 : 198446
123 : 243740
125 : 300530
127 : 370216
129 : 456911
131 : 560926
133 : 693346
135 : 853090
137 : 1051251
139 : 1294413
141 : 1597383
143 : 1963944
145 : 2423655
147 : 2983754
149 : 3676539
151 : 4527348
24048210 representatives in total.
71212.86 ms (1 min 11 s 212.86 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:23139278796544]
87525.71 ms (1 min 27 s 525.71 ms) taken to read 28040847 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. [tid:23139280897792]
109871.89 ms (1 min 49 s 871.89 ms) taken to read 38836822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs157-unfiltered153+.txt. [tid:23139282999040]
125644.13 ms (2 min 5 s 644.13 ms) taken to read 50013506 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs159-unfiltered153+.txt. [tid:23139285100288]
146203.59 ms (2 min 26 s 203.59 ms) taken to read 78239557 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs161-unfiltered153+.txt. [tid:23139287201536]
146249.87 ms (2 min 26 s 249.87 ms) additional read duration.
Loaded 5 more representative collections of sizes:
153 : 21395853
155 : 28040847
157 : 38836822
159 : 50013506
161 : 78239557
240574795 representatives in total.
Thu Nov 9 19:50:58 2023: Inserted ≈ 5% of D-proof conclusions. [ 12028739 of 240574795] (ETC: Thu Nov 9 20:00:04 2023 ; 9 min 6 s 458.26 ms remaining ; 9 min 35 s 219.22 ms total)
Thu Nov 9 19:51:31 2023: Inserted ≈10% of D-proof conclusions. [ 24057479 of 240574795] (ETC: Thu Nov 9 20:00:46 2023 ; 9 min 15 s 604.67 ms remaining ; 10 min 17 s 338.52 ms total)
Thu Nov 9 19:51:55 2023: Inserted ≈15% of D-proof conclusions. [ 36086219 of 240574795] (ETC: Thu Nov 9 20:00:02 2023 ; 8 min 6 s 729.10 ms remaining ; 9 min 32 s 622.47 ms total)
Thu Nov 9 19:52:20 2023: Inserted ≈20% of D-proof conclusions. [ 48114959 of 240574795] (ETC: Thu Nov 9 19:59:41 2023 ; 7 min 21 s 570.49 ms remaining ; 9 min 11 s 963.12 ms total)
Thu Nov 9 19:52:43 2023: Inserted ≈25% of D-proof conclusions. [ 60143698 of 240574795] (ETC: Thu Nov 9 19:59:24 2023 ; 6 min 40 s 964.73 ms remaining ; 8 min 54 s 619.63 ms total)
Thu Nov 9 19:53:08 2023: Inserted ≈30% of D-proof conclusions. [ 72172438 of 240574795] (ETC: Thu Nov 9 19:59:19 2023 ; 6 min 11 s 118.12 ms remaining ; 8 min 50 s 168.74 ms total)
Thu Nov 9 19:53:30 2023: Inserted ≈35% of D-proof conclusions. [ 84201178 of 240574795] (ETC: Thu Nov 9 19:59:07 2023 ; 5 min 36 s 457.30 ms remaining ; 8 min 37 s 626.62 ms total)
Thu Nov 9 19:53:54 2023: Inserted ≈40% of D-proof conclusions. [ 96229918 of 240574795] (ETC: Thu Nov 9 19:59:02 2023 ; 5 min 7 s 873.96 ms remaining ; 8 min 33 s 123.27 ms total)
Thu Nov 9 19:54:20 2023: Inserted ≈45% of D-proof conclusions. [108258657 of 240574795] (ETC: Thu Nov 9 19:59:01 2023 ; 4 min 41 s 633.40 ms remaining ; 8 min 32 s 60.72 ms total)
Thu Nov 9 19:54:49 2023: Inserted ≈50% of D-proof conclusions. [120287397 of 240574795] (ETC: Thu Nov 9 19:59:10 2023 ; 4 min 20 s 327.45 ms remaining ; 8 min 40 s 654.90 ms total)
Thu Nov 9 19:55:18 2023: Inserted ≈55% of D-proof conclusions. [132316137 of 240574795] (ETC: Thu Nov 9 19:59:14 2023 ; 3 min 56 s 287.79 ms remaining ; 8 min 45 s 83.97 ms total)
Thu Nov 9 19:55:46 2023: Inserted ≈60% of D-proof conclusions. [144344877 of 240574795] (ETC: Thu Nov 9 19:59:18 2023 ; 3 min 31 s 537.04 ms remaining ; 8 min 48 s 842.60 ms total)
Thu Nov 9 19:56:20 2023: Inserted ≈65% of D-proof conclusions. [156373616 of 240574795] (ETC: Thu Nov 9 19:59:29 2023 ; 3 min 9 s 77.41 ms remaining ; 9 min 221.17 ms total)
Thu Nov 9 19:56:53 2023: Inserted ≈70% of D-proof conclusions. [168402356 of 240574795] (ETC: Thu Nov 9 19:59:38 2023 ; 2 min 44 s 603.32 ms remaining ; 9 min 8 s 677.72 ms total)
Thu Nov 9 19:57:25 2023: Inserted ≈75% of D-proof conclusions. [180431096 of 240574795] (ETC: Thu Nov 9 19:59:44 2023 ; 2 min 18 s 602.35 ms remaining ; 9 min 14 s 409.41 ms total)
Thu Nov 9 19:57:57 2023: Inserted ≈80% of D-proof conclusions. [192459836 of 240574795] (ETC: Thu Nov 9 19:59:49 2023 ; 1 min 52 s 52.92 ms remaining ; 9 min 20 s 264.60 ms total)
Thu Nov 9 19:58:28 2023: Inserted ≈85% of D-proof conclusions. [204488575 of 240574795] (ETC: Thu Nov 9 19:59:52 2023 ; 1 min 24 s 507.21 ms remaining ; 9 min 23 s 381.37 ms total)
Thu Nov 9 19:58:57 2023: Inserted ≈90% of D-proof conclusions. [216517315 of 240574795] (ETC: Thu Nov 9 19:59:54 2023 ; 56 s 453.95 ms remaining ; 9 min 24 s 539.54 ms total)
Thu Nov 9 19:59:27 2023: Inserted ≈95% of D-proof conclusions. [228546055 of 240574795] (ETC: Thu Nov 9 19:59:55 2023 ; 28 s 290.58 ms remaining ; 9 min 25 s 811.52 ms total)
Thu Nov 9 19:59:53 2023: Inserted 100% of D-proof conclusions. [240574795 of 240574795] (ETC: Thu Nov 9 19:59:53 2023 ; 0.00 ms remaining ; 9 min 24 s 193.43 ms total)
564194.88 ms (9 min 24 s 194.88 ms) total insertion duration.
Known iteration count loaded from 163:1089248702.
Thu Nov 9 19:59:53 2023: Starting to generate D-proof representatives of length 163.
Thu Nov 9 20:16:08 2023: Iterated ≈ 2% of D-proof candidates. [ 21784974 of 1089248702] (ETC: Fri Nov 10 09:31:49 2023 ; 13 h 15 min 41 s 494.72 ms remaining ; 13 h 31 min 55 s 810.94 ms total)
Thu Nov 9 20:30:43 2023: Iterated ≈ 4% of D-proof candidates. [ 43569948 of 1089248702] (ETC: Fri Nov 10 08:50:40 2023 ; 12 h 19 min 56 s 339.53 ms remaining ; 12 h 50 min 46 s 187.01 ms total)
Thu Nov 9 20:44:57 2023: Iterated ≈ 6% of D-proof candidates. [ 65354922 of 1089248702] (ETC: Fri Nov 10 08:30:55 2023 ; 11 h 45 min 57 s 553.57 ms remaining ; 12 h 31 min 1 s 227.20 ms total)
Thu Nov 9 20:59:50 2023: Iterated ≈ 8% of D-proof candidates. [ 87139896 of 1089248702] (ETC: Fri Nov 10 08:29:05 2023 ; 11 h 29 min 15 s 698.22 ms remaining ; 12 h 29 min 11 s 845.88 ms total)
Thu Nov 9 21:16:18 2023: Iterated ≈10% of D-proof candidates. [ 108924870 of 1089248702] (ETC: Fri Nov 10 08:44:03 2023 ; 11 h 27 min 44 s 778.15 ms remaining ; 12 h 44 min 9 s 753.49 ms total)
Thu Nov 9 21:31:40 2023: Iterated ≈12% of D-proof candidates. [ 130709844 of 1089248702] (ETC: Fri Nov 10 08:44:46 2023 ; 11 h 13 min 5 s 379.51 ms remaining ; 12 h 44 min 52 s 476.71 ms total)
Thu Nov 9 21:46:23 2023: Iterated ≈14% of D-proof candidates. [ 152494818 of 1089248702] (ETC: Fri Nov 10 08:40:31 2023 ; 10 h 54 min 8 s 403.99 ms remaining ; 12 h 40 min 37 s 679.05 ms total)
Thu Nov 9 22:04:57 2023: Iterated ≈16% of D-proof candidates. [ 174279792 of 1089248702] (ETC: Fri Nov 10 09:01:29 2023 ; 10 h 56 min 31 s 987.29 ms remaining ; 13 h 1 min 35 s 222.95 ms total)
Thu Nov 9 22:22:09 2023: Iterated ≈18% of D-proof candidates. [ 196064766 of 1089248702] (ETC: Fri Nov 10 09:10:16 2023 ; 10 h 48 min 6 s 487.09 ms remaining ; 13 h 10 min 22 s 545.21 ms total)
Thu Nov 9 22:40:55 2023: Iterated ≈20% of D-proof candidates. [ 217849740 of 1089248702] (ETC: Fri Nov 10 09:25:00 2023 ; 10 h 44 min 5 s 447.95 ms remaining ; 13 h 25 min 6 s 809.91 ms total)
Thu Nov 9 22:58:16 2023: Iterated ≈22% of D-proof candidates. [ 239634714 of 1089248702] (ETC: Fri Nov 10 09:30:40 2023 ; 10 h 32 min 24 s 487.76 ms remaining ; 13 h 30 min 46 s 779.15 ms total)
Thu Nov 9 23:16:13 2023: Iterated ≈24% of D-proof candidates. [ 261419688 of 1089248702] (ETC: Fri Nov 10 09:37:54 2023 ; 10 h 21 min 41 s 683.43 ms remaining ; 13 h 38 min 1 s 162.38 ms total)
Thu Nov 9 23:37:53 2023: Iterated ≈26% of D-proof candidates. [ 283204662 of 1089248702] (ETC: Fri Nov 10 09:58:18 2023 ; 10 h 20 min 25 s 438.66 ms remaining ; 13 h 58 min 24 s 646.80 ms total)
Fri Nov 10 00:00:02 2023: Iterated ≈28% of D-proof candidates. [ 304989636 of 1089248702] (ETC: Fri Nov 10 10:17:34 2023 ; 10 h 17 min 31 s 852.18 ms remaining ; 14 h 17 min 40 s 905.77 ms total)
Fri Nov 10 00:18:00 2023: Iterated ≈30% of D-proof candidates. [ 326774610 of 1089248702] (ETC: Fri Nov 10 10:20:16 2023 ; 10 h 2 min 16 s 110.16 ms remaining ; 14 h 20 min 23 s 14.48 ms total)
Fri Nov 10 00:39:19 2023: Iterated ≈32% of D-proof candidates. [ 348559584 of 1089248702] (ETC: Fri Nov 10 10:33:05 2023 ; 9 h 53 min 46 s 33.48 ms remaining ; 14 h 33 min 11 s 225.66 ms total)
Fri Nov 10 01:00:59 2023: Iterated ≈34% of D-proof candidates. [ 370344558 of 1089248702] (ETC: Fri Nov 10 10:45:27 2023 ; 9 h 44 min 28 s 8.56 ms remaining ; 14 h 45 min 33 s 346.26 ms total)
Fri Nov 10 01:19:30 2023: Iterated ≈36% of D-proof candidates. [ 392129532 of 1089248702] (ETC: Fri Nov 10 10:47:42 2023 ; 9 h 28 min 11 s 903.32 ms remaining ; 14 h 47 min 48 s 598.89 ms total)
Fri Nov 10 01:38:32 2023: Iterated ≈38% of D-proof candidates. [ 413914506 of 1089248702] (ETC: Fri Nov 10 10:51:04 2023 ; 9 h 12 min 31 s 848.58 ms remaining ; 14 h 51 min 10 s 723.46 ms total)
Fri Nov 10 01:57:41 2023: Iterated ≈40% of D-proof candidates. [ 435699480 of 1089248702] (ETC: Fri Nov 10 10:54:22 2023 ; 8 h 56 min 41 s 162.70 ms remaining ; 14 h 54 min 28 s 604.44 ms total)
Fri Nov 10 02:16:50 2023: Iterated ≈42% of D-proof candidates. [ 457484454 of 1089248702] (ETC: Fri Nov 10 10:57:22 2023 ; 8 h 40 min 32 s 492.03 ms remaining ; 14 h 57 min 29 s 124.11 ms total)
Fri Nov 10 02:34:45 2023: Iterated ≈44% of D-proof candidates. [ 479269428 of 1089248702] (ETC: Fri Nov 10 10:57:18 2023 ; 8 h 22 min 32 s 780.72 ms remaining ; 14 h 57 min 24 s 251.21 ms total)
Fri Nov 10 02:55:36 2023: Iterated ≈46% of D-proof candidates. [ 501054402 of 1089248702] (ETC: Fri Nov 10 11:03:38 2023 ; 8 h 8 min 1 s 69.25 ms remaining ; 15 h 3 min 44 s 202.23 ms total)
Fri Nov 10 03:15:02 2023: Iterated ≈48% of D-proof candidates. [ 522839376 of 1089248702] (ETC: Fri Nov 10 11:06:26 2023 ; 7 h 51 min 24 s 293.55 ms remaining ; 15 h 6 min 32 s 872.11 ms total)
Fri Nov 10 03:34:24 2023: Iterated ≈50% of D-proof candidates. [ 544624351 of 1089248702] (ETC: Fri Nov 10 11:08:54 2023 ; 7 h 34 min 30 s 585.54 ms remaining ; 15 h 9 min 1 s 171.09 ms total)
Fri Nov 10 03:53:03 2023: Iterated ≈52% of D-proof candidates. [ 566409325 of 1089248702] (ETC: Fri Nov 10 11:09:49 2023 ; 7 h 16 min 45 s 879.47 ms remaining ; 15 h 9 min 55 s 582.22 ms total)
Fri Nov 10 04:11:20 2023: Iterated ≈54% of D-proof candidates. [ 588194299 of 1089248702] (ETC: Fri Nov 10 11:09:58 2023 ; 6 h 58 min 38 s 97.29 ms remaining ; 15 h 10 min 4 s 559.32 ms total)
Fri Nov 10 04:28:40 2023: Iterated ≈56% of D-proof candidates. [ 609979273 of 1089248702] (ETC: Fri Nov 10 11:08:25 2023 ; 6 h 39 min 45 s 130.67 ms remaining ; 15 h 8 min 31 s 660.59 ms total)
Fri Nov 10 04:45:38 2023: Iterated ≈58% of D-proof candidates. [ 631764247 of 1089248702] (ETC: Fri Nov 10 11:06:20 2023 ; 6 h 20 min 42 s 539.22 ms remaining ; 15 h 6 min 26 s 998.11 ms total)
Fri Nov 10 05:01:55 2023: Iterated ≈60% of D-proof candidates. [ 653549221 of 1089248702] (ETC: Fri Nov 10 11:03:15 2023 ; 6 h 1 min 20 s 857.79 ms remaining ; 15 h 3 min 22 s 144.45 ms total)
Fri Nov 10 05:17:59 2023: Iterated ≈62% of D-proof candidates. [ 675334195 of 1089248702] (ETC: Fri Nov 10 11:00:02 2023 ; 5 h 42 min 3 s 333.66 ms remaining ; 15 h 8 s 772.76 ms total)
Fri Nov 10 05:33:48 2023: Iterated ≈64% of D-proof candidates. [ 697119169 of 1089248702] (ETC: Fri Nov 10 10:56:38 2023 ; 5 h 22 min 49 s 518.11 ms remaining ; 14 h 56 min 44 s 216.93 ms total)
Fri Nov 10 05:49:11 2023: Iterated ≈66% of D-proof candidates. [ 718904143 of 1089248702] (ETC: Fri Nov 10 10:52:46 2023 ; 5 h 3 min 34 s 756.00 ms remaining ; 14 h 52 min 52 s 811.73 ms total)
Fri Nov 10 06:04:20 2023: Iterated ≈68% of D-proof candidates. [ 740689117 of 1089248702] (ETC: Fri Nov 10 10:48:46 2023 ; 4 h 44 min 26 s 441.47 ms remaining ; 14 h 48 min 52 s 629.53 ms total)
Fri Nov 10 06:19:16 2023: Iterated ≈70% of D-proof candidates. [ 762474091 of 1089248702] (ETC: Fri Nov 10 10:44:42 2023 ; 4 h 25 min 26 s 652.28 ms remaining ; 14 h 44 min 48 s 840.86 ms total)
Fri Nov 10 06:33:59 2023: Iterated ≈72% of D-proof candidates. [ 784259065 of 1089248702] (ETC: Fri Nov 10 10:40:35 2023 ; 4 h 6 min 35 s 574.96 ms remaining ; 14 h 40 min 41 s 339.06 ms total)
Fri Nov 10 06:48:19 2023: Iterated ≈74% of D-proof candidates. [ 806044039 of 1089248702] (ETC: Fri Nov 10 10:36:08 2023 ; 3 h 47 min 49 s 541.08 ms remaining ; 14 h 36 min 15 s 157.89 ms total)
Fri Nov 10 07:02:34 2023: Iterated ≈76% of D-proof candidates. [ 827829013 of 1089248702] (ETC: Fri Nov 10 10:31:50 2023 ; 3 h 29 min 15 s 924.26 ms remaining ; 14 h 31 min 56 s 350.99 ms total)
Fri Nov 10 07:16:24 2023: Iterated ≈78% of D-proof candidates. [ 849613987 of 1089248702] (ETC: Fri Nov 10 10:27:13 2023 ; 3 h 10 min 48 s 686.84 ms remaining ; 14 h 27 min 19 s 485.49 ms total)
Fri Nov 10 07:30:03 2023: Iterated ≈80% of D-proof candidates. [ 871398961 of 1089248702] (ETC: Fri Nov 10 10:22:35 2023 ; 2 h 52 min 32 s 433.21 ms remaining ; 14 h 22 min 42 s 165.89 ms total)
Fri Nov 10 07:43:40 2023: Iterated ≈82% of D-proof candidates. [ 893183935 of 1089248702] (ETC: Fri Nov 10 10:18:09 2023 ; 2 h 34 min 29 s 186.12 ms remaining ; 14 h 18 min 15 s 478.28 ms total)
Fri Nov 10 07:57:06 2023: Iterated ≈84% of D-proof candidates. [ 914968909 of 1089248702] (ETC: Fri Nov 10 10:13:43 2023 ; 2 h 16 min 36 s 786.40 ms remaining ; 14 h 13 min 49 s 914.83 ms total)
Fri Nov 10 08:10:28 2023: Iterated ≈86% of D-proof candidates. [ 936753883 of 1089248702] (ETC: Fri Nov 10 10:09:24 2023 ; 1 h 58 min 55 s 949.85 ms remaining ; 14 h 9 min 31 s 70.12 ms total)
Fri Nov 10 08:23:42 2023: Iterated ≈88% of D-proof candidates. [ 958538857 of 1089248702] (ETC: Fri Nov 10 10:05:08 2023 ; 1 h 41 min 25 s 795.98 ms remaining ; 14 h 5 min 14 s 966.17 ms total)
Fri Nov 10 08:36:54 2023: Iterated ≈90% of D-proof candidates. [ 980323831 of 1089248702] (ETC: Fri Nov 10 10:01:01 2023 ; 1 h 24 min 6 s 778.00 ms remaining ; 14 h 1 min 7 s 779.59 ms total)
Fri Nov 10 08:50:06 2023: Iterated ≈92% of D-proof candidates. [1002108805 of 1089248702] (ETC: Fri Nov 10 09:57:04 2023 ; 1 h 6 min 58 s 454.71 ms remaining ; 13 h 57 min 10 s 683.44 ms total)
Fri Nov 10 09:03:07 2023: Iterated ≈94% of D-proof candidates. [1023893779 of 1089248702] (ETC: Fri Nov 10 09:53:06 2023 ; 49 min 59 s 587.28 ms remaining ; 13 h 53 min 13 s 120.67 ms total)
Fri Nov 10 09:16:09 2023: Iterated ≈96% of D-proof candidates. [1045678753 of 1089248702] (ETC: Fri Nov 10 09:49:19 2023 ; 33 min 10 s 647.26 ms remaining ; 13 h 49 min 26 s 180.44 ms total)
Fri Nov 10 09:29:09 2023: Iterated ≈98% of D-proof candidates. [1067463727 of 1089248702] (ETC: Fri Nov 10 09:45:40 2023 ; 16 min 30 s 933.97 ms remaining ; 13 h 45 min 46 s 696.38 ms total)
Fri Nov 10 09:42:21 2023: Iterated 100% of D-proof candidates. [1089248702 of 1089248702] (ETC: Fri Nov 10 09:42:21 2023 ; 0.00 ms remaining ; 13 h 42 min 28 s 61.28 ms total)
49349065.90 ms (13 h 42 min 29 s 65.90 ms) taken to collect 101757325 D-proofs of length 163. [iterated 1089248702 condensed detachment proof strings]
[Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 3 }, { 9, 4 }, { 11, 7 }, { 13, 10 }, { 15, 13 }, { 17, 16 }, { 19, 26 }, { 21, 36 }, { 23, 42 }, { 25, 54 }, { 27, 80 }, { 29, 100 }, { 31, 126 }, { 33, 162 }, { 35, 221 }, { 37, 282 }, { 39, 359 }, { 41, 454 }, { 43, 615 }, { 45, 778 }, { 47, 1002 }, { 49, 1298 }, { 51, 1678 }, { 53, 2134 }, { 55, 2803 }, { 57, 3534 }, { 59, 4530 }, { 61, 5848 }, { 63, 7496 }, { 65, 9424 }, { 67, 12147 }, { 69, 15402 }, { 71, 19615 }, { 73, 24892 }, { 75, 31620 }, { 77, 39936 }, { 79, 50946 }, { 81, 64168 }, { 83, 81204 }, { 85, 102794 }, { 87, 130094 }, { 89, 163718 }, { 91, 207474 }, { 93, 261220 }, { 95, 329568 }, { 97, 415628 }, { 99, 524144 }, { 101, 658432 }, { 103, 831003 }, { 105, 1044792 }, { 107, 1313760 }, { 109, 1651616 }, { 111, 2077927 }, { 113, 2606646 }, { 115, 3277103 }, { 117, 4112052 }, { 119, 5160229 }, { 121, 6472942 }, { 123, 8122690 }, { 125, 10173684 }, { 127, 12760188 }, { 129, 15985436 }, { 131, 20022824 }, { 133, 25070468 }, { 135, 31402887 }, { 137, 39284338 }, { 139, 49176381 }, { 141, 61517174 }, { 143, 76945234 }, { 145, 96208206 }, { 147, 120320734 }, { 149, 150346484 }, { 151, 187924390 }, { 153, 234799156 }, { 155, 324945288 }, { 157, 440272080 }, { 159, 592215521 }, { 161, 784979956 }, { 163, 1089248702 } }
776722.83 ms (12 min 56 s 722.83 ms) taken to filter and order new representative proofs.
Found 101757325 representative, 187537763 redundant, and 799953614 invalid condensed detachment proof strings.
lengths up to 163 ; amounts per length: {(1,1), (3,1), (5,1), (7,1), (9,2), (11,2), (13,2), (15,2), (17,5), (19,5), (21,3), (23,6), (25,10), (27,7), (29,12), (31,14), (33,17), (35,21), (37,30), (39,28), (41,44), (43,56), (45,66), (47,80), (49,108), (51,123), (53,168), (55,197), (57,241), (59,303), (61,390), (63,444), (65,570), (67,707), (69,863), (71,1052), (73,1340), (75,1586), (77,1990), (79,2467), (81,3018), (83,3679), (85,4661), (87,5632), (89,6994), (91,8637), (93,10677), (95,13008), (97,16295), (99,19833), (101,24567), (103,30296), (105,37377), (107,45724), (109,56922), (111,69661), (113,85894), (115,105871), (117,130737), (119,160270), (121,198446), (123,243740), (125,300530), (127,370216), (129,456911), (131,560926), (133,693346), (135,853090), (137,1051251), (139,1294413), (141,1597383), (143,1963944), (145,2423655), (147,2983754), (149,3676539), (151,4527348), (153,21395853), (155,28040847), (157,38836822), (159,50013506), (161,78239557), (163,101757325)} ; 101757325 new representative proofs (187537763 redundant, 799953614 invalid)
Fri Nov 10 10:04:55 2023: Starting to write 101757325 entries to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs163-unfiltered153+.txt.
214250.74 ms (3 min 34 s 250.74 ms) taken to print and save 75698437452 bytes of representative condensed detachment proof strings to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs163-unfiltered153+.txt.
Fri Nov 10 10:10:34 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 163, unfiltered]
Fri Nov 10 10:13:49 2023: Process terminated. [pid: 254588, tid:23141686105984]