-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
67-65.log
122 lines (121 loc) · 13 KB
/
67-65.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
( This log file was generated by executing 'pmGenerator -c -n -s CpCCNqCCNrsCptCCtqCrq --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 MPI node
— 2-socket Intel Xeon Platinum 8160 (Skylake), 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory —
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
------------ ---------- ---------- ---------- -------- ---------- ----------
40227241 c18m_low 48 COMPLETED 0:0 00:11:44
40227241.ba+ 48 COMPLETED 0:0 00:11:44 90325016K
40227241.ex+ 48 COMPLETED 0:0 00:11:45 0
By 90325016 KiB = (90325016 / 1024^2) GiB = 86.14064788818359375 GiB, it used approximately 86.14 gibibytes of memory. )
Wed Oct 18 18:25:04 2023: Process started. [pid: 134807, tid:22818875479936]
Tasks:
1. resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true)
2. countNextIterationAmount(false, true)
[Main] Calling resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314]
(1) C0CCN1CCN2.3C0.4CC4.1C2.1 - CpCCNqCCNrsCptCCtqCrq - 0\imply((\not1\imply((\not2\imply3)\imply(0\imply4)))\imply((4\imply1)\imply(2\imply1)))
[Main] Calling countNextIterationAmount(false, true).
Wed Oct 18 18:25:04 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
21.00 ms taken to read 1 condensed detachment proof and conclusion from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs3.txt. [tid:22818815231744]
21.57 ms taken to read 2 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs5.txt. [tid:22818813130496]
51.83 ms taken to read 4 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs7.txt. [tid:22818811029248]
9.05 ms taken to read 7 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs9.txt. [tid:22818808928000]
17.82 ms taken to read 14 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs11.txt. [tid:22818806826752]
20.93 ms taken to read 23 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs13.txt. [tid:22818804725504]
15.05 ms taken to read 42 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs15.txt. [tid:22818802624256]
28.89 ms taken to read 72 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs17.txt. [tid:22818800523008]
54.17 ms taken to read 119 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs19.txt. [tid:22818798421760]
32.34 ms taken to read 180 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs21.txt. [tid:22818796320512]
32.55 ms taken to read 296 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs23.txt. [tid:22818794219264]
46.20 ms taken to read 493 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs25.txt. [tid:22818792118016]
50.40 ms taken to read 809 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs27.txt. [tid:22818790016768]
53.54 ms taken to read 1330 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs29.txt. [tid:22818787915520]
54.61 ms taken to read 2190 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs31.txt. [tid:22818785814272]
51.42 ms taken to read 3606 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs33.txt. [tid:22818783713024]
67.11 ms taken to read 5925 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs35.txt. [tid:22818781611776]
84.47 ms taken to read 9738 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs37.txt. [tid:22818779510528]
183.64 ms taken to read 15948 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs39.txt. [tid:22818777409280]
341.57 ms taken to read 26109 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs41.txt. [tid:22818775308032]
790.55 ms taken to read 42844 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs43.txt. [tid:22818773206784]
1993.84 ms (1 s 993.84 ms) taken to read 70083 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs45.txt. [tid:22818771105536]
5070.78 ms (5 s 70.78 ms) taken to read 115027 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs47.txt. [tid:22818769004288]
415.03 ms taken to read 188519 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs49.txt. [tid:22818766903040]
985.07 ms taken to read 308975 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs51.txt. [tid:22818764801792]
1435.94 ms (1 s 435.94 ms) taken to read 506415 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs53.txt. [tid:22818762700544]
2028.30 ms (2 s 28.30 ms) taken to read 830126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs55.txt. [tid:22817886172928]
2848.02 ms (2 s 848.02 ms) taken to read 1360461 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs57.txt. [tid:22817884071680]
4009.16 ms (4 s 9.16 ms) taken to read 2229126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs59.txt. [tid:22817881970432]
5753.08 ms (5 s 753.08 ms) taken to read 3652191 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs61.txt. [tid:22817879869184]
7591.41 ms (7 s 591.41 ms) taken to read 5983166 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs63.txt. [tid:22817877767936]
7612.35 ms (7 s 612.35 ms) total read duration.
Loaded 32 representative collections of sizes:
1 : 1
3 : 1
5 : 2
7 : 4
9 : 7
11 : 14
13 : 23
15 : 42
17 : 72
19 : 119
21 : 180
23 : 296
25 : 493
27 : 809
29 : 1330
31 : 2190
33 : 3606
35 : 5925
37 : 9738
39 : 15948
41 : 26109
43 : 42844
45 : 70083
47 : 115027
49 : 188519
51 : 308975
53 : 506415
55 : 830126
57 : 1360461
59 : 2229126
61 : 3652191
63 : 5983166
15353842 representatives in total.
19099.45 ms (19 s 99.45 ms) taken to read 15025264 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs65-unfiltered65+.txt. [tid:22817877767936]
37144.89 ms (37 s 144.89 ms) taken to read 32295163 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs67-unfiltered65+.txt. [tid:22817879869184]
37147.11 ms (37 s 147.11 ms) additional read duration.
Loaded 2 more representative collections of sizes:
65 : 15025264
67 : 32295163
62674269 representatives in total.
Wed Oct 18 18:25:53 2023: Inserted ≈ 5% of D-proof conclusions. [ 3133713 of 62674269] (ETC: Wed Oct 18 18:27:11 2023 ; 1 min 18 s 437.56 ms remaining ; 1 min 22 s 565.85 ms total)
Wed Oct 18 18:25:57 2023: Inserted ≈10% of D-proof conclusions. [ 6267426 of 62674269] (ETC: Wed Oct 18 18:27:15 2023 ; 1 min 17 s 929.38 ms remaining ; 1 min 26 s 588.20 ms total)
Wed Oct 18 18:26:02 2023: Inserted ≈15% of D-proof conclusions. [ 9401140 of 62674269] (ETC: Wed Oct 18 18:27:18 2023 ; 1 min 15 s 878.48 ms remaining ; 1 min 29 s 268.80 ms total)
Wed Oct 18 18:26:07 2023: Inserted ≈20% of D-proof conclusions. [12534853 of 62674269] (ETC: Wed Oct 18 18:27:19 2023 ; 1 min 12 s 282.10 ms remaining ; 1 min 30 s 352.62 ms total)
Wed Oct 18 18:26:11 2023: Inserted ≈25% of D-proof conclusions. [15668567 of 62674269] (ETC: Wed Oct 18 18:27:19 2023 ; 1 min 7 s 798.44 ms remaining ; 1 min 30 s 397.92 ms total)
Wed Oct 18 18:26:15 2023: Inserted ≈30% of D-proof conclusions. [18802280 of 62674269] (ETC: Wed Oct 18 18:27:16 2023 ; 1 min 1 s 3.94 ms remaining ; 1 min 27 s 148.49 ms total)
Wed Oct 18 18:26:19 2023: Inserted ≈35% of D-proof conclusions. [21935994 of 62674269] (ETC: Wed Oct 18 18:27:14 2023 ; 55 s 200.10 ms remaining ; 1 min 24 s 923.23 ms total)
Wed Oct 18 18:26:22 2023: Inserted ≈40% of D-proof conclusions. [25069707 of 62674269] (ETC: Wed Oct 18 18:27:12 2023 ; 49 s 793.26 ms remaining ; 1 min 22 s 988.76 ms total)
Wed Oct 18 18:26:26 2023: Inserted ≈45% of D-proof conclusions. [28203421 of 62674269] (ETC: Wed Oct 18 18:27:11 2023 ; 44 s 976.42 ms remaining ; 1 min 21 s 775.32 ms total)
Wed Oct 18 18:26:30 2023: Inserted ≈50% of D-proof conclusions. [31337134 of 62674269] (ETC: Wed Oct 18 18:27:11 2023 ; 40 s 973.70 ms remaining ; 1 min 21 s 947.39 ms total)
Wed Oct 18 18:26:34 2023: Inserted ≈55% of D-proof conclusions. [34470847 of 62674269] (ETC: Wed Oct 18 18:27:11 2023 ; 37 s 164.09 ms remaining ; 1 min 22 s 586.86 ms total)
Wed Oct 18 18:26:38 2023: Inserted ≈60% of D-proof conclusions. [37604561 of 62674269] (ETC: Wed Oct 18 18:27:11 2023 ; 33 s 36.99 ms remaining ; 1 min 22 s 592.47 ms total)
Wed Oct 18 18:26:42 2023: Inserted ≈65% of D-proof conclusions. [40738274 of 62674269] (ETC: Wed Oct 18 18:27:10 2023 ; 28 s 537.92 ms remaining ; 1 min 21 s 536.92 ms total)
Wed Oct 18 18:26:46 2023: Inserted ≈70% of D-proof conclusions. [43871988 of 62674269] (ETC: Wed Oct 18 18:27:10 2023 ; 24 s 291.13 ms remaining ; 1 min 20 s 970.42 ms total)
Wed Oct 18 18:26:49 2023: Inserted ≈75% of D-proof conclusions. [47005701 of 62674269] (ETC: Wed Oct 18 18:27:10 2023 ; 20 s 183.92 ms remaining ; 1 min 20 s 735.68 ms total)
Wed Oct 18 18:26:53 2023: Inserted ≈80% of D-proof conclusions. [50139415 of 62674269] (ETC: Wed Oct 18 18:27:09 2023 ; 16 s 131.88 ms remaining ; 1 min 20 s 659.40 ms total)
Wed Oct 18 18:26:57 2023: Inserted ≈85% of D-proof conclusions. [53273128 of 62674269] (ETC: Wed Oct 18 18:27:09 2023 ; 12 s 64.39 ms remaining ; 1 min 20 s 429.24 ms total)
Wed Oct 18 18:27:01 2023: Inserted ≈90% of D-proof conclusions. [56406842 of 62674269] (ETC: Wed Oct 18 18:27:09 2023 ; 8 s 44.65 ms remaining ; 1 min 20 s 446.54 ms total)
Wed Oct 18 18:27:05 2023: Inserted ≈95% of D-proof conclusions. [59540555 of 62674269] (ETC: Wed Oct 18 18:27:09 2023 ; 4 s 15.85 ms remaining ; 1 min 20 s 316.91 ms total)
Wed Oct 18 18:27:11 2023: Inserted 100% of D-proof conclusions. [62674269 of 62674269] (ETC: Wed Oct 18 18:27:11 2023 ; 0.00 ms remaining ; 1 min 21 s 764.48 ms total)
81764.69 ms (1 min 21 s 764.69 ms) total insertion duration.
Wed Oct 18 18:27:11 2023: Starting to iterate D-proof candidates of length 69.
438472.75 ms (7 min 18 s 472.75 ms) taken to iterate 682368918 condensed detachment proof strings of length 69.
[Copy] Next iteration count (unfiltered65+): { 69, 682368918 }
Wed Oct 18 18:34:29 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Wed Oct 18 18:36:37 2023: Process terminated. [pid: 134807, tid:22818875479936]