-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
77-71.log
132 lines (131 loc) · 14.2 KB
/
77-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
( 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
------------ ---------- ---------- ---------- -------- ---------- ----------
40400313 c18m_low 48 COMPLETED 0:0 00:31:54
40400313.ba+ 48 COMPLETED 0:0 00:31:54 190238488K
40400313.ex+ 48 COMPLETED 0:0 00:31:54 80K
By 190238488 KiB = (190238488 / 1024^2) GiB = 181.42555999755859375 GiB, it used approximately 181.43 gibibytes of memory. )
Fri Oct 27 05:34:32 2023: Process started. [pid: 228064, tid:23037665621888]
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).
Fri Oct 27 05:34:32 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.02 ms taken to load initial representatives.
7.78 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:23037605373696]
17.99 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:23037603272448]
21.79 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:23037399267072]
20.09 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:23037397165824]
17.61 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:23037395064576]
21.71 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:23037130831616]
23.06 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:23037392963328]
16.02 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:23037390862080]
22.33 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:23037388760832]
17.44 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:23037386659584]
24.33 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:23037384558336]
14.11 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:23037382457088]
28.81 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:23037380355840]
28.20 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:23037378254592]
22.29 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:23037376153344]
32.18 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:23037374052096]
58.01 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:23037371950848]
31.36 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:23037369849600]
53.88 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:23037367748352]
48.83 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:23037365647104]
60.72 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:23037363545856]
108.49 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:23037361444608]
187.31 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:23037359343360]
348.26 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:23037357242112]
853.57 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:23037355140864]
2065.11 ms (2 s 65.11 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:23037353039616]
5386.14 ms (5 s 386.14 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:23037350938368]
629.52 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:23037348837120]
991.88 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:23037346735872]
1427.99 ms (1 s 427.99 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:23037344634624]
2061.30 ms (2 s 61.30 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:23037342533376]
2769.20 ms (2 s 769.20 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:23037340432128]
4217.29 ms (4 s 217.29 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:23037338330880]
5712.35 ms (5 s 712.35 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:23037336229632]
5734.26 ms (5 s 734.26 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.
15159.64 ms (15 s 159.64 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:23037336229632]
31424.66 ms (31 s 424.66 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:23037338330880]
53664.14 ms (53 s 664.14 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:23037340432128]
89596.62 ms (1 min 29 s 596.62 ms) taken to read 143296899 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. [tid:23037342533376]
89609.23 ms (1 min 29 s 609.23 ms) additional read duration.
Loaded 4 more representative collections of sizes:
71 : 23150845
73 : 45156728
75 : 80141395
77 : 143296899
317049561 representatives in total.
Fri Oct 27 05:36:15 2023: Inserted ≈ 5% of D-proof conclusions. [ 15852478 of 317049561] (ETC: Fri Oct 27 05:38:46 2023 ; 2 min 30 s 443.65 ms remaining ; 2 min 38 s 361.74 ms total)
Fri Oct 27 05:36:23 2023: Inserted ≈10% of D-proof conclusions. [ 31704956 of 317049561] (ETC: Fri Oct 27 05:38:48 2023 ; 2 min 24 s 284.95 ms remaining ; 2 min 40 s 316.61 ms total)
Fri Oct 27 05:36:32 2023: Inserted ≈15% of D-proof conclusions. [ 47557434 of 317049561] (ETC: Fri Oct 27 05:38:52 2023 ; 2 min 20 s 142.32 ms remaining ; 2 min 44 s 873.31 ms total)
Fri Oct 27 05:36:41 2023: Inserted ≈20% of D-proof conclusions. [ 63409912 of 317049561] (ETC: Fri Oct 27 05:38:54 2023 ; 2 min 13 s 175.29 ms remaining ; 2 min 46 s 469.12 ms total)
Fri Oct 27 05:36:50 2023: Inserted ≈25% of D-proof conclusions. [ 79262390 of 317049561] (ETC: Fri Oct 27 05:38:57 2023 ; 2 min 6 s 870.38 ms remaining ; 2 min 49 s 160.51 ms total)
Fri Oct 27 05:36:58 2023: Inserted ≈30% of D-proof conclusions. [ 95114868 of 317049561] (ETC: Fri Oct 27 05:38:58 2023 ; 1 min 59 s 217.01 ms remaining ; 2 min 50 s 310.02 ms total)
Fri Oct 27 05:37:08 2023: Inserted ≈35% of D-proof conclusions. [110967346 of 317049561] (ETC: Fri Oct 27 05:39:00 2023 ; 1 min 52 s 395.67 ms remaining ; 2 min 52 s 916.41 ms total)
Fri Oct 27 05:37:17 2023: Inserted ≈40% of D-proof conclusions. [126819824 of 317049561] (ETC: Fri Oct 27 05:39:02 2023 ; 1 min 44 s 737.87 ms remaining ; 2 min 54 s 563.11 ms total)
Fri Oct 27 05:37:27 2023: Inserted ≈45% of D-proof conclusions. [142672302 of 317049561] (ETC: Fri Oct 27 05:39:04 2023 ; 1 min 37 s 369.25 ms remaining ; 2 min 57 s 35.00 ms total)
Fri Oct 27 05:37:36 2023: Inserted ≈50% of D-proof conclusions. [158524780 of 317049561] (ETC: Fri Oct 27 05:39:04 2023 ; 1 min 28 s 279.36 ms remaining ; 2 min 56 s 558.72 ms total)
Fri Oct 27 05:37:44 2023: Inserted ≈55% of D-proof conclusions. [174377258 of 317049561] (ETC: Fri Oct 27 05:39:03 2023 ; 1 min 19 s 198.27 ms remaining ; 2 min 55 s 996.15 ms total)
Fri Oct 27 05:37:52 2023: Inserted ≈60% of D-proof conclusions. [190229736 of 317049561] (ETC: Fri Oct 27 05:39:01 2023 ; 1 min 9 s 570.16 ms remaining ; 2 min 53 s 925.39 ms total)
Fri Oct 27 05:37:59 2023: Inserted ≈65% of D-proof conclusions. [206082214 of 317049561] (ETC: Fri Oct 27 05:39:00 2023 ; 1 min 356.69 ms remaining ; 2 min 52 s 447.67 ms total)
Fri Oct 27 05:38:07 2023: Inserted ≈70% of D-proof conclusions. [221934692 of 317049561] (ETC: Fri Oct 27 05:38:59 2023 ; 51 s 355.40 ms remaining ; 2 min 51 s 184.68 ms total)
Fri Oct 27 05:38:15 2023: Inserted ≈75% of D-proof conclusions. [237787170 of 317049561] (ETC: Fri Oct 27 05:38:57 2023 ; 42 s 495.78 ms remaining ; 2 min 49 s 983.12 ms total)
Fri Oct 27 05:38:22 2023: Inserted ≈80% of D-proof conclusions. [253639648 of 317049561] (ETC: Fri Oct 27 05:38:56 2023 ; 33 s 651.38 ms remaining ; 2 min 48 s 256.91 ms total)
Fri Oct 27 05:38:30 2023: Inserted ≈85% of D-proof conclusions. [269492126 of 317049561] (ETC: Fri Oct 27 05:38:55 2023 ; 25 s 207.55 ms remaining ; 2 min 48 s 50.36 ms total)
Fri Oct 27 05:38:39 2023: Inserted ≈90% of D-proof conclusions. [285344604 of 317049561] (ETC: Fri Oct 27 05:38:56 2023 ; 16 s 847.05 ms remaining ; 2 min 48 s 470.54 ms total)
Fri Oct 27 05:38:46 2023: Inserted ≈95% of D-proof conclusions. [301197082 of 317049561] (ETC: Fri Oct 27 05:38:54 2023 ; 8 s 349.49 ms remaining ; 2 min 46 s 989.74 ms total)
Fri Oct 27 05:38:52 2023: Inserted 100% of D-proof conclusions. [317049561 of 317049561] (ETC: Fri Oct 27 05:38:52 2023 ; 0.00 ms remaining ; 2 min 44 s 889.31 ms total)
164891.07 ms (2 min 44 s 891.07 ms) total insertion duration.
Fri Oct 27 05:38:52 2023: Starting to iterate D-proof candidates of length 79.
1159324.62 ms (19 min 19 s 324.62 ms) taken to iterate 2091875434 condensed detachment proof strings of length 79.
[Copy] Next iteration count (unfiltered71+): { 79, 2091875434 }
Fri Oct 27 05:58:12 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Fri Oct 27 06:06:06 2023: Process terminated. [pid: 228064, tid:23037665621888]