-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
dProofs49_24node_1152cpu.log
302 lines (301 loc) · 38.3 KB
/
dProofs49_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
( 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: 3.09 h
CPU utilization: 3559.68 core-h )
Mon Oct 23 03:42:17 2023: Process started. [pid: 166363, tid:22987896518528]
Mon Oct 23 03:42:17 2023: Process started. [pid: 161417, tid:23218173986688]
Mon Oct 23 03:42:17 2023: Process started. [pid: 268902, tid:22441279960960]
Mon Oct 23 03:42:17 2023: Process started. [pid: 85986, tid:22782196049792]
Mon Oct 23 03:42:17 2023: Process started. [pid: 188440, tid:22770325993344]
Mon Oct 23 03:42:17 2023: Process started. [pid: 162493, tid:22375476062080]
Mon Oct 23 03:42:17 2023: Process started. [pid: 166903, tid:22829834082176]
Mon Oct 23 03:42:17 2023: Process started. [pid: 186317, tid:22893723248512]
Mon Oct 23 03:42:17 2023: Process started. [pid: 172658, tid:23324746250112]
Mon Oct 23 03:42:17 2023: Process started. [pid: 111335, tid:22529070110592]
Mon Oct 23 03:42:17 2023: Process started. [pid: 92853, tid:22509334849408]
Mon Oct 23 03:42:17 2023: Process started. [pid: 217576, tid:22520543606656]
Mon Oct 23 03:42:17 2023: Process started. [pid: 231842, tid:22780543711104]
Mon Oct 23 03:42:17 2023: Process started. [pid: 63571, tid:22842480195456]
Mon Oct 23 03:42:17 2023: Process started. [pid: 212741, tid:23268658677632]
Mon Oct 23 03:42:17 2023: Process started. [pid: 82577, tid:22475653916544]
Mon Oct 23 03:42:17 2023: Process started. [pid: 154739, tid:22740978435968]
Mon Oct 23 03:42:17 2023: Process started. [pid: 131064, tid:23207789078400]
Mon Oct 23 03:42:17 2023: Process started. [pid: 95302, tid:23092832561024]
Mon Oct 23 03:42:17 2023: Process started. [pid: 97185, tid:23408963327872]
Mon Oct 23 03:42:17 2023: Process started. [pid: 202554, tid:23204300527488]
Mon Oct 23 03:42:17 2023: Process started. [pid: 109424, tid:22591423620992]
Mon Oct 23 03:42:17 2023: Process started. [pid: 94382, tid:23002790500224]
Mon Oct 23 03:42:17 2023: Process started. [pid: 200270, tid:23179364542336]
Tasks:
1. resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true)
2. mpi_filterDProofRepresentativeFile(49, true)
[Rank 0 ; pid: 200270 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72]
(1) CC0.1CCC2C3.4C1CN3N0C0.3 - CCpqCCCrCstCqCNsNpCps - (0\imply1)\imply(((2\imply(3\imply4))\imply(1\imply(\not3\imply\not0)))\imply(0\imply3))
[Rank 1 ; pid: 63571 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 2 ; pid: 92853 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 3 ; pid: 188440 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 4 ; pid: 231842 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 5 ; pid: 202554 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 6 ; pid: 212741 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 7 ; pid: 161417 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 8 ; pid: 154739 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 9 ; pid: 82577 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 10 ; pid: 162493 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 11 ; pid: 97185 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 12 ; pid: 111335 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 13 ; pid: 172658 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 14 ; pid: 94382 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 15 ; pid: 166363 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 16 ; pid: 109424 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 17 ; pid: 186317 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 18 ; pid: 268902 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 19 ; pid: 166903 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 20 ; pid: 95302 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 21 ; pid: 85986 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 22 ; pid: 217576 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 23 ; pid: 131064 ; 24 processes] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true), silently.
[Rank 0 ; pid: 200270 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 1 ; pid: 63571 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 2 ; pid: 92853 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 3 ; pid: 188440 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 4 ; pid: 231842 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 5 ; pid: 202554 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 6 ; pid: 212741 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 7 ; pid: 161417 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 8 ; pid: 154739 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 9 ; pid: 82577 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 10 ; pid: 162493 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 11 ; pid: 97185 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 12 ; pid: 111335 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 13 ; pid: 172658 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 14 ; pid: 94382 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 15 ; pid: 166363 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 16 ; pid: 109424 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 17 ; pid: 186317 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 18 ; pid: 268902 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 19 ; pid: 166903 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 20 ; pid: 95302 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 21 ; pid: 85986 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 22 ; pid: 217576 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
[Rank 23 ; pid: 131064 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(49, true).
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 0 on "ncm0113.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 1 on "ncm0114.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 2 on "ncm0116.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 3 on "ncm0117.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 4 on "ncm0119.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 5 on "ncm0121.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 6 on "ncm0122.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 7 on "ncm0123.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 8 on "ncm0124.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 9 on "ncm0125.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 10 on "ncm0128.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 11 on "ncm0129.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 12 on "ncm0130.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 13 on "ncm0131.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 14 on "ncm0132.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 15 on "ncm0134.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 16 on "ncm0136.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 17 on "ncm0137.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 18 on "ncm0138.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 19 on "ncm0139.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 20 on "ncm0140.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 21 on "ncm0141.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 22 on "ncm0142.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 03:42:18 2023: MPI-based D-proof representative filter started. [rank 23 on "ncm0144.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
0.01 ms taken to load initial representatives.
14.00 ms taken to read 1 condensed detachment proof and conclusion from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs3.txt. [tid:23179189384960]
18.29 ms taken to read 1 condensed detachment proof and conclusion from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs5.txt. [tid:23179187283712]
24.30 ms taken to read 2 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs7.txt. [tid:23179066078976]
16.76 ms taken to read 4 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs9.txt. [tid:23179185182464]
14.43 ms taken to read 7 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs11.txt. [tid:23179183081216]
18.10 ms taken to read 12 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs13.txt. [tid:23179180979968]
22.84 ms taken to read 22 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs15.txt. [tid:23179178878720]
14.31 ms taken to read 42 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs17.txt. [tid:23179176777472]
23.61 ms taken to read 80 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs19.txt. [tid:23179174676224]
33.39 ms taken to read 151 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs21.txt. [tid:23179172574976]
40.65 ms taken to read 287 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs23.txt. [tid:23179170473728]
43.02 ms taken to read 555 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs25.txt. [tid:23179168372480]
54.04 ms taken to read 1081 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs27.txt. [tid:23179166271232]
90.56 ms taken to read 2107 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs29.txt. [tid:23179164169984]
285.81 ms taken to read 4123 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs31.txt. [tid:23179162068736]
1104.14 ms (1 s 104.14 ms) taken to read 8112 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs33.txt. [tid:23179159967488]
4929.81 ms (4 s 929.81 ms) taken to read 16029 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs35.txt. [tid:23179157866240]
478.45 ms taken to read 31774 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs37.txt. [tid:23179155764992]
1019.55 ms (1 s 19.55 ms) taken to read 63152 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs39.txt. [tid:23179153663744]
1963.10 ms (1 s 963.10 ms) taken to read 125873 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs41.txt. [tid:23179151562496]
3197.79 ms (3 s 197.79 ms) taken to read 251561 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs43.txt. [tid:23179149461248]
5679.55 ms (5 s 679.56 ms) taken to read 503956 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs45.txt. [tid:23179147360000]
10288.34 ms (10 s 288.34 ms) taken to read 1011747 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs47.txt. [tid:23179145258752]
10304.53 ms (10 s 304.53 ms) total read duration.
Loaded 24 representative collections of sizes:
1 : 1
3 : 1
5 : 1
7 : 2
9 : 4
11 : 7
13 : 12
15 : 22
17 : 42
19 : 80
21 : 151
23 : 287
25 : 555
27 : 1081
29 : 2107
31 : 4123
33 : 8112
35 : 16029
37 : 31774
39 : 63152
41 : 125873
43 : 251561
45 : 503956
47 : 1011747
2020680 representatives in total.
18405.07 ms (18 s 405.07 ms) taken to read 2053180 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs49-unfiltered49+.txt. [tid:23179145258752]
18406.81 ms (18 s 406.81 ms) additional read duration.
Loaded 1 more representative collection of size:
49 : 2053180
4073860 representatives in total.
Mon Oct 23 03:42:51 2023: Representative collections were initialized successfully on all ranks.
Estimated removal count set to 18028, based on entry 47:8474 and last known pair (45:3983, 47:8474) with 8474/3983 ≈ 2.12754 and 8474 * (8474/3983)^1 ≈ 18028.79.
Mon Oct 23 03:42:52 2023: Inserted ≈ 5% of D-proof conclusions. [ 203693 of 4073860] (ETC: Mon Oct 23 03:43:20 2023 ; 27 s 147.54 ms remaining ; 28 s 576.36 ms total)
Mon Oct 23 03:42:54 2023: Inserted ≈10% of D-proof conclusions. [ 407386 of 4073860] (ETC: Mon Oct 23 03:43:24 2023 ; 29 s 764.54 ms remaining ; 33 s 71.71 ms total)
Mon Oct 23 03:42:57 2023: Inserted ≈15% of D-proof conclusions. [ 611079 of 4073860] (ETC: Mon Oct 23 03:43:28 2023 ; 31 s 392.93 ms remaining ; 36 s 932.86 ms total)
Mon Oct 23 03:42:59 2023: Inserted ≈20% of D-proof conclusions. [ 814772 of 4073860] (ETC: Mon Oct 23 03:43:33 2023 ; 33 s 204.61 ms remaining ; 41 s 505.76 ms total)
Mon Oct 23 03:43:02 2023: Inserted ≈25% of D-proof conclusions. [1018465 of 4073860] (ETC: Mon Oct 23 03:43:34 2023 ; 32 s 581.33 ms remaining ; 43 s 441.77 ms total)
Mon Oct 23 03:43:04 2023: Inserted ≈30% of D-proof conclusions. [1222158 of 4073860] (ETC: Mon Oct 23 03:43:34 2023 ; 30 s 410.97 ms remaining ; 43 s 444.24 ms total)
Mon Oct 23 03:43:07 2023: Inserted ≈35% of D-proof conclusions. [1425851 of 4073860] (ETC: Mon Oct 23 03:43:36 2023 ; 29 s 450.20 ms remaining ; 45 s 308.00 ms total)
Mon Oct 23 03:43:10 2023: Inserted ≈40% of D-proof conclusions. [1629544 of 4073860] (ETC: Mon Oct 23 03:43:39 2023 ; 28 s 817.30 ms remaining ; 48 s 28.84 ms total)
Mon Oct 23 03:43:13 2023: Inserted ≈45% of D-proof conclusions. [1833237 of 4073860] (ETC: Mon Oct 23 03:43:40 2023 ; 27 s 40.66 ms remaining ; 49 s 164.83 ms total)
Mon Oct 23 03:43:17 2023: Inserted ≈50% of D-proof conclusions. [2036930 of 4073860] (ETC: Mon Oct 23 03:43:42 2023 ; 25 s 681.02 ms remaining ; 51 s 362.04 ms total)
Mon Oct 23 03:43:18 2023: Inserted ≈55% of D-proof conclusions. [2240623 of 4073860] (ETC: Mon Oct 23 03:43:40 2023 ; 22 s 264.10 ms remaining ; 49 s 475.79 ms total)
Mon Oct 23 03:43:20 2023: Inserted ≈60% of D-proof conclusions. [2444316 of 4073860] (ETC: Mon Oct 23 03:43:39 2023 ; 19 s 112.72 ms remaining ; 47 s 781.80 ms total)
Mon Oct 23 03:43:21 2023: Inserted ≈65% of D-proof conclusions. [2648009 of 4073860] (ETC: Mon Oct 23 03:43:38 2023 ; 16 s 294.38 ms remaining ; 46 s 555.37 ms total)
Mon Oct 23 03:43:23 2023: Inserted ≈70% of D-proof conclusions. [2851702 of 4073860] (ETC: Mon Oct 23 03:43:36 2023 ; 13 s 543.69 ms remaining ; 45 s 145.64 ms total)
Mon Oct 23 03:43:24 2023: Inserted ≈75% of D-proof conclusions. [3055395 of 4073860] (ETC: Mon Oct 23 03:43:35 2023 ; 10 s 913.20 ms remaining ; 43 s 652.82 ms total)
Mon Oct 23 03:43:25 2023: Inserted ≈80% of D-proof conclusions. [3259088 of 4073860] (ETC: Mon Oct 23 03:43:33 2023 ; 8 s 491.58 ms remaining ; 42 s 457.91 ms total)
Mon Oct 23 03:43:26 2023: Inserted ≈85% of D-proof conclusions. [3462781 of 4073860] (ETC: Mon Oct 23 03:43:32 2023 ; 6 s 216.37 ms remaining ; 41 s 442.44 ms total)
Mon Oct 23 03:43:27 2023: Inserted ≈90% of D-proof conclusions. [3666474 of 4073860] (ETC: Mon Oct 23 03:43:32 2023 ; 4 s 49.26 ms remaining ; 40 s 492.59 ms total)
Mon Oct 23 03:43:29 2023: Inserted ≈95% of D-proof conclusions. [3870167 of 4073860] (ETC: Mon Oct 23 03:43:31 2023 ; 1 s 987.84 ms remaining ; 39 s 756.88 ms total)
Mon Oct 23 03:43:31 2023: Inserted 100% of D-proof conclusions. [4073860 of 4073860] (ETC: Mon Oct 23 03:43:31 2023 ; 0.00 ms remaining ; 40 s 56.15 ms total)
40056.24 ms (40 s 56.24 ms) total insertion duration.
Reservable workloads: { 0:[57033, 85548], 1:[142582, 171097], 2:[228131, 256646], 3:[313680, 342195], 4:[399229, 427744], 5:[484779, 513294], 6:[570328, 598843], 7:[655877, 684392], 8:[741426, 769941], 9:[826975, 855490], 10:[912524, 941039], 11:[998074, 1026589], 12:[1083623, 1112138], 13:[1169172, 1197687], 14:[1254721, 1283236], 15:[1340270, 1368785], 16:[1425819, 1454334], 17:[1511369, 1539884], 18:[1596918, 1625433], 19:[1682467, 1710982], 20:[1768016, 1796531], 21:[1853565, 1882080], 22:[1939114, 1967629], 23:[2024664, 2053179] }
Mon Oct 23 03:46:45 2023: Removed ≈ 2% of redundant conclusions. [ 360 of approximately 18028] (ETC: Mon Oct 23 06:24:12 2023 ; 2 h 37 min 27 s 362.63 ms remaining ; 2 h 40 min 39 s 860.40 ms total)
Mon Oct 23 03:49:38 2023: Removed ≈ 4% of redundant conclusions. [ 721 of approximately 18028] (ETC: Mon Oct 23 06:15:53 2023 ; 2 h 26 min 14 s 705.24 ms remaining ; 2 h 32 min 20 s 254.58 ms total)
Mon Oct 23 03:53:05 2023: Removed ≈ 6% of redundant conclusions. [ 1081 of approximately 18028] (ETC: Mon Oct 23 06:22:46 2023 ; 2 h 29 min 40 s 985.83 ms remaining ; 2 h 39 min 13 s 856.88 ms total)
Mon Oct 23 03:56:31 2023: Removed ≈ 8% of redundant conclusions. [ 1442 of approximately 18028] (ETC: Mon Oct 23 06:25:41 2023 ; 2 h 29 min 10 s 826.80 ms remaining ; 2 h 42 min 9 s 18.78 ms total)
Mon Oct 23 03:59:45 2023: Removed ≈ 10% of redundant conclusions. [ 1802 of approximately 18028] (ETC: Mon Oct 23 06:25:38 2023 ; 2 h 25 min 53 s 344.03 ms remaining ; 2 h 42 min 5 s 458.29 ms total)
Mon Oct 23 04:03:13 2023: Removed ≈ 12% of redundant conclusions. [ 2163 of approximately 18028] (ETC: Mon Oct 23 06:27:34 2023 ; 2 h 24 min 20 s 891.55 ms remaining ; 2 h 44 min 1 s 698.88 ms total)
Mon Oct 23 04:07:00 2023: Removed ≈ 14% of redundant conclusions. [ 2523 of approximately 18028] (ETC: Mon Oct 23 06:31:07 2023 ; 2 h 24 min 7 s 359.05 ms remaining ; 2 h 47 min 34 s 472.04 ms total)
Mon Oct 23 04:10:21 2023: Removed ≈ 16% of redundant conclusions. [ 2884 of approximately 18028] (ETC: Mon Oct 23 06:31:09 2023 ; 2 h 20 min 47 s 937.64 ms remaining ; 2 h 47 min 36 s 749.86 ms total)
Mon Oct 23 04:13:46 2023: Removed ≈ 18% of redundant conclusions. [ 3245 of approximately 18028] (ETC: Mon Oct 23 06:31:26 2023 ; 2 h 17 min 40 s 371.84 ms remaining ; 2 h 47 min 53 s 596.93 ms total)
Mon Oct 23 04:17:07 2023: Removed ≈ 20% of redundant conclusions. [ 3605 of approximately 18028] (ETC: Mon Oct 23 06:31:29 2023 ; 2 h 14 min 21 s 613.18 ms remaining ; 2 h 47 min 56 s 597.27 ms total)
Mon Oct 23 04:20:44 2023: Removed ≈ 22% of redundant conclusions. [ 3966 of approximately 18028] (ETC: Mon Oct 23 06:32:38 2023 ; 2 h 11 min 53 s 333.05 ms remaining ; 2 h 49 min 5 s 183.35 ms total)
Mon Oct 23 04:24:05 2023: Removed ≈ 24% of redundant conclusions. [ 4326 of approximately 18028] (ETC: Mon Oct 23 06:32:29 2023 ; 2 h 8 min 24 s 307.27 ms remaining ; 2 h 48 min 56 s 713.72 ms total)
Mon Oct 23 04:27:35 2023: Removed ≈ 26% of redundant conclusions. [ 4687 of approximately 18028] (ETC: Mon Oct 23 06:32:56 2023 ; 2 h 5 min 20 s 891.90 ms remaining ; 2 h 49 min 23 s 154.13 ms total)
Mon Oct 23 04:31:13 2023: Removed ≈ 28% of redundant conclusions. [ 5047 of approximately 18028] (ETC: Mon Oct 23 06:33:51 2023 ; 2 h 2 min 38 s 83.14 ms remaining ; 2 h 50 min 18 s 898.61 ms total)
Mon Oct 23 04:34:17 2023: Removed ≈ 30% of redundant conclusions. [ 5408 of approximately 18028] (ETC: Mon Oct 23 06:32:43 2023 ; 1 h 58 min 25 s 710.98 ms remaining ; 2 h 49 min 10 s 693.94 ms total)
Mon Oct 23 04:37:38 2023: Removed ≈ 32% of redundant conclusions. [ 5768 of approximately 18028] (ETC: Mon Oct 23 06:32:37 2023 ; 1 h 54 min 58 s 767.53 ms remaining ; 2 h 49 min 4 s 451.97 ms total)
Mon Oct 23 04:40:55 2023: Removed ≈ 34% of redundant conclusions. [ 6129 of approximately 18028] (ETC: Mon Oct 23 06:32:20 2023 ; 1 h 51 min 24 s 352.05 ms remaining ; 2 h 48 min 47 s 363.53 ms total)
Mon Oct 23 04:44:32 2023: Removed ≈ 36% of redundant conclusions. [ 6490 of approximately 18028] (ETC: Mon Oct 23 06:32:58 2023 ; 1 h 48 min 26 s 97.68 ms remaining ; 2 h 49 min 25 s 707.14 ms total)
Mon Oct 23 04:48:10 2023: Removed ≈ 38% of redundant conclusions. [ 6850 of approximately 18028] (ETC: Mon Oct 23 06:33:38 2023 ; 1 h 45 min 27 s 858.06 ms remaining ; 2 h 50 min 5 s 638.31 ms total)
Mon Oct 23 04:51:20 2023: Removed ≈ 40% of redundant conclusions. [ 7211 of approximately 18028] (ETC: Mon Oct 23 06:33:02 2023 ; 1 h 41 min 41 s 549.98 ms remaining ; 2 h 49 min 29 s 61.94 ms total)
Mon Oct 23 04:54:54 2023: Removed ≈ 42% of redundant conclusions. [ 7571 of approximately 18028] (ETC: Mon Oct 23 06:33:27 2023 ; 1 h 38 min 33 s 230.38 ms remaining ; 2 h 49 min 54 s 483.82 ms total)
Mon Oct 23 04:58:17 2023: Removed ≈ 44% of redundant conclusions. [ 7932 of approximately 18028] (ETC: Mon Oct 23 06:33:25 2023 ; 1 h 35 min 8 s 0.03 ms remaining ; 2 h 49 min 52 s 534.13 ms total)
Mon Oct 23 05:01:40 2023: Removed ≈ 46% of redundant conclusions. [ 8292 of approximately 18028] (ETC: Mon Oct 23 06:33:25 2023 ; 1 h 31 min 44 s 207.92 ms remaining ; 2 h 49 min 52 s 56.32 ms total)
Mon Oct 23 05:05:09 2023: Removed ≈ 48% of redundant conclusions. [ 8653 of approximately 18028] (ETC: Mon Oct 23 06:33:34 2023 ; 1 h 28 min 24 s 858.91 ms remaining ; 2 h 50 min 1 s 172.96 ms total)
Mon Oct 23 05:08:32 2023: Removed ≈ 50% of redundant conclusions. [ 9014 of approximately 18028] (ETC: Mon Oct 23 06:33:31 2023 ; 1 h 24 min 59 s 299.95 ms remaining ; 2 h 49 min 58 s 599.90 ms total)
Mon Oct 23 05:12:06 2023: Removed ≈ 52% of redundant conclusions. [ 9374 of approximately 18028] (ETC: Mon Oct 23 06:33:51 2023 ; 1 h 21 min 45 s 265.28 ms remaining ; 2 h 50 min 18 s 641.37 ms total)
Mon Oct 23 05:15:28 2023: Removed ≈ 54% of redundant conclusions. [ 9735 of approximately 18028] (ETC: Mon Oct 23 06:33:46 2023 ; 1 h 18 min 18 s 307.22 ms remaining ; 2 h 50 min 13 s 563.54 ms total)
Mon Oct 23 05:19:00 2023: Removed ≈ 56% of redundant conclusions. [10095 of approximately 18028] (ETC: Mon Oct 23 06:34:02 2023 ; 1 h 15 min 1 s 181.32 ms remaining ; 2 h 50 min 29 s 80.65 ms total)
Mon Oct 23 05:22:16 2023: Removed ≈ 58% of redundant conclusions. [10456 of approximately 18028] (ETC: Mon Oct 23 06:33:45 2023 ; 1 h 11 min 29 s 546.05 ms remaining ; 2 h 50 min 12 s 881.16 ms total)
Mon Oct 23 05:25:32 2023: Removed ≈ 60% of redundant conclusions. [10816 of approximately 18028] (ETC: Mon Oct 23 06:33:33 2023 ; 1 h 8 min 534.00 ms remaining ; 2 h 50 min 203.40 ms total)
Mon Oct 23 05:29:12 2023: Removed ≈ 62% of redundant conclusions. [11177 of approximately 18028] (ETC: Mon Oct 23 06:33:57 2023 ; 1 h 4 min 45 s 561.53 ms remaining ; 2 h 50 min 24 s 624.61 ms total)
Mon Oct 23 05:32:09 2023: Removed ≈ 64% of redundant conclusions. [11537 of approximately 18028] (ETC: Mon Oct 23 06:33:16 2023 ; 1 h 1 min 6 s 566.99 ms remaining ; 2 h 49 min 43 s 464.74 ms total)
Mon Oct 23 05:36:13 2023: Removed ≈ 66% of redundant conclusions. [11898 of approximately 18028] (ETC: Mon Oct 23 06:34:16 2023 ; 58 min 3 s 192.39 ms remaining ; 2 h 50 min 43 s 881.31 ms total)
Mon Oct 23 05:40:31 2023: Removed ≈ 68% of redundant conclusions. [12259 of approximately 18028] (ETC: Mon Oct 23 06:35:34 2023 ; 55 min 3 s 54.17 ms remaining ; 2 h 52 min 1 s 972.71 ms total)
Mon Oct 23 05:43:50 2023: Removed ≈ 70% of redundant conclusions. [12619 of approximately 18028] (ETC: Mon Oct 23 06:35:23 2023 ; 51 min 33 s 499.41 ms remaining ; 2 h 51 min 50 s 520.86 ms total)
Mon Oct 23 05:47:15 2023: Removed ≈ 72% of redundant conclusions. [12980 of approximately 18028] (ETC: Mon Oct 23 06:35:21 2023 ; 48 min 6 s 513.89 ms remaining ; 2 h 51 min 48 s 651.42 ms total)
Mon Oct 23 05:50:47 2023: Removed ≈ 74% of redundant conclusions. [13340 of approximately 18028] (ETC: Mon Oct 23 06:35:31 2023 ; 44 min 43 s 116.57 ms remaining ; 2 h 51 min 58 s 94.18 ms total)
Mon Oct 23 05:54:08 2023: Removed ≈ 76% of redundant conclusions. [13701 of approximately 18028] (ETC: Mon Oct 23 06:35:22 2023 ; 41 min 14 s 449.88 ms remaining ; 2 h 51 min 49 s 540.65 ms total)
Mon Oct 23 05:57:47 2023: Removed ≈ 78% of redundant conclusions. [14061 of approximately 18028] (ETC: Mon Oct 23 06:35:40 2023 ; 37 min 52 s 491.71 ms remaining ; 2 h 52 min 7 s 320.52 ms total)
Mon Oct 23 06:01:22 2023: Removed ≈ 80% of redundant conclusions. [14422 of approximately 18028] (ETC: Mon Oct 23 06:35:49 2023 ; 34 min 27 s 591.68 ms remaining ; 2 h 52 min 16 s 811.64 ms total)
Mon Oct 23 06:04:40 2023: Removed ≈ 82% of redundant conclusions. [14782 of approximately 18028] (ETC: Mon Oct 23 06:35:39 2023 ; 30 min 59 s 343.39 ms remaining ; 2 h 52 min 6 s 630.52 ms total)
Mon Oct 23 06:08:08 2023: Removed ≈ 84% of redundant conclusions. [15143 of approximately 18028] (ETC: Mon Oct 23 06:35:41 2023 ; 27 min 32 s 899.63 ms remaining ; 2 h 52 min 8 s 760.70 ms total)
Mon Oct 23 06:11:40 2023: Removed ≈ 86% of redundant conclusions. [15504 of approximately 18028] (ETC: Mon Oct 23 06:35:47 2023 ; 24 min 6 s 844.74 ms remaining ; 2 h 52 min 14 s 277.70 ms total)
Mon Oct 23 06:15:45 2023: Removed ≈ 88% of redundant conclusions. [15864 of approximately 18028] (ETC: Mon Oct 23 06:36:31 2023 ; 20 min 45 s 778.30 ms remaining ; 2 h 52 min 58 s 415.49 ms total)
Mon Oct 23 06:20:06 2023: Removed ≈ 90% of redundant conclusions. [16225 of approximately 18028] (ETC: Mon Oct 23 06:37:30 2023 ; 17 min 23 s 891.54 ms remaining ; 2 h 53 min 57 s 757.47 ms total)
Mon Oct 23 06:23:42 2023: Removed ≈ 92% of redundant conclusions. [16585 of approximately 18028] (ETC: Mon Oct 23 06:37:38 2023 ; 13 min 56 s 89.04 ms remaining ; 2 h 54 min 5 s 608.58 ms total)
Mon Oct 23 06:27:27 2023: Removed ≈ 94% of redundant conclusions. [16946 of approximately 18028] (ETC: Mon Oct 23 06:37:55 2023 ; 10 min 27 s 951.51 ms remaining ; 2 h 54 min 22 s 763.30 ms total)
Mon Oct 23 06:31:41 2023: Removed ≈ 96% of redundant conclusions. [17306 of approximately 18028] (ETC: Mon Oct 23 06:38:41 2023 ; 7 min 872.95 ms remaining ; 2 h 55 min 8 s 999.42 ms total)
[Rank 14] Workload transfer approved. Starting to work on 0:[76044, 82380].
[Rank 19] Workload transfer approved. Starting to work on 0:[82381, 84492].
[Rank 15] Workload transfer approved. Starting to work on 6:[595676, 597787].
[Rank 23] Workload transfer approved. Starting to work on 7:[681225, 683336].
[Rank 12] Workload transfer approved. Starting to work on 10:[937872, 939983].
Mon Oct 23 06:36:32 2023: Removed ≈ 98% of redundant conclusions. [17667 of approximately 18028] (ETC: Mon Oct 23 06:40:04 2023 ; 3 min 32 s 93.39 ms remaining ; 2 h 56 min 31 s 744.41 ms total)
[Rank 17] Workload transfer approved. Starting to work on 0:[84493, 85548].
[Rank 2] Workload transfer approved. Starting to work on 1:[170042, 171097].
[Rank 19] Workload transfer approved. Starting to work on 7:[683337, 684392].
[Rank 6] Workload transfer approved. Starting to work on 9:[854435, 855490].
[Rank 21] Workload transfer approved. Starting to work on 13:[1196632, 1197687].
[Rank 3] Workload transfer approved. Starting to work on 16:[1453279, 1454334].
10983155.23 ms (3 h 3 min 3 s 155.23 ms) taken to detect 17950 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 2035230 representative and 17950 redundant condensed detachment proof strings.
[Copy] Removal count: { 49, 17950 }
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 1 on "ncm0114.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 2 on "ncm0116.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 3 on "ncm0117.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 4 on "ncm0119.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 5 on "ncm0121.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 6 on "ncm0122.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 7 on "ncm0123.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 8 on "ncm0124.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 9 on "ncm0125.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 10 on "ncm0128.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 11 on "ncm0129.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 12 on "ncm0130.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 13 on "ncm0131.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 14 on "ncm0132.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 15 on "ncm0134.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 16 on "ncm0136.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 17 on "ncm0137.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 18 on "ncm0138.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 19 on "ncm0139.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 20 on "ncm0140.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 21 on "ncm0141.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 22 on "ncm0142.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:46:34 2023: MPI-based D-proof representative filter complete. [rank 23 on "ncm0144.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
26623.35 ms (26 s 623.36 ms) taken to filter and order new representative proofs.
Mon Oct 23 06:47:01 2023: Starting to write 2035230 entries to data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs49.txt.
30846.00 ms (30 s 846.00 ms) taken to print and save 17543709434 bytes of representative condensed detachment proof strings to data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs49.txt.
Mon Oct 23 06:47:32 2023: MPI-based D-proof representative filter complete. [rank 0 on "ncm0113.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 202554, tid:23204300527488]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 200270, tid:23179364542336]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 109424, tid:22591423620992]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 131064, tid:23207789078400]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 162493, tid:22375476062080]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 85986, tid:22782196049792]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 166903, tid:22829834082176]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 186317, tid:22893723248512]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 154739, tid:22740978435968]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 63571, tid:22842480195456]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 161417, tid:23218173986688]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 217576, tid:22520543606656]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 172658, tid:23324746250112]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 94382, tid:23002790500224]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 95302, tid:23092832561024]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 82577, tid:22475653916544]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 212741, tid:23268658677632]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 188440, tid:22770325993344]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 111335, tid:22529070110592]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 92853, tid:22509334849408]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 166363, tid:22987896518528]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 97185, tid:23408963327872]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 268902, tid:22441279960960]
Mon Oct 23 06:47:41 2023: Process terminated. [pid: 231842, tid:22780543711104]