-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
81-71.log
136 lines (135 loc) · 14.9 KB
/
81-71.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
( This log file was generated by executing 'pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --iterate -u' (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 a CLAIX-2018-OPTANE MPI node
— 2-socket Intel Xeon Gold 6338, 32 cores each (64 cores total per node), 2.0 GHz, 3.20 GHz turbo mode, 512 GiB DDR4-3200 caching for 2 TiB non-volatile memory (NVM) (Intel Optane DC Persistent Memory DIMMs) —
running Linux, Rocky 8.8.
The job led to the following output:
$ sacct --format="JobID,Partition,AllocCPUS,State,ExitCode,Elapsed,MaxRSS"
JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS
------------ ---------- ---------- ---------- -------- ---------- ----------
40510376 optane_low 64 COMPLETED 0:0 02:03:04
40510376.ba+ 64 COMPLETED 0:0 02:03:04 666514256K
40510376.ex+ 64 COMPLETED 0:0 02:03:04 0
By 666514256 KiB = (666514256 / 1024^2) GiB = 635.6375274658203125 GiB, it used approximately 635.64 gibibytes of memory. )
Sat Nov 4 00:54:17 2023: Process started. [pid: 49448, tid:23169322391424]
Tasks:
1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true)
2. countNextIterationAmount(false, true)
[Main] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed]
(1) CCCCC0.1CN2N3.2.4CC4.0C3.0 - CCCCCpqCNrNsrtCCtpCsp - ((((0\imply1)\imply(\not2\imply\not3))\imply2)\imply4)\imply((4\imply0)\imply(3\imply0))
[Main] Calling countNextIterationAmount(false, true).
Sat Nov 4 00:54:17 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered]
0.04 ms taken to load initial representatives.
23.96 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:23169262167808]
12.10 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:23169260066560]
16.29 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:23169257965312]
19.15 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:23169255864064]
20.53 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:23169253762816]
10.88 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:23169251661568]
13.59 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:23169249560320]
23.47 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:23169247459072]
28.29 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:23169245357824]
13.48 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:23169243256576]
15.10 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:23169241155328]
23.82 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:23169239054080]
33.33 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:23169236952832]
13.79 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:23169234851584]
23.11 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:23169232750336]
32.77 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:23169230649088]
43.28 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:23169228547840]
34.08 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:23169226446592]
30.55 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:23169224345344]
40.69 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:23169222244096]
69.79 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:23169220142848]
229.57 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:23169218041600]
251.22 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:23169215940352]
194.75 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:23169213839104]
658.44 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:23169211737856]
2128.05 ms (2 s 128.05 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:23169209636608]
4725.77 ms (4 s 725.77 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:23169207535360]
2736.31 ms (2 s 736.31 ms) taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:23169205434112]
2912.18 ms (2 s 912.18 ms) taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:23169203332864]
4344.18 ms (4 s 344.18 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:23168194443008]
5118.70 ms (5 s 118.70 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:23168192341760]
5971.98 ms (5 s 971.98 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:23168190240512]
6375.16 ms (6 s 375.16 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:23168188139264]
7912.69 ms (7 s 912.69 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:23168186038016]
8203.24 ms (8 s 203.24 ms) total read duration.
Loaded 35 representative collections of sizes:
1 : 1
3 : 1
5 : 1
7 : 3
9 : 7
11 : 10
13 : 13
15 : 19
17 : 37
19 : 56
21 : 87
23 : 140
25 : 227
27 : 369
29 : 579
31 : 918
33 : 1499
35 : 2408
37 : 3881
39 : 6254
41 : 10109
43 : 16460
45 : 26753
47 : 43360
49 : 70709
51 : 115604
53 : 188634
55 : 308241
57 : 504870
59 : 827701
61 : 1357539
63 : 2227822
65 : 3660735
67 : 6021110
69 : 9907537
25303694 representatives in total.
52714.22 ms (52 s 714.22 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:23168186038016]
97186.57 ms (1 min 37 s 186.57 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:23168188139264]
132410.79 ms (2 min 12 s 410.79 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:23168190240512]
181381.77 ms (3 min 1 s 381.77 ms) taken to read 143296899 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. [tid:23168192341760]
229239.27 ms (3 min 49 s 239.27 ms) taken to read 263540491 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs79-unfiltered71+.txt. [tid:23168194443008]
314492.63 ms (5 min 14 s 492.63 ms) taken to read 489824924 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs81-unfiltered71+.txt. [tid:23169203332864]
314620.18 ms (5 min 14 s 620.19 ms) additional read duration.
Loaded 6 more representative collections of sizes:
71 : 23150845
73 : 45156728
75 : 80141395
77 : 143296899
79 : 263540491
81 : 489824924
1070414976 representatives in total.
Sat Nov 4 01:00:52 2023: Inserted ≈ 5% of D-proof conclusions. [ 53520748 of 1070414976] (ETC: Sat Nov 4 01:23:48 2023 ; 22 min 55 s 575.68 ms remaining ; 24 min 7 s 974.40 ms total)
Sat Nov 4 01:02:13 2023: Inserted ≈10% of D-proof conclusions. [ 107041497 of 1070414976] (ETC: Sat Nov 4 01:25:17 2023 ; 23 min 3 s 209.01 ms remaining ; 25 min 36 s 898.90 ms total)
Sat Nov 4 01:03:38 2023: Inserted ≈15% of D-proof conclusions. [ 160562246 of 1070414976] (ETC: Sat Nov 4 01:26:06 2023 ; 22 min 27 s 997.37 ms remaining ; 26 min 25 s 879.26 ms total)
Sat Nov 4 01:05:04 2023: Inserted ≈20% of D-proof conclusions. [ 214082995 of 1070414976] (ETC: Sat Nov 4 01:26:40 2023 ; 21 min 36 s 296.96 ms remaining ; 27 min 371.20 ms total)
Sat Nov 4 01:06:33 2023: Inserted ≈25% of D-proof conclusions. [ 267603744 of 1070414976] (ETC: Sat Nov 4 01:27:15 2023 ; 20 min 41 s 366.06 ms remaining ; 27 min 35 s 154.75 ms total)
Sat Nov 4 01:08:01 2023: Inserted ≈30% of D-proof conclusions. [ 321124492 of 1070414976] (ETC: Sat Nov 4 01:27:30 2023 ; 19 min 29 s 498.89 ms remaining ; 27 min 50 s 712.70 ms total)
Sat Nov 4 01:09:32 2023: Inserted ≈35% of D-proof conclusions. [ 374645241 of 1070414976] (ETC: Sat Nov 4 01:27:52 2023 ; 18 min 20 s 128.64 ms remaining ; 28 min 12 s 505.60 ms total)
Sat Nov 4 01:11:02 2023: Inserted ≈40% of D-proof conclusions. [ 428165990 of 1070414976] (ETC: Sat Nov 4 01:28:04 2023 ; 17 min 2 s 791.20 ms remaining ; 28 min 24 s 652.00 ms total)
Sat Nov 4 01:12:29 2023: Inserted ≈45% of D-proof conclusions. [ 481686739 of 1070414976] (ETC: Sat Nov 4 01:28:09 2023 ; 15 min 40 s 300.39 ms remaining ; 28 min 29 s 637.07 ms total)
Sat Nov 4 01:13:58 2023: Inserted ≈50% of D-proof conclusions. [ 535207488 of 1070414976] (ETC: Sat Nov 4 01:28:17 2023 ; 14 min 18 s 697.47 ms remaining ; 28 min 37 s 394.95 ms total)
Sat Nov 4 01:15:30 2023: Inserted ≈55% of D-proof conclusions. [ 588728236 of 1070414976] (ETC: Sat Nov 4 01:28:28 2023 ; 12 min 57 s 720.33 ms remaining ; 28 min 48 s 267.39 ms total)
Sat Nov 4 01:16:52 2023: Inserted ≈60% of D-proof conclusions. [ 642248985 of 1070414976] (ETC: Sat Nov 4 01:28:20 2023 ; 11 min 28 s 122.55 ms remaining ; 28 min 40 s 306.36 ms total)
Sat Nov 4 01:18:10 2023: Inserted ≈65% of D-proof conclusions. [ 695769734 of 1070414976] (ETC: Sat Nov 4 01:28:07 2023 ; 9 min 57 s 715.10 ms remaining ; 28 min 27 s 757.43 ms total)
Sat Nov 4 01:19:26 2023: Inserted ≈70% of D-proof conclusions. [ 749290483 of 1070414976] (ETC: Sat Nov 4 01:27:55 2023 ; 8 min 28 s 588.88 ms remaining ; 28 min 15 s 296.27 ms total)
Sat Nov 4 01:20:47 2023: Inserted ≈75% of D-proof conclusions. [ 802811232 of 1070414976] (ETC: Sat Nov 4 01:27:49 2023 ; 7 min 2 s 377.65 ms remaining ; 28 min 9 s 510.60 ms total)
Sat Nov 4 01:22:09 2023: Inserted ≈80% of D-proof conclusions. [ 856331980 of 1070414976] (ETC: Sat Nov 4 01:27:46 2023 ; 5 min 37 s 316.21 ms remaining ; 28 min 6 s 581.07 ms total)
Sat Nov 4 01:23:23 2023: Inserted ≈85% of D-proof conclusions. [ 909852729 of 1070414976] (ETC: Sat Nov 4 01:27:35 2023 ; 4 min 11 s 243.59 ms remaining ; 27 min 54 s 957.29 ms total)
Sat Nov 4 01:24:35 2023: Inserted ≈90% of D-proof conclusions. [ 963373478 of 1070414976] (ETC: Sat Nov 4 01:27:22 2023 ; 2 min 46 s 192.31 ms remaining ; 27 min 41 s 923.09 ms total)
Sat Nov 4 01:25:46 2023: Inserted ≈95% of D-proof conclusions. [1016894227 of 1070414976] (ETC: Sat Nov 4 01:27:08 2023 ; 1 min 22 s 423.26 ms remaining ; 27 min 28 s 465.28 ms total)
Sat Nov 4 01:26:57 2023: Inserted 100% of D-proof conclusions. [1070414976 of 1070414976] (ETC: Sat Nov 4 01:26:57 2023 ; 0.00 ms remaining ; 27 min 17 s 104.54 ms total)
1637105.91 ms (27 min 17 s 105.91 ms) total insertion duration.
Sat Nov 4 01:26:57 2023: Starting to iterate D-proof candidates of length 83.
3539867.80 ms (58 min 59 s 867.80 ms) taken to iterate 6668078395 condensed detachment proof strings of length 83.
[Copy] Next iteration count (unfiltered71+): { 83, 6668078395 }
Sat Nov 4 02:26:32 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered]
Sat Nov 4 02:56:34 2023: Process terminated. [pid: 49448, tid:23169322391424]