-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
dProofs149_24node_1152cpu.log
414 lines (413 loc) · 50.2 KB
/
dProofs149_24node_1152cpu.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
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
( 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 24 CLAIX-2018 MPI nodes
— 2-socket Intel Xeon Platinum 8160 (Skylake) each, 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory each —
running Linux, Rocky 8.8. Initialization and completion messages with rank numbers have been grouped and sorted for better readability.
Wall-clock time: 5.4708333… h
CPU utilization: 6302.4 core-h )
Sat Oct 21 06:45:05 2023: Process started. [pid: 261788, tid:22980071835520]
Sat Oct 21 06:45:05 2023: Process started. [pid: 224362, tid:22793171609472]
Sat Oct 21 06:45:05 2023: Process started. [pid: 234875, tid:23112699856768]
Sat Oct 21 06:45:05 2023: Process started. [pid: 267421, tid:22577675212672]
Sat Oct 21 06:45:05 2023: Process started. [pid: 239250, tid:22493136877440]
Sat Oct 21 06:45:05 2023: Process started. [pid: 248549, tid:22975539472256]
Sat Oct 21 06:45:05 2023: Process started. [pid: 47280, tid:23011572561792]
Sat Oct 21 06:45:05 2023: Process started. [pid: 143108, tid:22807129577344]
Sat Oct 21 06:45:05 2023: Process started. [pid: 265810, tid:23397702719360]
Sat Oct 21 06:45:05 2023: Process started. [pid: 107773, tid:23445796722560]
Sat Oct 21 06:45:05 2023: Process started. [pid: 260069, tid:22562398766976]
Sat Oct 21 06:45:05 2023: Process started. [pid: 14971, tid:23073756407680]
Sat Oct 21 06:45:05 2023: Process started. [pid: 238327, tid:22817315653504]
Sat Oct 21 06:45:05 2023: Process started. [pid: 167917, tid:22949804918656]
Sat Oct 21 06:45:05 2023: Process started. [pid: 179907, tid:22514015463296]
Sat Oct 21 06:45:05 2023: Process started. [pid: 24920, tid:23287008069504]
Sat Oct 21 06:45:05 2023: Process started. [pid: 14615, tid:22787657873280]
Sat Oct 21 06:45:05 2023: Process started. [pid: 16288, tid:22997829887872]
Sat Oct 21 06:45:05 2023: Process started. [pid: 259852, tid:22606279636864]
Sat Oct 21 06:45:05 2023: Process started. [pid: 179296, tid:23189274511232]
Sat Oct 21 06:45:05 2023: Process started. [pid: 179250, tid:23051957557120]
Sat Oct 21 06:45:05 2023: Process started. [pid: 190819, tid:22777612744576]
Sat Oct 21 06:45:05 2023: Process started. [pid: 123973, tid:22926151501696]
Sat Oct 21 06:45:05 2023: Process started. [pid: 219186, tid:22897449146240]
Tasks:
1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true)
2. mpi_filterDProofRepresentativeFile(149, true)
[Rank 0 ; pid: 219186 ; 24 processes] 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)))
[Rank 1 ; pid: 179907 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 2 ; pid: 107773 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 3 ; pid: 259852 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 4 ; pid: 179296 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 5 ; pid: 265810 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 6 ; pid: 248549 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 7 ; pid: 234875 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 8 ; pid: 261788 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 9 ; pid: 14615 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 10 ; pid: 16288 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 11 ; pid: 123973 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 12 ; pid: 267421 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 13 ; pid: 179250 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 14 ; pid: 238327 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 15 ; pid: 14971 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 16 ; pid: 47280 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 17 ; pid: 190819 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 18 ; pid: 24920 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 19 ; pid: 260069 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 20 ; pid: 143108 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 21 ; pid: 167917 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 22 ; pid: 224362 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 23 ; pid: 239250 ; 24 processes] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true), silently.
[Rank 0 ; pid: 219186 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 1 ; pid: 179907 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 2 ; pid: 107773 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 3 ; pid: 259852 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 4 ; pid: 179296 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 5 ; pid: 265810 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 6 ; pid: 248549 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 7 ; pid: 234875 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 8 ; pid: 261788 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 9 ; pid: 14615 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 10 ; pid: 16288 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 11 ; pid: 123973 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 12 ; pid: 267421 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 13 ; pid: 179250 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 14 ; pid: 238327 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 15 ; pid: 14971 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 16 ; pid: 47280 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 17 ; pid: 190819 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 18 ; pid: 24920 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 19 ; pid: 260069 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 20 ; pid: 143108 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 21 ; pid: 167917 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 22 ; pid: 224362 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
[Rank 23 ; pid: 239250 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(149, true).
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 0 on "ncm0513.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 1 on "ncm0514.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 2 on "ncm0515.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 3 on "ncm0516.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 4 on "ncm0517.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 5 on "ncm0518.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 6 on "ncm0519.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 7 on "ncm0520.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 8 on "ncm0521.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 9 on "ncm0522.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 10 on "ncm0523.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 11 on "ncm0524.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 12 on "ncm0525.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 13 on "ncm0526.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 14 on "ncm0527.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 15 on "ncm0528.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 16 on "ncm0529.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 17 on "ncm0530.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 18 on "ncm0531.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 19 on "ncm0532.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 20 on "ncm0533.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 21 on "ncm0534.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 22 on "ncm0536.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 06:45:06 2023: MPI-based D-proof representative filter started. [rank 23 on "ncm0537.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
0.01 ms taken to load initial representatives.
6.65 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:22897261405952]
7.12 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:22897221482240]
0.01 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:22897269810944]
0.04 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:22897227785984]
1.75 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:22897248798464]
0.58 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:22897255102208]
0.40 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:22897234089728]
0.42 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:22897259304704]
0.20 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:22897253000960]
0.27 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:22897231988480]
0.61 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:22897267709696]
0.74 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:22897244595968]
0.74 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:22897242494720]
0.14 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:22897274013440]
1.58 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:22897215178496]
0.10 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:22897236190976]
2.39 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:22897271912192]
0.06 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:22897238292224]
0.18 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:22897265608448]
0.89 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:22897263507200]
0.00 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:22897141741312]
0.04 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:22897257203456]
2.07 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:22897225684736]
0.10 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:22897223583488]
0.24 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:22897240393472]
2164.03 ms (2 s 164.03 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:22897274013440]
3216.99 ms (3 s 216.99 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:22897271912192]
5780.44 ms (5 s 780.44 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:22897141741312]
358.56 ms taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:22897269810944]
8772.74 ms (8 s 772.75 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:22897267709696]
4525.18 ms (4 s 525.18 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:22897265608448]
5004.83 ms (5 s 4.83 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:22897263507200]
191.33 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:22897261405952]
2442.83 ms (2 s 442.83 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:22897259304704]
6431.18 ms (6 s 431.18 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:22897257203456]
1078.15 ms (1 s 78.15 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:22897255102208]
3687.30 ms (3 s 687.30 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:22897253000960]
3.37 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:22897250899712]
768.55 ms taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:22897248798464]
3.16 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:22897246697216]
1473.95 ms (1 s 473.95 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:22897244595968]
1794.34 ms (1 s 794.34 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:22897242494720]
7797.56 ms (7 s 797.56 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:22897240393472]
3786.12 ms (3 s 786.12 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:22897238292224]
2871.81 ms (2 s 871.81 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:22897236190976]
1757.74 ms (1 s 757.74 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:22897234089728]
5791.55 ms (5 s 791.56 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:22897231988480]
1.78 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:22897229887232]
380.58 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:22897227785984]
6890.42 ms (6 s 890.42 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:22897225684736]
7407.53 ms (7 s 407.53 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:22897223583488]
300.00 ms taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:22897221482240]
7.62 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:22897219380992]
2.27 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:22897217279744]
2268.86 ms (2 s 268.86 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:22897215178496]
2.30 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:22897213077248]
9.66 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:22897210976000]
1.53 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:22897139640064]
4.05 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:22897137538816]
28.95 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:22897135437568]
16.43 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:22897133336320]
39.65 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:22897131235072]
14.77 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:22897129133824]
119.40 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:22897127032576]
43.48 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:22897124931328]
28.80 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:22897122830080]
31.53 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:22897120728832]
30.23 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:22897118627584]
51.57 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:22897116526336]
44.12 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:22897114425088]
68.12 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:22897112323840]
92.47 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:22897110222592]
109.53 ms taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:22897108121344]
8832.62 ms (8 s 832.62 ms) total read duration.
Loaded 74 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
15844323 representatives in total.
12824.21 ms (12 s 824.21 ms) taken to read 13988367 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149-unfiltered149+.txt. [tid:22897108121344]
12825.56 ms (12 s 825.56 ms) additional read duration.
Loaded 1 more representative collection of size:
149 : 13988367
29832690 representatives in total.
Sat Oct 21 06:45:28 2023: Representative collections were initialized successfully on all ranks.
Estimated removal count set to 10332193, based on entry 147:8345930 and last known pair (145:6741506, 147:8345930) with 8345930/6741506 ≈ 1.23799 and 8345930 * (8345930/6741506)^1 ≈ 10332193.96.
Sat Oct 21 06:45:28 2023: Inserted ≈ 5% of D-proof conclusions. [ 1491634 of 29832690] (ETC: Sat Oct 21 06:45:40 2023 ; 11 s 632.05 ms remaining ; 12 s 244.26 ms total)
Sat Oct 21 06:45:29 2023: Inserted ≈10% of D-proof conclusions. [ 2983269 of 29832690] (ETC: Sat Oct 21 06:45:41 2023 ; 11 s 992.36 ms remaining ; 13 s 324.84 ms total)
Sat Oct 21 06:45:30 2023: Inserted ≈15% of D-proof conclusions. [ 4474903 of 29832690] (ETC: Sat Oct 21 06:45:42 2023 ; 11 s 792.50 ms remaining ; 13 s 873.53 ms total)
Sat Oct 21 06:45:31 2023: Inserted ≈20% of D-proof conclusions. [ 5966538 of 29832690] (ETC: Sat Oct 21 06:45:42 2023 ; 11 s 448.89 ms remaining ; 14 s 311.12 ms total)
Sat Oct 21 06:45:32 2023: Inserted ≈25% of D-proof conclusions. [ 7458172 of 29832690] (ETC: Sat Oct 21 06:45:45 2023 ; 13 s 55.95 ms remaining ; 17 s 407.94 ms total)
Sat Oct 21 06:45:34 2023: Inserted ≈30% of D-proof conclusions. [ 8949807 of 29832690] (ETC: Sat Oct 21 06:45:48 2023 ; 14 s 9.09 ms remaining ; 20 s 12.99 ms total)
Sat Oct 21 06:45:35 2023: Inserted ≈35% of D-proof conclusions. [10441441 of 29832690] (ETC: Sat Oct 21 06:45:50 2023 ; 14 s 348.52 ms remaining ; 22 s 74.65 ms total)
Sat Oct 21 06:45:37 2023: Inserted ≈40% of D-proof conclusions. [11933076 of 29832690] (ETC: Sat Oct 21 06:45:51 2023 ; 13 s 703.02 ms remaining ; 22 s 838.37 ms total)
Sat Oct 21 06:45:39 2023: Inserted ≈45% of D-proof conclusions. [13424710 of 29832690] (ETC: Sat Oct 21 06:45:52 2023 ; 13 s 596.68 ms remaining ; 24 s 721.24 ms total)
Sat Oct 21 06:45:41 2023: Inserted ≈50% of D-proof conclusions. [14916345 of 29832690] (ETC: Sat Oct 21 06:45:54 2023 ; 12 s 914.84 ms remaining ; 25 s 829.68 ms total)
Sat Oct 21 06:45:42 2023: Inserted ≈55% of D-proof conclusions. [16407979 of 29832690] (ETC: Sat Oct 21 06:45:54 2023 ; 11 s 775.90 ms remaining ; 26 s 168.68 ms total)
Sat Oct 21 06:45:43 2023: Inserted ≈60% of D-proof conclusions. [17899614 of 29832690] (ETC: Sat Oct 21 06:45:53 2023 ; 10 s 279.27 ms remaining ; 25 s 698.18 ms total)
Sat Oct 21 06:45:44 2023: Inserted ≈65% of D-proof conclusions. [19391248 of 29832690] (ETC: Sat Oct 21 06:45:53 2023 ; 8 s 790.73 ms remaining ; 25 s 116.38 ms total)
Sat Oct 21 06:45:45 2023: Inserted ≈70% of D-proof conclusions. [20882883 of 29832690] (ETC: Sat Oct 21 06:45:52 2023 ; 7 s 426.71 ms remaining ; 24 s 755.70 ms total)
Sat Oct 21 06:45:46 2023: Inserted ≈75% of D-proof conclusions. [22374517 of 29832690] (ETC: Sat Oct 21 06:45:52 2023 ; 6 s 134.97 ms remaining ; 24 s 539.90 ms total)
Sat Oct 21 06:45:47 2023: Inserted ≈80% of D-proof conclusions. [23866152 of 29832690] (ETC: Sat Oct 21 06:45:52 2023 ; 4 s 898.22 ms remaining ; 24 s 491.10 ms total)
Sat Oct 21 06:45:48 2023: Inserted ≈85% of D-proof conclusions. [25357786 of 29832690] (ETC: Sat Oct 21 06:45:52 2023 ; 3 s 660.57 ms remaining ; 24 s 403.80 ms total)
Sat Oct 21 06:45:49 2023: Inserted ≈90% of D-proof conclusions. [26849421 of 29832690] (ETC: Sat Oct 21 06:45:52 2023 ; 2 s 415.64 ms remaining ; 24 s 156.38 ms total)
Sat Oct 21 06:45:51 2023: Inserted ≈95% of D-proof conclusions. [28341055 of 29832690] (ETC: Sat Oct 21 06:45:52 2023 ; 1 s 201.34 ms remaining ; 24 s 26.91 ms total)
Sat Oct 21 06:45:52 2023: Inserted 100% of D-proof conclusions. [29832690 of 29832690] (ETC: Sat Oct 21 06:45:52 2023 ; 0.00 ms remaining ; 23 s 925.24 ms total)
23925.31 ms (23 s 925.31 ms) total insertion duration.
Reservable workloads: { 0:[388566, 582847], 1:[971414, 1165696], 2:[1554263, 1748544], 3:[2137111, 2331393], 4:[2719960, 2914242], 5:[3302809, 3497090], 6:[3885657, 4079939], 7:[4468506, 4662788], 8:[5051355, 5245636], 9:[5634203, 5828485], 10:[6217052, 6411333], 11:[6799900, 6994182], 12:[7382749, 7577031], 13:[7965598, 8159879], 14:[8548446, 8742728], 15:[9131295, 9325577], 16:[9714144, 9908425], 17:[10296992, 10491274], 18:[10879841, 11074122], 19:[11462689, 11656971], 20:[12045538, 12239820], 21:[12628387, 12822668], 22:[13211235, 13405517], 23:[13794084, 13988366] }
Sat Oct 21 06:52:55 2023: Removed ≈ 2% of redundant conclusions. [ 206643 of approximately 10332193] (ETC: Sat Oct 21 12:37:10 2023 ; 5 h 44 min 15 s 189.04 ms remaining ; 5 h 51 min 16 s 721.72 ms total)
Sat Oct 21 06:59:39 2023: Removed ≈ 4% of redundant conclusions. [ 413287 of approximately 10332193] (ETC: Sat Oct 21 12:30:09 2023 ; 5 h 30 min 29 s 198.72 ms remaining ; 5 h 44 min 15 s 413.83 ms total)
Sat Oct 21 07:06:23 2023: Removed ≈ 6% of redundant conclusions. [ 619931 of approximately 10332193] (ETC: Sat Oct 21 12:27:24 2023 ; 5 h 21 min 843.80 ms remaining ; 5 h 41 min 30 s 258.14 ms total)
Sat Oct 21 07:13:03 2023: Removed ≈ 8% of redundant conclusions. [ 826575 of approximately 10332193] (ETC: Sat Oct 21 12:25:28 2023 ; 5 h 12 min 25 s 73.88 ms remaining ; 5 h 39 min 35 s 79.36 ms total)
Sat Oct 21 07:19:42 2023: Removed ≈ 10% of redundant conclusions. [ 1033219 of approximately 10332193] (ETC: Sat Oct 21 12:23:59 2023 ; 5 h 4 min 17 s 592.83 ms remaining ; 5 h 38 min 6 s 213.60 ms total)
Sat Oct 21 07:26:21 2023: Removed ≈ 12% of redundant conclusions. [ 1239863 of approximately 10332193] (ETC: Sat Oct 21 12:23:02 2023 ; 4 h 56 min 41 s 687.58 ms remaining ; 5 h 37 min 9 s 190.08 ms total)
Sat Oct 21 07:32:59 2023: Removed ≈ 14% of redundant conclusions. [ 1446507 of approximately 10332193] (ETC: Sat Oct 21 12:22:21 2023 ; 4 h 49 min 21 s 104.53 ms remaining ; 5 h 36 min 27 s 330.80 ms total)
Sat Oct 21 07:39:36 2023: Removed ≈ 16% of redundant conclusions. [ 1653150 of approximately 10332193] (ETC: Sat Oct 21 12:21:38 2023 ; 4 h 42 min 1 s 535.11 ms remaining ; 5 h 35 min 44 s 682.62 ms total)
Sat Oct 21 07:46:14 2023: Removed ≈ 18% of redundant conclusions. [ 1859794 of approximately 10332193] (ETC: Sat Oct 21 12:21:06 2023 ; 4 h 34 min 52 s 337.58 ms remaining ; 5 h 35 min 12 s 605.05 ms total)
Sat Oct 21 07:52:50 2023: Removed ≈ 20% of redundant conclusions. [ 2066438 of approximately 10332193] (ETC: Sat Oct 21 12:20:38 2023 ; 4 h 27 min 47 s 428.15 ms remaining ; 5 h 34 min 44 s 283.73 ms total)
Sat Oct 21 07:59:26 2023: Removed ≈ 22% of redundant conclusions. [ 2273082 of approximately 10332193] (ETC: Sat Oct 21 12:20:10 2023 ; 4 h 20 min 44 s 82.25 ms remaining ; 5 h 34 min 16 s 514.57 ms total)
Sat Oct 21 08:06:01 2023: Removed ≈ 24% of redundant conclusions. [ 2479726 of approximately 10332193] (ETC: Sat Oct 21 12:19:45 2023 ; 4 h 13 min 43 s 885.84 ms remaining ; 5 h 33 min 51 s 427.91 ms total)
Sat Oct 21 08:12:34 2023: Removed ≈ 26% of redundant conclusions. [ 2686370 of approximately 10332193] (ETC: Sat Oct 21 12:19:15 2023 ; 4 h 6 min 41 s 278.28 ms remaining ; 5 h 33 min 21 s 726.94 ms total)
Sat Oct 21 08:19:05 2023: Removed ≈ 28% of redundant conclusions. [ 2893014 of approximately 10332193] (ETC: Sat Oct 21 12:18:44 2023 ; 3 h 59 min 39 s 246.29 ms remaining ; 5 h 32 min 51 s 175.30 ms total)
Sat Oct 21 08:25:36 2023: Removed ≈ 30% of redundant conclusions. [ 3099657 of approximately 10332193] (ETC: Sat Oct 21 12:18:15 2023 ; 3 h 52 min 38 s 960.59 ms remaining ; 5 h 32 min 21 s 369.78 ms total)
Sat Oct 21 08:32:05 2023: Removed ≈ 32% of redundant conclusions. [ 3306301 of approximately 10332193] (ETC: Sat Oct 21 12:17:45 2023 ; 3 h 45 min 39 s 849.88 ms remaining ; 5 h 31 min 51 s 541.78 ms total)
Sat Oct 21 08:38:32 2023: Removed ≈ 34% of redundant conclusions. [ 3512945 of approximately 10332193] (ETC: Sat Oct 21 12:17:11 2023 ; 3 h 38 min 39 s 330.33 ms remaining ; 5 h 31 min 17 s 771.43 ms total)
Sat Oct 21 08:44:57 2023: Removed ≈ 36% of redundant conclusions. [ 3719589 of approximately 10332193] (ETC: Sat Oct 21 12:16:36 2023 ; 3 h 31 min 39 s 540.16 ms remaining ; 5 h 30 min 43 s 30.06 ms total)
Sat Oct 21 08:51:23 2023: Removed ≈ 38% of redundant conclusions. [ 3926233 of approximately 10332193] (ETC: Sat Oct 21 12:16:07 2023 ; 3 h 24 min 44 s 300.73 ms remaining ; 5 h 30 min 13 s 387.22 ms total)
Sat Oct 21 08:57:44 2023: Removed ≈ 40% of redundant conclusions. [ 4132877 of approximately 10332193] (ETC: Sat Oct 21 12:15:31 2023 ; 3 h 17 min 46 s 622.22 ms remaining ; 5 h 29 min 37 s 703.07 ms total)
Sat Oct 21 09:04:04 2023: Removed ≈ 42% of redundant conclusions. [ 4339521 of approximately 10332193] (ETC: Sat Oct 21 12:14:54 2023 ; 3 h 10 min 49 s 358.34 ms remaining ; 5 h 29 min 272.80 ms total)
Sat Oct 21 09:10:23 2023: Removed ≈ 44% of redundant conclusions. [ 4546164 of approximately 10332193] (ETC: Sat Oct 21 12:14:17 2023 ; 3 h 3 min 54 s 64.26 ms remaining ; 5 h 28 min 23 s 683.05 ms total)
Sat Oct 21 09:16:41 2023: Removed ≈ 46% of redundant conclusions. [ 4752808 of approximately 10332193] (ETC: Sat Oct 21 12:13:43 2023 ; 2 h 57 min 1 s 461.38 ms remaining ; 5 h 27 min 49 s 370.17 ms total)
Sat Oct 21 09:22:57 2023: Removed ≈ 48% of redundant conclusions. [ 4959452 of approximately 10332193] (ETC: Sat Oct 21 12:13:06 2023 ; 2 h 50 min 9 s 27.32 ms remaining ; 5 h 27 min 12 s 742.52 ms total)
Sat Oct 21 09:29:12 2023: Removed ≈ 50% of redundant conclusions. [ 5166096 of approximately 10332193] (ETC: Sat Oct 21 12:12:30 2023 ; 2 h 43 min 18 s 609.07 ms remaining ; 5 h 26 min 37 s 216.25 ms total)
Sat Oct 21 09:35:25 2023: Removed ≈ 52% of redundant conclusions. [ 5372740 of approximately 10332193] (ETC: Sat Oct 21 12:11:54 2023 ; 2 h 36 min 29 s 108.87 ms remaining ; 5 h 26 min 642.05 ms total)
Sat Oct 21 09:41:36 2023: Removed ≈ 54% of redundant conclusions. [ 5579384 of approximately 10332193] (ETC: Sat Oct 21 12:11:16 2023 ; 2 h 29 min 40 s 674.62 ms remaining ; 5 h 25 min 23 s 204.80 ms total)
Sat Oct 21 09:47:45 2023: Removed ≈ 56% of redundant conclusions. [ 5786028 of approximately 10332193] (ETC: Sat Oct 21 12:10:38 2023 ; 2 h 22 min 53 s 429.61 ms remaining ; 5 h 24 min 45 s 66.96 ms total)
Sat Oct 21 09:53:55 2023: Removed ≈ 58% of redundant conclusions. [ 5992671 of approximately 10332193] (ETC: Sat Oct 21 12:10:04 2023 ; 2 h 16 min 9 s 509.07 ms remaining ; 5 h 24 min 11 s 207.85 ms total)
Sat Oct 21 10:00:04 2023: Removed ≈ 60% of redundant conclusions. [ 6199315 of approximately 10332193] (ETC: Sat Oct 21 12:09:31 2023 ; 2 h 9 min 27 s 287.32 ms remaining ; 5 h 23 min 38 s 214.53 ms total)
Sat Oct 21 10:06:13 2023: Removed ≈ 62% of redundant conclusions. [ 6405959 of approximately 10332193] (ETC: Sat Oct 21 12:09:01 2023 ; 2 h 2 min 47 s 204.86 ms remaining ; 5 h 23 min 7 s 377.96 ms total)
Sat Oct 21 10:12:24 2023: Removed ≈ 64% of redundant conclusions. [ 6612603 of approximately 10332193] (ETC: Sat Oct 21 12:08:33 2023 ; 1 h 56 min 9 s 583.33 ms remaining ; 5 h 22 min 39 s 951.00 ms total)
Sat Oct 21 10:18:44 2023: Removed ≈ 66% of redundant conclusions. [ 6819247 of approximately 10332193] (ETC: Sat Oct 21 12:08:23 2023 ; 1 h 49 min 38 s 897.45 ms remaining ; 5 h 22 min 29 s 696.30 ms total)
Sat Oct 21 10:25:01 2023: Removed ≈ 68% of redundant conclusions. [ 7025891 of approximately 10332193] (ETC: Sat Oct 21 12:08:09 2023 ; 1 h 43 min 7 s 366.96 ms remaining ; 5 h 22 min 15 s 520.35 ms total)
Sat Oct 21 10:31:03 2023: Removed ≈ 70% of redundant conclusions. [ 7232535 of approximately 10332193] (ETC: Sat Oct 21 12:07:34 2023 ; 1 h 36 min 30 s 93.89 ms remaining ; 5 h 21 min 40 s 312.33 ms total)
Sat Oct 21 10:37:08 2023: Removed ≈ 72% of redundant conclusions. [ 7439178 of approximately 10332193] (ETC: Sat Oct 21 12:07:04 2023 ; 1 h 29 min 55 s 871.72 ms remaining ; 5 h 21 min 10 s 964.05 ms total)
Sat Oct 21 10:43:09 2023: Removed ≈ 74% of redundant conclusions. [ 7645822 of approximately 10332193] (ETC: Sat Oct 21 12:06:31 2023 ; 1 h 23 min 21 s 705.69 ms remaining ; 5 h 20 min 37 s 323.71 ms total)
Sat Oct 21 10:49:10 2023: Removed ≈ 76% of redundant conclusions. [ 7852466 of approximately 10332193] (ETC: Sat Oct 21 12:05:59 2023 ; 1 h 16 min 49 s 367.42 ms remaining ; 5 h 20 min 5 s 692.30 ms total)
Sat Oct 21 10:55:13 2023: Removed ≈ 78% of redundant conclusions. [ 8059110 of approximately 10332193] (ETC: Sat Oct 21 12:05:32 2023 ; 1 h 10 min 19 s 307.00 ms remaining ; 5 h 19 min 38 s 663.61 ms total)
Sat Oct 21 11:01:15 2023: Removed ≈ 80% of redundant conclusions. [ 8265754 of approximately 10332193] (ETC: Sat Oct 21 12:05:06 2023 ; 1 h 3 min 50 s 461.62 ms remaining ; 5 h 19 min 12 s 304.38 ms total)
Sat Oct 21 11:07:18 2023: Removed ≈ 82% of redundant conclusions. [ 8472398 of approximately 10332193] (ETC: Sat Oct 21 12:04:41 2023 ; 57 min 23 s 76.86 ms remaining ; 5 h 18 min 48 s 202.12 ms total)
Sat Oct 21 11:13:25 2023: Removed ≈ 84% of redundant conclusions. [ 8679042 of approximately 10332193] (ETC: Sat Oct 21 12:04:22 2023 ; 50 min 57 s 458.48 ms remaining ; 5 h 18 min 29 s 114.12 ms total)
Sat Oct 21 11:19:32 2023: Removed ≈ 86% of redundant conclusions. [ 8885685 of approximately 10332193] (ETC: Sat Oct 21 12:04:04 2023 ; 44 min 32 s 738.00 ms remaining ; 5 h 18 min 10 s 972.75 ms total)
Sat Oct 21 11:25:42 2023: Removed ≈ 88% of redundant conclusions. [ 9092329 of approximately 10332193] (ETC: Sat Oct 21 12:03:51 2023 ; 38 min 9 s 355.71 ms remaining ; 5 h 17 min 57 s 951.31 ms total)
Sat Oct 21 11:31:47 2023: Removed ≈ 90% of redundant conclusions. [ 9298973 of approximately 10332193] (ETC: Sat Oct 21 12:03:33 2023 ; 31 min 45 s 963.89 ms remaining ; 5 h 17 min 39 s 625.96 ms total)
Sat Oct 21 11:37:51 2023: Removed ≈ 92% of redundant conclusions. [ 9505617 of approximately 10332193] (ETC: Sat Oct 21 12:03:14 2023 ; 25 min 23 s 270.88 ms remaining ; 5 h 17 min 20 s 873.08 ms total)
Sat Oct 21 11:43:55 2023: Removed ≈ 94% of redundant conclusions. [ 9712261 of approximately 10332193] (ETC: Sat Oct 21 12:02:56 2023 ; 19 min 1 s 373.34 ms remaining ; 5 h 17 min 2 s 876.12 ms total)
Sat Oct 21 11:50:00 2023: Removed ≈ 96% of redundant conclusions. [ 9918905 of approximately 10332193] (ETC: Sat Oct 21 12:02:40 2023 ; 12 min 40 s 266.43 ms remaining ; 5 h 16 min 46 s 647.90 ms total)
[Rank 10] Workload transfer approved. Starting to work on 9:[5806899, 5821290].
[Rank 21] Workload transfer approved. Starting to work on 20:[12218234, 12232625].
[Rank 15] Workload transfer approved. Starting to work on 22:[13383931, 13398322].
[Rank 18] Workload transfer approved. Starting to work on 0:[561262, 575652].
[Rank 12] Workload transfer approved. Starting to work on 0:[575653, 580449].
Sat Oct 21 11:56:12 2023: Removed ≈ 98% of redundant conclusions. [10125549 of approximately 10332193] (ETC: Sat Oct 21 12:02:32 2023 ; 6 min 19 s 971.58 ms remaining ; 5 h 16 min 38 s 566.26 ms total)
[Rank 2] Workload transfer approved. Starting to work on 1:[1158502, 1163298].
[Rank 5] Workload transfer approved. Starting to work on 6:[4072745, 4077541].
[Rank 13] Workload transfer approved. Starting to work on 9:[5821291, 5826087].
[Rank 3] Workload transfer approved. Starting to work on 14:[8735534, 8740330].
[Rank 4] Workload transfer approved. Starting to work on 17:[10484080, 10488876].
[Rank 11] Workload transfer approved. Starting to work on 20:[12232626, 12237422].
[Rank 12] Workload transfer approved. Starting to work on 22:[13398323, 13403119].
[Rank 0] Workload transfer approved. Starting to work on 6:[4077542, 4079140].
[Rank 7] Workload transfer approved. Starting to work on 9:[5826088, 5827686].
[Rank 2] Workload transfer approved. Starting to work on 14:[8740331, 8741929].
[Rank 5] Workload transfer approved. Starting to work on 19:[11654574, 11656172].
[Rank 13] Workload transfer approved. Starting to work on 20:[12237423, 12239021].
[Rank 1] Workload transfer approved. Starting to work on 22:[13403120, 13404718].
[Rank 0] Workload transfer approved. Starting to work on 9:[5827687, 5828485].
[Rank 23] Workload transfer approved. Starting to work on 16:[9907627, 9908425].
[Rank 6] Workload transfer approved. Starting to work on 19:[11656173, 11656971].
[Rank 7] Workload transfer approved. Starting to work on 20:[12239022, 12239820].
[Rank 8] Workload transfer approved. Starting to work on 22:[13404719, 13405517].
19604194.37 ms (5 h 26 min 44 s 194.37 ms) taken to detect 10311828 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 3676539 representative and 10311828 redundant condensed detachment proof strings.
[Copy] Removal count: { 149, 10311828 }
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 1 on "ncm0514.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 2 on "ncm0515.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 3 on "ncm0516.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 4 on "ncm0517.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 5 on "ncm0518.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 6 on "ncm0519.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 7 on "ncm0520.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 8 on "ncm0521.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 9 on "ncm0522.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 10 on "ncm0523.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 11 on "ncm0524.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 12 on "ncm0525.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 13 on "ncm0526.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 14 on "ncm0527.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 15 on "ncm0528.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 16 on "ncm0529.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 17 on "ncm0530.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 18 on "ncm0531.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 19 on "ncm0532.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 20 on "ncm0533.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 21 on "ncm0534.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 22 on "ncm0536.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:12:36 2023: MPI-based D-proof representative filter complete. [rank 23 on "ncm0537.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
2575.51 ms (2 s 575.51 ms) taken to filter and order new representative proofs.
Sat Oct 21 12:12:38 2023: Starting to write 3676539 entries to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt.
4791.46 ms (4 s 791.46 ms) taken to print and save 1898469358 bytes of representative condensed detachment proof strings to data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt.
Sat Oct 21 12:12:43 2023: MPI-based D-proof representative filter complete. [rank 0 on "ncm0513.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 248549, tid:22975539472256]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 239250, tid:22493136877440]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 179250, tid:23051957557120]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 265810, tid:23397702719360]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 107773, tid:23445796722560]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 259852, tid:22606279636864]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 260069, tid:22562398766976]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 16288, tid:22997829887872]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 24920, tid:23287008069504]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 167917, tid:22949804918656]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 267421, tid:22577675212672]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 47280, tid:23011572561792]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 261788, tid:22980071835520]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 14615, tid:22787657873280]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 179907, tid:22514015463296]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 14971, tid:23073756407680]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 179296, tid:23189274511232]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 234875, tid:23112699856768]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 123973, tid:22926151501696]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 219186, tid:22897449146240]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 190819, tid:22777612744576]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 224362, tid:22793171609472]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 238327, tid:22817315653504]
Sat Oct 21 12:13:20 2023: Process terminated. [pid: 143108, tid:22807129577344]