-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
51.log
103 lines (102 loc) · 11.1 KB
/
51.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
( This log file was generated by executing 'pmGenerator -c -n -s CCpqCCCrCstCqCNsNpCps --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
------------ ---------- ---------- ---------- -------- ---------- ----------
40319093 c18m_low 48 COMPLETED 0:0 00:03:55
40319093.ba+ 48 COMPLETED 0:0 00:03:55 142269532K
40319093.ex+ 48 COMPLETED 0:0 00:03:55 80K
By 142269532 KiB = (142269532 / 1024^2) GiB = 135.678798675537109375 GiB, it used approximately 135.68 gibibytes of memory. )
Tue Oct 24 13:29:07 2023: Process started. [pid: 194618, tid:23214756394880]
Tasks:
1. resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true)
2. countNextIterationAmount(false, true)
[Main] Calling resetRepresentativesFor("CCpqCCCrCstCqCNsNpCps", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72]
(1) CC0.1CCC2C3.4C1CN3N0C0.3 - CCpqCCCrCstCqCNsNpCps - (0\imply1)\imply(((2\imply(3\imply4))\imply(1\imply(\not3\imply\not0)))\imply(0\imply3))
[Main] Calling countNextIterationAmount(false, true).
Tue Oct 24 13:29:07 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
22.72 ms taken to read 1 condensed detachment proof and conclusion from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs3.txt. [tid:23214696146688]
15.99 ms taken to read 1 condensed detachment proof and conclusion from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs5.txt. [tid:23214694045440]
23.02 ms taken to read 2 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs7.txt. [tid:23214691944192]
18.43 ms taken to read 4 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs9.txt. [tid:23214689842944]
23.83 ms taken to read 7 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs11.txt. [tid:23214687741696]
20.67 ms taken to read 12 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs13.txt. [tid:23214685640448]
15.58 ms taken to read 22 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs15.txt. [tid:23214683539200]
23.35 ms taken to read 42 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs17.txt. [tid:23214681437952]
27.21 ms taken to read 80 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs19.txt. [tid:23214679336704]
32.84 ms taken to read 151 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs21.txt. [tid:23214677235456]
51.54 ms taken to read 287 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs23.txt. [tid:23214675134208]
40.89 ms taken to read 555 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs25.txt. [tid:23214673032960]
391.15 ms taken to read 1081 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs27.txt. [tid:23214670931712]
425.65 ms taken to read 2107 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs29.txt. [tid:23214668830464]
257.62 ms taken to read 4123 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs31.txt. [tid:23214666729216]
1003.84 ms (1 s 3.84 ms) taken to read 8112 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs33.txt. [tid:23214664627968]
4779.25 ms (4 s 779.25 ms) taken to read 16029 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs35.txt. [tid:23214662526720]
594.10 ms taken to read 31774 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs37.txt. [tid:23214660425472]
1465.76 ms (1 s 465.76 ms) taken to read 63152 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs39.txt. [tid:23214658324224]
2524.79 ms (2 s 524.79 ms) taken to read 125873 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs41.txt. [tid:23214656222976]
4555.70 ms (4 s 555.70 ms) taken to read 251561 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs43.txt. [tid:23214654121728]
7450.66 ms (7 s 450.67 ms) taken to read 503956 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs45.txt. [tid:23214652020480]
13984.66 ms (13 s 984.66 ms) taken to read 1011747 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs47.txt. [tid:23214649919232]
26284.05 ms (26 s 284.05 ms) taken to read 2035230 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs49.txt. [tid:23214647817984]
61034.55 ms (1 min 1 s 34.55 ms) taken to read 4101770 condensed detachment proofs and conclusions from data/1d5f27494b1a2312e223b7f8dd3551abf717590ceef694c08dcbed72/dProofs-withConclusions/dProofs51.txt. [tid:23214645716736]
61075.35 ms (1 min 1 s 75.35 ms) total read duration.
Loaded 26 representative collections of sizes:
1 : 1
3 : 1
5 : 1
7 : 2
9 : 4
11 : 7
13 : 12
15 : 22
17 : 42
19 : 80
21 : 151
23 : 287
25 : 555
27 : 1081
29 : 2107
31 : 4123
33 : 8112
35 : 16029
37 : 31774
39 : 63152
41 : 125873
43 : 251561
45 : 503956
47 : 1011747
49 : 2035230
51 : 4101770
8157680 representatives in total.
Tue Oct 24 13:30:12 2023: Inserted ≈ 5% of D-proof conclusions. [ 407884 of 8157680] (ETC: Tue Oct 24 13:31:28 2023 ; 1 min 16 s 257.17 ms remaining ; 1 min 20 s 270.70 ms total)
Tue Oct 24 13:30:17 2023: Inserted ≈10% of D-proof conclusions. [ 815768 of 8157680] (ETC: Tue Oct 24 13:31:36 2023 ; 1 min 19 s 219.13 ms remaining ; 1 min 28 s 21.25 ms total)
Tue Oct 24 13:30:21 2023: Inserted ≈15% of D-proof conclusions. [1223652 of 8157680] (ETC: Tue Oct 24 13:31:36 2023 ; 1 min 14 s 744.48 ms remaining ; 1 min 27 s 934.68 ms total)
Tue Oct 24 13:30:26 2023: Inserted ≈20% of D-proof conclusions. [1631536 of 8157680] (ETC: Tue Oct 24 13:31:37 2023 ; 1 min 11 s 425.91 ms remaining ; 1 min 29 s 282.39 ms total)
Tue Oct 24 13:30:34 2023: Inserted ≈25% of D-proof conclusions. [2039420 of 8157680] (ETC: Tue Oct 24 13:31:51 2023 ; 1 min 17 s 2.86 ms remaining ; 1 min 42 s 670.48 ms total)
Tue Oct 24 13:30:38 2023: Inserted ≈30% of D-proof conclusions. [2447304 of 8157680] (ETC: Tue Oct 24 13:31:46 2023 ; 1 min 8 s 763.36 ms remaining ; 1 min 38 s 233.37 ms total)
Tue Oct 24 13:30:42 2023: Inserted ≈35% of D-proof conclusions. [2855188 of 8157680] (ETC: Tue Oct 24 13:31:46 2023 ; 1 min 3 s 329.19 ms remaining ; 1 min 37 s 429.53 ms total)
Tue Oct 24 13:30:48 2023: Inserted ≈40% of D-proof conclusions. [3263072 of 8157680] (ETC: Tue Oct 24 13:31:49 2023 ; 1 min 277.94 ms remaining ; 1 min 40 s 463.23 ms total)
Tue Oct 24 13:30:55 2023: Inserted ≈45% of D-proof conclusions. [3670956 of 8157680] (ETC: Tue Oct 24 13:31:52 2023 ; 57 s 419.67 ms remaining ; 1 min 44 s 399.39 ms total)
Tue Oct 24 13:31:04 2023: Inserted ≈50% of D-proof conclusions. [4078840 of 8157680] (ETC: Tue Oct 24 13:31:59 2023 ; 55 s 617.22 ms remaining ; 1 min 51 s 234.43 ms total)
Tue Oct 24 13:31:07 2023: Inserted ≈55% of D-proof conclusions. [4486724 of 8157680] (ETC: Tue Oct 24 13:31:56 2023 ; 48 s 443.23 ms remaining ; 1 min 47 s 651.63 ms total)
Tue Oct 24 13:31:11 2023: Inserted ≈60% of D-proof conclusions. [4894608 of 8157680] (ETC: Tue Oct 24 13:31:53 2023 ; 41 s 992.90 ms remaining ; 1 min 44 s 982.26 ms total)
Tue Oct 24 13:31:15 2023: Inserted ≈65% of D-proof conclusions. [5302492 of 8157680] (ETC: Tue Oct 24 13:31:52 2023 ; 36 s 212.43 ms remaining ; 1 min 43 s 464.08 ms total)
Tue Oct 24 13:31:20 2023: Inserted ≈70% of D-proof conclusions. [5710376 of 8157680] (ETC: Tue Oct 24 13:31:51 2023 ; 30 s 793.00 ms remaining ; 1 min 42 s 643.34 ms total)
Tue Oct 24 13:31:25 2023: Inserted ≈75% of D-proof conclusions. [6118260 of 8157680] (ETC: Tue Oct 24 13:31:51 2023 ; 25 s 648.93 ms remaining ; 1 min 42 s 595.73 ms total)
Tue Oct 24 13:31:30 2023: Inserted ≈80% of D-proof conclusions. [6526144 of 8157680] (ETC: Tue Oct 24 13:31:50 2023 ; 20 s 482.49 ms remaining ; 1 min 42 s 412.44 ms total)
Tue Oct 24 13:31:36 2023: Inserted ≈85% of D-proof conclusions. [6934028 of 8157680] (ETC: Tue Oct 24 13:31:51 2023 ; 15 s 451.01 ms remaining ; 1 min 43 s 6.76 ms total)
Tue Oct 24 13:31:43 2023: Inserted ≈90% of D-proof conclusions. [7341912 of 8157680] (ETC: Tue Oct 24 13:31:53 2023 ; 10 s 534.32 ms remaining ; 1 min 45 s 343.17 ms total)
Tue Oct 24 13:31:50 2023: Inserted ≈95% of D-proof conclusions. [7749796 of 8157680] (ETC: Tue Oct 24 13:31:55 2023 ; 5 s 348.93 ms remaining ; 1 min 46 s 978.59 ms total)
Tue Oct 24 13:31:59 2023: Inserted 100% of D-proof conclusions. [8157680 of 8157680] (ETC: Tue Oct 24 13:31:59 2023 ; 0.00 ms remaining ; 1 min 51 s 195.88 ms total)
111223.37 ms (1 min 51 s 223.37 ms) total insertion duration.
Tue Oct 24 13:31:59 2023: Starting to iterate D-proof candidates of length 53.
32066.42 ms (32 s 66.42 ms) taken to iterate 29300562 condensed detachment proof strings of length 53.
[Copy] Next iteration count (filtered): { 53, 29300562 }
Tue Oct 24 13:32:31 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Tue Oct 24 13:32:48 2023: Process terminated. [pid: 194618, tid:23214756394880]