-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
dProofs67_24node_1152cpu.log
330 lines (329 loc) · 41.3 KB
/
dProofs67_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
( 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: 4.7747222… h
CPU utilization: 5500.48 core-h )
Mon Oct 2 06:34:44 2023: Process started. [pid: 111970, tid:22857417213824]
Mon Oct 2 06:34:44 2023: Process started. [pid: 5751, tid:22449433335680]
Mon Oct 2 06:34:44 2023: Process started. [pid: 124725, tid:22781777504128]
Mon Oct 2 06:34:44 2023: Process started. [pid: 226772, tid:22614551893888]
Mon Oct 2 06:34:44 2023: Process started. [pid: 8095, tid:23062790371200]
Mon Oct 2 06:34:44 2023: Process started. [pid: 242326, tid:22463318472576]
Mon Oct 2 06:34:44 2023: Process started. [pid: 54249, tid:23091502229376]
Mon Oct 2 06:34:44 2023: Process started. [pid: 185018, tid:23364230698880]
Mon Oct 2 06:34:44 2023: Process started. [pid: 88367, tid:22923894179712]
Mon Oct 2 06:34:44 2023: Process started. [pid: 173118, tid:22978271958912]
Mon Oct 2 06:34:44 2023: Process started. [pid: 117601, tid:23392514160512]
Mon Oct 2 06:34:44 2023: Process started. [pid: 184224, tid:22448603305856]
Mon Oct 2 06:34:44 2023: Process started. [pid: 109655, tid:22802563676032]
Mon Oct 2 06:34:44 2023: Process started. [pid: 120761, tid:22965041465216]
Mon Oct 2 06:34:44 2023: Process started. [pid: 134063, tid:22552512919424]
Mon Oct 2 06:34:44 2023: Process started. [pid: 244701, tid:22747728824192]
Mon Oct 2 06:34:44 2023: Process started. [pid: 166198, tid:23347205814144]
Mon Oct 2 06:34:44 2023: Process started. [pid: 122822, tid:22552118785920]
Mon Oct 2 06:34:44 2023: Process started. [pid: 81510, tid:23000346920832]
Mon Oct 2 06:34:44 2023: Process started. [pid: 223746, tid:22919053399936]
Mon Oct 2 06:34:44 2023: Process started. [pid: 245924, tid:22447319275392]
Mon Oct 2 06:34:44 2023: Process started. [pid: 118215, tid:23425335187328]
Mon Oct 2 06:34:44 2023: Process started. [pid: 99425, tid:23150151108480]
Mon Oct 2 06:34:44 2023: Process started. [pid: 94677, tid:23052874094464]
Tasks:
1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true)
2. mpi_filterDProofRepresentativeFile(67, true)
[Rank 0 ; pid: 94677 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed]
(1) CCCCC0.1CN2N3.2.4CC4.0C3.0 - CCCCCpqCNrNsrtCCtpCsp - ((((0\imply1)\imply(\not2\imply\not3))\imply2)\imply4)\imply((4\imply0)\imply(3\imply0))
[Rank 1 ; pid: 8095 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 2 ; pid: 223746 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 3 ; pid: 81510 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 4 ; pid: 244701 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 5 ; pid: 185018 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 6 ; pid: 120761 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 7 ; pid: 242326 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 8 ; pid: 226772 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 9 ; pid: 88367 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 10 ; pid: 134063 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 11 ; pid: 166198 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 12 ; pid: 118215 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 13 ; pid: 111970 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 14 ; pid: 109655 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 15 ; pid: 124725 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 16 ; pid: 245924 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 17 ; pid: 184224 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 18 ; pid: 173118 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 19 ; pid: 99425 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 20 ; pid: 117601 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 21 ; pid: 122822 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 22 ; pid: 54249 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 23 ; pid: 5751 ; 24 processes] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true), silently.
[Rank 0 ; pid: 94677 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 1 ; pid: 8095 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 2 ; pid: 223746 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 3 ; pid: 81510 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 4 ; pid: 244701 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 5 ; pid: 185018 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 6 ; pid: 120761 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 7 ; pid: 242326 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 8 ; pid: 226772 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 9 ; pid: 88367 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 10 ; pid: 134063 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 11 ; pid: 166198 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 12 ; pid: 118215 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 13 ; pid: 111970 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 14 ; pid: 109655 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 15 ; pid: 124725 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 16 ; pid: 245924 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 17 ; pid: 184224 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 18 ; pid: 173118 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 19 ; pid: 99425 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 20 ; pid: 117601 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 21 ; pid: 122822 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 22 ; pid: 54249 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
[Rank 23 ; pid: 5751 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(67, true).
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 0 on "ncm0225.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 1 on "ncm0226.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 2 on "ncm0227.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 3 on "ncm0228.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 4 on "ncm0230.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 5 on "ncm0231.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 6 on "ncm0232.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 7 on "ncm0234.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 8 on "ncm0235.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 9 on "ncm0236.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 10 on "ncm0237.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 11 on "ncm0238.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 12 on "ncm0242.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 13 on "ncm0243.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 14 on "ncm0244.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 15 on "ncm0245.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 16 on "ncm0246.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 17 on "ncm0247.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 18 on "ncm0248.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 19 on "ncm0251.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 20 on "ncm0252.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 21 on "ncm0253.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 22 on "ncm0254.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 06:34:45 2023: MPI-based D-proof representative filter started. [rank 23 on "ncm0255.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
0.01 ms taken to load initial representatives.
20.21 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:23052698937088]
13.23 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:23052696835840]
8.51 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:23052565870336]
22.53 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:23052694734592]
13.21 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:23052692633344]
20.24 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:23052690532096]
24.95 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:23052688430848]
16.97 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:23052686329600]
17.03 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:23052684228352]
19.38 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:23052682127104]
25.99 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:23052680025856]
22.50 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:23052677924608]
32.00 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:23052675823360]
34.99 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:23052673722112]
106.23 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:23052671620864]
54.84 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:23052669519616]
54.24 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:23052667418368]
51.05 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:23052665317120]
51.73 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:23052663215872]
77.27 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:23052661114624]
93.25 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:23052659013376]
103.16 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:23052656912128]
189.97 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:23052654810880]
336.86 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:23052652709632]
693.07 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:23052650608384]
1441.86 ms (1 s 441.86 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:23052648507136]
4207.91 ms (4 s 207.91 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:23052646405888]
490.25 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:23052644304640]
716.97 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:23052642203392]
942.89 ms taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:23052640102144]
1421.50 ms (1 s 421.50 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:23052638000896]
1856.77 ms (1 s 856.77 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:23052635899648]
4227.00 ms (4 s 227.00 ms) total read duration.
Loaded 33 representative collections of sizes:
1 : 1
3 : 1
5 : 1
7 : 3
9 : 7
11 : 10
13 : 13
15 : 19
17 : 37
19 : 56
21 : 87
23 : 140
25 : 227
27 : 369
29 : 579
31 : 918
33 : 1499
35 : 2408
37 : 3881
39 : 6254
41 : 10109
43 : 16460
45 : 26753
47 : 43360
49 : 70709
51 : 115604
53 : 188634
55 : 308241
57 : 504870
59 : 827701
61 : 1357539
63 : 2227822
65 : 3660735
9375047 representatives in total.
3413.14 ms (3 s 413.14 ms) taken to read 8541161 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67-unfiltered67+.txt. [tid:23052635899648]
3414.66 ms (3 s 414.66 ms) additional read duration.
Loaded 1 more representative collection of size:
67 : 8541161
17916208 representatives in total.
Mon Oct 2 06:34:53 2023: Representative collections were initialized successfully on all ranks.
Estimated removal count set to 2516702, based on entry 65:1531673 and last known pair (63:932181, 65:1531673) with 1531673/932181 ≈ 1.64311 and 1531673 * (1531673/932181)^1 ≈ 2516702.42.
Mon Oct 2 06:34:53 2023: Inserted ≈ 5% of D-proof conclusions. [ 895810 of 17916208] (ETC: Mon Oct 2 06:35:00 2023 ; 7 s 97.30 ms remaining ; 7 s 470.84 ms total)
Mon Oct 2 06:34:54 2023: Inserted ≈10% of D-proof conclusions. [ 1791620 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 7 s 251.60 ms remaining ; 8 s 57.33 ms total)
Mon Oct 2 06:34:54 2023: Inserted ≈15% of D-proof conclusions. [ 2687431 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 7 s 160.20 ms remaining ; 8 s 423.77 ms total)
Mon Oct 2 06:34:54 2023: Inserted ≈20% of D-proof conclusions. [ 3583241 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 6 s 703.35 ms remaining ; 8 s 379.19 ms total)
Mon Oct 2 06:34:55 2023: Inserted ≈25% of D-proof conclusions. [ 4479052 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 6 s 343.31 ms remaining ; 8 s 457.75 ms total)
Mon Oct 2 06:34:55 2023: Inserted ≈30% of D-proof conclusions. [ 5374862 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 5 s 862.95 ms remaining ; 8 s 375.64 ms total)
Mon Oct 2 06:34:56 2023: Inserted ≈35% of D-proof conclusions. [ 6270672 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 5 s 397.14 ms remaining ; 8 s 303.30 ms total)
Mon Oct 2 06:34:56 2023: Inserted ≈40% of D-proof conclusions. [ 7166483 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 4 s 922.15 ms remaining ; 8 s 203.59 ms total)
Mon Oct 2 06:34:56 2023: Inserted ≈45% of D-proof conclusions. [ 8062293 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 4 s 481.83 ms remaining ; 8 s 148.78 ms total)
Mon Oct 2 06:34:57 2023: Inserted ≈50% of D-proof conclusions. [ 8958104 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 4 s 102.38 ms remaining ; 8 s 204.75 ms total)
Mon Oct 2 06:34:57 2023: Inserted ≈55% of D-proof conclusions. [ 9853914 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 3 s 642.80 ms remaining ; 8 s 95.11 ms total)
Mon Oct 2 06:34:58 2023: Inserted ≈60% of D-proof conclusions. [10749724 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 3 s 201.15 ms remaining ; 8 s 2.88 ms total)
Mon Oct 2 06:34:58 2023: Inserted ≈65% of D-proof conclusions. [11645535 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 2 s 764.17 ms remaining ; 7 s 897.63 ms total)
Mon Oct 2 06:34:58 2023: Inserted ≈70% of D-proof conclusions. [12541345 of 17916208] (ETC: Mon Oct 2 06:35:01 2023 ; 2 s 346.38 ms remaining ; 7 s 821.25 ms total)
Mon Oct 2 06:34:59 2023: Inserted ≈75% of D-proof conclusions. [13437156 of 17916208] (ETC: Mon Oct 2 06:35:00 2023 ; 1 s 925.00 ms remaining ; 7 s 700.01 ms total)
Mon Oct 2 06:34:59 2023: Inserted ≈80% of D-proof conclusions. [14332966 of 17916208] (ETC: Mon Oct 2 06:35:00 2023 ; 1 s 536.51 ms remaining ; 7 s 682.56 ms total)
Mon Oct 2 06:34:59 2023: Inserted ≈85% of D-proof conclusions. [15228776 of 17916208] (ETC: Mon Oct 2 06:35:00 2023 ; 1 s 148.21 ms remaining ; 7 s 654.72 ms total)
Mon Oct 2 06:35:00 2023: Inserted ≈90% of D-proof conclusions. [16124587 of 17916208] (ETC: Mon Oct 2 06:35:00 2023 ; 763.33 ms remaining ; 7 s 633.31 ms total)
Mon Oct 2 06:35:00 2023: Inserted ≈95% of D-proof conclusions. [17020397 of 17916208] (ETC: Mon Oct 2 06:35:00 2023 ; 383.10 ms remaining ; 7 s 661.97 ms total)
Mon Oct 2 06:35:00 2023: Inserted 100% of D-proof conclusions. [17916208 of 17916208] (ETC: Mon Oct 2 06:35:00 2023 ; 0.00 ms remaining ; 7 s 685.76 ms total)
7685.85 ms (7 s 685.85 ms) total insertion duration.
Reservable workloads: { 0:[237254, 355880], 1:[593136, 711762], 2:[949018, 1067644], 3:[1304899, 1423525], 4:[1660781, 1779407], 5:[2016663, 2135289], 6:[2372544, 2491170], 7:[2728426, 2847052], 8:[3084308, 3202934], 9:[3440190, 3558816], 10:[3796071, 3914697], 11:[4151953, 4270579], 12:[4507835, 4626461], 13:[4863716, 4982342], 14:[5219598, 5338224], 15:[5575480, 5694106], 16:[5931362, 6049988], 17:[6287243, 6405869], 18:[6643125, 6761751], 19:[6999007, 7117633], 20:[7354888, 7473514], 21:[7710770, 7829396], 22:[8066652, 8185278], 23:[8422534, 8541160] }
Mon Oct 2 06:41:10 2023: Removed ≈ 2% of redundant conclusions. [ 50334 of approximately 2516702] (ETC: Mon Oct 2 11:42:06 2023 ; 5 h 55 s 736.57 ms remaining ; 5 h 7 min 4 s 220.69 ms total)
Mon Oct 2 06:47:17 2023: Removed ≈ 4% of redundant conclusions. [ 100668 of approximately 2516702] (ETC: Mon Oct 2 11:41:24 2023 ; 4 h 54 min 7 s 371.11 ms remaining ; 5 h 6 min 22 s 677.63 ms total)
Mon Oct 2 06:53:20 2023: Removed ≈ 6% of redundant conclusions. [ 151002 of approximately 2516702] (ETC: Mon Oct 2 11:40:10 2023 ; 4 h 46 min 50 s 303.85 ms remaining ; 5 h 5 min 8 s 832.95 ms total)
Mon Oct 2 06:59:18 2023: Removed ≈ 8% of redundant conclusions. [ 201336 of approximately 2516702] (ETC: Mon Oct 2 11:38:25 2023 ; 4 h 39 min 6 s 755.78 ms remaining ; 5 h 3 min 22 s 994.15 ms total)
Mon Oct 2 07:05:13 2023: Removed ≈ 10% of redundant conclusions. [ 251670 of approximately 2516702] (ETC: Mon Oct 2 11:36:57 2023 ; 4 h 31 min 43 s 829.17 ms remaining ; 5 h 1 min 55 s 364.15 ms total)
Mon Oct 2 07:11:05 2023: Removed ≈ 12% of redundant conclusions. [ 302004 of approximately 2516702] (ETC: Mon Oct 2 11:35:31 2023 ; 4 h 24 min 25 s 566.14 ms remaining ; 5 h 29 s 50.48 ms total)
Mon Oct 2 07:16:57 2023: Removed ≈ 14% of redundant conclusions. [ 352338 of approximately 2516702] (ETC: Mon Oct 2 11:34:29 2023 ; 4 h 17 min 31 s 865.29 ms remaining ; 4 h 59 min 27 s 282.89 ms total)
Mon Oct 2 07:22:46 2023: Removed ≈ 16% of redundant conclusions. [ 402672 of approximately 2516702] (ETC: Mon Oct 2 11:33:27 2023 ; 4 h 10 min 40 s 530.62 ms remaining ; 4 h 58 min 25 s 390.88 ms total)
Mon Oct 2 07:28:33 2023: Removed ≈ 18% of redundant conclusions. [ 453006 of approximately 2516702] (ETC: Mon Oct 2 11:32:22 2023 ; 4 h 3 min 49 s 403.79 ms remaining ; 4 h 57 min 20 s 733.21 ms total)
Mon Oct 2 07:34:18 2023: Removed ≈ 20% of redundant conclusions. [ 503340 of approximately 2516702] (ETC: Mon Oct 2 11:31:25 2023 ; 3 h 57 min 6 s 409.43 ms remaining ; 4 h 56 min 23 s 8.25 ms total)
Mon Oct 2 07:40:03 2023: Removed ≈ 22% of redundant conclusions. [ 553674 of approximately 2516702] (ETC: Mon Oct 2 11:30:34 2023 ; 3 h 50 min 31 s 493.78 ms remaining ; 4 h 55 min 32 s 680.36 ms total)
Mon Oct 2 07:45:48 2023: Removed ≈ 24% of redundant conclusions. [ 604008 of approximately 2516702] (ETC: Mon Oct 2 11:29:57 2023 ; 3 h 44 min 8 s 469.13 ms remaining ; 4 h 54 min 55 s 349.68 ms total)
Mon Oct 2 07:51:32 2023: Removed ≈ 26% of redundant conclusions. [ 654342 of approximately 2516702] (ETC: Mon Oct 2 11:29:19 2023 ; 3 h 37 min 46 s 592.84 ms remaining ; 4 h 54 min 17 s 552.96 ms total)
Mon Oct 2 07:57:20 2023: Removed ≈ 28% of redundant conclusions. [ 704676 of approximately 2516702] (ETC: Mon Oct 2 11:28:57 2023 ; 3 h 31 min 37 s 781.14 ms remaining ; 4 h 53 min 55 s 801.69 ms total)
Mon Oct 2 08:03:05 2023: Removed ≈ 30% of redundant conclusions. [ 755010 of approximately 2516702] (ETC: Mon Oct 2 11:28:34 2023 ; 3 h 25 min 29 s 91.55 ms remaining ; 4 h 53 min 32 s 981.92 ms total)
Mon Oct 2 08:08:50 2023: Removed ≈ 32% of redundant conclusions. [ 805344 of approximately 2516702] (ETC: Mon Oct 2 11:28:11 2023 ; 3 h 19 min 20 s 939.00 ms remaining ; 4 h 53 min 9 s 609.60 ms total)
Mon Oct 2 08:14:34 2023: Removed ≈ 34% of redundant conclusions. [ 855678 of approximately 2516702] (ETC: Mon Oct 2 11:27:47 2023 ; 3 h 13 min 12 s 982.48 ms remaining ; 4 h 52 min 45 s 117.78 ms total)
Mon Oct 2 08:20:14 2023: Removed ≈ 36% of redundant conclusions. [ 906012 of approximately 2516702] (ETC: Mon Oct 2 11:27:16 2023 ; 3 h 7 min 1 s 981.25 ms remaining ; 4 h 52 min 14 s 337.87 ms total)
Mon Oct 2 08:25:49 2023: Removed ≈ 38% of redundant conclusions. [ 956346 of approximately 2516702] (ETC: Mon Oct 2 11:26:36 2023 ; 3 h 46 s 602.41 ms remaining ; 4 h 51 min 34 s 511.49 ms total)
Mon Oct 2 08:31:22 2023: Removed ≈ 40% of redundant conclusions. [1006680 of approximately 2516702] (ETC: Mon Oct 2 11:25:52 2023 ; 2 h 54 min 30 s 346.78 ms remaining ; 4 h 50 min 50 s 568.73 ms total)
Mon Oct 2 08:36:53 2023: Removed ≈ 42% of redundant conclusions. [1057014 of approximately 2516702] (ETC: Mon Oct 2 11:25:09 2023 ; 2 h 48 min 16 s 611.74 ms remaining ; 4 h 50 min 7 s 941.26 ms total)
Mon Oct 2 08:42:22 2023: Removed ≈ 44% of redundant conclusions. [1107348 of approximately 2516702] (ETC: Mon Oct 2 11:24:27 2023 ; 2 h 42 min 4 s 757.71 ms remaining ; 4 h 49 min 25 s 627.93 ms total)
Mon Oct 2 08:47:51 2023: Removed ≈ 46% of redundant conclusions. [1157682 of approximately 2516702] (ETC: Mon Oct 2 11:23:46 2023 ; 2 h 35 min 55 s 500.47 ms remaining ; 4 h 48 min 44 s 989.14 ms total)
Mon Oct 2 08:53:24 2023: Removed ≈ 48% of redundant conclusions. [1208016 of approximately 2516702] (ETC: Mon Oct 2 11:23:18 2023 ; 2 h 29 min 54 s 436.74 ms remaining ; 4 h 48 min 16 s 981.03 ms total)
Mon Oct 2 08:58:55 2023: Removed ≈ 50% of redundant conclusions. [1258351 of approximately 2516702] (ETC: Mon Oct 2 11:22:48 2023 ; 2 h 23 min 53 s 482.15 ms remaining ; 4 h 47 min 46 s 964.30 ms total)
Mon Oct 2 09:04:28 2023: Removed ≈ 52% of redundant conclusions. [1308685 of approximately 2516702] (ETC: Mon Oct 2 11:22:25 2023 ; 2 h 17 min 56 s 948.51 ms remaining ; 4 h 47 min 23 s 642.16 ms total)
Mon Oct 2 09:10:04 2023: Removed ≈ 54% of redundant conclusions. [1359019 of approximately 2516702] (ETC: Mon Oct 2 11:22:08 2023 ; 2 h 12 min 4 s 69.49 ms remaining ; 4 h 47 min 6 s 236.84 ms total)
Mon Oct 2 09:15:40 2023: Removed ≈ 56% of redundant conclusions. [1409353 of approximately 2516702] (ETC: Mon Oct 2 11:21:53 2023 ; 2 h 6 min 13 s 236.34 ms remaining ; 4 h 46 min 51 s 898.90 ms total)
Mon Oct 2 09:21:12 2023: Removed ≈ 58% of redundant conclusions. [1459687 of approximately 2516702] (ETC: Mon Oct 2 11:21:32 2023 ; 2 h 20 s 78.71 ms remaining ; 4 h 46 min 30 s 660.99 ms total)
Mon Oct 2 09:26:46 2023: Removed ≈ 60% of redundant conclusions. [1510021 of approximately 2516702] (ETC: Mon Oct 2 11:21:16 2023 ; 1 h 54 min 29 s 808.69 ms remaining ; 4 h 46 min 14 s 518.31 ms total)
Mon Oct 2 09:32:20 2023: Removed ≈ 62% of redundant conclusions. [1560355 of approximately 2516702] (ETC: Mon Oct 2 11:21:00 2023 ; 1 h 48 min 40 s 106.11 ms remaining ; 4 h 45 min 58 s 169.66 ms total)
Mon Oct 2 09:37:50 2023: Removed ≈ 64% of redundant conclusions. [1610689 of approximately 2516702] (ETC: Mon Oct 2 11:20:40 2023 ; 1 h 42 min 49 s 947.72 ms remaining ; 4 h 45 min 38 s 738.37 ms total)
Mon Oct 2 09:43:27 2023: Removed ≈ 66% of redundant conclusions. [1661023 of approximately 2516702] (ETC: Mon Oct 2 11:20:31 2023 ; 1 h 37 min 3 s 886.64 ms remaining ; 4 h 45 min 29 s 71.95 ms total)
Mon Oct 2 09:49:08 2023: Removed ≈ 68% of redundant conclusions. [1711357 of approximately 2516702] (ETC: Mon Oct 2 11:20:29 2023 ; 1 h 31 min 20 s 803.96 ms remaining ; 4 h 45 min 27 s 504.71 ms total)
Mon Oct 2 09:54:36 2023: Removed ≈ 70% of redundant conclusions. [1761691 of approximately 2516702] (ETC: Mon Oct 2 11:20:08 2023 ; 1 h 25 min 31 s 802.62 ms remaining ; 4 h 45 min 5 s 999.66 ms total)
Mon Oct 2 10:00:02 2023: Removed ≈ 72% of redundant conclusions. [1812025 of approximately 2516702] (ETC: Mon Oct 2 11:19:46 2023 ; 1 h 19 min 43 s 673.91 ms remaining ; 4 h 44 min 44 s 539.01 ms total)
Mon Oct 2 10:05:29 2023: Removed ≈ 74% of redundant conclusions. [1862359 of approximately 2516702] (ETC: Mon Oct 2 11:19:26 2023 ; 1 h 13 min 56 s 782.51 ms remaining ; 4 h 44 min 24 s 535.60 ms total)
Mon Oct 2 10:10:56 2023: Removed ≈ 76% of redundant conclusions. [1912693 of approximately 2516702] (ETC: Mon Oct 2 11:19:07 2023 ; 1 h 8 min 10 s 971.69 ms remaining ; 4 h 44 min 5 s 700.72 ms total)
Mon Oct 2 10:16:25 2023: Removed ≈ 78% of redundant conclusions. [1963027 of approximately 2516702] (ETC: Mon Oct 2 11:18:52 2023 ; 1 h 2 min 26 s 762.29 ms remaining ; 4 h 43 min 50 s 720.44 ms total)
Mon Oct 2 10:21:54 2023: Removed ≈ 80% of redundant conclusions. [2013361 of approximately 2516702] (ETC: Mon Oct 2 11:18:38 2023 ; 56 min 43 s 207.27 ms remaining ; 4 h 43 min 36 s 16.06 ms total)
Mon Oct 2 10:27:25 2023: Removed ≈ 82% of redundant conclusions. [2063695 of approximately 2516702] (ETC: Mon Oct 2 11:18:25 2023 ; 51 min 666.31 ms remaining ; 4 h 43 min 23 s 677.70 ms total)
Mon Oct 2 10:32:58 2023: Removed ≈ 84% of redundant conclusions. [2114029 of approximately 2516702] (ETC: Mon Oct 2 11:18:18 2023 ; 45 min 19 s 371.53 ms remaining ; 4 h 43 min 16 s 43.39 ms total)
Mon Oct 2 10:38:31 2023: Removed ≈ 86% of redundant conclusions. [2164363 of approximately 2516702] (ETC: Mon Oct 2 11:18:10 2023 ; 39 min 38 s 333.35 ms remaining ; 4 h 43 min 8 s 60.66 ms total)
Mon Oct 2 10:44:03 2023: Removed ≈ 88% of redundant conclusions. [2214697 of approximately 2516702] (ETC: Mon Oct 2 11:18:00 2023 ; 33 min 57 s 441.99 ms remaining ; 4 h 42 min 58 s 640.53 ms total)
Mon Oct 2 10:49:39 2023: Removed ≈ 90% of redundant conclusions. [2265031 of approximately 2516702] (ETC: Mon Oct 2 11:17:57 2023 ; 28 min 17 s 527.36 ms remaining ; 4 h 42 min 55 s 219.62 ms total)
Mon Oct 2 10:55:08 2023: Removed ≈ 92% of redundant conclusions. [2315365 of approximately 2516702] (ETC: Mon Oct 2 11:17:45 2023 ; 22 min 37 s 85.62 ms remaining ; 4 h 42 min 43 s 499.45 ms total)
Mon Oct 2 11:00:38 2023: Removed ≈ 94% of redundant conclusions. [2365699 of approximately 2516702] (ETC: Mon Oct 2 11:17:35 2023 ; 16 min 57 s 243.81 ms remaining ; 4 h 42 min 33 s 964.68 ms total)
Mon Oct 2 11:06:12 2023: Removed ≈ 96% of redundant conclusions. [2416033 of approximately 2516702] (ETC: Mon Oct 2 11:17:30 2023 ; 11 min 17 s 950.09 ms remaining ; 4 h 42 min 28 s 597.32 ms total)
Mon Oct 2 11:11:44 2023: Removed ≈ 98% of redundant conclusions. [2466367 of approximately 2516702] (ETC: Mon Oct 2 11:17:23 2023 ; 5 min 38 s 837.87 ms remaining ; 4 h 42 min 21 s 570.54 ms total)
[Rank 10] Workload transfer approved. Starting to work on 0:[342701, 351487].
[Rank 21] Workload transfer approved. Starting to work on 7:[2833873, 2842659].
[Rank 2] Workload transfer approved. Starting to work on 0:[351488, 354416].
[Rank 19] Workload transfer approved. Starting to work on 3:[1419133, 1422061].
[Rank 18] Workload transfer approved. Starting to work on 4:[1775015, 1777943].
[Rank 16] Workload transfer approved. Starting to work on 6:[2486778, 2489706].
[Rank 8] Workload transfer approved. Starting to work on 7:[2842660, 2845588].
[Rank 2] Workload transfer approved. Starting to work on 15:[5689714, 5692642].
[Rank 19] Workload transfer approved. Starting to work on 0:[354417, 355392].
[Rank 18] Workload transfer approved. Starting to work on 3:[1422062, 1423037].
[Rank 11] Workload transfer approved. Starting to work on 7:[2845589, 2846564].
[Rank 1] Workload transfer approved. Starting to work on 13:[4980879, 4981854].
[Rank 22] Workload transfer approved. Starting to work on 15:[5692643, 5693618].
[Rank 4] Workload transfer approved. Starting to work on 0:[355393, 355880].
[Rank 19] Workload transfer approved. Starting to work on 3:[1423038, 1423525].
[Rank 12] Workload transfer approved. Starting to work on 5:[2134802, 2135289].
[Rank 3] Workload transfer approved. Starting to work on 7:[2846565, 2847052].
[Rank 13] Workload transfer approved. Starting to work on 14:[5337737, 5338224].
[Rank 18] Workload transfer approved. Starting to work on 17:[6405382, 6405869].
[Rank 6] Workload transfer approved. Starting to work on 20:[7473027, 7473514].
Mon Oct 2 11:17:53 2023: Removed ≈100% of redundant conclusions. [2516702 of approximately 2516702] (ETC: Mon Oct 2 11:17:53 2023 ; 0.00 ms remaining ; 4 h 42 min 51 s 246.58 ms total)
17154079.28 ms (4 h 45 min 54 s 79.28 ms) taken to detect 2520051 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 6021110 representative and 2520051 redundant condensed detachment proof strings.
[Copy] Removal count: { 67, 2520051 }
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 1 on "ncm0226.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 2 on "ncm0227.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 3 on "ncm0228.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 4 on "ncm0230.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 5 on "ncm0231.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 6 on "ncm0232.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 7 on "ncm0234.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 8 on "ncm0235.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 9 on "ncm0236.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 10 on "ncm0237.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 11 on "ncm0238.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 12 on "ncm0242.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 13 on "ncm0243.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 14 on "ncm0244.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 15 on "ncm0245.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 16 on "ncm0246.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 17 on "ncm0247.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 18 on "ncm0248.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 19 on "ncm0251.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 20 on "ncm0252.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 21 on "ncm0253.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 22 on "ncm0254.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:20:10 2023: MPI-based D-proof representative filter complete. [rank 23 on "ncm0255.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
1646.71 ms (1 s 646.71 ms) taken to filter and order new representative proofs.
Mon Oct 2 11:20:56 2023: Starting to write 6021110 entries to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt.
2621.39 ms (2 s 621.39 ms) taken to print and save 996579205 bytes of representative condensed detachment proof strings to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt.
Mon Oct 2 11:20:59 2023: MPI-based D-proof representative filter complete. [rank 0 on "ncm0225.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 134063, tid:22552512919424]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 88367, tid:22923894179712]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 226772, tid:22614551893888]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 120761, tid:22965041465216]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 166198, tid:23347205814144]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 185018, tid:23364230698880]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 244701, tid:22747728824192]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 81510, tid:23000346920832]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 118215, tid:23425335187328]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 242326, tid:22463318472576]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 99425, tid:23150151108480]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 117601, tid:23392514160512]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 54249, tid:23091502229376]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 8095, tid:23062790371200]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 111970, tid:22857417213824]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 109655, tid:22802563676032]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 173118, tid:22978271958912]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 122822, tid:22552118785920]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 245924, tid:22447319275392]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 5751, tid:22449433335680]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 223746, tid:22919053399936]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 94677, tid:23052874094464]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 184224, tid:22448603305856]
Mon Oct 2 11:21:13 2023: Process terminated. [pid: 124725, tid:22781777504128]