-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
73-71.log
128 lines (127 loc) · 13.4 KB
/
73-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
( 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
------------ ---------- ---------- ---------- -------- ---------- ----------
39731831 c18m 48 COMPLETED 0:0 00:12:11
39731831.ba+ 48 COMPLETED 0:0 00:12:11 53322280K
39731831.ex+ 48 COMPLETED 0:0 00:12:11 52K
By 53322280 KiB = (53322280 / 1024^2) GiB = 50.85208892822265625 GiB, it used approximately 50.85 gibibytes of memory. )
Wed Oct 4 21:54:28 2023: Process started. [pid: 172053, tid:23321358104448]
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 21:54:31 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
13.89 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:23321297856256]
22.63 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:23321295755008]
20.11 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:23321293653760]
12.58 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:23321291552512]
18.01 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:23321289451264]
14.22 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:23321287350016]
25.86 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:23321285248768]
20.29 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:23321283147520]
18.10 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:23321281046272]
22.79 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:23321278945024]
24.06 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:23321276843776]
19.36 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:23321274742528]
22.07 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:23321272641280]
30.04 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:23320464455424]
30.11 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:23320462354176]
74.91 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:23320460252928]
28.89 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:23320458151680]
49.55 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:23320456050432]
56.68 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:23320453949184]
64.81 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:23320451847936]
75.84 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:23320449746688]
88.43 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:23320447645440]
170.66 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:23320445544192]
352.66 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:23320443442944]
843.71 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:23320441341696]
2129.11 ms (2 s 129.11 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:23320439240448]
5230.78 ms (5 s 230.78 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:23320437139200]
540.40 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:23320435037952]
898.29 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:23320432936704]
1559.21 ms (1 s 559.21 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:23320430835456]
2104.97 ms (2 s 104.97 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:23320428734208]
2783.21 ms (2 s 783.21 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:23320426632960]
3889.23 ms (3 s 889.23 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:23320424531712]
5461.19 ms (5 s 461.19 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:23320422430464]
5481.30 ms (5 s 481.30 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.
10897.21 ms (10 s 897.21 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:23320422430464]
20226.48 ms (20 s 226.48 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:23320424531712]
20228.73 ms (20 s 228.73 ms) additional read duration.
Loaded 2 more representative collections of sizes:
71 : 23150845
73 : 45156728
93611267 representatives in total.
Wed Oct 4 21:55:00 2023: Inserted ≈ 5% of D-proof conclusions. [ 4680563 of 93611267] (ETC: Wed Oct 4 21:55:49 2023 ; 49 s 476.76 ms remaining ; 52 s 80.80 ms total)
Wed Oct 4 21:55:02 2023: Inserted ≈10% of D-proof conclusions. [ 9361126 of 93611267] (ETC: Wed Oct 4 21:55:46 2023 ; 44 s 377.51 ms remaining ; 49 s 308.34 ms total)
Wed Oct 4 21:55:04 2023: Inserted ≈15% of D-proof conclusions. [14041690 of 93611267] (ETC: Wed Oct 4 21:55:43 2023 ; 38 s 849.03 ms remaining ; 45 s 704.74 ms total)
Wed Oct 4 21:55:06 2023: Inserted ≈20% of D-proof conclusions. [18722253 of 93611267] (ETC: Wed Oct 4 21:55:40 2023 ; 34 s 334.78 ms remaining ; 42 s 918.47 ms total)
Wed Oct 4 21:55:07 2023: Inserted ≈25% of D-proof conclusions. [23402816 of 93611267] (ETC: Wed Oct 4 21:55:38 2023 ; 30 s 866.36 ms remaining ; 41 s 155.14 ms total)
Wed Oct 4 21:55:09 2023: Inserted ≈30% of D-proof conclusions. [28083380 of 93611267] (ETC: Wed Oct 4 21:55:36 2023 ; 27 s 623.16 ms remaining ; 39 s 461.66 ms total)
Wed Oct 4 21:55:10 2023: Inserted ≈35% of D-proof conclusions. [32763943 of 93611267] (ETC: Wed Oct 4 21:55:35 2023 ; 24 s 603.73 ms remaining ; 37 s 851.89 ms total)
Wed Oct 4 21:55:12 2023: Inserted ≈40% of D-proof conclusions. [37444506 of 93611267] (ETC: Wed Oct 4 21:55:34 2023 ; 22 s 254.38 ms remaining ; 37 s 90.63 ms total)
Wed Oct 4 21:55:13 2023: Inserted ≈45% of D-proof conclusions. [42125070 of 93611267] (ETC: Wed Oct 4 21:55:33 2023 ; 19 s 936.08 ms remaining ; 36 s 247.41 ms total)
Wed Oct 4 21:55:15 2023: Inserted ≈50% of D-proof conclusions. [46805633 of 93611267] (ETC: Wed Oct 4 21:55:33 2023 ; 17 s 775.71 ms remaining ; 35 s 551.42 ms total)
Wed Oct 4 21:55:16 2023: Inserted ≈55% of D-proof conclusions. [51486196 of 93611267] (ETC: Wed Oct 4 21:55:32 2023 ; 15 s 853.47 ms remaining ; 35 s 229.93 ms total)
Wed Oct 4 21:55:18 2023: Inserted ≈60% of D-proof conclusions. [56166760 of 93611267] (ETC: Wed Oct 4 21:55:32 2023 ; 14 s 38.73 ms remaining ; 35 s 96.82 ms total)
Wed Oct 4 21:55:20 2023: Inserted ≈65% of D-proof conclusions. [60847323 of 93611267] (ETC: Wed Oct 4 21:55:32 2023 ; 12 s 252.50 ms remaining ; 35 s 7.13 ms total)
Wed Oct 4 21:55:22 2023: Inserted ≈70% of D-proof conclusions. [65527886 of 93611267] (ETC: Wed Oct 4 21:55:32 2023 ; 10 s 542.90 ms remaining ; 35 s 143.00 ms total)
Wed Oct 4 21:55:24 2023: Inserted ≈75% of D-proof conclusions. [70208450 of 93611267] (ETC: Wed Oct 4 21:55:33 2023 ; 8 s 874.51 ms remaining ; 35 s 498.05 ms total)
Wed Oct 4 21:55:26 2023: Inserted ≈80% of D-proof conclusions. [74889013 of 93611267] (ETC: Wed Oct 4 21:55:33 2023 ; 7 s 187.21 ms remaining ; 35 s 936.05 ms total)
Wed Oct 4 21:55:28 2023: Inserted ≈85% of D-proof conclusions. [79569576 of 93611267] (ETC: Wed Oct 4 21:55:33 2023 ; 5 s 455.75 ms remaining ; 36 s 371.65 ms total)
Wed Oct 4 21:55:30 2023: Inserted ≈90% of D-proof conclusions. [84250140 of 93611267] (ETC: Wed Oct 4 21:55:34 2023 ; 3 s 665.86 ms remaining ; 36 s 658.56 ms total)
Wed Oct 4 21:55:32 2023: Inserted ≈95% of D-proof conclusions. [88930703 of 93611267] (ETC: Wed Oct 4 21:55:34 2023 ; 1 s 860.62 ms remaining ; 37 s 212.36 ms total)
Wed Oct 4 21:55:35 2023: Inserted 100% of D-proof conclusions. [93611267 of 93611267] (ETC: Wed Oct 4 21:55:35 2023 ; 0.00 ms remaining ; 37 s 850.75 ms total)
37851.01 ms (37 s 851.01 ms) total insertion duration.
Wed Oct 4 21:55:35 2023: Starting to iterate D-proof candidates of length 75.
523842.95 ms (8 min 43 s 842.95 ms) taken to iterate 692977377 condensed detachment proof strings of length 75.
[Copy] Next iteration count (unfiltered71+): { 75, 692977377 }
Wed Oct 4 22:04:19 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Wed Oct 4 22:06:27 2023: Process terminated. [pid: 172053, tid:23321358104448]