( 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%11" JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS ------------ ---------- ---------- ---------- -------- ---------- ----------- 40754284 optane_low 64 COMPLETED 0:0 03:52:56 40754284.ba+ 64 COMPLETED 0:0 03:52:56 1257111864K 40754284.ex+ 64 COMPLETED 0:0 03:52:56 40K By 1257111864 KiB = (1257111864 / 1024^2) GiB = 1198.87529754638671875 GiB, it used approximately 1198.88 gibibytes of memory. ) Tue Nov 14 09:34:23 2023: Process started. [pid: 208386, tid:23228290029440] 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). Tue Nov 14 09:34:23 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 0.47 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23228221376256] 1.94 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23228191958784] 2.78 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23228206667520] 1.30 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23228217173760] 0.80 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23228107949824] 1.80 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23228229781248] 9.07 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23228227680000] 9.54 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23228225578752] 7.24 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23228223477504] 11431.04 ms (11 s 431.04 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23228221376256] 6.46 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23228219275008] 12776.65 ms (12 s 776.65 ms) taken to read 4066027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. [tid:23228217173760] 14.51 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23228215072512] 6.75 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23228212971264] 3.29 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23228210870016] 21.71 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23228208768768] 12365.92 ms (12 s 365.92 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23228206667520] 2.93 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23228204566272] 16.16 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23228202465024] 9.69 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23228200363776] 2.78 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23228198262528] 3.98 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23228196161280] 8.38 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23228194060032] 11710.14 ms (11 s 710.14 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23228191958784] 22.14 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23228122658560] 6.61 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23228120557312] 1.17 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23228118456064] 9.03 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23228116354816] 10.99 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23228114253568] 2.66 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23228112152320] 9.12 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23228110051072] 13338.11 ms (13 s 338.11 ms) taken to read 5180139 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs139.txt. [tid:23228107949824] 15.48 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23228105848576] 9.48 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23228103747328] 18.61 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23228101646080] 15.02 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23228099544832] 22.66 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23228097443584] 35.40 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23228095342336] 32.10 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23228093241088] 26.02 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23228091139840] 37.21 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23228089038592] 47.23 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23228086937344] 40.81 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23228084836096] 44.61 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23228082734848] 45.07 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23228080633600] 59.12 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23228078532352] 37.64 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23228076431104] 248.65 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23228074329856] 759.30 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23228072228608] 69.25 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23228070127360] 288.73 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23228068026112] 732.86 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23228065924864] 1058.93 ms (1 s 58.94 ms) taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23228063823616] 1419.41 ms (1 s 419.41 ms) taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23228061722368] 223.14 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23228059621120] 1536.60 ms (1 s 536.60 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23226042283776] 1625.45 ms (1 s 625.45 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23226040182528] 1798.87 ms (1 s 798.87 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23226038081280] 4169.19 ms (4 s 169.19 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23226035980032] 6355.54 ms (6 s 355.54 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23226033878784] 8390.98 ms (8 s 390.98 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23226031777536] 3223.07 ms (3 s 223.07 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23226029676288] 3537.91 ms (3 s 537.91 ms) taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23226027575040] 4976.73 ms (4 s 976.73 ms) taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23226025473792] 4782.06 ms (4 s 782.06 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23226023372544] 1772.92 ms (1 s 772.92 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23226021271296] 6445.64 ms (6 s 445.64 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23226019170048] 7749.68 ms (7 s 749.68 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23226017068800] 9026.90 ms (9 s 26.90 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23226014967552] 13495.78 ms (13 s 495.78 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. 110306.18 ms (1 min 50 s 306.18 ms) taken to read 16952082 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs141-unfiltered141+.txt. [tid:23226014967552] 181923.19 ms (3 min 1 s 923.19 ms) taken to read 26431403 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs143-unfiltered141+.txt. [tid:23226017068800] 231842.57 ms (3 min 51 s 842.57 ms) taken to read 36855440 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs145-unfiltered141+.txt. [tid:23226019170048] 294620.93 ms (4 min 54 s 620.93 ms) taken to read 47814846 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs147-unfiltered141+.txt. [tid:23226021271296] 368105.36 ms (6 min 8 s 105.37 ms) taken to read 62366737 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs149-unfiltered141+.txt. [tid:23226023372544] 451393.51 ms (7 min 31 s 393.51 ms) taken to read 82234537 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs151-unfiltered141+.txt. [tid:23226025473792] 555356.10 ms (9 min 15 s 356.10 ms) taken to read 109705510 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs153-unfiltered141+.txt. [tid:23226027575040] 619239.07 ms (10 min 19 s 239.07 ms) taken to read 144348401 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs155-unfiltered141+.txt. [tid:23226029676288] 673126.50 ms (11 min 13 s 126.50 ms) taken to read 192661720 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs157-unfiltered141+.txt. [tid:23226031777536] 727934.86 ms (12 min 7 s 934.86 ms) taken to read 253992520 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs159-unfiltered141+.txt. [tid:23226033878784] 783115.86 ms (13 min 3 s 115.86 ms) taken to read 338777355 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs161-unfiltered141+.txt. [tid:23226035980032] 783164.75 ms (13 min 3 s 164.75 ms) additional read duration. Loaded 11 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 161 : 338777355 1336177059 representatives in total. Tue Nov 14 09:49:07 2023: Inserted ≈ 5% of D-proof conclusions. [ 66808852 of 1336177059] (ETC: Tue Nov 14 10:16:41 2023 ; 27 min 34 s 135.69 ms remaining ; 29 min 1 s 195.46 ms total) Tue Nov 14 09:50:53 2023: Inserted ≈10% of D-proof conclusions. [ 133617705 of 1336177059] (ETC: Tue Nov 14 10:19:50 2023 ; 28 min 57 s 58.09 ms remaining ; 32 min 10 s 64.54 ms total) Tue Nov 14 09:52:49 2023: Inserted ≈15% of D-proof conclusions. [ 200426558 of 1336177059] (ETC: Tue Nov 14 10:21:57 2023 ; 29 min 8 s 346.97 ms remaining ; 34 min 16 s 878.78 ms total) Tue Nov 14 09:55:01 2023: Inserted ≈20% of D-proof conclusions. [ 267235411 of 1336177059] (ETC: Tue Nov 14 10:24:24 2023 ; 29 min 22 s 810.35 ms remaining ; 36 min 43 s 512.94 ms total) Tue Nov 14 09:57:30 2023: Inserted ≈25% of D-proof conclusions. [ 334044264 of 1336177059] (ETC: Tue Nov 14 10:27:01 2023 ; 29 min 30 s 859.51 ms remaining ; 39 min 21 s 146.01 ms total) Tue Nov 14 10:00:00 2023: Inserted ≈30% of D-proof conclusions. [ 400853117 of 1336177059] (ETC: Tue Nov 14 10:28:47 2023 ; 28 min 46 s 894.77 ms remaining ; 41 min 6 s 992.53 ms total) Tue Nov 14 10:02:26 2023: Inserted ≈35% of D-proof conclusions. [ 467661970 of 1336177059] (ETC: Tue Nov 14 10:29:52 2023 ; 27 min 25 s 544.48 ms remaining ; 42 min 11 s 606.89 ms total) Tue Nov 14 10:04:49 2023: Inserted ≈40% of D-proof conclusions. [ 534470823 of 1336177059] (ETC: Tue Nov 14 10:30:32 2023 ; 25 min 43 s 326.47 ms remaining ; 42 min 52 s 210.78 ms total) Tue Nov 14 10:06:43 2023: Inserted ≈45% of D-proof conclusions. [ 601279676 of 1336177059] (ETC: Tue Nov 14 10:30:01 2023 ; 23 min 17 s 424.03 ms remaining ; 42 min 20 s 770.96 ms total) Tue Nov 14 10:08:53 2023: Inserted ≈50% of D-proof conclusions. [ 668088529 of 1336177059] (ETC: Tue Nov 14 10:30:06 2023 ; 21 min 12 s 989.02 ms remaining ; 42 min 25 s 978.03 ms total) Tue Nov 14 10:11:32 2023: Inserted ≈55% of D-proof conclusions. [ 734897382 of 1336177059] (ETC: Tue Nov 14 10:31:04 2023 ; 19 min 31 s 642.77 ms remaining ; 43 min 23 s 650.59 ms total) Tue Nov 14 10:13:34 2023: Inserted ≈60% of D-proof conclusions. [ 801706235 of 1336177059] (ETC: Tue Nov 14 10:30:50 2023 ; 17 min 15 s 846.76 ms remaining ; 43 min 9 s 616.90 ms total) Tue Nov 14 10:15:54 2023: Inserted ≈65% of D-proof conclusions. [ 868515088 of 1336177059] (ETC: Tue Nov 14 10:31:06 2023 ; 15 min 11 s 994.17 ms remaining ; 43 min 25 s 697.63 ms total) Tue Nov 14 10:18:07 2023: Inserted ≈70% of D-proof conclusions. [ 935323941 of 1336177059] (ETC: Tue Nov 14 10:31:10 2023 ; 13 min 2 s 914.31 ms remaining ; 43 min 29 s 714.35 ms total) Tue Nov 14 10:20:11 2023: Inserted ≈75% of D-proof conclusions. [1002132794 of 1336177059] (ETC: Tue Nov 14 10:31:02 2023 ; 10 min 50 s 429.26 ms remaining ; 43 min 21 s 717.03 ms total) Tue Nov 14 10:22:03 2023: Inserted ≈80% of D-proof conclusions. [1068941647 of 1336177059] (ETC: Tue Nov 14 10:30:39 2023 ; 8 min 35 s 824.51 ms remaining ; 42 min 59 s 122.57 ms total) Tue Nov 14 10:24:11 2023: Inserted ≈85% of D-proof conclusions. [1135750500 of 1336177059] (ETC: Tue Nov 14 10:30:38 2023 ; 6 min 26 s 671.33 ms remaining ; 42 min 57 s 808.87 ms total) Tue Nov 14 10:26:09 2023: Inserted ≈90% of D-proof conclusions. [1202559353 of 1336177059] (ETC: Tue Nov 14 10:30:26 2023 ; 4 min 16 s 605.50 ms remaining ; 42 min 46 s 54.95 ms total) Tue Nov 14 10:28:13 2023: Inserted ≈95% of D-proof conclusions. [1269368206 of 1336177059] (ETC: Tue Nov 14 10:30:21 2023 ; 2 min 8 s 46.63 ms remaining ; 42 min 40 s 932.53 ms total) Tue Nov 14 10:30:26 2023: Inserted 100% of D-proof conclusions. [1336177059 of 1336177059] (ETC: Tue Nov 14 10:30:26 2023 ; 0.00 ms remaining ; 42 min 45 s 681.78 ms total) 2565683.20 ms (42 min 45 s 683.20 ms) total insertion duration. Tue Nov 14 10:30:26 2023: Starting to iterate D-proof candidates of length 163. 7234586.58 ms (2 h 34 s 586.58 ms) taken to iterate 5149688506 condensed detachment proof strings of length 163. [Copy] Next iteration count (unfiltered141+): { 163, 5149688506 } Tue Nov 14 12:31:44 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Tue Nov 14 13:26:05 2023: Process terminated. [pid: 208386, tid:23228290029440]