forked from xamidi/pmGenerator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path75-71.log
130 lines (129 loc) · 13.9 KB
/
75-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
( 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
------------ ---------- ---------- ---------- -------- ---------- ----------
39734329 c18m 48 COMPLETED 0:0 00:18:00
39734329.ba+ 48 COMPLETED 0:0 00:18:00 101941908K
39734329.ex+ 48 COMPLETED 0:0 00:18:00 76K
By 101941908 KiB = (101941908 / 1024^2) GiB = 97.219379425048828125 GiB, it used approximately 97.22 gibibytes of memory. )
Thu Oct 5 08:33:24 2023: Process started. [pid: 167857, tid:22845139355520]
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).
Thu Oct 5 08:33:24 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
7.67 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22845079107328]
25.87 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22845077006080]
21.23 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22845074904832]
18.19 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22845072803584]
4.91 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22845070702336]
16.33 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22845068601088]
8.12 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22844662609664]
22.96 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22844528391936]
15.41 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22844660508416]
19.87 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22844658407168]
21.79 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22844656305920]
12.75 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22844654204672]
24.93 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22844652103424]
8.53 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22844650002176]
23.05 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22844647900928]
92.36 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22844645799680]
39.32 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22844643698432]
51.89 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22844641597184]
56.14 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22844639495936]
75.74 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22844637394688]
73.61 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22844635293440]
96.61 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22844633192192]
176.30 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22844631090944]
369.87 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22844628989696]
825.63 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22844626888448]
2093.06 ms (2 s 93.06 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22844624787200]
5098.63 ms (5 s 98.63 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22844622685952]
539.08 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22844620584704]
863.96 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22844618483456]
1384.24 ms (1 s 384.24 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22844616382208]
2085.85 ms (2 s 85.85 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22844614280960]
2659.45 ms (2 s 659.45 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22844612179712]
3724.82 ms (3 s 724.82 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22844610078464]
5321.18 ms (5 s 321.18 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22844607977216]
5342.41 ms (5 s 342.41 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.
14436.70 ms (14 s 436.70 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:22844607977216]
26545.86 ms (26 s 545.86 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:22844610078464]
41716.56 ms (41 s 716.56 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:22844612179712]
41719.96 ms (41 s 719.96 ms) additional read duration.
Loaded 3 more representative collections of sizes:
71 : 23150845
73 : 45156728
75 : 80141395
173752662 representatives in total.
Thu Oct 5 08:34:18 2023: Inserted ≈ 5% of D-proof conclusions. [ 8687633 of 173752662] (ETC: Thu Oct 5 08:36:16 2023 ; 1 min 58 s 651.70 ms remaining ; 2 min 4 s 896.52 ms total)
Thu Oct 5 08:34:23 2023: Inserted ≈10% of D-proof conclusions. [ 17375266 of 173752662] (ETC: Thu Oct 5 08:36:03 2023 ; 1 min 40 s 325.21 ms remaining ; 1 min 51 s 472.45 ms total)
Thu Oct 5 08:34:27 2023: Inserted ≈15% of D-proof conclusions. [ 26062899 of 173752662] (ETC: Thu Oct 5 08:35:56 2023 ; 1 min 28 s 506.80 ms remaining ; 1 min 44 s 125.65 ms total)
Thu Oct 5 08:34:31 2023: Inserted ≈20% of D-proof conclusions. [ 34750532 of 173752662] (ETC: Thu Oct 5 08:35:51 2023 ; 1 min 19 s 406.47 ms remaining ; 1 min 39 s 258.09 ms total)
Thu Oct 5 08:34:35 2023: Inserted ≈25% of D-proof conclusions. [ 43438165 of 173752662] (ETC: Thu Oct 5 08:35:47 2023 ; 1 min 11 s 903.85 ms remaining ; 1 min 35 s 871.80 ms total)
Thu Oct 5 08:34:39 2023: Inserted ≈30% of D-proof conclusions. [ 52125798 of 173752662] (ETC: Thu Oct 5 08:35:44 2023 ; 1 min 4 s 926.21 ms remaining ; 1 min 32 s 751.73 ms total)
Thu Oct 5 08:34:43 2023: Inserted ≈35% of D-proof conclusions. [ 60813431 of 173752662] (ETC: Thu Oct 5 08:35:41 2023 ; 58 s 538.01 ms remaining ; 1 min 30 s 58.48 ms total)
Thu Oct 5 08:34:47 2023: Inserted ≈40% of D-proof conclusions. [ 69501064 of 173752662] (ETC: Thu Oct 5 08:35:40 2023 ; 53 s 432.52 ms remaining ; 1 min 29 s 54.21 ms total)
Thu Oct 5 08:34:52 2023: Inserted ≈45% of D-proof conclusions. [ 78188697 of 173752662] (ETC: Thu Oct 5 08:35:41 2023 ; 49 s 231.70 ms remaining ; 1 min 29 s 512.18 ms total)
Thu Oct 5 08:34:55 2023: Inserted ≈50% of D-proof conclusions. [ 86876331 of 173752662] (ETC: Thu Oct 5 08:35:39 2023 ; 44 s 5.88 ms remaining ; 1 min 28 s 11.76 ms total)
Thu Oct 5 08:34:59 2023: Inserted ≈55% of D-proof conclusions. [ 95563964 of 173752662] (ETC: Thu Oct 5 08:35:38 2023 ; 38 s 845.52 ms remaining ; 1 min 26 s 323.39 ms total)
Thu Oct 5 08:35:02 2023: Inserted ≈60% of D-proof conclusions. [104251597 of 173752662] (ETC: Thu Oct 5 08:35:35 2023 ; 33 s 530.56 ms remaining ; 1 min 23 s 826.40 ms total)
Thu Oct 5 08:35:05 2023: Inserted ≈65% of D-proof conclusions. [112939230 of 173752662] (ETC: Thu Oct 5 08:35:34 2023 ; 29 s 10.69 ms remaining ; 1 min 22 s 887.69 ms total)
Thu Oct 5 08:35:08 2023: Inserted ≈70% of D-proof conclusions. [121626863 of 173752662] (ETC: Thu Oct 5 08:35:33 2023 ; 24 s 338.55 ms remaining ; 1 min 21 s 128.50 ms total)
Thu Oct 5 08:35:11 2023: Inserted ≈75% of D-proof conclusions. [130314496 of 173752662] (ETC: Thu Oct 5 08:35:31 2023 ; 19 s 912.03 ms remaining ; 1 min 19 s 648.13 ms total)
Thu Oct 5 08:35:15 2023: Inserted ≈80% of D-proof conclusions. [139002129 of 173752662] (ETC: Thu Oct 5 08:35:31 2023 ; 15 s 953.09 ms remaining ; 1 min 19 s 765.45 ms total)
Thu Oct 5 08:35:19 2023: Inserted ≈85% of D-proof conclusions. [147689762 of 173752662] (ETC: Thu Oct 5 08:35:31 2023 ; 11 s 879.35 ms remaining ; 1 min 19 s 195.69 ms total)
Thu Oct 5 08:35:23 2023: Inserted ≈90% of D-proof conclusions. [156377395 of 173752662] (ETC: Thu Oct 5 08:35:30 2023 ; 7 s 898.41 ms remaining ; 1 min 18 s 984.09 ms total)
Thu Oct 5 08:35:26 2023: Inserted ≈95% of D-proof conclusions. [165065028 of 173752662] (ETC: Thu Oct 5 08:35:30 2023 ; 3 s 936.21 ms remaining ; 1 min 18 s 724.13 ms total)
Thu Oct 5 08:35:30 2023: Inserted 100% of D-proof conclusions. [173752662 of 173752662] (ETC: Thu Oct 5 08:35:30 2023 ; 0.00 ms remaining ; 1 min 18 s 493.92 ms total)
78495.09 ms (1 min 18 s 495.09 ms) total insertion duration.
Thu Oct 5 08:35:30 2023: Starting to iterate D-proof candidates of length 77.
769711.36 ms (12 min 49 s 711.36 ms) taken to iterate 1198182438 condensed detachment proof strings of length 77.
[Copy] Next iteration count (unfiltered71+): { 77, 1198182438 }
Thu Oct 5 08:48:20 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Thu Oct 5 08:51:14 2023: Process terminated. [pid: 167857, tid:22845139355520]