-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
69.log
121 lines (120 loc) · 12.7 KB
/
69.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
( 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 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
------------ ---------- ---------- ---------- -------- ---------- ----------
39699731 c18m 48 COMPLETED 0:0 00:02:51
39699731.ba+ 48 COMPLETED 0:0 00:02:51 13414456K
39699731.ex+ 48 COMPLETED 0:0 00:02:51 80K
By 13414456 KiB = (13414456 / 1024^2) GiB = 12.79302215576171875 GiB, it used approximately 12.79 gibibytes of memory. )
Wed Oct 4 06:36:54 2023: Process started. [pid: 43812, tid:22989020551040]
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).
Wed Oct 4 06:36:54 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
0.00 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22988960302848]
0.09 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22988958201600]
0.00 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22988956100352]
0.07 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22988953999104]
0.01 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22988951897856]
0.18 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22988949796608]
0.02 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22988611122944]
0.07 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22988609021696]
0.81 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22988606920448]
0.21 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22988604819200]
0.04 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22988602717952]
0.04 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22988600616704]
3.50 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22988598515456]
3.95 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22988596414208]
0.89 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22988594312960]
0.50 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22988592211712]
4.19 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22988590110464]
2.45 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22988588009216]
6.29 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22988585907968]
11.63 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22988583806720]
22.50 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22988581705472]
55.03 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22988579604224]
122.33 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22988577502976]
339.00 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22988575401728]
814.70 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22988573300480]
2039.43 ms (2 s 39.43 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22988571199232]
5466.03 ms (5 s 466.03 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22988569097984]
582.85 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22988566996736]
937.61 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22988564895488]
1507.64 ms (1 s 507.64 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22988562794240]
2091.49 ms (2 s 91.49 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22988560692992]
2741.12 ms (2 s 741.13 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22988558591744]
3951.30 ms (3 s 951.30 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22988556490496]
5450.94 ms (5 s 450.94 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22988554389248]
5486.70 ms (5 s 486.70 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.
Wed Oct 4 06:37:00 2023: Inserted ≈ 5% of D-proof conclusions. [ 1265184 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 7 s 224.83 ms remaining ; 7 s 605.08 ms total)
Wed Oct 4 06:37:00 2023: Inserted ≈10% of D-proof conclusions. [ 2530369 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 7 s 52.30 ms remaining ; 7 s 835.89 ms total)
Wed Oct 4 06:37:00 2023: Inserted ≈15% of D-proof conclusions. [ 3795554 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 6 s 329.88 ms remaining ; 7 s 446.91 ms total)
Wed Oct 4 06:37:01 2023: Inserted ≈20% of D-proof conclusions. [ 5060738 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 6 s 249.76 ms remaining ; 7 s 812.20 ms total)
Wed Oct 4 06:37:01 2023: Inserted ≈25% of D-proof conclusions. [ 6325923 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 5 s 781.02 ms remaining ; 7 s 708.03 ms total)
Wed Oct 4 06:37:02 2023: Inserted ≈30% of D-proof conclusions. [ 7591108 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 5 s 320.63 ms remaining ; 7 s 600.90 ms total)
Wed Oct 4 06:37:02 2023: Inserted ≈35% of D-proof conclusions. [ 8856292 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 5 s 23.00 ms remaining ; 7 s 727.70 ms total)
Wed Oct 4 06:37:02 2023: Inserted ≈40% of D-proof conclusions. [10121477 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 4 s 660.41 ms remaining ; 7 s 767.36 ms total)
Wed Oct 4 06:37:03 2023: Inserted ≈45% of D-proof conclusions. [11386662 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 4 s 309.15 ms remaining ; 7 s 834.82 ms total)
Wed Oct 4 06:37:03 2023: Inserted ≈50% of D-proof conclusions. [12651847 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 3 s 966.45 ms remaining ; 7 s 932.89 ms total)
Wed Oct 4 06:37:04 2023: Inserted ≈55% of D-proof conclusions. [13917031 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 3 s 624.06 ms remaining ; 8 s 53.46 ms total)
Wed Oct 4 06:37:04 2023: Inserted ≈60% of D-proof conclusions. [15182216 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 3 s 231.78 ms remaining ; 8 s 79.46 ms total)
Wed Oct 4 06:37:05 2023: Inserted ≈65% of D-proof conclusions. [16447401 of 25303694] (ETC: Wed Oct 4 06:37:07 2023 ; 2 s 818.19 ms remaining ; 8 s 51.97 ms total)
Wed Oct 4 06:37:05 2023: Inserted ≈70% of D-proof conclusions. [17712585 of 25303694] (ETC: Wed Oct 4 06:37:08 2023 ; 2 s 450.89 ms remaining ; 8 s 169.64 ms total)
Wed Oct 4 06:37:05 2023: Inserted ≈75% of D-proof conclusions. [18977770 of 25303694] (ETC: Wed Oct 4 06:37:08 2023 ; 2 s 43.80 ms remaining ; 8 s 175.19 ms total)
Wed Oct 4 06:37:06 2023: Inserted ≈80% of D-proof conclusions. [20242955 of 25303694] (ETC: Wed Oct 4 06:37:08 2023 ; 1 s 646.59 ms remaining ; 8 s 232.97 ms total)
Wed Oct 4 06:37:06 2023: Inserted ≈85% of D-proof conclusions. [21508139 of 25303694] (ETC: Wed Oct 4 06:37:08 2023 ; 1 s 238.55 ms remaining ; 8 s 257.01 ms total)
Wed Oct 4 06:37:07 2023: Inserted ≈90% of D-proof conclusions. [22773324 of 25303694] (ETC: Wed Oct 4 06:37:08 2023 ; 826.15 ms remaining ; 8 s 261.53 ms total)
Wed Oct 4 06:37:07 2023: Inserted ≈95% of D-proof conclusions. [24038509 of 25303694] (ETC: Wed Oct 4 06:37:08 2023 ; 415.83 ms remaining ; 8 s 316.65 ms total)
Wed Oct 4 06:37:08 2023: Inserted 100% of D-proof conclusions. [25303694 of 25303694] (ETC: Wed Oct 4 06:37:08 2023 ; 0.00 ms remaining ; 8 s 393.08 ms total)
8393.35 ms (8 s 393.35 ms) total insertion duration.
Wed Oct 4 06:37:08 2023: Starting to iterate D-proof candidates of length 71.
130942.38 ms (2 min 10 s 942.38 ms) taken to iterate 229211380 condensed detachment proof strings of length 71.
[Copy] Next iteration count (filtered): { 71, 229211380 }
Wed Oct 4 06:39:19 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Wed Oct 4 06:39:40 2023: Process terminated. [pid: 43812, tid:22989020551040]