-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
83-71.log
138 lines (137 loc) · 15.2 KB
/
83-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
137
138
( 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%11"
JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS
------------ ---------- ---------- ---------- -------- ---------- -----------
40551987 optane_low 64 COMPLETED 0:0 03:58:23
40551987.ba+ 64 COMPLETED 0:0 03:58:23 1254916708K
40551987.ex+ 64 COMPLETED 0:0 03:58:23 16K
By 1254916708 KiB = (1254916708 / 1024^2) GiB = 1196.781833648681640625 GiB, it used approximately 1196.78 gibibytes of memory. )
Tue Nov 7 20:18:44 2023: Process started. [pid: 149312, tid:22361510446976]
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).
Tue Nov 7 20:18:44 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered]
0.04 ms taken to load initial representatives.
14.08 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22361450198784]
16.52 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22361448097536]
19.03 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22361445996288]
21.12 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22361443895040]
11.47 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22361441793792]
16.83 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22361439692544]
21.39 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22361437591296]
18.08 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22361435490048]
22.27 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22361433388800]
28.11 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22361431287552]
12.76 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22361429186304]
25.82 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22361427085056]
21.42 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22361424983808]
34.41 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22361422882560]
34.75 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22361420781312]
39.30 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22361418680064]
46.78 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22361416578816]
87.18 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22361414477568]
116.51 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22360606373632]
125.38 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22360604272384]
205.95 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22360602171136]
201.00 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22360600069888]
709.42 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22360597968640]
846.38 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22360595867392]
982.77 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22360593766144]
3154.58 ms (3 s 154.58 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22360591664896]
5275.55 ms (5 s 275.56 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22360589563648]
4151.15 ms (4 s 151.15 ms) taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22360587462400]
3419.11 ms (3 s 419.11 ms) taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22360585361152]
4721.30 ms (4 s 721.30 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22360583259904]
5821.87 ms (5 s 821.87 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22360581158656]
6656.56 ms (6 s 656.56 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22360579057408]
7808.62 ms (7 s 808.63 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22360576956160]
9426.52 ms (9 s 426.52 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22360574854912]
9497.97 ms (9 s 497.97 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.
80436.15 ms (1 min 20 s 436.15 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:22360574854912]
136677.51 ms (2 min 16 s 677.51 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:22360576956160]
206936.90 ms (3 min 26 s 936.90 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:22360579057408]
291840.50 ms (4 min 51 s 840.50 ms) taken to read 143296899 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. [tid:22360581158656]
403408.47 ms (6 min 43 s 408.47 ms) taken to read 263540491 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs79-unfiltered71+.txt. [tid:22360583259904]
488525.53 ms (8 min 8 s 525.53 ms) taken to read 489824924 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs81-unfiltered71+.txt. [tid:22360585361152]
655549.71 ms (10 min 55 s 549.71 ms) taken to read 905043886 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs83-unfiltered71+.txt. [tid:22360587462400]
655595.67 ms (10 min 55 s 595.67 ms) additional read duration.
Loaded 7 more representative collections of sizes:
71 : 23150845
73 : 45156728
75 : 80141395
77 : 143296899
79 : 263540491
81 : 489824924
83 : 905043886
1975458862 representatives in total.
Tue Nov 7 20:32:13 2023: Inserted ≈ 5% of D-proof conclusions. [ 98772943 of 1975458862] (ETC: Tue Nov 7 21:17:39 2023 ; 45 min 26 s 506.73 ms remaining ; 47 min 50 s 7.08 ms total)
Tue Nov 7 20:34:50 2023: Inserted ≈10% of D-proof conclusions. [ 197545886 of 1975458862] (ETC: Tue Nov 7 21:19:53 2023 ; 45 min 3 s 335.36 ms remaining ; 50 min 3 s 705.95 ms total)
Tue Nov 7 20:37:34 2023: Inserted ≈15% of D-proof conclusions. [ 296318829 of 1975458862] (ETC: Tue Nov 7 21:21:30 2023 ; 43 min 55 s 307.71 ms remaining ; 51 min 40 s 362.01 ms total)
Tue Nov 7 20:40:43 2023: Inserted ≈20% of D-proof conclusions. [ 395091772 of 1975458862] (ETC: Tue Nov 7 21:24:19 2023 ; 43 min 35 s 429.71 ms remaining ; 54 min 29 s 287.14 ms total)
Tue Nov 7 20:44:04 2023: Inserted ≈25% of D-proof conclusions. [ 493864715 of 1975458862] (ETC: Tue Nov 7 21:26:50 2023 ; 42 min 45 s 349.03 ms remaining ; 57 min 465.37 ms total)
Tue Nov 7 20:47:21 2023: Inserted ≈30% of D-proof conclusions. [ 592637658 of 1975458862] (ETC: Tue Nov 7 21:28:14 2023 ; 40 min 53 s 539.11 ms remaining ; 58 min 25 s 55.87 ms total)
Tue Nov 7 20:50:09 2023: Inserted ≈35% of D-proof conclusions. [ 691410601 of 1975458862] (ETC: Tue Nov 7 21:27:55 2023 ; 37 min 45 s 884.63 ms remaining ; 58 min 5 s 976.36 ms total)
Tue Nov 7 20:53:13 2023: Inserted ≈40% of D-proof conclusions. [ 790183544 of 1975458862] (ETC: Tue Nov 7 21:28:18 2023 ; 35 min 5 s 494.29 ms remaining ; 58 min 29 s 157.14 ms total)
Tue Nov 7 20:56:13 2023: Inserted ≈45% of D-proof conclusions. [ 888956487 of 1975458862] (ETC: Tue Nov 7 21:28:29 2023 ; 32 min 15 s 976.07 ms remaining ; 58 min 39 s 956.49 ms total)
Tue Nov 7 20:59:17 2023: Inserted ≈50% of D-proof conclusions. [ 987729431 of 1975458862] (ETC: Tue Nov 7 21:28:44 2023 ; 29 min 27 s 440.59 ms remaining ; 58 min 54 s 881.19 ms total)
Tue Nov 7 21:02:22 2023: Inserted ≈55% of D-proof conclusions. [1086502374 of 1975458862] (ETC: Tue Nov 7 21:29:00 2023 ; 26 min 37 s 697.22 ms remaining ; 59 min 10 s 438.26 ms total)
Tue Nov 7 21:04:26 2023: Inserted ≈60% of D-proof conclusions. [1185275317 of 1975458862] (ETC: Tue Nov 7 21:27:30 2023 ; 23 min 4 s 165.86 ms remaining ; 57 min 40 s 414.66 ms total)
Tue Nov 7 21:06:42 2023: Inserted ≈65% of D-proof conclusions. [1284048260 of 1975458862] (ETC: Tue Nov 7 21:26:34 2023 ; 19 min 51 s 568.27 ms remaining ; 56 min 44 s 480.77 ms total)
Tue Nov 7 21:09:08 2023: Inserted ≈70% of D-proof conclusions. [1382821203 of 1975458862] (ETC: Tue Nov 7 21:26:00 2023 ; 16 min 51 s 63.07 ms remaining ; 56 min 10 s 210.24 ms total)
Tue Nov 7 21:11:41 2023: Inserted ≈75% of D-proof conclusions. [1481594146 of 1975458862] (ETC: Tue Nov 7 21:25:38 2023 ; 13 min 57 s 291.19 ms remaining ; 55 min 49 s 164.75 ms total)
Tue Nov 7 21:14:31 2023: Inserted ≈80% of D-proof conclusions. [1580367089 of 1975458862] (ETC: Tue Nov 7 21:25:41 2023 ; 11 min 10 s 408.94 ms remaining ; 55 min 52 s 44.69 ms total)
Tue Nov 7 21:17:35 2023: Inserted ≈85% of D-proof conclusions. [1679140032 of 1975458862] (ETC: Tue Nov 7 21:26:00 2023 ; 8 min 25 s 639.46 ms remaining ; 56 min 10 s 929.73 ms total)
Tue Nov 7 21:20:37 2023: Inserted ≈90% of D-proof conclusions. [1777912975 of 1975458862] (ETC: Tue Nov 7 21:26:16 2023 ; 5 min 38 s 657.57 ms remaining ; 56 min 26 s 575.70 ms total)
Tue Nov 7 21:23:50 2023: Inserted ≈95% of D-proof conclusions. [1876685918 of 1975458862] (ETC: Tue Nov 7 21:26:40 2023 ; 2 min 50 s 553.88 ms remaining ; 56 min 51 s 77.66 ms total)
Tue Nov 7 21:27:09 2023: Inserted 100% of D-proof conclusions. [1975458862 of 1975458862] (ETC: Tue Nov 7 21:27:09 2023 ; 0.00 ms remaining ; 57 min 19 s 442.68 ms total)
3439465.55 ms (57 min 19 s 465.55 ms) total insertion duration.
Tue Nov 7 21:27:09 2023: Starting to iterate D-proof candidates of length 85.
6414598.53 ms (1 h 46 min 54 s 598.53 ms) taken to iterate 11946174746 condensed detachment proof strings of length 85.
[Copy] Next iteration count (unfiltered71+): { 85, 11946174746 }
Tue Nov 7 23:14:37 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered]
Wed Nov 8 00:15:52 2023: Process terminated. [pid: 149312, tid:22361510446976]