forked from xamidi/pmGenerator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
dProofs23_24node_1152cpu.log
319 lines (318 loc) · 40.7 KB
/
dProofs23_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
( 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: 2.419444… h
CPU utilization: 2787.2 core-h )
Fri Oct 27 00:47:45 2023: Process started. [pid: 195180, tid:22615813879680]
Fri Oct 27 00:47:45 2023: Process started. [pid: 185639, tid:23222660892544]
Fri Oct 27 00:47:45 2023: Process started. [pid: 6742, tid:23265365071744]
Fri Oct 27 00:47:45 2023: Process started. [pid: 47687, tid:23305550317440]
Fri Oct 27 00:47:45 2023: Process started. [pid: 153457, tid:23363187156864]
Fri Oct 27 00:47:46 2023: Process started. [pid: 152309, tid:22366428624768]
Fri Oct 27 00:47:46 2023: Process started. [pid: 106400, tid:22718135322496]
Fri Oct 27 00:47:46 2023: Process started. [pid: 23955, tid:23265754683264]
Fri Oct 27 00:47:46 2023: Process started. [pid: 150078, tid:22486426503040]
Fri Oct 27 00:47:46 2023: Process started. [pid: 176373, tid:23206503413632]
Fri Oct 27 00:47:46 2023: Process started. [pid: 63746, tid:22766388647808]
Fri Oct 27 00:47:46 2023: Process started. [pid: 246332, tid:22736222459776]
Fri Oct 27 00:47:46 2023: Process started. [pid: 159799, tid:22735652059008]
Fri Oct 27 00:47:46 2023: Process started. [pid: 69068, tid:22749978830720]
Fri Oct 27 00:47:46 2023: Process started. [pid: 239394, tid:22867941705600]
Fri Oct 27 00:47:46 2023: Process started. [pid: 206513, tid:22612983666560]
Fri Oct 27 00:47:46 2023: Process started. [pid: 199614, tid:23064401663872]
Fri Oct 27 00:47:46 2023: Process started. [pid: 79285, tid:22822008141696]
Fri Oct 27 00:47:46 2023: Process started. [pid: 248389, tid:23234871269248]
Fri Oct 27 00:47:46 2023: Process started. [pid: 164029, tid:22521813096320]
Fri Oct 27 00:47:46 2023: Process started. [pid: 218692, tid:23407688628096]
Fri Oct 27 00:47:46 2023: Process started. [pid: 73797, tid:22412916524928]
Fri Oct 27 00:47:46 2023: Process started. [pid: 252063, tid:22647885965184]
Fri Oct 27 00:47:46 2023: Process started. [pid: 73209, tid:23135330285440]
Tasks:
1. resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true)
2. mpi_filterDProofRepresentativeFile(23, true)
[Rank 0 ; pid: 195180 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true).
Loaded 6 custom axioms. [SHA-512/224 hash: d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f]
(1) C0C1.0 - CpCqp - 0\imply(1\imply0)
(2) CC0C1.2CC0.1C0.2 - CCpCqrCCpqCpr - (0\imply(1\imply2))\imply((0\imply1)\imply(0\imply2))
(3) CCN0N1C1.0 - CCNpNqCqp - (\not0\imply\not1)\imply(1\imply0)
(4) CL0.0 - CLpp - \nece0\imply0
(5) CLC0.1CL0L1 - CLCpqCLpLq - \nece(0\imply1)\imply(\nece0\imply\nece1)
(6) CNLN0LNLN0 - CNLNpLNLNp - \not\nece\not0\imply\nece\not\nece\not0
Supports necessitation steps.
[Rank 1 ; pid: 63746 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 2 ; pid: 73797 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 3 ; pid: 218692 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 4 ; pid: 248389 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 5 ; pid: 47687 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 6 ; pid: 153457 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 7 ; pid: 23955 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 8 ; pid: 185639 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 9 ; pid: 246332 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 10 ; pid: 239394 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 11 ; pid: 69068 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 12 ; pid: 79285 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 13 ; pid: 152309 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 14 ; pid: 164029 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 15 ; pid: 159799 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 16 ; pid: 206513 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 17 ; pid: 252063 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 18 ; pid: 6742 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 19 ; pid: 73209 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 20 ; pid: 150078 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 21 ; pid: 199614 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 22 ; pid: 106400 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 23 ; pid: 176373 ; 24 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently.
[Rank 0 ; pid: 195180 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 1 ; pid: 63746 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 2 ; pid: 73797 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 3 ; pid: 218692 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 4 ; pid: 248389 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 5 ; pid: 47687 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 6 ; pid: 153457 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 7 ; pid: 23955 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 8 ; pid: 185639 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 9 ; pid: 246332 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 10 ; pid: 239394 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 11 ; pid: 69068 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 12 ; pid: 79285 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 13 ; pid: 152309 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 14 ; pid: 164029 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 15 ; pid: 159799 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 16 ; pid: 206513 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 17 ; pid: 252063 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 18 ; pid: 6742 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 19 ; pid: 73209 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 20 ; pid: 150078 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 21 ; pid: 199614 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 22 ; pid: 106400 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
[Rank 23 ; pid: 176373 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(23, true).
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 0 on "nrm082.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 1 on "nrm084.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 2 on "nrm085.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 3 on "nrm086.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 4 on "nrm087.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 5 on "nrm088.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 6 on "nrm089.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 7 on "nrm090.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 8 on "nrm091.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 9 on "nrm094.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 10 on "nrm095.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 11 on "nrm096.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 12 on "nrm097.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 13 on "nrm098.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 14 on "nrm099.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 15 on "nrm100.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 16 on "nrm101.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 17 on "nrm102.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 18 on "nrm103.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 19 on "nrm104.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 20 on "nrm105.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 21 on "nrm106.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 22 on "nrm107.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 00:47:47 2023: MPI-based D-proof representative filter started. [rank 23 on "nrm108.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
0.03 ms taken to load initial representatives.
14.86 ms taken to read 6 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs2.txt. [tid:22615489971968]
14.85 ms taken to read 17 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs3.txt. [tid:22614768568064]
18.43 ms taken to read 28 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs4.txt. [tid:22614766466816]
20.31 ms taken to read 56 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs5.txt. [tid:22614764365568]
21.40 ms taken to read 89 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs6.txt. [tid:22614762264320]
18.99 ms taken to read 203 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs7.txt. [tid:22614760163072]
26.26 ms taken to read 325 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs8.txt. [tid:22614758061824]
30.68 ms taken to read 666 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs9.txt. [tid:22614755960576]
28.11 ms taken to read 1174 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs10.txt. [tid:22614753859328]
27.11 ms taken to read 2340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs11.txt. [tid:22614751758080]
36.61 ms taken to read 4106 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs12.txt. [tid:22614680532736]
42.60 ms taken to read 8396 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs13.txt. [tid:22614678431488]
56.50 ms taken to read 15153 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs14.txt. [tid:22614676330240]
69.70 ms taken to read 30340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs15.txt. [tid:22614674228992]
122.02 ms taken to read 56725 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs16.txt. [tid:22614672127744]
230.11 ms taken to read 113539 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs17.txt. [tid:22614670026496]
591.83 ms taken to read 214468 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs18.txt. [tid:22614667925248]
1982.76 ms (1 s 982.76 ms) taken to read 431896 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs19.txt. [tid:22614665824000]
6555.34 ms (6 s 555.34 ms) taken to read 829754 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs20.txt. [tid:22614663722752]
998.59 ms taken to read 1666562 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs21.txt. [tid:22614661621504]
1357.97 ms (1 s 357.97 ms) taken to read 3250922 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs22.txt. [tid:22614659520256]
6569.11 ms (6 s 569.11 ms) total read duration.
Loaded 22 representative collections of sizes:
1 : 6
2 : 6
3 : 17
4 : 28
5 : 56
6 : 89
7 : 203
8 : 325
9 : 666
10 : 1174
11 : 2340
12 : 4106
13 : 8396
14 : 15153
15 : 30340
16 : 56725
17 : 113539
18 : 214468
19 : 431896
20 : 829754
21 : 1666562
22 : 3250922
6626771 representatives in total.
1868.25 ms (1 s 868.25 ms) taken to read 7247110 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs23-unfiltered23+.txt. [tid:22614659520256]
1869.95 ms (1 s 869.95 ms) additional read duration.
Loaded 1 more representative collection of size:
23 : 7247110
13873881 representatives in total.
Fri Oct 27 00:47:56 2023: Representative collections were initialized successfully on all ranks.
Estimated removal count set to 688396, based on entry 21:183513 and last known odd pair (19:48921, 21:183513) with 183513/48921 ≈ 3.75121 and 183513 * (183513/48921)^1 ≈ 688396.01.
Fri Oct 27 00:47:56 2023: Inserted ≈ 5% of D-proof conclusions. [ 693694 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 4 s 572.71 ms remaining ; 4 s 813.38 ms total)
Fri Oct 27 00:47:56 2023: Inserted ≈10% of D-proof conclusions. [ 1387388 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 4 s 171.19 ms remaining ; 4 s 634.65 ms total)
Fri Oct 27 00:47:56 2023: Inserted ≈15% of D-proof conclusions. [ 2081082 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 3 s 936.95 ms remaining ; 4 s 631.71 ms total)
Fri Oct 27 00:47:57 2023: Inserted ≈20% of D-proof conclusions. [ 2774776 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 3 s 859.28 ms remaining ; 4 s 824.10 ms total)
Fri Oct 27 00:47:57 2023: Inserted ≈25% of D-proof conclusions. [ 3468470 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 3 s 583.77 ms remaining ; 4 s 778.36 ms total)
Fri Oct 27 00:47:57 2023: Inserted ≈30% of D-proof conclusions. [ 4162164 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 3 s 302.05 ms remaining ; 4 s 717.22 ms total)
Fri Oct 27 00:47:57 2023: Inserted ≈35% of D-proof conclusions. [ 4855858 of 13873881] (ETC: Fri Oct 27 00:48:01 2023 ; 3 s 190.12 ms remaining ; 4 s 907.88 ms total)
Fri Oct 27 00:47:58 2023: Inserted ≈40% of D-proof conclusions. [ 5549552 of 13873881] (ETC: Fri Oct 27 00:48:01 2023 ; 2 s 943.41 ms remaining ; 4 s 905.69 ms total)
Fri Oct 27 00:47:58 2023: Inserted ≈45% of D-proof conclusions. [ 6243246 of 13873881] (ETC: Fri Oct 27 00:48:01 2023 ; 2 s 670.69 ms remaining ; 4 s 855.80 ms total)
Fri Oct 27 00:47:58 2023: Inserted ≈50% of D-proof conclusions. [ 6936940 of 13873881] (ETC: Fri Oct 27 00:48:01 2023 ; 2 s 417.34 ms remaining ; 4 s 834.69 ms total)
Fri Oct 27 00:47:58 2023: Inserted ≈55% of D-proof conclusions. [ 7630634 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 2 s 149.53 ms remaining ; 4 s 776.73 ms total)
Fri Oct 27 00:47:58 2023: Inserted ≈60% of D-proof conclusions. [ 8324328 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 1 s 887.41 ms remaining ; 4 s 718.54 ms total)
Fri Oct 27 00:47:59 2023: Inserted ≈65% of D-proof conclusions. [ 9018022 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 1 s 676.00 ms remaining ; 4 s 788.57 ms total)
Fri Oct 27 00:47:59 2023: Inserted ≈70% of D-proof conclusions. [ 9711716 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 1 s 441.63 ms remaining ; 4 s 805.44 ms total)
Fri Oct 27 00:47:59 2023: Inserted ≈75% of D-proof conclusions. [10405410 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 1 s 200.86 ms remaining ; 4 s 803.43 ms total)
Fri Oct 27 00:47:59 2023: Inserted ≈80% of D-proof conclusions. [11099104 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 957.42 ms remaining ; 4 s 787.12 ms total)
Fri Oct 27 00:48:00 2023: Inserted ≈85% of D-proof conclusions. [11792798 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 716.62 ms remaining ; 4 s 777.49 ms total)
Fri Oct 27 00:48:00 2023: Inserted ≈90% of D-proof conclusions. [12486492 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 475.00 ms remaining ; 4 s 750.00 ms total)
Fri Oct 27 00:48:00 2023: Inserted ≈95% of D-proof conclusions. [13180186 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 236.01 ms remaining ; 4 s 720.14 ms total)
Fri Oct 27 00:48:00 2023: Inserted 100% of D-proof conclusions. [13873881 of 13873881] (ETC: Fri Oct 27 00:48:00 2023 ; 0.00 ms remaining ; 4 s 692.97 ms total)
4693.06 ms (4 s 693.06 ms) total insertion duration.
Reservable workloads: { 0:[201308, 301961], 1:[503271, 603924], 2:[805234, 905887], 3:[1107197, 1207850], 4:[1409160, 1509813], 5:[1711123, 1811776], 6:[2013086, 2113739], 7:[2315049, 2415702], 8:[2617012, 2717665], 9:[2918975, 3019628], 10:[3220938, 3321591], 11:[3522901, 3623554], 12:[3824863, 3925516], 13:[4126826, 4227479], 14:[4428789, 4529442], 15:[4730752, 4831405], 16:[5032715, 5133368], 17:[5334678, 5435331], 18:[5636641, 5737294], 19:[5938604, 6039257], 20:[6240567, 6341220], 21:[6542530, 6643183], 22:[6844493, 6945146], 23:[7146456, 7247109] }
Fri Oct 27 00:51:08 2023: Removed ≈ 2% of redundant conclusions. [ 13767 of approximately 688396] (ETC: Fri Oct 27 03:23:07 2023 ; 2 h 31 min 59 s 308.66 ms remaining ; 2 h 35 min 5 s 404.31 ms total)
Fri Oct 27 00:54:11 2023: Removed ≈ 4% of redundant conclusions. [ 27535 of approximately 688396] (ETC: Fri Oct 27 03:21:55 2023 ; 2 h 27 min 44 s 433.09 ms remaining ; 2 h 33 min 53 s 772.73 ms total)
Fri Oct 27 00:57:16 2023: Removed ≈ 6% of redundant conclusions. [ 41303 of approximately 688396] (ETC: Fri Oct 27 03:22:08 2023 ; 2 h 24 min 51 s 729.86 ms remaining ; 2 h 34 min 6 s 510.27 ms total)
Fri Oct 27 01:00:18 2023: Removed ≈ 8% of redundant conclusions. [ 55071 of approximately 688396] (ETC: Fri Oct 27 03:21:23 2023 ; 2 h 21 min 4 s 962.16 ms remaining ; 2 h 33 min 21 s 35.95 ms total)
Fri Oct 27 01:03:17 2023: Removed ≈ 10% of redundant conclusions. [ 68839 of approximately 688396] (ETC: Fri Oct 27 03:20:33 2023 ; 2 h 17 min 16 s 459.17 ms remaining ; 2 h 32 min 31 s 612.43 ms total)
Fri Oct 27 01:06:14 2023: Removed ≈ 12% of redundant conclusions. [ 82607 of approximately 688396] (ETC: Fri Oct 27 03:19:44 2023 ; 2 h 13 min 29 s 876.83 ms remaining ; 2 h 31 min 42 s 124.95 ms total)
Fri Oct 27 01:09:09 2023: Removed ≈ 14% of redundant conclusions. [ 96375 of approximately 688396] (ETC: Fri Oct 27 03:18:55 2023 ; 2 h 9 min 46 s 89.43 ms remaining ; 2 h 30 min 53 s 585.63 ms total)
Fri Oct 27 01:12:02 2023: Removed ≈ 16% of redundant conclusions. [110143 of approximately 688396] (ETC: Fri Oct 27 03:18:03 2023 ; 2 h 6 min 1 s 379.38 ms remaining ; 2 h 30 min 1 s 636.52 ms total)
Fri Oct 27 01:14:55 2023: Removed ≈ 18% of redundant conclusions. [123911 of approximately 688396] (ETC: Fri Oct 27 03:17:28 2023 ; 2 h 2 min 32 s 92.72 ms remaining ; 2 h 29 min 25 s 962.29 ms total)
Fri Oct 27 01:17:47 2023: Removed ≈ 20% of redundant conclusions. [137679 of approximately 688396] (ETC: Fri Oct 27 03:16:49 2023 ; 1 h 59 min 2 s 159.10 ms remaining ; 2 h 28 min 47 s 695.64 ms total)
Fri Oct 27 01:20:40 2023: Removed ≈ 22% of redundant conclusions. [151447 of approximately 688396] (ETC: Fri Oct 27 03:16:25 2023 ; 1 h 55 min 44 s 719.89 ms remaining ; 2 h 28 min 23 s 485.05 ms total)
Fri Oct 27 01:23:33 2023: Removed ≈ 24% of redundant conclusions. [165215 of approximately 688396] (ETC: Fri Oct 27 03:16:03 2023 ; 1 h 52 min 30 s 64.10 ms remaining ; 2 h 28 min 1 s 662.61 ms total)
Fri Oct 27 01:26:26 2023: Removed ≈ 26% of redundant conclusions. [178982 of approximately 688396] (ETC: Fri Oct 27 03:15:45 2023 ; 1 h 49 min 18 s 854.04 ms remaining ; 2 h 27 min 43 s 299.57 ms total)
Fri Oct 27 01:29:18 2023: Removed ≈ 28% of redundant conclusions. [192750 of approximately 688396] (ETC: Fri Oct 27 03:15:27 2023 ; 1 h 46 min 8 s 888.19 ms remaining ; 2 h 27 min 25 s 662.34 ms total)
Fri Oct 27 01:32:10 2023: Removed ≈ 30% of redundant conclusions. [206518 of approximately 688396] (ETC: Fri Oct 27 03:15:11 2023 ; 1 h 43 min 609.56 ms remaining ; 2 h 27 min 9 s 427.57 ms total)
Fri Oct 27 01:35:01 2023: Removed ≈ 32% of redundant conclusions. [220286 of approximately 688396] (ETC: Fri Oct 27 03:14:51 2023 ; 1 h 39 min 50 s 596.82 ms remaining ; 2 h 26 min 49 s 687.65 ms total)
Fri Oct 27 01:37:50 2023: Removed ≈ 34% of redundant conclusions. [234054 of approximately 688396] (ETC: Fri Oct 27 03:14:32 2023 ; 1 h 36 min 41 s 590.85 ms remaining ; 2 h 26 min 30 s 276.78 ms total)
Fri Oct 27 01:40:39 2023: Removed ≈ 36% of redundant conclusions. [247822 of approximately 688396] (ETC: Fri Oct 27 03:14:12 2023 ; 1 h 33 min 32 s 990.79 ms remaining ; 2 h 26 min 10 s 286.96 ms total)
Fri Oct 27 01:43:26 2023: Removed ≈ 38% of redundant conclusions. [261590 of approximately 688396] (ETC: Fri Oct 27 03:13:50 2023 ; 1 h 30 min 23 s 850.31 ms remaining ; 2 h 25 min 48 s 135.81 ms total)
Fri Oct 27 01:46:09 2023: Removed ≈ 40% of redundant conclusions. [275358 of approximately 688396] (ETC: Fri Oct 27 03:13:21 2023 ; 1 h 27 min 11 s 718.18 ms remaining ; 2 h 25 min 19 s 521.86 ms total)
Fri Oct 27 01:48:55 2023: Removed ≈ 42% of redundant conclusions. [289126 of approximately 688396] (ETC: Fri Oct 27 03:12:59 2023 ; 1 h 24 min 4 s 745.09 ms remaining ; 2 h 24 min 57 s 829.39 ms total)
Fri Oct 27 01:51:37 2023: Removed ≈ 44% of redundant conclusions. [302894 of approximately 688396] (ETC: Fri Oct 27 03:12:33 2023 ; 1 h 20 min 55 s 817.44 ms remaining ; 2 h 24 min 31 s 97.17 ms total)
Fri Oct 27 01:54:20 2023: Removed ≈ 46% of redundant conclusions. [316662 of approximately 688396] (ETC: Fri Oct 27 03:12:11 2023 ; 1 h 17 min 50 s 577.34 ms remaining ; 2 h 24 min 9 s 213.57 ms total)
Fri Oct 27 01:57:04 2023: Removed ≈ 48% of redundant conclusions. [330430 of approximately 688396] (ETC: Fri Oct 27 03:11:51 2023 ; 1 h 14 min 47 s 421.24 ms remaining ; 2 h 23 min 49 s 654.30 ms total)
Fri Oct 27 01:59:47 2023: Removed ≈ 50% of redundant conclusions. [344198 of approximately 688396] (ETC: Fri Oct 27 03:11:32 2023 ; 1 h 11 min 45 s 343.55 ms remaining ; 2 h 23 min 30 s 687.10 ms total)
Fri Oct 27 02:02:32 2023: Removed ≈ 52% of redundant conclusions. [357965 of approximately 688396] (ETC: Fri Oct 27 03:11:18 2023 ; 1 h 8 min 46 s 163.54 ms remaining ; 2 h 23 min 16 s 150.11 ms total)
Fri Oct 27 02:05:16 2023: Removed ≈ 54% of redundant conclusions. [371733 of approximately 688396] (ETC: Fri Oct 27 03:11:04 2023 ; 1 h 5 min 47 s 896.88 ms remaining ; 2 h 23 min 2 s 361.76 ms total)
Fri Oct 27 02:08:00 2023: Removed ≈ 56% of redundant conclusions. [385501 of approximately 688396] (ETC: Fri Oct 27 03:10:51 2023 ; 1 h 2 min 50 s 468.66 ms remaining ; 2 h 22 min 49 s 225.44 ms total)
Fri Oct 27 02:10:45 2023: Removed ≈ 58% of redundant conclusions. [399269 of approximately 688396] (ETC: Fri Oct 27 03:10:38 2023 ; 59 min 53 s 897.79 ms remaining ; 2 h 22 min 36 s 879.38 ms total)
Fri Oct 27 02:13:28 2023: Removed ≈ 60% of redundant conclusions. [413037 of approximately 688396] (ETC: Fri Oct 27 03:10:26 2023 ; 56 min 57 s 942.54 ms remaining ; 2 h 22 min 24 s 837.74 ms total)
Fri Oct 27 02:16:14 2023: Removed ≈ 62% of redundant conclusions. [426805 of approximately 688396] (ETC: Fri Oct 27 03:10:17 2023 ; 54 min 3 s 616.84 ms remaining ; 2 h 22 min 15 s 816.82 ms total)
Fri Oct 27 02:18:58 2023: Removed ≈ 64% of redundant conclusions. [440573 of approximately 688396] (ETC: Fri Oct 27 03:10:08 2023 ; 51 min 9 s 489.71 ms remaining ; 2 h 22 min 6 s 345.17 ms total)
Fri Oct 27 02:21:44 2023: Removed ≈ 66% of redundant conclusions. [454341 of approximately 688396] (ETC: Fri Oct 27 03:10:00 2023 ; 48 min 16 s 377.78 ms remaining ; 2 h 21 min 58 s 745.07 ms total)
Fri Oct 27 02:24:29 2023: Removed ≈ 68% of redundant conclusions. [468109 of approximately 688396] (ETC: Fri Oct 27 03:09:53 2023 ; 45 min 23 s 702.77 ms remaining ; 2 h 21 min 51 s 560.35 ms total)
Fri Oct 27 02:27:14 2023: Removed ≈ 70% of redundant conclusions. [481877 of approximately 688396] (ETC: Fri Oct 27 03:09:45 2023 ; 42 min 31 s 33.23 ms remaining ; 2 h 21 min 43 s 435.88 ms total)
Fri Oct 27 02:29:58 2023: Removed ≈ 72% of redundant conclusions. [495645 of approximately 688396] (ETC: Fri Oct 27 03:09:36 2023 ; 39 min 38 s 433.72 ms remaining ; 2 h 21 min 34 s 400.87 ms total)
Fri Oct 27 02:32:40 2023: Removed ≈ 74% of redundant conclusions. [509413 of approximately 688396] (ETC: Fri Oct 27 03:09:26 2023 ; 36 min 46 s 32.09 ms remaining ; 2 h 21 min 24 s 736.92 ms total)
Fri Oct 27 02:35:24 2023: Removed ≈ 76% of redundant conclusions. [523180 of approximately 688396] (ETC: Fri Oct 27 03:09:18 2023 ; 33 min 54 s 409.51 ms remaining ; 2 h 21 min 16 s 657.03 ms total)
Fri Oct 27 02:38:07 2023: Removed ≈ 78% of redundant conclusions. [536948 of approximately 688396] (ETC: Fri Oct 27 03:09:10 2023 ; 31 min 3 s 119.04 ms remaining ; 2 h 21 min 8 s 673.71 ms total)
Fri Oct 27 02:40:50 2023: Removed ≈ 80% of redundant conclusions. [550716 of approximately 688396] (ETC: Fri Oct 27 03:09:02 2023 ; 28 min 12 s 17.86 ms remaining ; 2 h 21 min 40.12 ms total)
Fri Oct 27 02:43:32 2023: Removed ≈ 82% of redundant conclusions. [564484 of approximately 688396] (ETC: Fri Oct 27 03:08:53 2023 ; 25 min 21 s 318.28 ms remaining ; 2 h 20 min 51 s 719.11 ms total)
Fri Oct 27 02:46:17 2023: Removed ≈ 84% of redundant conclusions. [578252 of approximately 688396] (ETC: Fri Oct 27 03:08:49 2023 ; 22 min 31 s 558.96 ms remaining ; 2 h 20 min 47 s 194.39 ms total)
Fri Oct 27 02:49:00 2023: Removed ≈ 86% of redundant conclusions. [592020 of approximately 688396] (ETC: Fri Oct 27 03:08:42 2023 ; 19 min 41 s 620.19 ms remaining ; 2 h 20 min 40 s 95.14 ms total)
Fri Oct 27 02:51:45 2023: Removed ≈ 88% of redundant conclusions. [605788 of approximately 688396] (ETC: Fri Oct 27 03:08:37 2023 ; 16 min 52 s 267.65 ms remaining ; 2 h 20 min 35 s 514.77 ms total)
Fri Oct 27 02:54:29 2023: Removed ≈ 90% of redundant conclusions. [619556 of approximately 688396] (ETC: Fri Oct 27 03:08:32 2023 ; 14 min 3 s 23.68 ms remaining ; 2 h 20 min 30 s 187.87 ms total)
Fri Oct 27 02:57:14 2023: Removed ≈ 92% of redundant conclusions. [633324 of approximately 688396] (ETC: Fri Oct 27 03:08:28 2023 ; 11 min 14 s 124.06 ms remaining ; 2 h 20 min 26 s 501.85 ms total)
Fri Oct 27 02:59:59 2023: Removed ≈ 94% of redundant conclusions. [647092 of approximately 688396] (ETC: Fri Oct 27 03:08:25 2023 ; 8 min 25 s 404.10 ms remaining ; 2 h 20 min 23 s 352.73 ms total)
Fri Oct 27 03:02:42 2023: Removed ≈ 96% of redundant conclusions. [660860 of approximately 688396] (ETC: Fri Oct 27 03:08:19 2023 ; 5 min 36 s 694.44 ms remaining ; 2 h 20 min 17 s 312.08 ms total)
[Rank 7] Workload transfer approved. Starting to work on 0:[290779, 298234].
Fri Oct 27 03:05:27 2023: Removed ≈ 98% of redundant conclusions. [674628 of approximately 688396] (ETC: Fri Oct 27 03:08:15 2023 ; 2 min 48 s 275.37 ms remaining ; 2 h 20 min 13 s 719.56 ms total)
[Rank 4] Workload transfer approved. Starting to work on 1:[592742, 600197].
[Rank 5] Workload transfer approved. Starting to work on 2:[894705, 902160].
[Rank 15] Workload transfer approved. Starting to work on 12:[3914334, 3921789].
[Rank 10] Workload transfer approved. Starting to work on 18:[5726112, 5733567].
[Rank 20] Workload transfer approved. Starting to work on 0:[298235, 300719].
[Rank 7] Workload transfer approved. Starting to work on 3:[1204124, 1206608].
Fri Oct 27 03:08:12 2023: Removed ≈100% of redundant conclusions. [688396 of approximately 688396] (ETC: Fri Oct 27 03:08:12 2023 ; 0.00 ms remaining ; 2 h 20 min 10 s 116.64 ms total)
[Rank 20] Workload transfer approved. Starting to work on 6:[2110013, 2112497].
[Rank 16] Workload transfer approved. Starting to work on 9:[3015902, 3018386].
[Rank 7] Workload transfer approved. Starting to work on 11:[3619828, 3622312].
[Rank 4] Workload transfer approved. Starting to work on 13:[4223753, 4226237].
[Rank 2] Workload transfer approved. Starting to work on 19:[6035531, 6038015].
[Rank 20] Workload transfer approved. Starting to work on 22:[6941420, 6943904].
[Rank 18] Workload transfer approved. Starting to work on 0:[300720, 301547].
[Rank 17] Workload transfer approved. Starting to work on 3:[1206609, 1207436].
[Rank 1] Workload transfer approved. Starting to work on 9:[3018387, 3019214].
[Rank 5] Workload transfer approved. Starting to work on 14:[4528201, 4529028].
[Rank 16] Workload transfer approved. Starting to work on 21:[6641942, 6642769].
[Rank 11] Workload transfer approved. Starting to work on 23:[7245868, 7246695].
[Rank 6] Workload transfer approved. Starting to work on 0:[301548, 301961].
[Rank 18] Workload transfer approved. Starting to work on 8:[2717252, 2717665].
[Rank 13] Workload transfer approved. Starting to work on 9:[3019215, 3019628].
[Rank 8] Workload transfer approved. Starting to work on 19:[6038844, 6039257].
[Rank 9] Workload transfer approved. Starting to work on 22:[6944733, 6945146].
[Rank 19] Workload transfer approved. Starting to work on 23:[7246696, 7247109].
8682926.43 ms (2 h 24 min 42 s 926.43 ms) taken to detect 699371 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 6547739 representative and 699371 redundant condensed detachment proof strings.
[Copy] Removal count: { 23, 699371 }
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 1 on "nrm084.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 2 on "nrm085.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 3 on "nrm086.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 4 on "nrm087.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 5 on "nrm088.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 6 on "nrm089.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 7 on "nrm090.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 8 on "nrm091.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 9 on "nrm094.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 10 on "nrm095.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 11 on "nrm096.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 12 on "nrm097.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 13 on "nrm098.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 14 on "nrm099.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 15 on "nrm100.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 16 on "nrm101.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 17 on "nrm102.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 18 on "nrm103.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 19 on "nrm104.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 20 on "nrm105.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 21 on "nrm106.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 22 on "nrm107.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:10:38 2023: MPI-based D-proof representative filter complete. [rank 23 on "nrm108.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
1380.73 ms (1 s 380.73 ms) taken to filter and order new representative proofs.
Fri Oct 27 03:12:45 2023: Starting to write 6547739 entries to data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs23.txt.
1578.94 ms (1 s 578.94 ms) taken to print and save 486227545 bytes of representative condensed detachment proof strings to data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs23.txt.
Fri Oct 27 03:12:47 2023: MPI-based D-proof representative filter complete. [rank 0 on "nrm082.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 63746, tid:22766388647808]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 150078, tid:22486426503040]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 206513, tid:22612983666560]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 248389, tid:23234871269248]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 6742, tid:23265365071744]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 47687, tid:23305550317440]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 185639, tid:23222660892544]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 239394, tid:22867941705600]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 23955, tid:23265754683264]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 159799, tid:22735652059008]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 69068, tid:22749978830720]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 246332, tid:22736222459776]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 252063, tid:22647885965184]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 73209, tid:23135330285440]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 153457, tid:23363187156864]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 152309, tid:22366428624768]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 73797, tid:22412916524928]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 195180, tid:22615813879680]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 218692, tid:23407688628096]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 79285, tid:22822008141696]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 199614, tid:23064401663872]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 176373, tid:23206503413632]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 106400, tid:22718135322496]
Fri Oct 27 03:12:55 2023: Process terminated. [pid: 164029, tid:22521813096320]