( This log file was generated by executing 'pmGenerator -c -n -s CpCCNqCCNrsCtqCCrtCrq --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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40744891 optane_low 64 COMPLETED 0:0 01:46:22 40744891.ba+ 64 COMPLETED 0:0 01:46:22 807590844K 40744891.ex+ 64 COMPLETED 0:0 01:46:22 0 By 807590844 KiB = (807590844 / 1024^2) GiB = 770.178646087646484375 GiB, it used approximately 770.18 gibibytes of memory. ) Sat Nov 11 12:23:18 2023: Process started. [pid: 265722, tid:23110513694592] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CpCCNqCCNrsCtqCCrtCrq", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9] (1) C0CCN1CCN2.3C4.1CC2.4C2.1 - CpCCNqCCNrsCtqCCrtCrq - 0\imply((\not1\imply((\not2\imply3)\imply(4\imply1)))\imply((2\imply4)\imply(2\imply1))) [Main] Calling countNextIterationAmount(false, true). Sat Nov 11 12:23:18 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 1.36 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs11.txt. [tid:23110445041408] 1.88 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs7.txt. [tid:23110449243904] 1.87 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs15.txt. [tid:23110442940160] 1.29 ms taken to read 3 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs21.txt. [tid:23110436636416] 3.00 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs9.txt. [tid:23110447142656] 3.68 ms taken to read 707 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs67.txt. [tid:23110319286016] 3.89 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs19.txt. [tid:23110438737664] 0.43 ms taken to read 2 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs13.txt. [tid:23110308722432] 0.12 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs3.txt. [tid:23110453446400] 0.40 ms taken to read 5 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs17.txt. [tid:23110440838912] 0.12 ms taken to read 7 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs27.txt. [tid:23110430332672] 19126.97 ms (19 s 126.97 ms) taken to read 2983754 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs147.txt. [tid:23110453446400] 6.68 ms taken to read 1 condensed detachment proof and conclusion from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs5.txt. [tid:23110451345152] 8724.85 ms (8 s 724.85 ms) taken to read 693346 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs133.txt. [tid:23110449243904] 17296.36 ms (17 s 296.37 ms) taken to read 1294413 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs139.txt. [tid:23110447142656] 6763.53 ms (6 s 763.53 ms) taken to read 560926 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs131.txt. [tid:23110445041408] 19459.60 ms (19 s 459.60 ms) taken to read 2423655 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs145.txt. [tid:23110308722432] 9705.56 ms (9 s 705.56 ms) taken to read 853090 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs135.txt. [tid:23110442940160] 19927.02 ms (19 s 927.02 ms) taken to read 3676539 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs149.txt. [tid:23110440838912] 16923.11 ms (16 s 923.11 ms) taken to read 1963944 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs143.txt. [tid:23110438737664] 14767.25 ms (14 s 767.25 ms) taken to read 1051251 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs137.txt. [tid:23110436636416] 14.69 ms taken to read 6 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs23.txt. [tid:23110434535168] 5.10 ms taken to read 10 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs25.txt. [tid:23110432433920] 20595.01 ms (20 s 595.01 ms) taken to read 4527348 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs151.txt. [tid:23110430332672] 8.44 ms taken to read 12 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs29.txt. [tid:23110428231424] 0.01 ms taken to read 14 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs31.txt. [tid:23110426130176] 12.09 ms taken to read 17 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs33.txt. [tid:23110424028928] 12.10 ms taken to read 21 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs35.txt. [tid:23110421927680] 0.79 ms taken to read 30 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs37.txt. [tid:23110419826432] 2.91 ms taken to read 28 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs39.txt. [tid:23110417725184] 0.26 ms taken to read 44 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs41.txt. [tid:23110346602240] 0.25 ms taken to read 56 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs43.txt. [tid:23110344500992] 11.11 ms taken to read 66 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs45.txt. [tid:23110342399744] 11.02 ms taken to read 80 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs47.txt. [tid:23110340298496] 0.65 ms taken to read 108 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs49.txt. [tid:23110338197248] 34.96 ms taken to read 123 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs51.txt. [tid:23110336096000] 10.07 ms taken to read 168 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs53.txt. [tid:23110333994752] 58.66 ms taken to read 197 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs55.txt. [tid:23110331893504] 12.18 ms taken to read 241 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs57.txt. [tid:23110329792256] 6.19 ms taken to read 303 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs59.txt. [tid:23110327691008] 14.88 ms taken to read 390 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs61.txt. [tid:23110325589760] 2.05 ms taken to read 444 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs63.txt. [tid:23110323488512] 16.68 ms taken to read 570 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs65.txt. [tid:23110321387264] 15330.81 ms (15 s 330.81 ms) taken to read 1597383 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs141.txt. [tid:23110319286016] 46.74 ms taken to read 863 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs69.txt. [tid:23110317184768] 44.62 ms taken to read 1052 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs71.txt. [tid:23110315083520] 34.62 ms taken to read 1340 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs73.txt. [tid:23110312982272] 32.21 ms taken to read 1586 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs75.txt. [tid:23110310881024] 27.42 ms taken to read 1990 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs77.txt. [tid:23110306621184] 39.52 ms taken to read 2467 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs79.txt. [tid:23110304519936] 27.99 ms taken to read 3018 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs81.txt. [tid:23110302418688] 538.73 ms taken to read 3679 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs83.txt. [tid:23110300317440] 90.48 ms taken to read 4661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs85.txt. [tid:23110298216192] 49.08 ms taken to read 5632 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs87.txt. [tid:23110296114944] 577.16 ms taken to read 6994 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs89.txt. [tid:23110294013696] 466.35 ms taken to read 8637 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs91.txt. [tid:23110291912448] 335.35 ms taken to read 10677 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs93.txt. [tid:23110289811200] 973.03 ms taken to read 13008 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs95.txt. [tid:23110287709952] 1102.67 ms (1 s 102.67 ms) taken to read 16295 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs97.txt. [tid:23110285608704] 534.88 ms taken to read 19833 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs99.txt. [tid:23110283507456] 1005.03 ms (1 s 5.03 ms) taken to read 24567 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs101.txt. [tid:23108199118592] 1422.54 ms (1 s 422.54 ms) taken to read 30296 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs103.txt. [tid:23108197017344] 440.57 ms taken to read 37377 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs105.txt. [tid:23108194916096] 847.85 ms taken to read 45724 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs107.txt. [tid:23108192814848] 2129.82 ms (2 s 129.82 ms) taken to read 56922 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs109.txt. [tid:23108190713600] 2645.18 ms (2 s 645.18 ms) taken to read 69661 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs111.txt. [tid:23108188612352] 2564.70 ms (2 s 564.71 ms) taken to read 85894 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs113.txt. [tid:23108186511104] 4582.17 ms (4 s 582.17 ms) taken to read 105871 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs115.txt. [tid:23108184409856] 6484.32 ms (6 s 484.32 ms) taken to read 130737 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs117.txt. [tid:23108182308608] 7931.55 ms (7 s 931.55 ms) taken to read 160270 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs119.txt. [tid:23108180207360] 4527.75 ms (4 s 527.75 ms) taken to read 198446 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs121.txt. [tid:23108178106112] 4710.69 ms (4 s 710.69 ms) taken to read 243740 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs123.txt. [tid:23108176004864] 5092.48 ms (5 s 92.48 ms) taken to read 300530 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs125.txt. [tid:23108173903616] 5457.28 ms (5 s 457.28 ms) taken to read 370216 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs127.txt. [tid:23108171802368] 7593.33 ms (7 s 593.33 ms) taken to read 456911 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs129.txt. [tid:23108169701120] 20753.59 ms (20 s 753.59 ms) total read duration. Loaded 76 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 1 9 : 2 11 : 2 13 : 2 15 : 2 17 : 5 19 : 5 21 : 3 23 : 6 25 : 10 27 : 7 29 : 12 31 : 14 33 : 17 35 : 21 37 : 30 39 : 28 41 : 44 43 : 56 45 : 66 47 : 80 49 : 108 51 : 123 53 : 168 55 : 197 57 : 241 59 : 303 61 : 390 63 : 444 65 : 570 67 : 707 69 : 863 71 : 1052 73 : 1340 75 : 1586 77 : 1990 79 : 2467 81 : 3018 83 : 3679 85 : 4661 87 : 5632 89 : 6994 91 : 8637 93 : 10677 95 : 13008 97 : 16295 99 : 19833 101 : 24567 103 : 30296 105 : 37377 107 : 45724 109 : 56922 111 : 69661 113 : 85894 115 : 105871 117 : 130737 119 : 160270 121 : 198446 123 : 243740 125 : 300530 127 : 370216 129 : 456911 131 : 560926 133 : 693346 135 : 853090 137 : 1051251 139 : 1294413 141 : 1597383 143 : 1963944 145 : 2423655 147 : 2983754 149 : 3676539 151 : 4527348 24048210 representatives in total. 163959.60 ms (2 min 43 s 959.60 ms) taken to read 21395853 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs153-unfiltered153+.txt. [tid:23108169701120] 202844.99 ms (3 min 22 s 844.99 ms) taken to read 28040847 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs155-unfiltered153+.txt. [tid:23108171802368] 251006.29 ms (4 min 11 s 6.29 ms) taken to read 38836822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs157-unfiltered153+.txt. [tid:23108173903616] 282170.89 ms (4 min 42 s 170.90 ms) taken to read 50013506 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs159-unfiltered153+.txt. [tid:23108176004864] 346515.08 ms (5 min 46 s 515.08 ms) taken to read 78239557 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs161-unfiltered153+.txt. [tid:23108178106112] 377623.68 ms (6 min 17 s 623.68 ms) taken to read 101757325 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs163-unfiltered153+.txt. [tid:23108180207360] 444734.37 ms (7 min 24 s 734.37 ms) taken to read 147063822 condensed detachment proofs and conclusions from data/fe7117b8aad7634fae344172b9fee05f77e5e23b035276b17d8c6ec9/dProofs-withConclusions/dProofs165-unfiltered153+.txt. [tid:23108182308608] 444755.48 ms (7 min 24 s 755.48 ms) additional read duration. Loaded 7 more representative collections of sizes: 153 : 21395853 155 : 28040847 157 : 38836822 159 : 50013506 161 : 78239557 163 : 101757325 165 : 147063822 489395942 representatives in total. Sat Nov 11 12:31:56 2023: Inserted ≈ 5% of D-proof conclusions. [ 24469797 of 489395942] (ETC: Sat Nov 11 12:48:28 2023 ; 16 min 31 s 614.94 ms remaining ; 17 min 23 s 805.20 ms total) Sat Nov 11 12:33:00 2023: Inserted ≈10% of D-proof conclusions. [ 48939594 of 489395942] (ETC: Sat Nov 11 12:50:29 2023 ; 17 min 28 s 283.08 ms remaining ; 19 min 24 s 758.97 ms total) Sat Nov 11 12:34:08 2023: Inserted ≈15% of D-proof conclusions. [ 73409391 of 489395942] (ETC: Sat Nov 11 12:51:30 2023 ; 17 min 21 s 862.01 ms remaining ; 20 min 25 s 720.01 ms total) Sat Nov 11 12:35:20 2023: Inserted ≈20% of D-proof conclusions. [ 97879188 of 489395942] (ETC: Sat Nov 11 12:52:26 2023 ; 17 min 5 s 955.58 ms remaining ; 21 min 22 s 444.47 ms total) Sat Nov 11 12:36:29 2023: Inserted ≈25% of D-proof conclusions. [122348985 of 489395942] (ETC: Sat Nov 11 12:52:43 2023 ; 16 min 14 s 269.69 ms remaining ; 21 min 39 s 26.25 ms total) Sat Nov 11 12:37:40 2023: Inserted ≈30% of D-proof conclusions. [146818782 of 489395942] (ETC: Sat Nov 11 12:53:06 2023 ; 15 min 25 s 218.93 ms remaining ; 22 min 1 s 741.33 ms total) Sat Nov 11 12:38:55 2023: Inserted ≈35% of D-proof conclusions. [171288579 of 489395942] (ETC: Sat Nov 11 12:53:30 2023 ; 14 min 35 s 21.56 ms remaining ; 22 min 26 s 187.01 ms total) Sat Nov 11 12:40:08 2023: Inserted ≈40% of D-proof conclusions. [195758376 of 489395942] (ETC: Sat Nov 11 12:53:43 2023 ; 13 min 35 s 446.08 ms remaining ; 22 min 39 s 76.80 ms total) Sat Nov 11 12:41:31 2023: Inserted ≈45% of D-proof conclusions. [220228173 of 489395942] (ETC: Sat Nov 11 12:54:18 2023 ; 12 min 46 s 512.20 ms remaining ; 23 min 13 s 658.53 ms total) Sat Nov 11 12:42:53 2023: Inserted ≈50% of D-proof conclusions. [244697971 of 489395942] (ETC: Sat Nov 11 12:54:41 2023 ; 11 min 48 s 640.03 ms remaining ; 23 min 37 s 280.05 ms total) Sat Nov 11 12:43:53 2023: Inserted ≈55% of D-proof conclusions. [269167768 of 489395942] (ETC: Sat Nov 11 12:54:22 2023 ; 10 min 29 s 156.56 ms remaining ; 23 min 18 s 125.70 ms total) Sat Nov 11 12:44:59 2023: Inserted ≈60% of D-proof conclusions. [293637565 of 489395942] (ETC: Sat Nov 11 12:54:16 2023 ; 9 min 16 s 797.00 ms remaining ; 23 min 11 s 992.50 ms total) Sat Nov 11 12:46:29 2023: Inserted ≈65% of D-proof conclusions. [318107362 of 489395942] (ETC: Sat Nov 11 12:54:47 2023 ; 8 min 18 s 238.18 ms remaining ; 23 min 43 s 537.64 ms total) Sat Nov 11 12:47:57 2023: Inserted ≈70% of D-proof conclusions. [342577159 of 489395942] (ETC: Sat Nov 11 12:55:11 2023 ; 7 min 14 s 33.14 ms remaining ; 24 min 6 s 777.12 ms total) Sat Nov 11 12:49:05 2023: Inserted ≈75% of D-proof conclusions. [367046956 of 489395942] (ETC: Sat Nov 11 12:55:05 2023 ; 6 min 326.63 ms remaining ; 24 min 1 s 306.54 ms total) Sat Nov 11 12:50:14 2023: Inserted ≈80% of D-proof conclusions. [391516753 of 489395942] (ETC: Sat Nov 11 12:55:02 2023 ; 4 min 47 s 557.04 ms remaining ; 23 min 57 s 785.17 ms total) Sat Nov 11 12:51:19 2023: Inserted ≈85% of D-proof conclusions. [415986550 of 489395942] (ETC: Sat Nov 11 12:54:54 2023 ; 3 min 34 s 515.17 ms remaining ; 23 min 50 s 101.14 ms total) Sat Nov 11 12:52:33 2023: Inserted ≈90% of D-proof conclusions. [440456347 of 489395942] (ETC: Sat Nov 11 12:54:57 2023 ; 2 min 23 s 286.38 ms remaining ; 23 min 52 s 863.77 ms total) Sat Nov 11 12:53:56 2023: Inserted ≈95% of D-proof conclusions. [464926144 of 489395942] (ETC: Sat Nov 11 12:55:09 2023 ; 1 min 12 s 234.51 ms remaining ; 24 min 4 s 690.09 ms total) Sat Nov 11 12:55:27 2023: Inserted 100% of D-proof conclusions. [489395942 of 489395942] (ETC: Sat Nov 11 12:55:27 2023 ; 0.00 ms remaining ; 24 min 23 s 613.22 ms total) 1463617.32 ms (24 min 23 s 617.32 ms) total insertion duration. Sat Nov 11 12:55:28 2023: Starting to iterate D-proof candidates of length 167. 2767313.24 ms (46 min 7 s 313.24 ms) taken to iterate 2016753823 condensed detachment proof strings of length 167. [Copy] Next iteration count (unfiltered153+): { 167, 2016753823 } Sat Nov 11 13:42:24 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Sat Nov 11 14:08:57 2023: Process terminated. [pid: 265722, tid:23110513694592]