( This log file was generated by executing 'pmGenerator -c -n -s CCpCCNpqrCsCCNtCrtCpt --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-OPTANE MPI node
— 2-socket Intel Xeon Gold 6338, 32 cores each (64 cores total per node), 2.0 GHz, 3.20 GHz turbo mode, 512 GiB DDR4-3200 caching for 2 TiB non-volatile memory (NVM) (Intel Optane DC Persistent Memory DIMMs) —
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
------------ ---------- ---------- ---------- -------- ---------- ----------
40717588 optane_low 64 COMPLETED 0:0 02:53:50
40717588.ba+ 64 COMPLETED 0:0 02:53:50 924093320K
40717588.ex+ 64 COMPLETED 0:0 02:53:50 0
By 924093320 KiB = (924093320 / 1024^2) GiB = 881.28406524658203125 GiB, it used approximately 881.28 gibibytes of memory. )
Sat Nov 11 03:59:52 2023: Process started. [pid: 115597, tid:23100977575808]
Tasks:
1. resetRepresentativesFor("CCpCCNpqrCsCCNtCrtCpt", true, 0, true)
2. countNextIterationAmount(false, true)
[Main] Calling resetRepresentativesFor("CCpCCNpqrCsCCNtCrtCpt", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: 02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c]
(1) CC0CCN0.1.2C3CCN4C2.4C0.4 - CCpCCNpqrCsCCNtCrtCpt - (0\imply((\not0\imply1)\imply2))\imply(3\imply((\not4\imply(2\imply4))\imply(0\imply4)))
[Main] Calling countNextIterationAmount(false, true).
Sat Nov 11 03:59:52 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered]
0.03 ms taken to load initial representatives.
0.07 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23100911023872]
0.69 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23100896315136]
2.37 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23100900517632]
0.63 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23100906821376]
3.11 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23100887910144]
5.73 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23100917327616]
3.97 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23100915226368]
6.24 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23100913125120]
8.39 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23100817143552]
12124.90 ms (12 s 124.90 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23100911023872]
3.17 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23100908922624]
13152.64 ms (13 s 152.64 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23100906821376]
2.73 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23100904720128]
0.50 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23100902618880]
12535.54 ms (12 s 535.54 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23100900517632]
2.47 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23100898416384]
12186.52 ms (12 s 186.52 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23100896315136]
1.18 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23100894213888]
0.94 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23100892112640]
5.53 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23100890011392]
13699.74 ms (13 s 699.74 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23100887910144]
10.84 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23100815042304]
4.61 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23100812941056]
10.19 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23100810839808]
2.73 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23100808738560]
10.56 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23100806637312]
14.47 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23100804536064]
18.89 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23100802434816]
16.13 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23100800333568]
10.92 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23100798232320]
2.17 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23100796131072]
17.76 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23100794029824]
22.12 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23100791928576]
18.66 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23100789827328]
396.19 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23100787726080]
11.59 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23100785624832]
17.54 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23100783523584]
30.67 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23100781422336]
41.58 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23100779321088]
69.00 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23100777219840]
31.03 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23100775118592]
28.37 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23100773017344]
22.52 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23100770916096]
45.49 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23100768814848]
111.21 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23100766713600]
38.81 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23100764612352]
44.98 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23100762511104]
662.21 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23100760409856]
538.39 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23100758308608]
520.67 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23100756207360]
288.34 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23100754106112]
583.71 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23099877619456]
395.65 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23099875518208]
549.50 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23099873416960]
1635.37 ms (1 s 635.37 ms) taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23099871315712]
2204.84 ms (2 s 204.84 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23099869214464]
2845.12 ms (2 s 845.12 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23099867113216]
3252.17 ms (3 s 252.17 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23099865011968]
5446.32 ms (5 s 446.32 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23099862910720]
6655.81 ms (6 s 655.81 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23099860809472]
9960.18 ms (9 s 960.18 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23099858708224]
3544.09 ms (3 s 544.09 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23099856606976]
3387.96 ms (3 s 387.96 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23099854505728]
4969.60 ms (4 s 969.60 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23099852404480]
5443.82 ms (5 s 443.82 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23099850303232]
5435.49 ms (5 s 435.50 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23099848201984]
7652.63 ms (7 s 652.63 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23099846100736]
7518.24 ms (7 s 518.24 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23099843999488]
9429.33 ms (9 s 429.33 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23099841898240]
14207.97 ms (14 s 207.97 ms) total read duration.
Loaded 70 representative collections of sizes:
1 : 1
3 : 1
5 : 2
7 : 2
9 : 1
11 : 0
13 : 1
15 : 2
17 : 3
19 : 4
21 : 5
23 : 5
25 : 5
27 : 6
29 : 7
31 : 15
33 : 20
35 : 25
37 : 30
39 : 37
41 : 42
43 : 51
45 : 63
47 : 85
49 : 122
51 : 162
53 : 206
55 : 251
57 : 292
59 : 339
61 : 444
63 : 598
65 : 781
67 : 1016
69 : 1303
71 : 1593
73 : 1922
75 : 2359
77 : 2986
79 : 3875
81 : 5006
83 : 6466
85 : 8184
87 : 10182
89 : 12488
91 : 15534
93 : 19614
95 : 25087
97 : 32452
99 : 41840
101 : 53343
103 : 67105
105 : 84222
107 : 105925
109 : 134564
111 : 172053
113 : 221055
115 : 283569
117 : 361751
119 : 458509
121 : 579502
123 : 734352
125 : 935212
127 : 1197027
129 : 1534565
131 : 1965596
133 : 2509883
135 : 3196594
137 : 4066027
139 : 5180139
24036508 representatives in total.
96021.62 ms (1 min 36 s 21.62 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23099841898240]
150557.60 ms (2 min 30 s 557.60 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:23099843999488]
215247.40 ms (3 min 35 s 247.40 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:23099846100736]
276961.10 ms (4 min 36 s 961.10 ms) taken to read 47814846 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. [tid:23099848201984]
352901.76 ms (5 min 52 s 901.75 ms) taken to read 62366737 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs149-unfiltered141+.txt. [tid:23099850303232]
395740.59 ms (6 min 35 s 740.59 ms) taken to read 82234537 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs151-unfiltered141+.txt. [tid:23099852404480]
437240.38 ms (7 min 17 s 240.38 ms) taken to read 109705510 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs153-unfiltered141+.txt. [tid:23099854505728]
481535.14 ms (8 min 1 s 535.14 ms) taken to read 144348401 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs155-unfiltered141+.txt. [tid:23099856606976]
517325.23 ms (8 min 37 s 325.23 ms) taken to read 192661720 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs157-unfiltered141+.txt. [tid:23099858708224]
548878.75 ms (9 min 8 s 878.75 ms) taken to read 253992520 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs159-unfiltered141+.txt. [tid:23099860809472]
549056.74 ms (9 min 9 s 56.74 ms) additional read duration.
Loaded 10 more representative collections of sizes:
141 : 16952082
143 : 26431403
145 : 36855440
147 : 47814846
149 : 62366737
151 : 82234537
153 : 109705510
155 : 144348401
157 : 192661720
159 : 253992520
997399704 representatives in total.
Sat Nov 11 04:10:21 2023: Inserted ≈ 5% of D-proof conclusions. [ 49869985 of 997399704] (ETC: Sat Nov 11 04:31:14 2023 ; 20 min 52 s 808.86 ms remaining ; 21 min 58 s 746.16 ms total)
Sat Nov 11 04:11:33 2023: Inserted ≈10% of D-proof conclusions. [ 99739970 of 997399704] (ETC: Sat Nov 11 04:32:11 2023 ; 20 min 38 s 385.39 ms remaining ; 22 min 55 s 983.76 ms total)
Sat Nov 11 04:12:54 2023: Inserted ≈15% of D-proof conclusions. [149609955 of 997399704] (ETC: Sat Nov 11 04:33:38 2023 ; 20 min 43 s 159.19 ms remaining ; 24 min 22 s 540.22 ms total)
Sat Nov 11 04:14:31 2023: Inserted ≈20% of D-proof conclusions. [199479940 of 997399704] (ETC: Sat Nov 11 04:35:37 2023 ; 21 min 5 s 290.69 ms remaining ; 26 min 21 s 613.36 ms total)
Sat Nov 11 04:16:03 2023: Inserted ≈25% of D-proof conclusions. [249349926 of 997399704] (ETC: Sat Nov 11 04:36:29 2023 ; 20 min 25 s 58.48 ms remaining ; 27 min 13 s 411.30 ms total)
Sat Nov 11 04:17:36 2023: Inserted ≈30% of D-proof conclusions. [299219911 of 997399704] (ETC: Sat Nov 11 04:37:05 2023 ; 19 min 28 s 951.83 ms remaining ; 27 min 49 s 931.18 ms total)
Sat Nov 11 04:18:57 2023: Inserted ≈35% of D-proof conclusions. [349089896 of 997399704] (ETC: Sat Nov 11 04:36:56 2023 ; 17 min 59 s 755.35 ms remaining ; 27 min 41 s 162.08 ms total)
Sat Nov 11 04:20:38 2023: Inserted ≈40% of D-proof conclusions. [398959881 of 997399704] (ETC: Sat Nov 11 04:37:42 2023 ; 17 min 4 s 120.79 ms remaining ; 28 min 26 s 867.99 ms total)
Sat Nov 11 04:22:19 2023: Inserted ≈45% of D-proof conclusions. [448829866 of 997399704] (ETC: Sat Nov 11 04:38:17 2023 ; 15 min 58 s 231.97 ms remaining ; 29 min 2 s 239.95 ms total)
Sat Nov 11 04:23:45 2023: Inserted ≈50% of D-proof conclusions. [498699852 of 997399704] (ETC: Sat Nov 11 04:38:14 2023 ; 14 min 29 s 434.30 ms remaining ; 28 min 58 s 868.60 ms total)
Sat Nov 11 04:25:09 2023: Inserted ≈55% of D-proof conclusions. [548569837 of 997399704] (ETC: Sat Nov 11 04:38:10 2023 ; 13 min 719.84 ms remaining ; 28 min 54 s 932.98 ms total)
Sat Nov 11 04:26:31 2023: Inserted ≈60% of D-proof conclusions. [598439822 of 997399704] (ETC: Sat Nov 11 04:38:01 2023 ; 11 min 30 s 366.38 ms remaining ; 28 min 45 s 915.94 ms total)
Sat Nov 11 04:27:52 2023: Inserted ≈65% of D-proof conclusions. [648309807 of 997399704] (ETC: Sat Nov 11 04:37:54 2023 ; 10 min 1 s 515.63 ms remaining ; 28 min 38 s 616.07 ms total)
Sat Nov 11 04:29:12 2023: Inserted ≈70% of D-proof conclusions. [698179792 of 997399704] (ETC: Sat Nov 11 04:37:44 2023 ; 8 min 32 s 748.77 ms remaining ; 28 min 29 s 162.57 ms total)
Sat Nov 11 04:30:39 2023: Inserted ≈75% of D-proof conclusions. [748049778 of 997399704] (ETC: Sat Nov 11 04:37:46 2023 ; 7 min 7 s 841.35 ms remaining ; 28 min 31 s 365.42 ms total)
Sat Nov 11 04:32:07 2023: Inserted ≈80% of D-proof conclusions. [797919763 of 997399704] (ETC: Sat Nov 11 04:37:50 2023 ; 5 min 43 s 55.76 ms remaining ; 28 min 35 s 278.78 ms total)
Sat Nov 11 04:33:40 2023: Inserted ≈85% of D-proof conclusions. [847789748 of 997399704] (ETC: Sat Nov 11 04:37:59 2023 ; 4 min 18 s 513.98 ms remaining ; 28 min 43 s 426.54 ms total)
Sat Nov 11 04:35:06 2023: Inserted ≈90% of D-proof conclusions. [897659733 of 997399704] (ETC: Sat Nov 11 04:37:58 2023 ; 2 min 52 s 301.26 ms remaining ; 28 min 43 s 12.63 ms total)
Sat Nov 11 04:36:25 2023: Inserted ≈95% of D-proof conclusions. [947529718 of 997399704] (ETC: Sat Nov 11 04:37:51 2023 ; 1 min 25 s 807.38 ms remaining ; 28 min 36 s 147.68 ms total)
Sat Nov 11 04:37:45 2023: Inserted 100% of D-proof conclusions. [997399704 of 997399704] (ETC: Sat Nov 11 04:37:45 2023 ; 0.00 ms remaining ; 28 min 29 s 591.41 ms total)
1709592.84 ms (28 min 29 s 592.84 ms) total insertion duration.
Sat Nov 11 04:37:45 2023: Starting to iterate D-proof candidates of length 161.
5200567.18 ms (1 h 26 min 40 s 567.18 ms) taken to iterate 3806955248 condensed detachment proof strings of length 161.
[Copy] Next iteration count (unfiltered141+): { 161, 3806955248 }
Sat Nov 11 06:04:36 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered]
Sat Nov 11 06:52:39 2023: Process terminated. [pid: 115597, tid:23100977575808]