( 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-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. Wall-clock time: 11.5980555… h CPU utilization: 742.27555… core-h ) Thu Oct 26 17:56:30 2023: Process started. [pid: 214617, tid:22424174839680] Tasks: 1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(77, 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(77, false, true). Thu Oct 26 17:56:30 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 77, unfiltered] 0.02 ms taken to load initial representatives. 22.36 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22424114591488] 7.85 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22424112490240] 20.29 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22424110388992] 18.26 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22424108287744] 25.79 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22424106186496] 8.06 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22424104085248] 19.39 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22424101984000] 18.05 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22424099882752] 18.60 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22424097781504] 15.56 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22424095680256] 14.32 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22424093579008] 31.43 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22423890032384] 21.29 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22423887931136] 36.55 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22423885829888] 32.80 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22423883728640] 193.36 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22423881627392] 35.22 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22423879526144] 183.87 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22423877424896] 185.43 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22423875323648] 329.46 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22423873222400] 45.05 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22423871121152] 194.26 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22423869019904] 222.22 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22423866918656] 293.86 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22423864817408] 524.11 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22423862716160] 1240.58 ms (1 s 240.58 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22423860614912] 4122.33 ms (4 s 122.33 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22423858513664] 1017.16 ms (1 s 17.16 ms) taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22423856412416] 2583.18 ms (2 s 583.19 ms) taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22423854311168] 3662.44 ms (3 s 662.44 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22423852209920] 3652.39 ms (3 s 652.39 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22423850108672] 4584.62 ms (4 s 584.62 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22423848007424] 5359.07 ms (5 s 359.07 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22423845906176] 6357.85 ms (6 s 357.85 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22423843804928] 6432.01 ms (6 s 432.01 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. 11956.25 ms (11 s 956.25 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:22423843804928] 21447.75 ms (21 s 447.75 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:22423845906176] 32292.25 ms (32 s 292.25 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:22423848007424] 32300.94 ms (32 s 300.94 ms) additional read duration. Loaded 3 more representative collections of sizes: 71 : 23150845 73 : 45156728 75 : 80141395 173752662 representatives in total. Thu Oct 26 17:57:17 2023: Inserted ≈ 5% of D-proof conclusions. [ 8687633 of 173752662] (ETC: Thu Oct 26 18:00:01 2023 ; 2 min 43 s 993.05 ms remaining ; 2 min 52 s 624.26 ms total) Thu Oct 26 17:57:27 2023: Inserted ≈10% of D-proof conclusions. [ 17375266 of 173752662] (ETC: Thu Oct 26 18:00:10 2023 ; 2 min 43 s 666.60 ms remaining ; 3 min 1 s 851.77 ms total) Thu Oct 26 17:57:36 2023: Inserted ≈15% of D-proof conclusions. [ 26062899 of 173752662] (ETC: Thu Oct 26 18:00:11 2023 ; 2 min 35 s 232.62 ms remaining ; 3 min 2 s 626.62 ms total) Thu Oct 26 17:57:44 2023: Inserted ≈20% of D-proof conclusions. [ 34750532 of 173752662] (ETC: Thu Oct 26 18:00:08 2023 ; 2 min 23 s 581.05 ms remaining ; 2 min 59 s 476.31 ms total) Thu Oct 26 17:57:54 2023: Inserted ≈25% of D-proof conclusions. [ 43438165 of 173752662] (ETC: Thu Oct 26 18:00:10 2023 ; 2 min 16 s 457.77 ms remaining ; 3 min 1 s 943.69 ms total) Thu Oct 26 17:58:03 2023: Inserted ≈30% of D-proof conclusions. [ 52125798 of 173752662] (ETC: Thu Oct 26 18:00:11 2023 ; 2 min 7 s 721.59 ms remaining ; 3 min 2 s 459.41 ms total) Thu Oct 26 17:58:11 2023: Inserted ≈35% of D-proof conclusions. [ 60813431 of 173752662] (ETC: Thu Oct 26 18:00:08 2023 ; 1 min 56 s 819.50 ms remaining ; 2 min 59 s 722.30 ms total) Thu Oct 26 17:58:20 2023: Inserted ≈40% of D-proof conclusions. [ 69501064 of 173752662] (ETC: Thu Oct 26 18:00:08 2023 ; 1 min 47 s 553.77 ms remaining ; 2 min 59 s 256.28 ms total) Thu Oct 26 17:58:28 2023: Inserted ≈45% of D-proof conclusions. [ 78188697 of 173752662] (ETC: Thu Oct 26 18:00:06 2023 ; 1 min 37 s 799.19 ms remaining ; 2 min 57 s 816.72 ms total) Thu Oct 26 17:58:37 2023: Inserted ≈50% of D-proof conclusions. [ 86876331 of 173752662] (ETC: Thu Oct 26 18:00:06 2023 ; 1 min 28 s 651.79 ms remaining ; 2 min 57 s 303.58 ms total) Thu Oct 26 17:58:45 2023: Inserted ≈55% of D-proof conclusions. [ 95563964 of 173752662] (ETC: Thu Oct 26 18:00:04 2023 ; 1 min 19 s 162.69 ms remaining ; 2 min 55 s 917.08 ms total) Thu Oct 26 17:58:52 2023: Inserted ≈60% of D-proof conclusions. [104251597 of 173752662] (ETC: Thu Oct 26 18:00:02 2023 ; 1 min 9 s 411.64 ms remaining ; 2 min 53 s 529.09 ms total) Thu Oct 26 17:59:00 2023: Inserted ≈65% of D-proof conclusions. [112939230 of 173752662] (ETC: Thu Oct 26 18:00:00 2023 ; 1 min 141.32 ms remaining ; 2 min 51 s 832.35 ms total) Thu Oct 26 17:59:08 2023: Inserted ≈70% of D-proof conclusions. [121626863 of 173752662] (ETC: Thu Oct 26 17:59:59 2023 ; 51 s 184.56 ms remaining ; 2 min 50 s 615.19 ms total) Thu Oct 26 17:59:16 2023: Inserted ≈75% of D-proof conclusions. [130314496 of 173752662] (ETC: Thu Oct 26 17:59:58 2023 ; 42 s 497.27 ms remaining ; 2 min 49 s 989.07 ms total) Thu Oct 26 17:59:24 2023: Inserted ≈80% of D-proof conclusions. [139002129 of 173752662] (ETC: Thu Oct 26 17:59:58 2023 ; 33 s 962.78 ms remaining ; 2 min 49 s 813.88 ms total) Thu Oct 26 17:59:31 2023: Inserted ≈85% of D-proof conclusions. [147689762 of 173752662] (ETC: Thu Oct 26 17:59:56 2023 ; 25 s 225.01 ms remaining ; 2 min 48 s 166.71 ms total) Thu Oct 26 17:59:38 2023: Inserted ≈90% of D-proof conclusions. [156377395 of 173752662] (ETC: Thu Oct 26 17:59:54 2023 ; 16 s 605.92 ms remaining ; 2 min 46 s 59.18 ms total) Thu Oct 26 17:59:44 2023: Inserted ≈95% of D-proof conclusions. [165065028 of 173752662] (ETC: Thu Oct 26 17:59:52 2023 ; 8 s 204.84 ms remaining ; 2 min 44 s 96.90 ms total) Thu Oct 26 17:59:52 2023: Inserted 100% of D-proof conclusions. [173752662 of 173752662] (ETC: Thu Oct 26 17:59:52 2023 ; 0.00 ms remaining ; 2 min 44 s 126.91 ms total) 164127.11 ms (2 min 44 s 127.11 ms) total insertion duration. Known iteration count loaded from 77:1198182438. Thu Oct 26 17:59:52 2023: Starting to generate D-proof representatives of length 77. Thu Oct 26 18:15:13 2023: Iterated ≈ 2% of D-proof candidates. [ 23963648 of 1198182438] (ETC: Fri Oct 27 06:47:22 2023 ; 12 h 32 min 8 s 283.41 ms remaining ; 12 h 47 min 29 s 268.76 ms total) Thu Oct 26 18:30:24 2023: Iterated ≈ 4% of D-proof candidates. [ 47927297 of 1198182438] (ETC: Fri Oct 27 06:43:11 2023 ; 12 h 12 min 46 s 277.13 ms remaining ; 12 h 43 min 18 s 205.32 ms total) Thu Oct 26 18:45:32 2023: Iterated ≈ 6% of D-proof candidates. [ 71890946 of 1198182438] (ETC: Fri Oct 27 06:40:55 2023 ; 11 h 55 min 23 s 52.36 ms remaining ; 12 h 41 min 2 s 821.64 ms total) Thu Oct 26 19:01:22 2023: Iterated ≈ 8% of D-proof candidates. [ 95854595 of 1198182438] (ETC: Fri Oct 27 06:48:34 2023 ; 11 h 47 min 11 s 837.90 ms remaining ; 12 h 48 min 41 s 562.93 ms total) Thu Oct 26 19:16:31 2023: Iterated ≈10% of D-proof candidates. [ 119818243 of 1198182438] (ETC: Fri Oct 27 06:46:23 2023 ; 11 h 29 min 51 s 231.89 ms remaining ; 12 h 46 min 30 s 257.62 ms total) Thu Oct 26 19:30:29 2023: Iterated ≈12% of D-proof candidates. [ 143781892 of 1198182438] (ETC: Fri Oct 27 06:35:01 2023 ; 11 h 4 min 31 s 152.13 ms remaining ; 12 h 35 min 8 s 127.39 ms total) Thu Oct 26 19:45:36 2023: Iterated ≈14% of D-proof candidates. [ 167745541 of 1198182438] (ETC: Fri Oct 27 06:35:04 2023 ; 10 h 49 min 27 s 958.50 ms remaining ; 12 h 35 min 11 s 579.64 ms total) Thu Oct 26 20:00:20 2023: Iterated ≈16% of D-proof candidates. [ 191709190 of 1198182438] (ETC: Fri Oct 27 06:32:43 2023 ; 10 h 32 min 22 s 847.44 ms remaining ; 12 h 32 min 50 s 56.47 ms total) Thu Oct 26 20:15:00 2023: Iterated ≈18% of D-proof candidates. [ 215672838 of 1198182438] (ETC: Fri Oct 27 06:30:32 2023 ; 10 h 15 min 32 s 446.24 ms remaining ; 12 h 30 min 39 s 568.55 ms total) Thu Oct 26 20:28:51 2023: Iterated ≈20% of D-proof candidates. [ 239636487 of 1198182438] (ETC: Fri Oct 27 06:24:46 2023 ; 9 h 55 min 55 s 223.65 ms remaining ; 12 h 24 min 54 s 29.53 ms total) Thu Oct 26 20:42:48 2023: Iterated ≈22% of D-proof candidates. [ 263600136 of 1198182438] (ETC: Fri Oct 27 06:20:25 2023 ; 9 h 37 min 37 s 632.94 ms remaining ; 12 h 20 min 32 s 862.72 ms total) Thu Oct 26 20:56:23 2023: Iterated ≈24% of D-proof candidates. [ 287563785 of 1198182438] (ETC: Fri Oct 27 06:15:18 2023 ; 9 h 18 min 55 s 306.69 ms remaining ; 12 h 15 min 25 s 403.54 ms total) Thu Oct 26 21:09:43 2023: Iterated ≈26% of D-proof candidates. [ 311527433 of 1198182438] (ETC: Fri Oct 27 06:10:02 2023 ; 9 h 19 s 326.61 ms remaining ; 12 h 10 min 9 s 900.78 ms total) Thu Oct 26 21:23:22 2023: Iterated ≈28% of D-proof candidates. [ 335491082 of 1198182438] (ETC: Fri Oct 27 06:06:39 2023 ; 8 h 43 min 16 s 748.24 ms remaining ; 12 h 6 min 46 s 594.75 ms total) Thu Oct 26 21:36:30 2023: Iterated ≈30% of D-proof candidates. [ 359454731 of 1198182438] (ETC: Fri Oct 27 06:01:58 2023 ; 8 h 25 min 27 s 668.85 ms remaining ; 12 h 2 min 5 s 241.20 ms total) Thu Oct 26 21:50:01 2023: Iterated ≈32% of D-proof candidates. [ 383418380 of 1198182438] (ETC: Fri Oct 27 05:59:03 2023 ; 8 h 9 min 2 s 257.05 ms remaining ; 11 h 59 min 10 s 378.00 ms total) Thu Oct 26 22:03:45 2023: Iterated ≈34% of D-proof candidates. [ 407382028 of 1198182438] (ETC: Fri Oct 27 05:57:10 2023 ; 7 h 53 min 25 s 66.60 ms remaining ; 11 h 57 min 17 s 979.64 ms total) Thu Oct 26 22:16:56 2023: Iterated ≈36% of D-proof candidates. [ 431345677 of 1198182438] (ETC: Fri Oct 27 05:53:56 2023 ; 7 h 37 min 18.03 ms remaining ; 11 h 54 min 3 s 778.14 ms total) Thu Oct 26 22:30:27 2023: Iterated ≈38% of D-proof candidates. [ 455309326 of 1198182438] (ETC: Fri Oct 27 05:51:55 2023 ; 7 h 21 min 27 s 905.13 ms remaining ; 11 h 52 min 2 s 427.61 ms total) Thu Oct 26 22:44:17 2023: Iterated ≈40% of D-proof candidates. [ 479272975 of 1198182438] (ETC: Fri Oct 27 05:50:53 2023 ; 7 h 6 min 36 s 424.19 ms remaining ; 11 h 51 min 706.97 ms total) Thu Oct 26 22:58:03 2023: Iterated ≈42% of D-proof candidates. [ 503236623 of 1198182438] (ETC: Fri Oct 27 05:49:48 2023 ; 6 h 51 min 45 s 523.90 ms remaining ; 11 h 49 min 55 s 730.81 ms total) Thu Oct 26 23:11:29 2023: Iterated ≈44% of D-proof candidates. [ 527200272 of 1198182438] (ETC: Fri Oct 27 05:48:06 2023 ; 6 h 36 min 36 s 131.96 ms remaining ; 11 h 48 min 13 s 92.73 ms total) Thu Oct 26 23:24:50 2023: Iterated ≈46% of D-proof candidates. [ 551163921 of 1198182438] (ETC: Fri Oct 27 05:46:18 2023 ; 6 h 21 min 28 s 175.47 ms remaining ; 11 h 46 min 25 s 510.09 ms total) Thu Oct 26 23:38:04 2023: Iterated ≈48% of D-proof candidates. [ 575127570 of 1198182438] (ETC: Fri Oct 27 05:44:26 2023 ; 6 h 6 min 22 s 217.45 ms remaining ; 11 h 44 min 33 s 495.08 ms total) Thu Oct 26 23:51:02 2023: Iterated ≈50% of D-proof candidates. [ 599091219 of 1198182438] (ETC: Fri Oct 27 05:42:12 2023 ; 5 h 51 min 9 s 945.23 ms remaining ; 11 h 42 min 19 s 890.45 ms total) Fri Oct 27 00:03:59 2023: Iterated ≈52% of D-proof candidates. [ 623054867 of 1198182438] (ETC: Fri Oct 27 05:40:04 2023 ; 5 h 36 min 5 s 662.19 ms remaining ; 11 h 40 min 11 s 796.17 ms total) Fri Oct 27 00:16:50 2023: Iterated ≈54% of D-proof candidates. [ 647018516 of 1198182438] (ETC: Fri Oct 27 05:37:56 2023 ; 5 h 21 min 6 s 549.48 ms remaining ; 11 h 38 min 3 s 803.18 ms total) Fri Oct 27 00:29:35 2023: Iterated ≈56% of D-proof candidates. [ 670982165 of 1198182438] (ETC: Fri Oct 27 05:35:47 2023 ; 5 h 6 min 12 s 66.26 ms remaining ; 11 h 35 min 54 s 696.02 ms total) Fri Oct 27 00:42:19 2023: Iterated ≈58% of D-proof candidates. [ 694945814 of 1198182438] (ETC: Fri Oct 27 05:33:44 2023 ; 4 h 51 min 25 s 139.92 ms remaining ; 11 h 33 min 51 s 285.52 ms total) Fri Oct 27 00:55:09 2023: Iterated ≈60% of D-proof candidates. [ 718909462 of 1198182438] (ETC: Fri Oct 27 05:32:00 2023 ; 4 h 36 min 51 s 15.40 ms remaining ; 11 h 32 min 7 s 538.42 ms total) Fri Oct 27 01:07:58 2023: Iterated ≈62% of D-proof candidates. [ 742873111 of 1198182438] (ETC: Fri Oct 27 05:30:21 2023 ; 4 h 22 min 22 s 970.37 ms remaining ; 11 h 30 min 28 s 869.35 ms total) Fri Oct 27 01:20:39 2023: Iterated ≈64% of D-proof candidates. [ 766836760 of 1198182438] (ETC: Fri Oct 27 05:28:35 2023 ; 4 h 7 min 56 s 228.23 ms remaining ; 11 h 28 min 42 s 856.17 ms total) Fri Oct 27 01:33:22 2023: Iterated ≈66% of D-proof candidates. [ 790800409 of 1198182438] (ETC: Fri Oct 27 05:26:59 2023 ; 3 h 53 min 37 s 71.11 ms remaining ; 11 h 27 min 6 s 679.72 ms total) Fri Oct 27 01:45:54 2023: Iterated ≈68% of D-proof candidates. [ 814764057 of 1198182438] (ETC: Fri Oct 27 05:25:13 2023 ; 3 h 39 min 18 s 439.75 ms remaining ; 11 h 25 min 20 s 124.12 ms total) Fri Oct 27 01:58:30 2023: Iterated ≈70% of D-proof candidates. [ 838727706 of 1198182438] (ETC: Fri Oct 27 05:23:37 2023 ; 3 h 25 min 7 s 497.45 ms remaining ; 11 h 23 min 44 s 991.43 ms total) Fri Oct 27 02:10:58 2023: Iterated ≈72% of D-proof candidates. [ 862691355 of 1198182438] (ETC: Fri Oct 27 05:21:57 2023 ; 3 h 10 min 58 s 748.72 ms remaining ; 11 h 22 min 4 s 102.54 ms total) Fri Oct 27 02:23:30 2023: Iterated ≈74% of D-proof candidates. [ 886655004 of 1198182438] (ETC: Fri Oct 27 05:20:27 2023 ; 2 h 56 min 56 s 945.97 ms remaining ; 11 h 20 min 34 s 407.56 ms total) Fri Oct 27 02:35:56 2023: Iterated ≈76% of D-proof candidates. [ 910618652 of 1198182438] (ETC: Fri Oct 27 05:18:54 2023 ; 2 h 42 min 57 s 875.24 ms remaining ; 11 h 19 min 1 s 146.71 ms total) Fri Oct 27 02:48:23 2023: Iterated ≈78% of D-proof candidates. [ 934582301 of 1198182438] (ETC: Fri Oct 27 05:17:27 2023 ; 2 h 29 min 3 s 984.52 ms remaining ; 11 h 17 min 34 s 475.02 ms total) Fri Oct 27 03:00:47 2023: Iterated ≈80% of D-proof candidates. [ 958545950 of 1198182438] (ETC: Fri Oct 27 05:16:01 2023 ; 2 h 15 min 13 s 642.00 ms remaining ; 11 h 16 min 8 s 209.91 ms total) Fri Oct 27 03:13:10 2023: Iterated ≈82% of D-proof candidates. [ 982509599 of 1198182438] (ETC: Fri Oct 27 05:14:37 2023 ; 2 h 1 min 27 s 197.05 ms remaining ; 11 h 14 min 44 s 428.01 ms total) Fri Oct 27 03:25:29 2023: Iterated ≈84% of D-proof candidates. [1006473247 of 1198182438] (ETC: Fri Oct 27 05:13:13 2023 ; 1 h 47 min 44 s 92.79 ms remaining ; 11 h 13 min 20 s 579.73 ms total) Fri Oct 27 03:37:49 2023: Iterated ≈86% of D-proof candidates. [1030436896 of 1198182438] (ETC: Fri Oct 27 05:11:54 2023 ; 1 h 34 min 5 s 35.55 ms remaining ; 11 h 12 min 1 s 682.30 ms total) Fri Oct 27 03:50:06 2023: Iterated ≈88% of D-proof candidates. [1054400545 of 1198182438] (ETC: Fri Oct 27 05:10:35 2023 ; 1 h 20 min 29 s 79.70 ms remaining ; 11 h 10 min 42 s 330.68 ms total) Fri Oct 27 04:02:21 2023: Iterated ≈90% of D-proof candidates. [1078364194 of 1198182438] (ETC: Fri Oct 27 05:09:17 2023 ; 1 h 6 min 56 s 478.01 ms remaining ; 11 h 9 min 24 s 780.01 ms total) Fri Oct 27 04:14:37 2023: Iterated ≈92% of D-proof candidates. [1102327842 of 1198182438] (ETC: Fri Oct 27 05:08:04 2023 ; 53 min 27 s 362.02 ms remaining ; 11 h 8 min 12 s 24.83 ms total) Fri Oct 27 04:26:52 2023: Iterated ≈94% of D-proof candidates. [1126291491 of 1198182438] (ETC: Fri Oct 27 05:06:53 2023 ; 40 min 1 s 238.50 ms remaining ; 11 h 7 min 641.21 ms total) Fri Oct 27 04:39:07 2023: Iterated ≈96% of D-proof candidates. [1150255140 of 1198182438] (ETC: Fri Oct 27 05:05:45 2023 ; 26 min 38 s 89.91 ms remaining ; 11 h 5 min 52 s 247.45 ms total) Fri Oct 27 04:51:14 2023: Iterated ≈98% of D-proof candidates. [1174218789 of 1198182438] (ETC: Fri Oct 27 05:04:31 2023 ; 13 min 17 s 572.59 ms remaining ; 11 h 4 min 38 s 628.92 ms total) Fri Oct 27 05:03:28 2023: Iterated 100% of D-proof candidates. [1198182438 of 1198182438] (ETC: Fri Oct 27 05:03:28 2023 ; 0.00 ms remaining ; 11 h 3 min 35 s 511.29 ms total) 39817246.01 ms (11 h 3 min 37 s 246.01 ms) taken to collect 143296899 D-proofs of length 77. [iterated 1198182438 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 }, { 77, 1198182438 } } 1136244.94 ms (18 min 56 s 244.94 ms) taken to filter and order new representative proofs. Found 143296899 representative, 613071460 redundant, and 441814079 invalid condensed detachment proof strings. lengths up to 77 ; 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), (77,143296899)} ; 143296899 new representative proofs (613071460 redundant, 441814079 invalid) Fri Oct 27 05:26:06 2023: Starting to write 143296899 entries to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. 140179.91 ms (2 min 20 s 179.91 ms) taken to print and save 29440512597 bytes of representative condensed detachment proof strings to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. Fri Oct 27 05:29:43 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 77, unfiltered] Fri Oct 27 05:32:23 2023: Process terminated. [pid: 214617, tid:22424174839680]