( This log file was generated by 'pmGenerator 1.2' (master branch), compiled by 'Intel(R) oneAPI DPC++/C++ Compiler 2022.1.0 (2022.1.0.20220316)'. The run was executed on a CLAIX-2018 MPI node — 2-socket Intel Xeon Platinum 8160 (Skylake), 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory — running Linux, Rocky 8.8. Wall-clock time: 7.751666… h CPU utilization: 372.08 core-h ) Thu Oct 5 00:07:15 2023: Process started. [pid: 4678, tid:23146311763840] Tasks: 1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(75, false, true) [Main] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed] (1) CCCCC0.1CN2N3.2.4CC4.0C3.0 - CCCCCpqCNrNsrtCCtpCsp - ((((0\imply1)\imply(\not2\imply\not3))\imply2)\imply4)\imply((4\imply0)\imply(3\imply0)) [Main] Calling generateDProofRepresentativeFiles(75, false, true). Thu Oct 5 00:07:15 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 75, unfiltered] 0.03 ms taken to load initial representatives. 24.55 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:23146251515648] 17.21 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:23146249414400] 20.92 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:23146247313152] 28.42 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:23146245211904] 20.63 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:23146243110656] 25.85 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:23146241009408] 12.81 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:23146238908160] 17.95 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:23146236806912] 26.09 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:23146234705664] 18.17 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:23146232604416] 19.46 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:23146230503168] 20.95 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:23146228401920] 22.23 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:23146226300672] 26.48 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:23146224199424] 28.97 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:23146222098176] 43.89 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:23146219996928] 29.84 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:23146217895680] 53.74 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:23146215794432] 66.84 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:23146213693184] 76.97 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:23146211591936] 72.70 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:23146209490688] 102.74 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:23146207389440] 184.95 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:23146205288192] 383.63 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:23146203186944] 850.93 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:23146201085696] 2152.24 ms (2 s 152.24 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:23146198984448] 5134.95 ms (5 s 134.95 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:23146196883200] 623.66 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:23146194781952] 765.54 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:23146192680704] 1190.68 ms (1 s 190.68 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:23146190579456] 1761.74 ms (1 s 761.74 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:23146188478208] 2352.09 ms (2 s 352.09 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:23146186376960] 3328.03 ms (3 s 328.03 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:23144370796288] 4864.28 ms (4 s 864.27 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:23144368695040] 5155.04 ms (5 s 155.04 ms) total read duration. Loaded 35 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 7 11 : 10 13 : 13 15 : 19 17 : 37 19 : 56 21 : 87 23 : 140 25 : 227 27 : 369 29 : 579 31 : 918 33 : 1499 35 : 2408 37 : 3881 39 : 6254 41 : 10109 43 : 16460 45 : 26753 47 : 43360 49 : 70709 51 : 115604 53 : 188634 55 : 308241 57 : 504870 59 : 827701 61 : 1357539 63 : 2227822 65 : 3660735 67 : 6021110 69 : 9907537 25303694 representatives in total. 11393.55 ms (11 s 393.55 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:23144368695040] 20517.39 ms (20 s 517.39 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:23144370796288] 20519.59 ms (20 s 519.59 ms) additional read duration. Loaded 2 more representative collections of sizes: 71 : 23150845 73 : 45156728 93611267 representatives in total. Thu Oct 5 00:07:43 2023: Inserted ≈ 5% of D-proof conclusions. [ 4680563 of 93611267] (ETC: Thu Oct 5 00:08:31 2023 ; 47 s 729.52 ms remaining ; 50 s 241.60 ms total) Thu Oct 5 00:07:45 2023: Inserted ≈10% of D-proof conclusions. [ 9361126 of 93611267] (ETC: Thu Oct 5 00:08:25 2023 ; 40 s 341.16 ms remaining ; 44 s 823.51 ms total) Thu Oct 5 00:07:47 2023: Inserted ≈15% of D-proof conclusions. [14041690 of 93611267] (ETC: Thu Oct 5 00:08:22 2023 ; 35 s 181.54 ms remaining ; 41 s 390.05 ms total) Thu Oct 5 00:07:48 2023: Inserted ≈20% of D-proof conclusions. [18722253 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 31 s 623.88 ms remaining ; 39 s 529.85 ms total) Thu Oct 5 00:07:50 2023: Inserted ≈25% of D-proof conclusions. [23402816 of 93611267] (ETC: Thu Oct 5 00:08:19 2023 ; 29 s 122.73 ms remaining ; 38 s 830.30 ms total) Thu Oct 5 00:07:52 2023: Inserted ≈30% of D-proof conclusions. [28083380 of 93611267] (ETC: Thu Oct 5 00:08:19 2023 ; 26 s 998.56 ms remaining ; 38 s 569.37 ms total) Thu Oct 5 00:07:54 2023: Inserted ≈35% of D-proof conclusions. [32763943 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 25 s 559.51 ms remaining ; 39 s 322.32 ms total) Thu Oct 5 00:07:57 2023: Inserted ≈40% of D-proof conclusions. [37444506 of 93611267] (ETC: Thu Oct 5 00:08:21 2023 ; 24 s 397.67 ms remaining ; 40 s 662.78 ms total) Thu Oct 5 00:07:59 2023: Inserted ≈45% of D-proof conclusions. [42125070 of 93611267] (ETC: Thu Oct 5 00:08:21 2023 ; 22 s 509.86 ms remaining ; 40 s 927.01 ms total) Thu Oct 5 00:08:00 2023: Inserted ≈50% of D-proof conclusions. [46805633 of 93611267] (ETC: Thu Oct 5 00:08:21 2023 ; 20 s 161.06 ms remaining ; 40 s 322.11 ms total) Thu Oct 5 00:08:02 2023: Inserted ≈55% of D-proof conclusions. [51486196 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 17 s 993.86 ms remaining ; 39 s 986.35 ms total) Thu Oct 5 00:08:04 2023: Inserted ≈60% of D-proof conclusions. [56166760 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 15 s 838.62 ms remaining ; 39 s 596.54 ms total) Thu Oct 5 00:08:06 2023: Inserted ≈65% of D-proof conclusions. [60847323 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 13 s 775.04 ms remaining ; 39 s 357.25 ms total) Thu Oct 5 00:08:08 2023: Inserted ≈70% of D-proof conclusions. [65527886 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 11 s 772.11 ms remaining ; 39 s 240.38 ms total) Thu Oct 5 00:08:10 2023: Inserted ≈75% of D-proof conclusions. [70208450 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 9 s 874.38 ms remaining ; 39 s 497.52 ms total) Thu Oct 5 00:08:12 2023: Inserted ≈80% of D-proof conclusions. [74889013 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 7 s 914.36 ms remaining ; 39 s 571.78 ms total) Thu Oct 5 00:08:14 2023: Inserted ≈85% of D-proof conclusions. [79569576 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 5 s 940.59 ms remaining ; 39 s 603.91 ms total) Thu Oct 5 00:08:16 2023: Inserted ≈90% of D-proof conclusions. [84250140 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 3 s 968.46 ms remaining ; 39 s 684.62 ms total) Thu Oct 5 00:08:18 2023: Inserted ≈95% of D-proof conclusions. [88930703 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 1 s 998.31 ms remaining ; 39 s 966.10 ms total) Thu Oct 5 00:08:20 2023: Inserted 100% of D-proof conclusions. [93611267 of 93611267] (ETC: Thu Oct 5 00:08:20 2023 ; 0.00 ms remaining ; 40 s 16.81 ms total) 40017.14 ms (40 s 17.14 ms) total insertion duration. Known iteration count loaded from 75:692977377. Thu Oct 5 00:08:20 2023: Starting to generate D-proof representatives of length 75. Thu Oct 5 00:21:55 2023: Iterated ≈ 2% of D-proof candidates. [ 13859547 of 692977377] (ETC: Thu Oct 5 11:26:59 2023 ; 11 h 5 min 3 s 815.39 ms remaining ; 11 h 18 min 38 s 178.94 ms total) Thu Oct 5 00:33:50 2023: Iterated ≈ 4% of D-proof candidates. [ 27719095 of 692977377] (ETC: Thu Oct 5 10:45:43 2023 ; 10 h 11 min 53 s 102.85 ms remaining ; 10 h 37 min 22 s 815.46 ms total) Thu Oct 5 00:44:22 2023: Iterated ≈ 6% of D-proof candidates. [ 41578642 of 692977377] (ETC: Thu Oct 5 10:08:47 2023 ; 9 h 24 min 24 s 723.10 ms remaining ; 10 h 26 s 301.14 ms total) Thu Oct 5 00:55:31 2023: Iterated ≈ 8% of D-proof candidates. [ 55438190 of 692977377] (ETC: Thu Oct 5 09:58:07 2023 ; 9 h 2 min 35 s 375.59 ms remaining ; 9 h 49 min 46 s 277.80 ms total) Thu Oct 5 01:05:45 2023: Iterated ≈10% of D-proof candidates. [ 69297737 of 692977377] (ETC: Thu Oct 5 09:42:30 2023 ; 8 h 36 min 44 s 889.18 ms remaining ; 9 h 34 min 9 s 876.83 ms total) Thu Oct 5 01:15:09 2023: Iterated ≈12% of D-proof candidates. [ 83157285 of 692977377] (ETC: Thu Oct 5 09:25:03 2023 ; 8 h 9 min 54 s 585.22 ms remaining ; 9 h 16 min 42 s 937.74 ms total) Thu Oct 5 01:25:44 2023: Iterated ≈14% of D-proof candidates. [ 97016832 of 692977377] (ETC: Thu Oct 5 09:21:10 2023 ; 7 h 55 min 26 s 231.10 ms remaining ; 9 h 12 min 50 s 36.12 ms total) Thu Oct 5 01:35:41 2023: Iterated ≈16% of D-proof candidates. [110876380 of 692977377] (ETC: Thu Oct 5 09:14:15 2023 ; 7 h 38 min 33 s 652.05 ms remaining ; 9 h 5 min 54 s 347.66 ms total) Thu Oct 5 01:45:49 2023: Iterated ≈18% of D-proof candidates. [124735927 of 692977377] (ETC: Thu Oct 5 09:09:54 2023 ; 7 h 24 min 4 s 406.92 ms remaining ; 9 h 1 min 33 s 179.12 ms total) Thu Oct 5 01:55:01 2023: Iterated ≈20% of D-proof candidates. [138595475 of 692977377] (ETC: Thu Oct 5 09:01:43 2023 ; 7 h 6 min 41 s 763.24 ms remaining ; 8 h 53 min 22 s 204.03 ms total) Thu Oct 5 02:04:16 2023: Iterated ≈22% of D-proof candidates. [152455022 of 692977377] (ETC: Thu Oct 5 08:55:19 2023 ; 6 h 51 min 2 s 502.21 ms remaining ; 8 h 46 min 58 s 592.52 ms total) Thu Oct 5 02:13:23 2023: Iterated ≈24% of D-proof candidates. [166314570 of 692977377] (ETC: Thu Oct 5 08:49:21 2023 ; 6 h 35 min 58 s 137.00 ms remaining ; 8 h 41 min 706.54 ms total) Thu Oct 5 02:22:48 2023: Iterated ≈26% of D-proof candidates. [180174118 of 692977377] (ETC: Thu Oct 5 08:45:31 2023 ; 6 h 22 min 42 s 618.54 ms remaining ; 8 h 37 min 10 s 565.59 ms total) Thu Oct 5 02:31:32 2023: Iterated ≈28% of D-proof candidates. [194033665 of 692977377] (ETC: Thu Oct 5 08:39:43 2023 ; 6 h 8 min 11 s 552.58 ms remaining ; 8 h 31 min 22 s 711.88 ms total) Thu Oct 5 02:40:38 2023: Iterated ≈30% of D-proof candidates. [207893213 of 692977377] (ETC: Thu Oct 5 08:35:58 2023 ; 5 h 55 min 20 s 669.33 ms remaining ; 8 h 27 min 38 s 99.04 ms total) Thu Oct 5 02:50:00 2023: Iterated ≈32% of D-proof candidates. [221752760 of 692977377] (ETC: Thu Oct 5 08:33:33 2023 ; 5 h 43 min 32 s 551.01 ms remaining ; 8 h 25 min 12 s 574.97 ms total) Thu Oct 5 02:58:58 2023: Iterated ≈34% of D-proof candidates. [235612308 of 692977377] (ETC: Thu Oct 5 08:30:11 2023 ; 5 h 31 min 13 s 316.85 ms remaining ; 8 h 21 min 51 s 86.13 ms total) Thu Oct 5 03:07:50 2023: Iterated ≈36% of D-proof candidates. [249471855 of 692977377] (ETC: Thu Oct 5 08:26:55 2023 ; 5 h 19 min 5 s 421.74 ms remaining ; 8 h 18 min 34 s 721.41 ms total) Thu Oct 5 03:17:01 2023: Iterated ≈38% of D-proof candidates. [263331403 of 692977377] (ETC: Thu Oct 5 08:24:50 2023 ; 5 h 7 min 49 s 726.04 ms remaining ; 8 h 16 min 29 s 880.70 ms total) Thu Oct 5 03:26:25 2023: Iterated ≈40% of D-proof candidates. [277190950 of 692977377] (ETC: Thu Oct 5 08:23:32 2023 ; 4 h 57 min 6 s 764.66 ms remaining ; 8 h 15 min 11 s 274.38 ms total) Thu Oct 5 03:35:11 2023: Iterated ≈42% of D-proof candidates. [291050498 of 692977377] (ETC: Thu Oct 5 08:20:49 2023 ; 4 h 45 min 38 s 186.96 ms remaining ; 8 h 12 min 28 s 598.18 ms total) Thu Oct 5 03:44:10 2023: Iterated ≈44% of D-proof candidates. [304910045 of 692977377] (ETC: Thu Oct 5 08:18:51 2023 ; 4 h 34 min 41 s 134.63 ms remaining ; 8 h 10 min 30 s 597.48 ms total) Thu Oct 5 03:52:57 2023: Iterated ≈46% of D-proof candidates. [318769593 of 692977377] (ETC: Thu Oct 5 08:16:37 2023 ; 4 h 23 min 40 s 172.59 ms remaining ; 8 h 8 min 16 s 615.88 ms total) Thu Oct 5 04:01:29 2023: Iterated ≈48% of D-proof candidates. [332629140 of 692977377] (ETC: Thu Oct 5 08:14:03 2023 ; 4 h 12 min 34 s 136.31 ms remaining ; 8 h 5 min 42 s 569.75 ms total) Thu Oct 5 04:10:01 2023: Iterated ≈50% of D-proof candidates. [346488688 of 692977377] (ETC: Thu Oct 5 08:11:41 2023 ; 4 h 1 min 40 s 528.72 ms remaining ; 8 h 3 min 21 s 57.41 ms total) Thu Oct 5 04:18:23 2023: Iterated ≈52% of D-proof candidates. [360348236 of 692977377] (ETC: Thu Oct 5 08:09:11 2023 ; 3 h 50 min 48 s 542.62 ms remaining ; 8 h 51 s 130.46 ms total) Thu Oct 5 04:26:53 2023: Iterated ≈54% of D-proof candidates. [374207783 of 692977377] (ETC: Thu Oct 5 08:07:08 2023 ; 3 h 40 min 14 s 680.97 ms remaining ; 7 h 58 min 47 s 567.28 ms total) Thu Oct 5 04:35:16 2023: Iterated ≈56% of D-proof candidates. [388067331 of 692977377] (ETC: Thu Oct 5 08:04:59 2023 ; 3 h 29 min 43 s 463.22 ms remaining ; 7 h 56 min 38 s 780.04 ms total) Thu Oct 5 04:43:27 2023: Iterated ≈58% of D-proof candidates. [401926878 of 692977377] (ETC: Thu Oct 5 08:02:41 2023 ; 3 h 19 min 13 s 398.30 ms remaining ; 7 h 54 min 20 s 472.08 ms total) Thu Oct 5 04:51:44 2023: Iterated ≈60% of D-proof candidates. [415786426 of 692977377] (ETC: Thu Oct 5 08:00:39 2023 ; 3 h 8 min 55 s 399.95 ms remaining ; 7 h 52 min 18 s 499.86 ms total) Thu Oct 5 05:00:05 2023: Iterated ≈62% of D-proof candidates. [429645973 of 692977377] (ETC: Thu Oct 5 07:58:53 2023 ; 2 h 58 min 48 s 402.48 ms remaining ; 7 h 50 min 32 s 638.02 ms total) Thu Oct 5 05:08:23 2023: Iterated ≈64% of D-proof candidates. [443505521 of 692977377] (ETC: Thu Oct 5 07:57:10 2023 ; 2 h 48 min 46 s 500.03 ms remaining ; 7 h 48 min 49 s 166.73 ms total) Thu Oct 5 05:16:36 2023: Iterated ≈66% of D-proof candidates. [457365068 of 692977377] (ETC: Thu Oct 5 07:55:24 2023 ; 2 h 38 min 48 s 171.43 ms remaining ; 7 h 47 min 4 s 33.53 ms total) Thu Oct 5 05:24:42 2023: Iterated ≈68% of D-proof candidates. [471224616 of 692977377] (ETC: Thu Oct 5 07:53:35 2023 ; 2 h 28 min 52 s 692.08 ms remaining ; 7 h 45 min 14 s 662.71 ms total) Thu Oct 5 05:32:46 2023: Iterated ≈70% of D-proof candidates. [485084163 of 692977377] (ETC: Thu Oct 5 07:51:48 2023 ; 2 h 19 min 2 s 304.88 ms remaining ; 7 h 43 min 27 s 682.81 ms total) Thu Oct 5 05:40:50 2023: Iterated ≈72% of D-proof candidates. [498943711 of 692977377] (ETC: Thu Oct 5 07:50:08 2023 ; 2 h 9 min 18 s 136.16 ms remaining ; 7 h 41 min 47 s 629.08 ms total) Thu Oct 5 05:48:52 2023: Iterated ≈74% of D-proof candidates. [512803258 of 692977377] (ETC: Thu Oct 5 07:48:30 2023 ; 1 h 59 min 38 s 617.46 ms remaining ; 7 h 40 min 10 s 67.01 ms total) Thu Oct 5 05:56:57 2023: Iterated ≈76% of D-proof candidates. [526662806 of 692977377] (ETC: Thu Oct 5 07:47:02 2023 ; 1 h 50 min 5 s 174.74 ms remaining ; 7 h 38 min 41 s 561.35 ms total) Thu Oct 5 06:04:58 2023: Iterated ≈78% of D-proof candidates. [540522354 of 692977377] (ETC: Thu Oct 5 07:45:34 2023 ; 1 h 40 min 35 s 294.78 ms remaining ; 7 h 37 min 13 s 158.07 ms total) Thu Oct 5 06:12:58 2023: Iterated ≈80% of D-proof candidates. [554381901 of 692977377] (ETC: Thu Oct 5 07:44:07 2023 ; 1 h 31 min 9 s 319.30 ms remaining ; 7 h 35 min 46 s 596.38 ms total) Thu Oct 5 06:20:53 2023: Iterated ≈82% of D-proof candidates. [568241449 of 692977377] (ETC: Thu Oct 5 07:42:40 2023 ; 1 h 21 min 46 s 755.30 ms remaining ; 7 h 34 min 19 s 751.64 ms total) Thu Oct 5 06:28:48 2023: Iterated ≈84% of D-proof candidates. [582100996 of 692977377] (ETC: Thu Oct 5 07:41:16 2023 ; 1 h 12 min 28 s 39.91 ms remaining ; 7 h 32 min 55 s 249.30 ms total) Thu Oct 5 06:36:41 2023: Iterated ≈86% of D-proof candidates. [595960544 of 692977377] (ETC: Thu Oct 5 07:39:54 2023 ; 1 h 3 min 13 s 146.40 ms remaining ; 7 h 31 min 33 s 902.79 ms total) Thu Oct 5 06:44:32 2023: Iterated ≈88% of D-proof candidates. [609820091 of 692977377] (ETC: Thu Oct 5 07:38:34 2023 ; 54 min 1 s 621.50 ms remaining ; 7 h 30 min 13 s 512.27 ms total) Thu Oct 5 06:52:22 2023: Iterated ≈90% of D-proof candidates. [623679639 of 692977377] (ETC: Thu Oct 5 07:37:16 2023 ; 44 min 53 s 546.01 ms remaining ; 7 h 28 min 55 s 459.97 ms total) Thu Oct 5 07:00:09 2023: Iterated ≈92% of D-proof candidates. [637539186 of 692977377] (ETC: Thu Oct 5 07:35:58 2023 ; 35 min 48 s 575.75 ms remaining ; 7 h 27 min 37 s 196.48 ms total) Thu Oct 5 07:07:57 2023: Iterated ≈94% of D-proof candidates. [651398734 of 692977377] (ETC: Thu Oct 5 07:34:44 2023 ; 26 min 47 s 33.17 ms remaining ; 7 h 26 min 23 s 885.92 ms total) Thu Oct 5 07:15:46 2023: Iterated ≈96% of D-proof candidates. [665258281 of 692977377] (ETC: Thu Oct 5 07:33:34 2023 ; 17 min 48 s 550.93 ms remaining ; 7 h 25 min 13 s 772.45 ms total) Thu Oct 5 07:23:31 2023: Iterated ≈98% of D-proof candidates. [679117829 of 692977377] (ETC: Thu Oct 5 07:32:24 2023 ; 8 min 52 s 875.25 ms remaining ; 7 h 24 min 3 s 761.42 ms total) Thu Oct 5 07:31:14 2023: Iterated 100% of D-proof candidates. [692977377 of 692977377] (ETC: Thu Oct 5 07:31:14 2023 ; 0.00 ms remaining ; 7 h 22 min 53 s 469.70 ms total) 26574214.22 ms (7 h 22 min 54 s 214.22 ms) taken to collect 80141395 D-proofs of length 75. [iterated 692977377 condensed detachment proof strings] [Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 3 }, { 9, 8 }, { 11, 21 }, { 13, 40 }, { 15, 69 }, { 17, 126 }, { 19, 247 }, { 21, 442 }, { 23, 756 }, { 25, 1314 }, { 27, 2311 }, { 29, 4012 }, { 31, 6851 }, { 33, 11656 }, { 35, 19943 }, { 37, 33920 }, { 39, 57366 }, { 41, 96836 }, { 43, 163405 }, { 45, 275584 }, { 47, 463792 }, { 49, 779092 }, { 51, 1308757 }, { 53, 2198024 }, { 55, 3688065 }, { 57, 6183668 }, { 59, 10366617 }, { 61, 17377700 }, { 63, 29119708 }, { 65, 48779702 }, { 67, 81708667 }, { 69, 136861838 }, { 71, 229211380 }, { 73, 397509772 }, { 75, 692977377 } } 818364.83 ms (13 min 38 s 364.83 ms) taken to filter and order new representative proofs. Found 80141395 representative, 357473791 redundant, and 255362191 invalid condensed detachment proof strings. lengths up to 75 ; amounts per length: {(1,1), (3,1), (5,1), (7,3), (9,7), (11,10), (13,13), (15,19), (17,37), (19,56), (21,87), (23,140), (25,227), (27,369), (29,579), (31,918), (33,1499), (35,2408), (37,3881), (39,6254), (41,10109), (43,16460), (45,26753), (47,43360), (49,70709), (51,115604), (53,188634), (55,308241), (57,504870), (59,827701), (61,1357539), (63,2227822), (65,3660735), (67,6021110), (69,9907537), (71,23150845), (73,45156728), (75,80141395)} ; 80141395 new representative proofs (357473791 redundant, 255362191 invalid) Thu Oct 5 07:45:49 2023: Starting to write 80141395 entries to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. 100161.86 ms (1 min 40 s 161.86 ms) taken to print and save 15912038278 bytes of representative condensed detachment proof strings to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. Thu Oct 5 07:48:31 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 75, unfiltered] Thu Oct 5 07:52:21 2023: Process terminated. [pid: 4678, tid:23146311763840]