-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
93-83.log
148 lines (147 loc) · 16.2 KB
/
93-83.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
( This log file was generated by executing 'pmGenerator -c -n -s CCCpqCCCNrNsrtCCtpCsp --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
------------ ---------- ---------- ---------- -------- ---------- ----------
40833947 optane_low 64 COMPLETED 0:0 01:54:06
40833947.ba+ 64 COMPLETED 0:0 01:54:06 682020752K
40833947.ex+ 64 COMPLETED 0:0 01:54:06 16K
By 682020752 KiB = (682020752 / 1024^2) GiB = 650.4256744384765625 GiB, it used approximately 650.43 gibibytes of memory. )
Sun Nov 19 12:23:44 2023: Process started. [pid: 268874, tid:23185404274560]
Tasks:
1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true)
2. countNextIterationAmount(false, true)
[Main] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69]
(1) CCC0.1CCCN2N3.2.4CC4.0C3.0 - CCCpqCCCNrNsrtCCtpCsp - ((0\imply1)\imply(((\not2\imply\not3)\imply2)\imply4))\imply((4\imply0)\imply(3\imply0))
[Main] Calling countNextIterationAmount(false, true).
Sun Nov 19 12:23:44 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
25.17 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:23185344050944]
6.42 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:23185341949696]
12.27 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:23185339848448]
15.26 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:23185337747200]
10.41 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:23185335645952]
12.35 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:23185240094464]
18.26 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:23185333544704]
14.56 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:23185331443456]
16.32 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:23185329342208]
20.17 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:23185327240960]
19.20 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:23185325139712]
26.32 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:23185323038464]
23.37 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:23185320937216]
25.90 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:23185318835968]
27.45 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:23185316734720]
34.75 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:23185314633472]
24.24 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:23185312532224]
30.16 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:23185310430976]
37.50 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:23185237993216]
162.49 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:23185235891968]
163.33 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:23185233790720]
317.18 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:23185231689472]
66.28 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:23185229588224]
177.69 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:23185227486976]
407.33 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:23185225385728]
427.59 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:23185223284480]
920.47 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:23185221183232]
996.29 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:23185219081984]
1085.75 ms (1 s 85.75 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:23185216980736]
2202.84 ms (2 s 202.84 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:23185214879488]
5703.49 ms (5 s 703.49 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:23185212778240]
7891.77 ms (7 s 891.77 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:23185210676992]
2933.77 ms (2 s 933.77 ms) taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:23185208575744]
3581.71 ms (3 s 581.71 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:23185206474496]
1470.16 ms (1 s 470.16 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:23185204373248]
5288.32 ms (5 s 288.32 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:23185202272000]
6563.95 ms (6 s 563.95 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:23185200170752]
7533.69 ms (7 s 533.69 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:23185198069504]
8106.81 ms (8 s 106.81 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:23185195968256]
9299.42 ms (9 s 299.42 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:23185193867008]
9625.33 ms (9 s 625.33 ms) total read duration.
Loaded 41 representative collections of sizes:
1 : 1
3 : 1
5 : 2
7 : 3
9 : 6
11 : 7
13 : 12
15 : 15
17 : 23
19 : 36
21 : 61
23 : 99
25 : 152
27 : 214
29 : 299
31 : 400
33 : 560
35 : 797
37 : 1162
39 : 1706
41 : 2502
43 : 3673
45 : 5333
47 : 7756
49 : 11285
51 : 16457
53 : 24156
55 : 35569
57 : 52769
59 : 78319
61 : 116867
63 : 174207
65 : 260535
67 : 389264
69 : 582969
71 : 872258
73 : 1307863
75 : 1959086
77 : 2940441
79 : 4409199
81 : 6623647
19879711 representatives in total.
105434.31 ms (1 min 45 s 434.31 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:23185193867008]
139190.20 ms (2 min 19 s 190.20 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:23185195968256]
180632.82 ms (3 min 632.82 ms) taken to read 62716073 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt. [tid:23185198069504]
228088.82 ms (3 min 48 s 88.82 ms) taken to read 101227436 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs89-unfiltered83+.txt. [tid:23185200170752]
276829.56 ms (4 min 36 s 829.56 ms) taken to read 157874085 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs91-unfiltered83+.txt. [tid:23185202272000]
331035.76 ms (5 min 31 s 35.76 ms) taken to read 251856137 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs93-unfiltered83+.txt. [tid:23185204373248]
331190.76 ms (5 min 31 s 190.76 ms) additional read duration.
Loaded 6 more representative collections of sizes:
83 : 22730041
85 : 38726684
87 : 62716073
89 : 101227436
91 : 157874085
93 : 251856137
655010167 representatives in total.
Sun Nov 19 12:30:33 2023: Inserted ≈ 5% of D-proof conclusions. [ 32750508 of 655010167] (ETC: Sun Nov 19 12:52:10 2023 ; 21 min 36 s 459.79 ms remaining ; 22 min 44 s 694.51 ms total)
Sun Nov 19 12:31:58 2023: Inserted ≈10% of D-proof conclusions. [ 65501016 of 655010167] (ETC: Sun Nov 19 12:54:58 2023 ; 22 min 59 s 660.40 ms remaining ; 25 min 32 s 956.00 ms total)
Sun Nov 19 12:33:28 2023: Inserted ≈15% of D-proof conclusions. [ 98251525 of 655010167] (ETC: Sun Nov 19 12:56:26 2023 ; 22 min 57 s 728.23 ms remaining ; 27 min 856.74 ms total)
Sun Nov 19 12:34:47 2023: Inserted ≈20% of D-proof conclusions. [131002033 of 655010167] (ETC: Sun Nov 19 12:56:14 2023 ; 21 min 27 s 153.37 ms remaining ; 26 min 48 s 941.71 ms total)
Sun Nov 19 12:35:57 2023: Inserted ≈25% of D-proof conclusions. [163752541 of 655010167] (ETC: Sun Nov 19 12:55:35 2023 ; 19 min 37 s 683.22 ms remaining ; 26 min 10 s 244.30 ms total)
Sun Nov 19 12:37:13 2023: Inserted ≈30% of D-proof conclusions. [196503050 of 655010167] (ETC: Sun Nov 19 12:55:26 2023 ; 18 min 12 s 568.40 ms remaining ; 26 min 812.00 ms total)
Sun Nov 19 12:38:31 2023: Inserted ≈35% of D-proof conclusions. [229253558 of 655010167] (ETC: Sun Nov 19 12:55:26 2023 ; 16 min 54 s 987.06 ms remaining ; 26 min 1 s 518.55 ms total)
Sun Nov 19 12:39:42 2023: Inserted ≈40% of D-proof conclusions. [262004066 of 655010167] (ETC: Sun Nov 19 12:55:09 2023 ; 15 min 26 s 284.36 ms remaining ; 25 min 43 s 807.26 ms total)
Sun Nov 19 12:40:51 2023: Inserted ≈45% of D-proof conclusions. [294754575 of 655010167] (ETC: Sun Nov 19 12:54:50 2023 ; 13 min 58 s 805.33 ms remaining ; 25 min 25 s 100.59 ms total)
Sun Nov 19 12:42:16 2023: Inserted ≈50% of D-proof conclusions. [327505083 of 655010167] (ETC: Sun Nov 19 12:55:07 2023 ; 12 min 51 s 197.74 ms remaining ; 25 min 42 s 395.48 ms total)
Sun Nov 19 12:43:52 2023: Inserted ≈55% of D-proof conclusions. [360255591 of 655010167] (ETC: Sun Nov 19 12:55:42 2023 ; 11 min 49 s 585.24 ms remaining ; 26 min 16 s 856.08 ms total)
Sun Nov 19 12:45:29 2023: Inserted ≈60% of D-proof conclusions. [393006100 of 655010167] (ETC: Sun Nov 19 12:56:12 2023 ; 10 min 42 s 964.82 ms remaining ; 26 min 47 s 412.06 ms total)
Sun Nov 19 12:46:39 2023: Inserted ≈65% of D-proof conclusions. [425756608 of 655010167] (ETC: Sun Nov 19 12:55:56 2023 ; 9 min 16 s 806.16 ms remaining ; 26 min 30 s 874.74 ms total)
Sun Nov 19 12:47:33 2023: Inserted ≈70% of D-proof conclusions. [458507116 of 655010167] (ETC: Sun Nov 19 12:55:19 2023 ; 7 min 46 s 189.32 ms remaining ; 25 min 53 s 964.41 ms total)
Sun Nov 19 12:48:31 2023: Inserted ≈75% of D-proof conclusions. [491257625 of 655010167] (ETC: Sun Nov 19 12:54:53 2023 ; 6 min 21 s 946.85 ms remaining ; 25 min 27 s 787.40 ms total)
Sun Nov 19 12:49:34 2023: Inserted ≈80% of D-proof conclusions. [524008133 of 655010167] (ETC: Sun Nov 19 12:54:36 2023 ; 5 min 2 s 281.67 ms remaining ; 25 min 11 s 408.35 ms total)
Sun Nov 19 12:50:45 2023: Inserted ≈85% of D-proof conclusions. [556758641 of 655010167] (ETC: Sun Nov 19 12:54:31 2023 ; 3 min 45 s 978.09 ms remaining ; 25 min 6 s 520.56 ms total)
Sun Nov 19 12:51:57 2023: Inserted ≈90% of D-proof conclusions. [589509150 of 655010167] (ETC: Sun Nov 19 12:54:27 2023 ; 2 min 30 s 196.79 ms remaining ; 25 min 1 s 967.86 ms total)
Sun Nov 19 12:53:23 2023: Inserted ≈95% of D-proof conclusions. [622259658 of 655010167] (ETC: Sun Nov 19 12:54:38 2023 ; 1 min 15 s 675.33 ms remaining ; 25 min 13 s 506.55 ms total)
Sun Nov 19 12:55:23 2023: Inserted 100% of D-proof conclusions. [655010167 of 655010167] (ETC: Sun Nov 19 12:55:23 2023 ; 0.00 ms remaining ; 25 min 57 s 934.45 ms total)
1557936.15 ms (25 min 57 s 936.15 ms) total insertion duration.
Sun Nov 19 12:55:23 2023: Starting to iterate D-proof candidates of length 95.
3422205.13 ms (57 min 2 s 205.13 ms) taken to iterate 4844444054 condensed detachment proof strings of length 95.
[Copy] Next iteration count (unfiltered83+): { 95, 4844444054 }
Sun Nov 19 13:52:25 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered]
Sun Nov 19 14:17:01 2023: Process terminated. [pid: 268874, tid:23185404274560]