( 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]