-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
71-71.log
126 lines (125 loc) · 13.2 KB
/
71-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
( 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
------------ ---------- ---------- ---------- -------- ---------- ----------
39699862 c18m 48 COMPLETED 0:0 00:05:30
39699862.ba+ 48 COMPLETED 0:0 00:05:30 26282436K
39699862.ex+ 48 COMPLETED 0:0 00:05:30 0
By 26282436 KiB = (26282436 / 1024^2) GiB = 25.064884185791015625 GiB, it used approximately 25.06 gibibytes of memory. )
Wed Oct 4 07:43:10 2023: Process started. [pid: 209238, tid:23174865581952]
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 07:43:10 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.02 ms taken to load initial representatives.
17.50 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:23174805333760]
17.38 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:23174803232512]
23.30 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:23174801131264]
25.59 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:23174799030016]
20.53 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:23174796928768]
18.21 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:23174794827520]
19.89 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:23174792726272]
7.56 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:23174790625024]
16.63 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:23174788523776]
17.32 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:23174786422528]
14.55 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:23174784321280]
20.34 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:23174782220032]
31.10 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:23174780118784]
30.13 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:23174778017536]
29.00 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:23174775916288]
64.96 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:23174773815040]
45.65 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:23173630260992]
41.87 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:23173628159744]
52.08 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:23173496043264]
51.93 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:23173626058496]
85.74 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:23173623957248]
92.64 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:23173621856000]
183.80 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:23173619754752]
383.25 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:23173617653504]
863.54 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:23173615552256]
2166.37 ms (2 s 166.37 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:23173613451008]
5134.28 ms (5 s 134.28 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:23173611349760]
539.11 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:23173609248512]
850.62 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:23173607147264]
1415.47 ms (1 s 415.47 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:23173605046016]
1976.76 ms (1 s 976.76 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:23173602944768]
2545.83 ms (2 s 545.83 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:23173600843520]
3627.11 ms (3 s 627.11 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:23173598742272]
5094.80 ms (5 s 94.80 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:23173596641024]
5157.35 ms (5 s 157.35 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.
8844.87 ms (8 s 844.87 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:23173596641024]
8847.31 ms (8 s 847.31 ms) additional read duration.
Loaded 1 more representative collection of size:
71 : 23150845
48454539 representatives in total.
Wed Oct 4 07:43:25 2023: Inserted ≈ 5% of D-proof conclusions. [ 2422726 of 48454539] (ETC: Wed Oct 4 07:43:37 2023 ; 12 s 354.58 ms remaining ; 13 s 4.83 ms total)
Wed Oct 4 07:43:26 2023: Inserted ≈10% of D-proof conclusions. [ 4845453 of 48454539] (ETC: Wed Oct 4 07:43:38 2023 ; 12 s 312.10 ms remaining ; 13 s 680.11 ms total)
Wed Oct 4 07:43:26 2023: Inserted ≈15% of D-proof conclusions. [ 7268180 of 48454539] (ETC: Wed Oct 4 07:43:38 2023 ; 11 s 783.08 ms remaining ; 13 s 862.44 ms total)
Wed Oct 4 07:43:27 2023: Inserted ≈20% of D-proof conclusions. [ 9690907 of 48454539] (ETC: Wed Oct 4 07:43:39 2023 ; 11 s 848.72 ms remaining ; 14 s 810.90 ms total)
Wed Oct 4 07:43:28 2023: Inserted ≈25% of D-proof conclusions. [12113634 of 48454539] (ETC: Wed Oct 4 07:43:40 2023 ; 11 s 905.55 ms remaining ; 15 s 874.07 ms total)
Wed Oct 4 07:43:29 2023: Inserted ≈30% of D-proof conclusions. [14536361 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 11 s 778.24 ms remaining ; 16 s 826.06 ms total)
Wed Oct 4 07:43:30 2023: Inserted ≈35% of D-proof conclusions. [16959088 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 11 s 168.46 ms remaining ; 17 s 182.25 ms total)
Wed Oct 4 07:43:31 2023: Inserted ≈40% of D-proof conclusions. [19381815 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 10 s 362.54 ms remaining ; 17 s 270.91 ms total)
Wed Oct 4 07:43:32 2023: Inserted ≈45% of D-proof conclusions. [21804542 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 9 s 561.40 ms remaining ; 17 s 384.36 ms total)
Wed Oct 4 07:43:33 2023: Inserted ≈50% of D-proof conclusions. [24227269 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 8 s 780.24 ms remaining ; 17 s 560.48 ms total)
Wed Oct 4 07:43:34 2023: Inserted ≈55% of D-proof conclusions. [26649996 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 7 s 897.59 ms remaining ; 17 s 550.19 ms total)
Wed Oct 4 07:43:35 2023: Inserted ≈60% of D-proof conclusions. [29072723 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 7 s 34.40 ms remaining ; 17 s 586.00 ms total)
Wed Oct 4 07:43:36 2023: Inserted ≈65% of D-proof conclusions. [31495450 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 6 s 95.96 ms remaining ; 17 s 417.02 ms total)
Wed Oct 4 07:43:36 2023: Inserted ≈70% of D-proof conclusions. [33918177 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 5 s 180.73 ms remaining ; 17 s 269.11 ms total)
Wed Oct 4 07:43:37 2023: Inserted ≈75% of D-proof conclusions. [36340904 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 4 s 275.97 ms remaining ; 17 s 103.87 ms total)
Wed Oct 4 07:43:38 2023: Inserted ≈80% of D-proof conclusions. [38763631 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 3 s 395.47 ms remaining ; 16 s 977.37 ms total)
Wed Oct 4 07:43:39 2023: Inserted ≈85% of D-proof conclusions. [41186358 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 2 s 543.46 ms remaining ; 16 s 956.42 ms total)
Wed Oct 4 07:43:39 2023: Inserted ≈90% of D-proof conclusions. [43609085 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 1 s 685.09 ms remaining ; 16 s 850.90 ms total)
Wed Oct 4 07:43:40 2023: Inserted ≈95% of D-proof conclusions. [46031812 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 837.09 ms remaining ; 16 s 741.80 ms total)
Wed Oct 4 07:43:41 2023: Inserted 100% of D-proof conclusions. [48454539 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 0.00 ms remaining ; 16 s 611.68 ms total)
16611.87 ms (16 s 611.87 ms) total insertion duration.
Wed Oct 4 07:43:41 2023: Starting to iterate D-proof candidates of length 73.
247928.78 ms (4 min 7 s 928.78 ms) taken to iterate 397509772 condensed detachment proof strings of length 73.
[Copy] Next iteration count (unfiltered71+): { 73, 397509772 }
Wed Oct 4 07:47:49 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Wed Oct 4 07:48:35 2023: Process terminated. [pid: 209238, tid:23174865581952]