-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
dProofs29_6node_288cpu.log
152 lines (151 loc) · 18.8 KB
/
dProofs29_6node_288cpu.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
( This log file was generated by 'pmGenerator 1.1' (master branch), compiled by 'GCC: (GNU) 11.3.0'.
The run was executed on 6 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.7. Initialization and completion messages with rank numbers have been grouped and sorted for better readability.
Wall-clock time: 4.4330555… h
CPU utilization: 1276.72 core-h )
Sat May 20 18:58:32 2023: Process started. [pid: 2450761, tid:22413964543872]
Sat May 20 18:58:32 2023: Process started. [pid: 608599, tid:22503617062784]
Sat May 20 18:58:32 2023: Process started. [pid: 2325280, tid:22974053103488]
Sat May 20 18:58:32 2023: Process started. [pid: 2712734, tid:23451071190912]
Sat May 20 18:58:32 2023: Process started. [pid: 2462464, tid:23033916716928]
Sat May 20 18:58:33 2023: Process started. [pid: 2634279, tid:22415606060928]
Tasks:
1. mpi_filterDProofRepresentativeFile(29, true)
[Rank 0 ; pid: 2450761 ; 6 processes] Calling mpi_filterDProofRepresentativeFile(29, true).
[Rank 1 ; pid: 2462464 ; 6 processes] Calling mpi_filterDProofRepresentativeFile(29, true).
[Rank 2 ; pid: 2634279 ; 6 processes] Calling mpi_filterDProofRepresentativeFile(29, true).
[Rank 3 ; pid: 2712734 ; 6 processes] Calling mpi_filterDProofRepresentativeFile(29, true).
[Rank 4 ; pid: 608599 ; 6 processes] Calling mpi_filterDProofRepresentativeFile(29, true).
[Rank 5 ; pid: 2325280 ; 6 processes] Calling mpi_filterDProofRepresentativeFile(29, true).
Sat May 20 18:58:34 2023: MPI-based D-proof representative filter started. [rank 0 on "ncm0516.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 18:58:34 2023: MPI-based D-proof representative filter started. [rank 1 on "ncm0520.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 18:58:34 2023: MPI-based D-proof representative filter started. [rank 2 on "ncm0521.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 18:58:34 2023: MPI-based D-proof representative filter started. [rank 3 on "ncm0522.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 18:58:34 2023: MPI-based D-proof representative filter started. [rank 4 on "ncm0525.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 18:58:34 2023: MPI-based D-proof representative filter started. [rank 5 on "ncm0526.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
0.35 ms taken to load built-in representatives.
35.98 ms taken to read 5221 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs17.txt. [tid:22413798516480]
60.88 ms taken to read 15275 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs19.txt. [tid:22413796415232]
128.71 ms taken to read 44206 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs21.txt. [tid:22413794313984]
634.50 ms taken to read 129885 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs23.txt. [tid:22413792212736]
5962.41 ms (5 s 962.41 ms) taken to read 385789 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs25.txt. [tid:22413790111488]
497.19 ms taken to read 1149058 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs27.txt. [tid:22413788010240]
5967.92 ms (5 s 967.92 ms) total read duration.
Loaded 14 representative collections of sizes:
1 : 3
3 : 6
5 : 12
7 : 38
9 : 89
11 : 229
13 : 672
15 : 1844
17 : 5221
19 : 15275
21 : 44206
23 : 129885
25 : 385789
27 : 1149058
1732327 representatives in total.
1549.33 ms (1 s 549.33 ms) taken to read 4375266 condensed detachment proofs and conclusions from data/dProofs-withConclusions/dProofs29-unfiltered29+.txt. [tid:22413788010240]
1551.19 ms (1 s 551.19 ms) additional read duration.
Loaded 1 more representative collection of size:
29 : 4375266
6107593 representatives in total.
Sat May 20 18:58:41 2023: Representative collections were initialized successfully on all ranks.
Known removal count loaded from 29:926015.
Sat May 20 18:58:41 2023: Inserted 5% of D-proof conclusions. [ 305379 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 2 s 936.68 ms remaining ; 3 s 91.25 ms total)
Sat May 20 18:58:41 2023: Inserted 10% of D-proof conclusions. [ 610759 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 2 s 559.81 ms remaining ; 2 s 844.23 ms total)
Sat May 20 18:58:41 2023: Inserted 15% of D-proof conclusions. [ 916138 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 2 s 385.66 ms remaining ; 2 s 806.66 ms total)
Sat May 20 18:58:42 2023: Inserted 20% of D-proof conclusions. [1221518 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 2 s 394.00 ms remaining ; 2 s 992.50 ms total)
Sat May 20 18:58:42 2023: Inserted 25% of D-proof conclusions. [1526898 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 2 s 197.31 ms remaining ; 2 s 929.74 ms total)
Sat May 20 18:58:42 2023: Inserted 30% of D-proof conclusions. [1832277 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 2 s 15.32 ms remaining ; 2 s 879.02 ms total)
Sat May 20 18:58:42 2023: Inserted 35% of D-proof conclusions. [2137657 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 1 s 854.57 ms remaining ; 2 s 853.18 ms total)
Sat May 20 18:58:42 2023: Inserted 40% of D-proof conclusions. [2443037 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 1 s 686.03 ms remaining ; 2 s 810.05 ms total)
Sat May 20 18:58:42 2023: Inserted 45% of D-proof conclusions. [2748416 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 1 s 503.71 ms remaining ; 2 s 734.02 ms total)
Sat May 20 18:58:42 2023: Inserted 50% of D-proof conclusions. [3053796 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 1 s 332.06 ms remaining ; 2 s 664.12 ms total)
Sat May 20 18:58:42 2023: Inserted 55% of D-proof conclusions. [3359176 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 1 s 170.27 ms remaining ; 2 s 600.59 ms total)
Sat May 20 18:58:43 2023: Inserted 60% of D-proof conclusions. [3664555 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 1 s 15.95 ms remaining ; 2 s 539.88 ms total)
Sat May 20 18:58:43 2023: Inserted 65% of D-proof conclusions. [3969935 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 871.24 ms remaining ; 2 s 489.26 ms total)
Sat May 20 18:58:43 2023: Inserted 70% of D-proof conclusions. [4275315 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 756.77 ms remaining ; 2 s 522.57 ms total)
Sat May 20 18:58:43 2023: Inserted 75% of D-proof conclusions. [4580694 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 649.55 ms remaining ; 2 s 598.19 ms total)
Sat May 20 18:58:43 2023: Inserted 80% of D-proof conclusions. [4886074 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 527.27 ms remaining ; 2 s 636.33 ms total)
Sat May 20 18:58:43 2023: Inserted 85% of D-proof conclusions. [5191454 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 401.36 ms remaining ; 2 s 675.76 ms total)
Sat May 20 18:58:43 2023: Inserted 90% of D-proof conclusions. [5496833 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 264.59 ms remaining ; 2 s 645.87 ms total)
Sat May 20 18:58:44 2023: Inserted 95% of D-proof conclusions. [5802213 of 6107593] (ETC: Sat May 20 18:58:44 2023 ; 130.74 ms remaining ; 2 s 614.80 ms total)
2590.39 ms (2 s 590.39 ms) total insertion duration.
Reservable workloads: { 0:[486141, 729210], 1:[1215352, 1458421], 2:[1944563, 2187632], 3:[2673774, 2916843], 4:[3402985, 3646054], 5:[4132196, 4375265] }
Sat May 20 19:04:16 2023: Removed 2% of redundant conclusions. [ 18520 of 926015] (ETC: Sat May 20 23:35:10 2023 ; 4 h 30 min 54 s 71.60 ms remaining ; 4 h 36 min 25 s 781.86 ms total)
Sat May 20 19:09:39 2023: Removed 4% of redundant conclusions. [ 37040 of 926015] (ETC: Sat May 20 23:31:45 2023 ; 4 h 22 min 5 s 794.11 ms remaining ; 4 h 33 min 1 s 24.47 ms total)
Sat May 20 19:14:55 2023: Removed 6% of redundant conclusions. [ 55560 of 926015] (ETC: Sat May 20 23:28:19 2023 ; 4 h 13 min 24 s 704.49 ms remaining ; 4 h 29 min 35 s 200.81 ms total)
Sat May 20 19:20:04 2023: Removed 8% of redundant conclusions. [ 74081 of 926015] (ETC: Sat May 20 23:25:17 2023 ; 4 h 5 min 13 s 746.78 ms remaining ; 4 h 26 min 33 s 199.26 ms total)
Sat May 20 19:25:13 2023: Removed 10% of redundant conclusions. [ 92601 of 926015] (ETC: Sat May 20 23:23:35 2023 ; 3 h 58 min 21 s 636.76 ms remaining ; 4 h 24 min 50 s 697.98 ms total)
Sat May 20 19:30:22 2023: Removed 12% of redundant conclusions. [111121 of 926015] (ETC: Sat May 20 23:22:21 2023 ; 3 h 51 min 58 s 799.23 ms remaining ; 4 h 23 min 36 s 801.78 ms total)
Sat May 20 19:35:31 2023: Removed 14% of redundant conclusions. [129642 of 926015] (ETC: Sat May 20 23:21:29 2023 ; 3 h 45 min 57 s 464.98 ms remaining ; 4 h 22 min 44 s 492.18 ms total)
Sat May 20 19:40:37 2023: Removed 16% of redundant conclusions. [148162 of 926015] (ETC: Sat May 20 23:20:30 2023 ; 3 h 39 min 52 s 950.19 ms remaining ; 4 h 21 min 45 s 885.01 ms total)
Sat May 20 19:45:43 2023: Removed 18% of redundant conclusions. [166682 of 926015] (ETC: Sat May 20 23:19:45 2023 ; 3 h 34 min 1 s 645.65 ms remaining ; 4 h 21 min 529.03 ms total)
Sat May 20 19:50:54 2023: Removed 20% of redundant conclusions. [185203 of 926015] (ETC: Sat May 20 23:19:36 2023 ; 3 h 28 min 41 s 255.94 ms remaining ; 4 h 20 min 51 s 569.93 ms total)
Sat May 20 19:56:02 2023: Removed 22% of redundant conclusions. [203723 of 926015] (ETC: Sat May 20 23:19:12 2023 ; 3 h 23 min 10 s 17.68 ms remaining ; 4 h 20 min 28 s 221.30 ms total)
Sat May 20 20:01:10 2023: Removed 24% of redundant conclusions. [222243 of 926015] (ETC: Sat May 20 23:18:53 2023 ; 3 h 17 min 42 s 512.84 ms remaining ; 4 h 20 min 8 s 556.22 ms total)
Sat May 20 20:06:18 2023: Removed 26% of redundant conclusions. [240763 of 926015] (ETC: Sat May 20 23:18:38 2023 ; 3 h 12 min 19 s 176.59 ms remaining ; 4 h 19 min 53 s 461.39 ms total)
Sat May 20 20:11:25 2023: Removed 28% of redundant conclusions. [259284 of 926015] (ETC: Sat May 20 23:18:20 2023 ; 3 h 6 min 54 s 388.07 ms remaining ; 4 h 19 min 35 s 534.32 ms total)
Sat May 20 20:16:32 2023: Removed 30% of redundant conclusions. [277804 of 926015] (ETC: Sat May 20 23:18:03 2023 ; 3 h 1 min 31 s 6.26 ms remaining ; 4 h 19 min 18 s 568.37 ms total)
Sat May 20 20:21:38 2023: Removed 32% of redundant conclusions. [296324 of 926015] (ETC: Sat May 20 23:17:47 2023 ; 2 h 56 min 9 s 136.16 ms remaining ; 4 h 19 min 2 s 827.54 ms total)
Sat May 20 20:26:44 2023: Removed 34% of redundant conclusions. [314845 of 926015] (ETC: Sat May 20 23:17:34 2023 ; 2 h 50 min 49 s 912.00 ms remaining ; 4 h 18 min 50 s 167.16 ms total)
Sat May 20 20:31:50 2023: Removed 36% of redundant conclusions. [333365 of 926015] (ETC: Sat May 20 23:17:21 2023 ; 2 h 45 min 30 s 856.17 ms remaining ; 4 h 18 min 36 s 952.29 ms total)
Sat May 20 20:36:58 2023: Removed 38% of redundant conclusions. [351885 of 926015] (ETC: Sat May 20 23:17:14 2023 ; 2 h 40 min 16 s 153.89 ms remaining ; 4 h 18 min 29 s 906.72 ms total)
Sat May 20 20:42:07 2023: Removed 40% of redundant conclusions. [370406 of 926015] (ETC: Sat May 20 23:17:12 2023 ; 2 h 35 min 4 s 868.05 ms remaining ; 4 h 18 min 28 s 113.42 ms total)
Sat May 20 20:47:16 2023: Removed 42% of redundant conclusions. [388926 of 926015] (ETC: Sat May 20 23:17:09 2023 ; 2 h 29 min 52 s 662.99 ms remaining ; 4 h 18 min 24 s 582.70 ms total)
Sat May 20 20:52:26 2023: Removed 44% of redundant conclusions. [407446 of 926015] (ETC: Sat May 20 23:17:07 2023 ; 2 h 24 min 41 s 844.54 ms remaining ; 4 h 18 min 23 s 275.89 ms total)
Sat May 20 20:57:36 2023: Removed 46% of redundant conclusions. [425966 of 926015] (ETC: Sat May 20 23:17:09 2023 ; 2 h 19 min 32 s 536.95 ms remaining ; 4 h 18 min 24 s 670.16 ms total)
Sat May 20 21:02:50 2023: Removed 48% of redundant conclusions. [444487 of 926015] (ETC: Sat May 20 23:17:16 2023 ; 2 h 14 min 26 s 273.42 ms remaining ; 4 h 18 min 32 s 57.83 ms total)
Sat May 20 21:08:04 2023: Removed 50% of redundant conclusions. [463007 of 926015] (ETC: Sat May 20 23:17:24 2023 ; 2 h 9 min 20 s 16.22 ms remaining ; 4 h 18 min 40 s 15.68 ms total)
Sat May 20 21:13:16 2023: Removed 52% of redundant conclusions. [481527 of 926015] (ETC: Sat May 20 23:17:27 2023 ; 2 h 4 min 10 s 868.89 ms remaining ; 4 h 18 min 42 s 615.58 ms total)
Sat May 20 21:18:28 2023: Removed 54% of redundant conclusions. [500048 of 926015] (ETC: Sat May 20 23:17:30 2023 ; 1 h 59 min 1 s 899.03 ms remaining ; 4 h 18 min 45 s 863.80 ms total)
Sat May 20 21:23:40 2023: Removed 56% of redundant conclusions. [518568 of 926015] (ETC: Sat May 20 23:17:33 2023 ; 1 h 53 min 52 s 593.97 ms remaining ; 4 h 18 min 48 s 607.40 ms total)
Sat May 20 21:28:51 2023: Removed 58% of redundant conclusions. [537088 of 926015] (ETC: Sat May 20 23:17:33 2023 ; 1 h 48 min 41 s 965.73 ms remaining ; 4 h 18 min 48 s 461.89 ms total)
Sat May 20 21:34:03 2023: Removed 60% of redundant conclusions. [555609 of 926015] (ETC: Sat May 20 23:17:36 2023 ; 1 h 43 min 32 s 793.59 ms remaining ; 4 h 18 min 51 s 983.98 ms total)
Sat May 20 21:39:19 2023: Removed 62% of redundant conclusions. [574129 of 926015] (ETC: Sat May 20 23:17:44 2023 ; 1 h 38 min 25 s 19.25 ms remaining ; 4 h 18 min 59 s 511.08 ms total)
Sat May 20 21:44:30 2023: Removed 64% of redundant conclusions. [592649 of 926015] (ETC: Sat May 20 23:17:45 2023 ; 1 h 33 min 14 s 703.41 ms remaining ; 4 h 19 min 814.83 ms total)
Sat May 20 21:49:56 2023: Removed 66% of redundant conclusions. [611169 of 926015] (ETC: Sat May 20 23:18:07 2023 ; 1 h 28 min 11 s 393.51 ms remaining ; 4 h 19 min 22 s 877.61 ms total)
Sat May 20 21:55:07 2023: Removed 68% of redundant conclusions. [629690 of 926015] (ETC: Sat May 20 23:18:07 2023 ; 1 h 23 min 149.31 ms remaining ; 4 h 19 min 22 s 956.10 ms total)
Sat May 20 22:00:15 2023: Removed 70% of redundant conclusions. [648210 of 926015] (ETC: Sat May 20 23:18:02 2023 ; 1 h 17 min 47 s 358.57 ms remaining ; 4 h 19 min 17 s 833.91 ms total)
Sat May 20 22:05:27 2023: Removed 72% of redundant conclusions. [666730 of 926015] (ETC: Sat May 20 23:18:04 2023 ; 1 h 12 min 36 s 750.75 ms remaining ; 4 h 19 min 19 s 776.09 ms total)
Sat May 20 22:10:32 2023: Removed 74% of redundant conclusions. [685251 of 926015] (ETC: Sat May 20 23:17:56 2023 ; 1 h 7 min 23 s 474.82 ms remaining ; 4 h 19 min 11 s 819.77 ms total)
Sat May 20 22:15:42 2023: Removed 76% of redundant conclusions. [703771 of 926015] (ETC: Sat May 20 23:17:53 2023 ; 1 h 2 min 11 s 856.01 ms remaining ; 4 h 19 min 9 s 372.06 ms total)
Sat May 20 22:20:51 2023: Removed 78% of redundant conclusions. [722291 of 926015] (ETC: Sat May 20 23:17:52 2023 ; 57 min 529.07 ms remaining ; 4 h 19 min 7 s 805.97 ms total)
Sat May 20 22:26:01 2023: Removed 80% of redundant conclusions. [740812 of 926015] (ETC: Sat May 20 23:17:50 2023 ; 51 min 49 s 217.98 ms remaining ; 4 h 19 min 6 s 89.89 ms total)
Sat May 20 22:31:12 2023: Removed 82% of redundant conclusions. [759332 of 926015] (ETC: Sat May 20 23:17:51 2023 ; 46 min 38 s 440.86 ms remaining ; 4 h 19 min 6 s 865.70 ms total)
Sat May 20 22:36:22 2023: Removed 84% of redundant conclusions. [777852 of 926015] (ETC: Sat May 20 23:17:49 2023 ; 41 min 27 s 274.09 ms remaining ; 4 h 19 min 5 s 400.10 ms total)
Sat May 20 22:41:35 2023: Removed 86% of redundant conclusions. [796372 of 926015] (ETC: Sat May 20 23:17:52 2023 ; 36 min 16 s 669.03 ms remaining ; 4 h 19 min 7 s 528.01 ms total)
Sat May 20 22:46:55 2023: Removed 88% of redundant conclusions. [814893 of 926015] (ETC: Sat May 20 23:18:02 2023 ; 31 min 6 s 942.03 ms remaining ; 4 h 19 min 17 s 822.25 ms total)
Sat May 20 22:52:04 2023: Removed 90% of redundant conclusions. [833413 of 926015] (ETC: Sat May 20 23:17:59 2023 ; 25 min 55 s 525.20 ms remaining ; 4 h 19 min 15 s 168.05 ms total)
Sat May 20 22:57:14 2023: Removed 92% of redundant conclusions. [851933 of 926015] (ETC: Sat May 20 23:17:58 2023 ; 20 min 44 s 356.10 ms remaining ; 4 h 19 min 14 s 283.27 ms total)
Sat May 20 23:02:23 2023: Removed 94% of redundant conclusions. [870454 of 926015] (ETC: Sat May 20 23:17:56 2023 ; 15 min 33 s 122.90 ms remaining ; 4 h 19 min 12 s 20.28 ms total)
Sat May 20 23:07:34 2023: Removed 96% of redundant conclusions. [888974 of 926015] (ETC: Sat May 20 23:17:57 2023 ; 10 min 22 s 107.63 ms remaining ; 4 h 19 min 12 s 522.88 ms total)
[Rank 4] Workload transfer approved. Starting to work on 0:[702204, 720208].
Sat May 20 23:12:45 2023: Removed 98% of redundant conclusions. [907494 of 926015] (ETC: Sat May 20 23:17:57 2023 ; 5 min 11 s 60.59 ms remaining ; 4 h 19 min 12 s 441.62 ms total)
[Rank 1] Workload transfer approved. Starting to work on 0:[720209, 726210].
[Rank 5] Workload transfer approved. Starting to work on 3:[2907842, 2913843].
[Rank 2] Workload transfer approved. Starting to work on 0:[726211, 728210].
[Rank 2] Workload transfer approved. Starting to work on 3:[2913844, 2915843].
[Rank 1] Workload transfer approved. Starting to work on 0:[728211, 729210].
15940452.67 ms (4 h 25 min 40 s 452.67 ms) taken to detect 926015 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 3449251 representative and 926015 redundant condensed detachment proof strings.
[Copy] Removal count: { 29, 926015 }
Sat May 20 23:18:41 2023: MPI-based D-proof representative filter complete. [rank 1 on "ncm0520.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 23:18:41 2023: MPI-based D-proof representative filter complete. [rank 2 on "ncm0521.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 23:18:41 2023: MPI-based D-proof representative filter complete. [rank 3 on "ncm0522.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 23:18:41 2023: MPI-based D-proof representative filter complete. [rank 4 on "ncm0525.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 23:18:41 2023: MPI-based D-proof representative filter complete. [rank 5 on "ncm0526.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
945.01 ms taken to filter and order new representative proofs.
Sat May 20 23:24:25 2023: Starting to write 3449251 entries to data/dProofs-withConclusions/dProofs29.txt.
1459.06 ms (1 s 459.06 ms) taken to print and save 516720692 bytes of representative condensed detachment proof strings to data/dProofs-withConclusions/dProofs29.txt.
Sat May 20 23:24:26 2023: MPI-based D-proof representative filter complete. [rank 0 on "ncm0516.hpc.itc.rwth-aachen.de" ; 6 processes ; 48 local hardware thread contexts]
Sat May 20 23:24:31 2023: Process terminated. [pid: 2450761, tid:22413964543872]
Sat May 20 23:24:31 2023: Process terminated. [pid: 2634279, tid:22415606060928]
Sat May 20 23:24:31 2023: Process terminated. [pid: 608599, tid:22503617062784]
Sat May 20 23:24:31 2023: Process terminated. [pid: 2712734, tid:23451071190912]
Sat May 20 23:24:31 2023: Process terminated. [pid: 2462464, tid:23033916716928]
Sat May 20 23:24:31 2023: Process terminated. [pid: 2325280, tid:22974053103488]