-
-
Notifications
You must be signed in to change notification settings - Fork 3
/
79.log
131 lines (130 loc) · 13.8 KB
/
79.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
( This log file was generated by executing 'pmGenerator -c -n -s CCCpqCCCNrNsrtCCtpCsp --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
------------ ---------- ---------- ---------- -------- ---------- ----------
40352656 c18m_low 48 COMPLETED 0:0 00:02:15
40352656.ba+ 48 COMPLETED 0:0 00:02:15 9811228K
40352656.ex+ 48 COMPLETED 0:0 00:02:15 0
By 9811228 KiB = (9811228 / 1024^2) GiB = 9.356716156005859375 GiB, it used approximately 9.36 gibibytes of memory. )
Wed Oct 25 13:48:25 2023: Process started. [pid: 80047, tid:22787730933632]
Tasks:
1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true)
2. countNextIterationAmount(false, true)
[Main] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69]
(1) CCC0.1CCCN2N3.2.4CC4.0C3.0 - CCCpqCCCNrNsrtCCtpCsp - ((0\imply1)\imply(((\not2\imply\not3)\imply2)\imply4))\imply((4\imply0)\imply(3\imply0))
[Main] Calling countNextIterationAmount(false, true).
Wed Oct 25 13:48:25 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered]
0.01 ms taken to load initial representatives.
11.61 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22787670685440]
17.72 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22787668584192]
19.42 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22787666482944]
13.45 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22787664381696]
23.51 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22787662280448]
26.01 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22787660179200]
26.94 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22787658077952]
17.21 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22787655976704]
23.91 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22787653875456]
20.74 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22787651774208]
29.31 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22787649672960]
22.09 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22787647571712]
13.23 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22787645470464]
19.98 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22787643369216]
29.34 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22787641267968]
30.12 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22787639166720]
23.85 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22787637065472]
30.98 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22787634964224]
37.27 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22787632862976]
72.44 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22787630761728]
57.09 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22787628660480]
52.41 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22787626559232]
74.32 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22787624457984]
76.95 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22787622356736]
117.84 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22786076571392]
165.88 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22786074470144]
305.25 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22786072368896]
502.85 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22786070267648]
968.47 ms taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22786068166400]
2126.13 ms (2 s 126.13 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22786066065152]
4403.20 ms (4 s 403.19 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22786063963904]
9786.03 ms (9 s 786.03 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22786061862656]
743.98 ms taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22786059761408]
1050.32 ms (1 s 50.32 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22786057660160]
1397.05 ms (1 s 397.05 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22786055558912]
1830.81 ms (1 s 830.81 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22786053457664]
2376.18 ms (2 s 376.18 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22786051356416]
2958.87 ms (2 s 958.87 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22786049255168]
3740.37 ms (3 s 740.37 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:22786047153920]
9810.95 ms (9 s 810.95 ms) total read duration.
Loaded 40 representative collections of sizes:
1 : 1
3 : 1
5 : 2
7 : 3
9 : 6
11 : 7
13 : 12
15 : 15
17 : 23
19 : 36
21 : 61
23 : 99
25 : 152
27 : 214
29 : 299
31 : 400
33 : 560
35 : 797
37 : 1162
39 : 1706
41 : 2502
43 : 3673
45 : 5333
47 : 7756
49 : 11285
51 : 16457
53 : 24156
55 : 35569
57 : 52769
59 : 78319
61 : 116867
63 : 174207
65 : 260535
67 : 389264
69 : 582969
71 : 872258
73 : 1307863
75 : 1959086
77 : 2940441
79 : 4409199
13256064 representatives in total.
Wed Oct 25 13:48:35 2023: Inserted ≈ 5% of D-proof conclusions. [ 662803 of 13256064] (ETC: Wed Oct 25 13:48:44 2023 ; 9 s 481.74 ms remaining ; 9 s 980.78 ms total)
Wed Oct 25 13:48:36 2023: Inserted ≈10% of D-proof conclusions. [ 1325606 of 13256064] (ETC: Wed Oct 25 13:48:44 2023 ; 8 s 931.96 ms remaining ; 9 s 924.40 ms total)
Wed Oct 25 13:48:36 2023: Inserted ≈15% of D-proof conclusions. [ 1988409 of 13256064] (ETC: Wed Oct 25 13:48:44 2023 ; 8 s 477.72 ms remaining ; 9 s 973.78 ms total)
Wed Oct 25 13:48:36 2023: Inserted ≈20% of D-proof conclusions. [ 2651212 of 13256064] (ETC: Wed Oct 25 13:48:44 2023 ; 7 s 721.80 ms remaining ; 9 s 652.25 ms total)
Wed Oct 25 13:48:37 2023: Inserted ≈25% of D-proof conclusions. [ 3314016 of 13256064] (ETC: Wed Oct 25 13:48:44 2023 ; 6 s 857.70 ms remaining ; 9 s 143.60 ms total)
Wed Oct 25 13:48:37 2023: Inserted ≈30% of D-proof conclusions. [ 3976819 of 13256064] (ETC: Wed Oct 25 13:48:43 2023 ; 6 s 248.60 ms remaining ; 8 s 926.57 ms total)
Wed Oct 25 13:48:38 2023: Inserted ≈35% of D-proof conclusions. [ 4639622 of 13256064] (ETC: Wed Oct 25 13:48:43 2023 ; 5 s 786.26 ms remaining ; 8 s 901.94 ms total)
Wed Oct 25 13:48:38 2023: Inserted ≈40% of D-proof conclusions. [ 5302425 of 13256064] (ETC: Wed Oct 25 13:48:43 2023 ; 5 s 142.45 ms remaining ; 8 s 570.75 ms total)
Wed Oct 25 13:48:38 2023: Inserted ≈45% of D-proof conclusions. [ 5965228 of 13256064] (ETC: Wed Oct 25 13:48:43 2023 ; 4 s 595.16 ms remaining ; 8 s 354.83 ms total)
Wed Oct 25 13:48:39 2023: Inserted ≈50% of D-proof conclusions. [ 6628032 of 13256064] (ETC: Wed Oct 25 13:48:43 2023 ; 4 s 108.82 ms remaining ; 8 s 217.65 ms total)
Wed Oct 25 13:48:39 2023: Inserted ≈55% of D-proof conclusions. [ 7290835 of 13256064] (ETC: Wed Oct 25 13:48:43 2023 ; 3 s 630.98 ms remaining ; 8 s 68.84 ms total)
Wed Oct 25 13:48:39 2023: Inserted ≈60% of D-proof conclusions. [ 7953638 of 13256064] (ETC: Wed Oct 25 13:48:42 2023 ; 3 s 173.30 ms remaining ; 7 s 933.24 ms total)
Wed Oct 25 13:48:40 2023: Inserted ≈65% of D-proof conclusions. [ 8616441 of 13256064] (ETC: Wed Oct 25 13:48:42 2023 ; 2 s 749.11 ms remaining ; 7 s 854.59 ms total)
Wed Oct 25 13:48:40 2023: Inserted ≈70% of D-proof conclusions. [ 9279244 of 13256064] (ETC: Wed Oct 25 13:48:42 2023 ; 2 s 347.61 ms remaining ; 7 s 825.37 ms total)
Wed Oct 25 13:48:40 2023: Inserted ≈75% of D-proof conclusions. [ 9942048 of 13256064] (ETC: Wed Oct 25 13:48:42 2023 ; 1 s 956.56 ms remaining ; 7 s 826.23 ms total)
Wed Oct 25 13:48:41 2023: Inserted ≈80% of D-proof conclusions. [10604851 of 13256064] (ETC: Wed Oct 25 13:48:42 2023 ; 1 s 570.36 ms remaining ; 7 s 851.79 ms total)
Wed Oct 25 13:48:41 2023: Inserted ≈85% of D-proof conclusions. [11267654 of 13256064] (ETC: Wed Oct 25 13:48:42 2023 ; 1 s 169.14 ms remaining ; 7 s 794.27 ms total)
Wed Oct 25 13:48:42 2023: Inserted ≈90% of D-proof conclusions. [11930457 of 13256064] (ETC: Wed Oct 25 13:48:42 2023 ; 776.59 ms remaining ; 7 s 765.88 ms total)
Wed Oct 25 13:48:42 2023: Inserted ≈95% of D-proof conclusions. [12593260 of 13256064] (ETC: Wed Oct 25 13:48:42 2023 ; 384.34 ms remaining ; 7 s 686.78 ms total)
Wed Oct 25 13:48:42 2023: Inserted 100% of D-proof conclusions. [13256064 of 13256064] (ETC: Wed Oct 25 13:48:42 2023 ; 0.00 ms remaining ; 7 s 579.37 ms total)
7579.85 ms (7 s 579.85 ms) total insertion duration.
Wed Oct 25 13:48:42 2023: Starting to iterate D-proof candidates of length 81.
98966.11 ms (1 min 38 s 966.11 ms) taken to iterate 176882404 condensed detachment proof strings of length 81.
[Copy] Next iteration count (filtered): { 81, 176882404 }
Wed Oct 25 13:50:21 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered]
Wed Oct 25 13:50:36 2023: Process terminated. [pid: 80047, tid:22787730933632]