( 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: 5.301666… h CPU utilization: 254.48 core-h ) Wed Oct 4 07:13:06 2023: Process started. [pid: 56272, tid:22361525340032] Tasks: 1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(73, 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(73, false, true). Wed Oct 4 07:13:06 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 73, unfiltered] 0.05 ms taken to load initial representatives. 11.91 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22361465116416] 20.05 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22361463015168] 15.43 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22361460913920] 11.11 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22361458812672] 20.04 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22361456711424] 14.85 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22361454610176] 17.44 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22361452508928] 24.67 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22361450407680] 19.02 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22361448306432] 20.12 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22361446205184] 9.54 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22361444103936] 26.50 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22361442002688] 28.59 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22361439901440] 52.23 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22361437800192] 30.44 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22361435698944] 47.10 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22361433597696] 35.52 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22361431496448] 31.77 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22361429395200] 51.43 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22361427293952] 49.02 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22361425192704] 71.75 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22361423091456] 112.17 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22361420990208] 197.93 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22361418888960] 367.73 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22361416787712] 852.89 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22361414686464] 2012.70 ms (2 s 12.70 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22359868176128] 5112.56 ms (5 s 112.56 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22359866074880] 620.43 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22359863973632] 922.48 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22359861872384] 1369.77 ms (1 s 369.77 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22359859771136] 1930.62 ms (1 s 930.62 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22359857669888] 2611.95 ms (2 s 611.95 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22359855568640] 3827.18 ms (3 s 827.18 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22359853467392] 5246.66 ms (5 s 246.66 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22359851366144] 5268.45 ms (5 s 268.45 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. 9026.35 ms (9 s 26.35 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:22359851366144] 9028.27 ms (9 s 28.27 ms) additional read duration. Loaded 1 more representative collection of size: 71 : 23150845 48454539 representatives in total. Wed Oct 4 07:13:21 2023: Inserted ≈ 5% of D-proof conclusions. [ 2422726 of 48454539] (ETC: Wed Oct 4 07:13:47 2023 ; 25 s 899.80 ms remaining ; 27 s 262.95 ms total) Wed Oct 4 07:13:22 2023: Inserted ≈10% of D-proof conclusions. [ 4845453 of 48454539] (ETC: Wed Oct 4 07:13:45 2023 ; 22 s 657.31 ms remaining ; 25 s 174.78 ms total) Wed Oct 4 07:13:23 2023: Inserted ≈15% of D-proof conclusions. [ 7268180 of 48454539] (ETC: Wed Oct 4 07:13:43 2023 ; 19 s 594.63 ms remaining ; 23 s 52.50 ms total) Wed Oct 4 07:13:24 2023: Inserted ≈20% of D-proof conclusions. [ 9690907 of 48454539] (ETC: Wed Oct 4 07:13:42 2023 ; 17 s 885.63 ms remaining ; 22 s 357.03 ms total) Wed Oct 4 07:13:25 2023: Inserted ≈25% of D-proof conclusions. [12113634 of 48454539] (ETC: Wed Oct 4 07:13:41 2023 ; 16 s 91.36 ms remaining ; 21 s 455.15 ms total) Wed Oct 4 07:13:26 2023: Inserted ≈30% of D-proof conclusions. [14536361 of 48454539] (ETC: Wed Oct 4 07:13:41 2023 ; 14 s 689.47 ms remaining ; 20 s 984.96 ms total) Wed Oct 4 07:13:27 2023: Inserted ≈35% of D-proof conclusions. [16959088 of 48454539] (ETC: Wed Oct 4 07:13:41 2023 ; 13 s 489.56 ms remaining ; 20 s 753.17 ms total) Wed Oct 4 07:13:28 2023: Inserted ≈40% of D-proof conclusions. [19381815 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 12 s 262.42 ms remaining ; 20 s 437.37 ms total) Wed Oct 4 07:13:29 2023: Inserted ≈45% of D-proof conclusions. [21804542 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 11 s 104.08 ms remaining ; 20 s 189.24 ms total) Wed Oct 4 07:13:30 2023: Inserted ≈50% of D-proof conclusions. [24227269 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 10 s 23.02 ms remaining ; 20 s 46.04 ms total) Wed Oct 4 07:13:31 2023: Inserted ≈55% of D-proof conclusions. [26649996 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 8 s 948.05 ms remaining ; 19 s 884.57 ms total) Wed Oct 4 07:13:32 2023: Inserted ≈60% of D-proof conclusions. [29072723 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 7 s 912.67 ms remaining ; 19 s 781.68 ms total) Wed Oct 4 07:13:33 2023: Inserted ≈65% of D-proof conclusions. [31495450 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 6 s 904.58 ms remaining ; 19 s 727.38 ms total) Wed Oct 4 07:13:34 2023: Inserted ≈70% of D-proof conclusions. [33918177 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 5 s 976.58 ms remaining ; 19 s 921.95 ms total) Wed Oct 4 07:13:35 2023: Inserted ≈75% of D-proof conclusions. [36340904 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 5 s 10.19 ms remaining ; 20 s 40.75 ms total) Wed Oct 4 07:13:36 2023: Inserted ≈80% of D-proof conclusions. [38763631 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 4 s 31.60 ms remaining ; 20 s 158.00 ms total) Wed Oct 4 07:13:37 2023: Inserted ≈85% of D-proof conclusions. [41186358 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 3 s 29.27 ms remaining ; 20 s 195.15 ms total) Wed Oct 4 07:13:38 2023: Inserted ≈90% of D-proof conclusions. [43609085 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 2 s 22.66 ms remaining ; 20 s 226.64 ms total) Wed Oct 4 07:13:39 2023: Inserted ≈95% of D-proof conclusions. [46031812 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 1 s 13.33 ms remaining ; 20 s 266.58 ms total) Wed Oct 4 07:13:40 2023: Inserted 100% of D-proof conclusions. [48454539 of 48454539] (ETC: Wed Oct 4 07:13:40 2023 ; 0.00 ms remaining ; 20 s 496.54 ms total) 20496.91 ms (20 s 496.91 ms) total insertion duration. Estimated iteration count set to 383875136, based on entry 71:229211380 and last known pair (69:136861838, 71:229211380) with 229211380/136861838 ≈ 1.67476 and 229211380 * (229211380/136861838)^1 ≈ 383875136.34. Wed Oct 4 07:13:40 2023: Starting to generate D-proof representatives of length 73. Wed Oct 4 07:22:02 2023: Iterated ≈ 2% of D-proof candidates. [ 7677502 of approximately 383875136] (ETC: Wed Oct 4 14:11:40 2023 ; 6 h 49 min 37 s 955.23 ms remaining ; 6 h 57 min 59 s 546.10 ms total) Wed Oct 4 07:29:01 2023: Iterated ≈ 4% of D-proof candidates. [ 15355005 of approximately 383875136] (ETC: Wed Oct 4 13:37:10 2023 ; 6 h 8 min 9 s 423.08 ms remaining ; 6 h 23 min 29 s 815.68 ms total) Wed Oct 4 07:35:27 2023: Iterated ≈ 6% of D-proof candidates. [ 23032508 of approximately 383875136] (ETC: Wed Oct 4 13:16:41 2023 ; 5 h 41 min 13 s 558.75 ms remaining ; 6 h 3 min 381.63 ms total) Wed Oct 4 07:42:14 2023: Iterated ≈ 8% of D-proof candidates. [ 30710010 of approximately 383875136] (ETC: Wed Oct 4 13:10:37 2023 ; 5 h 28 min 23 s 473.23 ms remaining ; 5 h 56 min 56 s 818.68 ms total) Wed Oct 4 07:48:30 2023: Iterated ≈ 10% of D-proof candidates. [ 38387513 of approximately 383875136] (ETC: Wed Oct 4 13:01:55 2023 ; 5 h 13 min 25 s 308.45 ms remaining ; 5 h 48 min 14 s 787.13 ms total) Wed Oct 4 07:54:56 2023: Iterated ≈ 12% of D-proof candidates. [ 46065016 of approximately 383875136] (ETC: Wed Oct 4 12:57:29 2023 ; 5 h 2 min 33 s 340.06 ms remaining ; 5 h 43 min 48 s 795.50 ms total) Wed Oct 4 08:01:16 2023: Iterated ≈ 14% of D-proof candidates. [ 53742519 of approximately 383875136] (ETC: Wed Oct 4 12:53:38 2023 ; 4 h 52 min 22 s 176.19 ms remaining ; 5 h 39 min 57 s 879.29 ms total) Wed Oct 4 08:07:31 2023: Iterated ≈ 16% of D-proof candidates. [ 61420021 of approximately 383875136] (ETC: Wed Oct 4 12:50:13 2023 ; 4 h 42 min 41 s 647.64 ms remaining ; 5 h 36 min 32 s 437.62 ms total) Wed Oct 4 08:13:38 2023: Iterated ≈ 18% of D-proof candidates. [ 69097524 of approximately 383875136] (ETC: Wed Oct 4 12:46:49 2023 ; 4 h 33 min 10 s 676.54 ms remaining ; 5 h 33 min 8 s 629.89 ms total) Wed Oct 4 08:19:46 2023: Iterated ≈ 20% of D-proof candidates. [ 76775027 of approximately 383875136] (ETC: Wed Oct 4 12:44:08 2023 ; 4 h 24 min 22 s 76.15 ms remaining ; 5 h 30 min 27 s 595.17 ms total) Wed Oct 4 08:25:51 2023: Iterated ≈ 22% of D-proof candidates. [ 84452529 of approximately 383875136] (ETC: Wed Oct 4 12:41:43 2023 ; 4 h 15 min 52 s 242.18 ms remaining ; 5 h 28 min 2 s 361.70 ms total) Wed Oct 4 08:31:57 2023: Iterated ≈ 24% of D-proof candidates. [ 92130032 of approximately 383875136] (ETC: Wed Oct 4 12:39:51 2023 ; 4 h 7 min 53 s 826.66 ms remaining ; 5 h 26 min 10 s 824.51 ms total) Wed Oct 4 08:37:51 2023: Iterated ≈ 26% of D-proof candidates. [ 99807535 of approximately 383875136] (ETC: Wed Oct 4 12:37:27 2023 ; 3 h 59 min 35 s 328.98 ms remaining ; 5 h 23 min 46 s 120.22 ms total) Wed Oct 4 08:44:02 2023: Iterated ≈ 28% of D-proof candidates. [107485038 of approximately 383875136] (ETC: Wed Oct 4 12:36:21 2023 ; 3 h 52 min 19 s 928.50 ms remaining ; 5 h 22 min 41 s 11.80 ms total) Wed Oct 4 08:50:09 2023: Iterated ≈ 30% of D-proof candidates. [115162540 of approximately 383875136] (ETC: Wed Oct 4 12:35:14 2023 ; 3 h 45 min 5 s 701.95 ms remaining ; 5 h 21 min 33 s 859.88 ms total) Wed Oct 4 08:56:25 2023: Iterated ≈ 32% of D-proof candidates. [122840043 of approximately 383875136] (ETC: Wed Oct 4 12:34:45 2023 ; 3 h 38 min 19 s 584.63 ms remaining ; 5 h 21 min 4 s 95.00 ms total) Wed Oct 4 09:02:27 2023: Iterated ≈ 34% of D-proof candidates. [130517546 of approximately 383875136] (ETC: Wed Oct 4 12:33:37 2023 ; 3 h 31 min 9 s 722.29 ms remaining ; 5 h 19 min 56 s 548.90 ms total) Wed Oct 4 09:08:46 2023: Iterated ≈ 36% of D-proof candidates. [138195048 of approximately 383875136] (ETC: Wed Oct 4 12:33:23 2023 ; 3 h 24 min 36 s 586.25 ms remaining ; 5 h 19 min 42 s 165.94 ms total) Wed Oct 4 09:15:04 2023: Iterated ≈ 38% of D-proof candidates. [145872551 of approximately 383875136] (ETC: Wed Oct 4 12:33:06 2023 ; 3 h 18 min 2 s 885.93 ms remaining ; 5 h 19 min 25 s 944.99 ms total) Wed Oct 4 09:21:18 2023: Iterated ≈ 40% of D-proof candidates. [153550054 of approximately 383875136] (ETC: Wed Oct 4 12:32:44 2023 ; 3 h 11 min 26 s 115.81 ms remaining ; 5 h 19 min 3 s 526.32 ms total) Wed Oct 4 09:27:20 2023: Iterated ≈ 42% of D-proof candidates. [161227557 of approximately 383875136] (ETC: Wed Oct 4 12:31:55 2023 ; 3 h 4 min 35 s 102.65 ms remaining ; 5 h 18 min 15 s 4.56 ms total) Wed Oct 4 09:33:20 2023: Iterated ≈ 44% of D-proof candidates. [168905059 of approximately 383875136] (ETC: Wed Oct 4 12:31:06 2023 ; 2 h 57 min 45 s 217.72 ms remaining ; 5 h 17 min 25 s 31.56 ms total) Wed Oct 4 09:39:15 2023: Iterated ≈ 46% of D-proof candidates. [176582562 of approximately 383875136] (ETC: Wed Oct 4 12:30:09 2023 ; 2 h 50 min 53 s 568.03 ms remaining ; 5 h 16 min 28 s 88.89 ms total) Wed Oct 4 09:45:04 2023: Iterated ≈ 48% of D-proof candidates. [184260065 of approximately 383875136] (ETC: Wed Oct 4 12:29:04 2023 ; 2 h 44 min 232.91 ms remaining ; 5 h 15 min 23 s 524.81 ms total) Wed Oct 4 09:50:49 2023: Iterated ≈ 50% of D-proof candidates. [191937568 of approximately 383875136] (ETC: Wed Oct 4 12:27:58 2023 ; 2 h 37 min 8 s 685.82 ms remaining ; 5 h 14 min 17 s 371.64 ms total) Wed Oct 4 09:56:37 2023: Iterated ≈ 52% of D-proof candidates. [199615070 of approximately 383875136] (ETC: Wed Oct 4 12:27:01 2023 ; 2 h 30 min 24 s 302.49 ms remaining ; 5 h 13 min 20 s 630.11 ms total) Wed Oct 4 10:02:21 2023: Iterated ≈ 54% of D-proof candidates. [207292573 of approximately 383875136] (ETC: Wed Oct 4 12:26:02 2023 ; 2 h 23 min 40 s 978.21 ms remaining ; 5 h 12 min 21 s 256.93 ms total) Wed Oct 4 10:08:02 2023: Iterated ≈ 56% of D-proof candidates. [214970076 of approximately 383875136] (ETC: Wed Oct 4 12:25:01 2023 ; 2 h 16 min 59 s 623.65 ms remaining ; 5 h 11 min 20 s 962.83 ms total) Wed Oct 4 10:13:49 2023: Iterated ≈ 58% of D-proof candidates. [222647578 of approximately 383875136] (ETC: Wed Oct 4 12:24:16 2023 ; 2 h 10 min 26 s 894.42 ms remaining ; 5 h 10 min 35 s 462.80 ms total) Wed Oct 4 10:19:31 2023: Iterated ≈ 60% of D-proof candidates. [230325081 of approximately 383875136] (ETC: Wed Oct 4 12:23:24 2023 ; 2 h 3 min 53 s 401.95 ms remaining ; 5 h 9 min 43 s 504.81 ms total) Wed Oct 4 10:25:16 2023: Iterated ≈ 62% of D-proof candidates. [238002584 of approximately 383875136] (ETC: Wed Oct 4 12:22:42 2023 ; 1 h 57 min 25 s 871.54 ms remaining ; 5 h 9 min 1 s 767.18 ms total) Wed Oct 4 10:31:01 2023: Iterated ≈ 64% of D-proof candidates. [245680087 of approximately 383875136] (ETC: Wed Oct 4 12:22:01 2023 ; 1 h 51 min 339.76 ms remaining ; 5 h 8 min 20 s 943.78 ms total) Wed Oct 4 10:36:42 2023: Iterated ≈ 66% of D-proof candidates. [253357589 of approximately 383875136] (ETC: Wed Oct 4 12:21:17 2023 ; 1 h 44 min 35 s 90.98 ms remaining ; 5 h 7 min 36 s 149.82 ms total) Wed Oct 4 10:42:24 2023: Iterated ≈ 68% of D-proof candidates. [261035092 of approximately 383875136] (ETC: Wed Oct 4 12:20:37 2023 ; 1 h 38 min 13 s 403.22 ms remaining ; 5 h 6 min 56 s 884.99 ms total) Wed Oct 4 10:48:07 2023: Iterated ≈ 70% of D-proof candidates. [268712595 of approximately 383875136] (ETC: Wed Oct 4 12:20:01 2023 ; 1 h 31 min 54 s 41.38 ms remaining ; 5 h 6 min 20 s 137.90 ms total) Wed Oct 4 10:53:49 2023: Iterated ≈ 72% of D-proof candidates. [276390097 of approximately 383875136] (ETC: Wed Oct 4 12:19:25 2023 ; 1 h 25 min 36 s 551.20 ms remaining ; 5 h 5 min 44 s 825.57 ms total) Wed Oct 4 10:59:25 2023: Iterated ≈ 74% of D-proof candidates. [284067600 of approximately 383875136] (ETC: Wed Oct 4 12:18:44 2023 ; 1 h 19 min 18 s 912.21 ms remaining ; 5 h 5 min 3 s 508.38 ms total) Wed Oct 4 11:05:02 2023: Iterated ≈ 76% of D-proof candidates. [291745103 of approximately 383875136] (ETC: Wed Oct 4 12:18:06 2023 ; 1 h 13 min 3 s 791.29 ms remaining ; 5 h 4 min 25 s 796.98 ms total) Wed Oct 4 11:10:43 2023: Iterated ≈ 78% of D-proof candidates. [299422606 of approximately 383875136] (ETC: Wed Oct 4 12:17:34 2023 ; 1 h 6 min 51 s 457.76 ms remaining ; 5 h 3 min 53 s 898.91 ms total) Wed Oct 4 11:16:19 2023: Iterated ≈ 80% of D-proof candidates. [307100108 of approximately 383875136] (ETC: Wed Oct 4 12:16:58 2023 ; 1 h 39 s 500.89 ms remaining ; 5 h 3 min 17 s 504.25 ms total) Wed Oct 4 11:21:59 2023: Iterated ≈ 82% of D-proof candidates. [314777611 of approximately 383875136] (ETC: Wed Oct 4 12:16:30 2023 ; 54 min 30 s 501.35 ms remaining ; 5 h 2 min 49 s 451.79 ms total) Wed Oct 4 11:27:42 2023: Iterated ≈ 84% of D-proof candidates. [322455114 of approximately 383875136] (ETC: Wed Oct 4 12:16:06 2023 ; 48 min 23 s 212.76 ms remaining ; 5 h 2 min 25 s 79.69 ms total) Wed Oct 4 11:33:22 2023: Iterated ≈ 86% of D-proof candidates. [330132616 of approximately 383875136] (ETC: Wed Oct 4 12:15:38 2023 ; 42 min 16 s 450.25 ms remaining ; 5 h 1 min 57 s 501.48 ms total) Wed Oct 4 11:38:59 2023: Iterated ≈ 88% of D-proof candidates. [337810119 of approximately 383875136] (ETC: Wed Oct 4 12:15:10 2023 ; 36 min 10 s 772.54 ms remaining ; 5 h 1 min 29 s 770.89 ms total) Wed Oct 4 11:44:41 2023: Iterated ≈ 90% of D-proof candidates. [345487622 of approximately 383875136] (ETC: Wed Oct 4 12:14:47 2023 ; 30 min 6 s 691.34 ms remaining ; 5 h 1 min 6 s 913.22 ms total) Wed Oct 4 11:50:18 2023: Iterated ≈ 92% of D-proof candidates. [353165125 of approximately 383875136] (ETC: Wed Oct 4 12:14:21 2023 ; 24 min 3 s 234.21 ms remaining ; 5 h 40 s 427.58 ms total) Wed Oct 4 11:55:55 2023: Iterated ≈ 94% of D-proof candidates. [360842627 of approximately 383875136] (ETC: Wed Oct 4 12:13:56 2023 ; 18 min 923.95 ms remaining ; 5 h 15 s 398.57 ms total) Wed Oct 4 12:01:35 2023: Iterated ≈ 96% of D-proof candidates. [368520130 of approximately 383875136] (ETC: Wed Oct 4 12:13:34 2023 ; 11 min 59 s 758.39 ms remaining ; 4 h 59 min 53 s 959.05 ms total) Wed Oct 4 12:07:09 2023: Iterated ≈ 98% of D-proof candidates. [376197633 of approximately 383875136] (ETC: Wed Oct 4 12:13:09 2023 ; 5 min 59 s 367.39 ms remaining ; 4 h 59 min 28 s 368.84 ms total) Wed Oct 4 12:12:49 2023: Iterated ≈100% of D-proof candidates. [383875136 of approximately 383875136] (ETC: Wed Oct 4 12:12:49 2023 ; 0.00 ms remaining ; 4 h 59 min 8 s 615.34 ms total) 18535559.16 ms (5 h 8 min 55 s 559.16 ms) taken to collect 45156728 D-proofs of length 73. [iterated 397509772 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 } } 232987.29 ms (3 min 52 s 987.29 ms) taken to filter and order new representative proofs. Found 45156728 representative, 208697967 redundant, and 143655077 invalid condensed detachment proof strings. lengths up to 73 ; 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)} ; 45156728 new representative proofs (208697967 redundant, 143655077 invalid) Wed Oct 4 12:28:22 2023: Starting to write 45156728 entries to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. 41518.22 ms (41 s 518.23 ms) taken to print and save 8690446595 bytes of representative condensed detachment proof strings to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. Wed Oct 4 12:29:27 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 73, unfiltered] Wed Oct 4 12:31:12 2023: Process terminated. [pid: 56272, tid:22361525340032]