( 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: 3.0980555… h CPU utilization: 148.70666… core-h ) Wed Oct 4 04:00:54 2023: Process started. [pid: 90034, tid:22859625056128] Tasks: 1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(71, 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(71, false, true). Wed Oct 4 04:00:54 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 71, unfiltered] 0.01 ms taken to load initial representatives. 17.79 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22859564807936] 17.43 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22859562706688] 26.43 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22859560605440] 18.93 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22859558504192] 21.36 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22859556402944] 15.92 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22859554301696] 11.86 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22859552200448] 23.81 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22859550099200] 26.56 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22859547997952] 27.92 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22859545896704] 15.57 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22859543795456] 27.83 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22859541694208] 26.50 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22859539592960] 25.58 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22859537491712] 29.12 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22859535390464] 54.64 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22859533289216] 54.95 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22859531187968] 42.74 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22859529086720] 62.12 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22859526985472] 63.37 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22859524884224] 73.19 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22859522782976] 94.83 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22859520681728] 180.78 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22859518580480] 361.34 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22859516479232] 856.03 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22859514377984] 2191.59 ms (2 s 191.59 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22859512276736] 5090.24 ms (5 s 90.24 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22859510175488] 686.14 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22859508074240] 1042.28 ms (1 s 42.28 ms) taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22859505972992] 1611.69 ms (1 s 611.69 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22859503871744] 2109.50 ms (2 s 109.50 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22859501770496] 2656.56 ms (2 s 656.56 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22859499669248] 3583.86 ms (3 s 583.86 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22859497568000] 5096.83 ms (5 s 96.83 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22857279076096] 5117.69 ms (5 s 117.69 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. Wed Oct 4 04:00:59 2023: Inserted ≈ 5% of D-proof conclusions. [ 1265184 of 25303694] (ETC: Wed Oct 4 04:01:06 2023 ; 6 s 671.61 ms remaining ; 7 s 22.74 ms total) Wed Oct 4 04:01:00 2023: Inserted ≈10% of D-proof conclusions. [ 2530369 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 7 s 794.51 ms remaining ; 8 s 660.57 ms total) Wed Oct 4 04:01:00 2023: Inserted ≈15% of D-proof conclusions. [ 3795554 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 7 s 158.73 ms remaining ; 8 s 422.04 ms total) Wed Oct 4 04:01:00 2023: Inserted ≈20% of D-proof conclusions. [ 5060738 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 6 s 948.07 ms remaining ; 8 s 685.09 ms total) Wed Oct 4 04:01:01 2023: Inserted ≈25% of D-proof conclusions. [ 6325923 of 25303694] (ETC: Wed Oct 4 04:01:08 2023 ; 6 s 611.27 ms remaining ; 8 s 815.03 ms total) Wed Oct 4 04:01:01 2023: Inserted ≈30% of D-proof conclusions. [ 7591108 of 25303694] (ETC: Wed Oct 4 04:01:08 2023 ; 6 s 178.53 ms remaining ; 8 s 826.47 ms total) Wed Oct 4 04:01:02 2023: Inserted ≈35% of D-proof conclusions. [ 8856292 of 25303694] (ETC: Wed Oct 4 04:01:08 2023 ; 5 s 700.56 ms remaining ; 8 s 770.09 ms total) Wed Oct 4 04:01:02 2023: Inserted ≈40% of D-proof conclusions. [10121477 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 5 s 226.89 ms remaining ; 8 s 711.49 ms total) Wed Oct 4 04:01:03 2023: Inserted ≈45% of D-proof conclusions. [11386662 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 4 s 780.45 ms remaining ; 8 s 691.72 ms total) Wed Oct 4 04:01:03 2023: Inserted ≈50% of D-proof conclusions. [12651847 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 4 s 313.30 ms remaining ; 8 s 626.61 ms total) Wed Oct 4 04:01:03 2023: Inserted ≈55% of D-proof conclusions. [13917031 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 3 s 839.23 ms remaining ; 8 s 531.62 ms total) Wed Oct 4 04:01:04 2023: Inserted ≈60% of D-proof conclusions. [15182216 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 3 s 369.24 ms remaining ; 8 s 423.11 ms total) Wed Oct 4 04:01:04 2023: Inserted ≈65% of D-proof conclusions. [16447401 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 2 s 938.96 ms remaining ; 8 s 397.04 ms total) Wed Oct 4 04:01:05 2023: Inserted ≈70% of D-proof conclusions. [17712585 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 2 s 521.71 ms remaining ; 8 s 405.69 ms total) Wed Oct 4 04:01:05 2023: Inserted ≈75% of D-proof conclusions. [18977770 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 2 s 105.15 ms remaining ; 8 s 420.62 ms total) Wed Oct 4 04:01:05 2023: Inserted ≈80% of D-proof conclusions. [20242955 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 1 s 681.98 ms remaining ; 8 s 409.91 ms total) Wed Oct 4 04:01:06 2023: Inserted ≈85% of D-proof conclusions. [21508139 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 1 s 248.34 ms remaining ; 8 s 322.28 ms total) Wed Oct 4 04:01:06 2023: Inserted ≈90% of D-proof conclusions. [22773324 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 826.26 ms remaining ; 8 s 262.63 ms total) Wed Oct 4 04:01:07 2023: Inserted ≈95% of D-proof conclusions. [24038509 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 408.87 ms remaining ; 8 s 177.32 ms total) Wed Oct 4 04:01:07 2023: Inserted 100% of D-proof conclusions. [25303694 of 25303694] (ETC: Wed Oct 4 04:01:07 2023 ; 0.00 ms remaining ; 8 s 107.83 ms total) 8107.96 ms (8 s 107.96 ms) total insertion duration. Estimated iteration count set to 229243278, based on entry 69:136861838 and last known pair (67:81708667, 69:136861838) with 136861838/81708667 ≈ 1.675 and 136861838 * (136861838/81708667)^1 ≈ 229243278.45. Wed Oct 4 04:01:07 2023: Starting to generate D-proof representatives of length 71. Wed Oct 4 04:05:53 2023: Iterated ≈ 2% of D-proof candidates. [ 4584865 of approximately 229243278] (ETC: Wed Oct 4 07:59:46 2023 ; 3 h 53 min 53 s 159.62 ms remaining ; 3 h 58 min 39 s 550.60 ms total) Wed Oct 4 04:10:09 2023: Iterated ≈ 4% of D-proof candidates. [ 9169731 of approximately 229243278] (ETC: Wed Oct 4 07:46:51 2023 ; 3 h 36 min 42 s 807.83 ms remaining ; 3 h 45 min 44 s 591.48 ms total) Wed Oct 4 04:14:18 2023: Iterated ≈ 6% of D-proof candidates. [ 13754596 of approximately 229243278] (ETC: Wed Oct 4 07:40:46 2023 ; 3 h 26 min 28 s 104.39 ms remaining ; 3 h 39 min 38 s 834.42 ms total) Wed Oct 4 04:18:09 2023: Iterated ≈ 8% of D-proof candidates. [ 18339462 of approximately 229243278] (ETC: Wed Oct 4 07:34:09 2023 ; 3 h 15 min 59 s 173.95 ms remaining ; 3 h 33 min 1 s 710.80 ms total) Wed Oct 4 04:22:09 2023: Iterated ≈ 10% of D-proof candidates. [ 22924327 of approximately 229243278] (ETC: Wed Oct 4 07:31:26 2023 ; 3 h 9 min 16 s 944.33 ms remaining ; 3 h 30 min 18 s 826.98 ms total) Wed Oct 4 04:26:00 2023: Iterated ≈ 12% of D-proof candidates. [ 27509193 of approximately 229243278] (ETC: Wed Oct 4 07:28:34 2023 ; 3 h 2 min 33 s 289.52 ms remaining ; 3 h 27 min 26 s 919.89 ms total) Wed Oct 4 04:29:48 2023: Iterated ≈ 14% of D-proof candidates. [ 32094058 of approximately 229243278] (ETC: Wed Oct 4 07:26:02 2023 ; 2 h 56 min 13 s 775.85 ms remaining ; 3 h 24 min 55 s 88.14 ms total) Wed Oct 4 04:33:33 2023: Iterated ≈ 16% of D-proof candidates. [ 36678924 of approximately 229243278] (ETC: Wed Oct 4 07:23:51 2023 ; 2 h 50 min 17 s 622.82 ms remaining ; 3 h 22 min 43 s 836.66 ms total) Wed Oct 4 04:37:17 2023: Iterated ≈ 18% of D-proof candidates. [ 41263790 of approximately 229243278] (ETC: Wed Oct 4 07:22:05 2023 ; 2 h 44 min 47 s 914.82 ms remaining ; 3 h 20 min 58 s 432.70 ms total) Wed Oct 4 04:41:01 2023: Iterated ≈ 20% of D-proof candidates. [ 45848655 of approximately 229243278] (ETC: Wed Oct 4 07:20:39 2023 ; 2 h 39 min 38 s 56.37 ms remaining ; 3 h 19 min 32 s 570.43 ms total) Wed Oct 4 04:44:43 2023: Iterated ≈ 22% of D-proof candidates. [ 50433521 of approximately 229243278] (ETC: Wed Oct 4 07:19:17 2023 ; 2 h 34 min 34 s 155.43 ms remaining ; 3 h 18 min 9 s 942.85 ms total) Wed Oct 4 04:48:25 2023: Iterated ≈ 24% of D-proof candidates. [ 55018386 of approximately 229243278] (ETC: Wed Oct 4 07:18:13 2023 ; 2 h 29 min 47 s 721.08 ms remaining ; 3 h 17 min 5 s 948.75 ms total) Wed Oct 4 04:52:15 2023: Iterated ≈ 26% of D-proof candidates. [ 59603252 of approximately 229243278] (ETC: Wed Oct 4 07:17:47 2023 ; 2 h 25 min 32 s 433.85 ms remaining ; 3 h 16 min 40 s 586.26 ms total) Wed Oct 4 04:55:57 2023: Iterated ≈ 28% of D-proof candidates. [ 64188117 of approximately 229243278] (ETC: Wed Oct 4 07:16:58 2023 ; 2 h 21 min 1 s 51.07 ms remaining ; 3 h 15 min 51 s 459.76 ms total) Wed Oct 4 04:59:47 2023: Iterated ≈ 30% of D-proof candidates. [ 68772983 of approximately 229243278] (ETC: Wed Oct 4 07:16:39 2023 ; 2 h 16 min 52 s 496.96 ms remaining ; 3 h 15 min 32 s 138.49 ms total) Wed Oct 4 05:03:33 2023: Iterated ≈ 32% of D-proof candidates. [ 73357848 of approximately 229243278] (ETC: Wed Oct 4 07:16:13 2023 ; 2 h 12 min 39 s 887.24 ms remaining ; 3 h 15 min 5 s 716.46 ms total) Wed Oct 4 05:07:21 2023: Iterated ≈ 34% of D-proof candidates. [ 77942714 of approximately 229243278] (ETC: Wed Oct 4 07:15:56 2023 ; 2 h 8 min 34 s 980.97 ms remaining ; 3 h 14 min 49 s 365.07 ms total) Wed Oct 4 05:11:08 2023: Iterated ≈ 36% of D-proof candidates. [ 82527580 of approximately 229243278] (ETC: Wed Oct 4 07:15:38 2023 ; 2 h 4 min 29 s 456.34 ms remaining ; 3 h 14 min 31 s 25.53 ms total) Wed Oct 4 05:14:53 2023: Iterated ≈ 38% of D-proof candidates. [ 87112445 of approximately 229243278] (ETC: Wed Oct 4 07:15:15 2023 ; 2 h 21 s 856.58 ms remaining ; 3 h 14 min 8 s 155.72 ms total) Wed Oct 4 05:18:39 2023: Iterated ≈ 40% of D-proof candidates. [ 91697311 of approximately 229243278] (ETC: Wed Oct 4 07:14:56 2023 ; 1 h 56 min 17 s 728.68 ms remaining ; 3 h 13 min 49 s 547.79 ms total) Wed Oct 4 05:22:20 2023: Iterated ≈ 42% of D-proof candidates. [ 96282176 of approximately 229243278] (ETC: Wed Oct 4 07:14:30 2023 ; 1 h 52 min 9 s 833.31 ms remaining ; 3 h 13 min 23 s 160.81 ms total) Wed Oct 4 05:25:59 2023: Iterated ≈ 44% of D-proof candidates. [100867042 of approximately 229243278] (ETC: Wed Oct 4 07:14:00 2023 ; 1 h 48 min 980.57 ms remaining ; 3 h 12 min 53 s 179.57 ms total) Wed Oct 4 05:29:37 2023: Iterated ≈ 46% of D-proof candidates. [105451907 of approximately 229243278] (ETC: Wed Oct 4 07:13:31 2023 ; 1 h 43 min 53 s 758.44 ms remaining ; 3 h 12 min 23 s 997.02 ms total) Wed Oct 4 05:33:13 2023: Iterated ≈ 48% of D-proof candidates. [110036773 of approximately 229243278] (ETC: Wed Oct 4 07:12:59 2023 ; 1 h 39 min 46 s 327.15 ms remaining ; 3 h 11 min 52 s 167.55 ms total) Wed Oct 4 05:36:49 2023: Iterated ≈ 50% of D-proof candidates. [114621639 of approximately 229243278] (ETC: Wed Oct 4 07:12:30 2023 ; 1 h 35 min 41 s 660.36 ms remaining ; 3 h 11 min 23 s 320.71 ms total) Wed Oct 4 05:40:24 2023: Iterated ≈ 52% of D-proof candidates. [119206504 of approximately 229243278] (ETC: Wed Oct 4 07:12:03 2023 ; 1 h 31 min 38 s 827.10 ms remaining ; 3 h 10 min 55 s 889.74 ms total) Wed Oct 4 05:43:57 2023: Iterated ≈ 54% of D-proof candidates. [123791370 of approximately 229243278] (ETC: Wed Oct 4 07:11:33 2023 ; 1 h 27 min 35 s 866.69 ms remaining ; 3 h 10 min 25 s 797.13 ms total) Wed Oct 4 05:47:32 2023: Iterated ≈ 56% of D-proof candidates. [128376235 of approximately 229243278] (ETC: Wed Oct 4 07:11:09 2023 ; 1 h 23 min 36 s 826.91 ms remaining ; 3 h 10 min 1 s 879.28 ms total) Wed Oct 4 05:51:02 2023: Iterated ≈ 58% of D-proof candidates. [132961101 of approximately 229243278] (ETC: Wed Oct 4 07:10:38 2023 ; 1 h 19 min 35 s 741.25 ms remaining ; 3 h 9 min 30 s 812.48 ms total) Wed Oct 4 05:54:31 2023: Iterated ≈ 60% of D-proof candidates. [137545966 of approximately 229243278] (ETC: Wed Oct 4 07:10:06 2023 ; 1 h 15 min 35 s 815.39 ms remaining ; 3 h 8 min 59 s 538.38 ms total) Wed Oct 4 05:58:01 2023: Iterated ≈ 62% of D-proof candidates. [142130832 of approximately 229243278] (ETC: Wed Oct 4 07:09:40 2023 ; 1 h 11 min 39 s 85.64 ms remaining ; 3 h 8 min 33 s 383.23 ms total) Wed Oct 4 06:01:28 2023: Iterated ≈ 64% of D-proof candidates. [146715697 of approximately 229243278] (ETC: Wed Oct 4 07:09:11 2023 ; 1 h 7 min 42 s 113.62 ms remaining ; 3 h 8 min 3 s 648.83 ms total) Wed Oct 4 06:04:56 2023: Iterated ≈ 66% of D-proof candidates. [151300563 of approximately 229243278] (ETC: Wed Oct 4 07:08:43 2023 ; 1 h 3 min 47 s 33.85 ms remaining ; 3 h 7 min 35 s 981.86 ms total) Wed Oct 4 06:08:23 2023: Iterated ≈ 68% of D-proof candidates. [155885429 of approximately 229243278] (ETC: Wed Oct 4 07:08:16 2023 ; 59 min 53 s 317.42 ms remaining ; 3 h 7 min 9 s 116.92 ms total) Wed Oct 4 06:11:48 2023: Iterated ≈ 70% of D-proof candidates. [160470294 of approximately 229243278] (ETC: Wed Oct 4 07:07:48 2023 ; 56 min 479.88 ms remaining ; 3 h 6 min 41 s 599.49 ms total) Wed Oct 4 06:15:16 2023: Iterated ≈ 72% of D-proof candidates. [165055160 of approximately 229243278] (ETC: Wed Oct 4 07:07:26 2023 ; 52 min 10 s 45.60 ms remaining ; 3 h 6 min 18 s 734.26 ms total) Wed Oct 4 06:18:42 2023: Iterated ≈ 74% of D-proof candidates. [169640025 of approximately 229243278] (ETC: Wed Oct 4 07:07:03 2023 ; 48 min 20 s 607.40 ms remaining ; 3 h 5 min 56 s 182.19 ms total) Wed Oct 4 06:22:07 2023: Iterated ≈ 76% of D-proof candidates. [174224891 of approximately 229243278] (ETC: Wed Oct 4 07:06:39 2023 ; 44 min 31 s 653.24 ms remaining ; 3 h 5 min 31 s 888.46 ms total) Wed Oct 4 06:25:32 2023: Iterated ≈ 78% of D-proof candidates. [178809756 of approximately 229243278] (ETC: Wed Oct 4 07:06:17 2023 ; 40 min 44 s 126.05 ms remaining ; 3 h 5 min 9 s 663.68 ms total) Wed Oct 4 06:28:57 2023: Iterated ≈ 80% of D-proof candidates. [183394622 of approximately 229243278] (ETC: Wed Oct 4 07:05:54 2023 ; 36 min 57 s 490.19 ms remaining ; 3 h 4 min 47 s 450.85 ms total) Wed Oct 4 06:32:20 2023: Iterated ≈ 82% of D-proof candidates. [187979487 of approximately 229243278] (ETC: Wed Oct 4 07:05:31 2023 ; 33 min 11 s 626.16 ms remaining ; 3 h 4 min 24 s 589.51 ms total) Wed Oct 4 06:35:43 2023: Iterated ≈ 84% of D-proof candidates. [192564353 of approximately 229243278] (ETC: Wed Oct 4 07:05:10 2023 ; 29 min 26 s 925.16 ms remaining ; 3 h 4 min 3 s 282.07 ms total) Wed Oct 4 06:39:07 2023: Iterated ≈ 86% of D-proof candidates. [197149219 of approximately 229243278] (ETC: Wed Oct 4 07:04:51 2023 ; 25 min 43 s 320.82 ms remaining ; 3 h 3 min 43 s 720.15 ms total) Wed Oct 4 06:42:30 2023: Iterated ≈ 88% of D-proof candidates. [201734084 of approximately 229243278] (ETC: Wed Oct 4 07:04:31 2023 ; 22 min 438.98 ms remaining ; 3 h 3 min 23 s 657.88 ms total) Wed Oct 4 06:45:54 2023: Iterated ≈ 90% of D-proof candidates. [206318950 of approximately 229243278] (ETC: Wed Oct 4 07:04:12 2023 ; 18 min 18 s 523.56 ms remaining ; 3 h 3 min 5 s 235.51 ms total) Wed Oct 4 06:49:16 2023: Iterated ≈ 92% of D-proof candidates. [210903815 of approximately 229243278] (ETC: Wed Oct 4 07:03:53 2023 ; 14 min 37 s 308.98 ms remaining ; 3 h 2 min 46 s 361.81 ms total) Wed Oct 4 06:52:40 2023: Iterated ≈ 94% of D-proof candidates. [215488681 of approximately 229243278] (ETC: Wed Oct 4 07:03:36 2023 ; 10 min 56 s 976.91 ms remaining ; 3 h 2 min 29 s 614.94 ms total) Wed Oct 4 06:56:00 2023: Iterated ≈ 96% of D-proof candidates. [220073546 of approximately 229243278] (ETC: Wed Oct 4 07:03:18 2023 ; 7 min 17 s 231.83 ms remaining ; 3 h 2 min 10 s 794.62 ms total) Wed Oct 4 06:59:22 2023: Iterated ≈ 98% of D-proof candidates. [224658412 of approximately 229243278] (ETC: Wed Oct 4 07:03:01 2023 ; 3 min 38 s 273.86 ms remaining ; 3 h 1 min 53 s 692.01 ms total) 10896565.77 ms (3 h 1 min 36 s 565.77 ms) taken to collect 23150845 D-proofs of length 71. [iterated 229211380 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 } } 90309.48 ms (1 min 30 s 309.48 ms) taken to filter and order new representative proofs. Found 23150845 representative, 122847968 redundant, and 83212567 invalid condensed detachment proof strings. lengths up to 71 ; 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)} ; 23150845 new representative proofs (122847968 redundant, 83212567 invalid) Wed Oct 4 07:05:12 2023: Starting to write 23150845 entries to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. 20807.23 ms (20 s 807.23 ms) taken to print and save 4269010294 bytes of representative condensed detachment proof strings to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. Wed Oct 4 07:05:44 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 71, unfiltered] Wed Oct 4 07:06:47 2023: Process terminated. [pid: 90034, tid:22859625056128]