( 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.3430555… h CPU utilization: 352.4666… core-h ) Sat Oct 14 20:24:59 2023: Process started. [pid: 102266, tid:22823897167744] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true) 2. generateDProofRepresentativeFiles(65, false, true) [Main] Calling resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314] (1) C0CCN1CCN2.3C0.4CC4.1C2.1 - CpCCNqCCNrsCptCCtqCrq - 0\imply((\not1\imply((\not2\imply3)\imply(0\imply4)))\imply((4\imply1)\imply(2\imply1))) [Main] Calling generateDProofRepresentativeFiles(65, false, true). Sat Oct 14 20:24:59 2023: Limited D-proof representative generator started. [parallel ; 48 hardware thread contexts, limit: 65, unfiltered] 0.01 ms taken to load initial representatives. 18.68 ms taken to read 1 condensed detachment proof and conclusion from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs3.txt. [tid:22823836919552] 11.99 ms taken to read 2 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs5.txt. [tid:22823834818304] 25.11 ms taken to read 4 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs7.txt. [tid:22823832717056] 12.08 ms taken to read 7 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs9.txt. [tid:22823830615808] 13.35 ms taken to read 14 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs11.txt. [tid:22823828514560] 16.86 ms taken to read 23 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs13.txt. [tid:22823826413312] 29.05 ms taken to read 42 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs15.txt. [tid:22823824312064] 11.91 ms taken to read 72 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs17.txt. [tid:22823822210816] 32.48 ms taken to read 119 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs19.txt. [tid:22823820109568] 16.39 ms taken to read 180 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs21.txt. [tid:22823818008320] 29.68 ms taken to read 296 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs23.txt. [tid:22823815907072] 35.51 ms taken to read 493 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs25.txt. [tid:22823813805824] 37.91 ms taken to read 809 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs27.txt. [tid:22823811704576] 45.11 ms taken to read 1330 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs29.txt. [tid:22823809603328] 58.99 ms taken to read 2190 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs31.txt. [tid:22823807502080] 52.80 ms taken to read 3606 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs33.txt. [tid:22823805400832] 80.28 ms taken to read 5925 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs35.txt. [tid:22823803299584] 83.03 ms taken to read 9738 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs37.txt. [tid:22823801198336] 199.16 ms taken to read 15948 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs39.txt. [tid:22823799097088] 343.13 ms taken to read 26109 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs41.txt. [tid:22823796995840] 778.95 ms taken to read 42844 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs43.txt. [tid:22823794894592] 1868.11 ms (1 s 868.11 ms) taken to read 70083 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs45.txt. [tid:22823187773184] 5293.60 ms (5 s 293.60 ms) taken to read 115027 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs47.txt. [tid:22823185671936] 649.10 ms taken to read 188519 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs49.txt. [tid:22823183570688] 969.61 ms taken to read 308975 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs51.txt. [tid:22823181469440] 1447.87 ms (1 s 447.87 ms) taken to read 506415 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs53.txt. [tid:22823179368192] 2078.90 ms (2 s 78.91 ms) taken to read 830126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs55.txt. [tid:22823177266944] 2917.15 ms (2 s 917.15 ms) taken to read 1360461 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs57.txt. [tid:22823175165696] 3888.36 ms (3 s 888.36 ms) taken to read 2229126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs59.txt. [tid:22823173064448] 5145.72 ms (5 s 145.72 ms) taken to read 3652191 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs61.txt. [tid:22823170963200] 7056.46 ms (7 s 56.46 ms) taken to read 5983166 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs63.txt. [tid:22823168861952] 7077.98 ms (7 s 77.98 ms) total read duration. Loaded 32 representative collections of sizes: 1 : 1 3 : 1 5 : 2 7 : 4 9 : 7 11 : 14 13 : 23 15 : 42 17 : 72 19 : 119 21 : 180 23 : 296 25 : 493 27 : 809 29 : 1330 31 : 2190 33 : 3606 35 : 5925 37 : 9738 39 : 15948 41 : 26109 43 : 42844 45 : 70083 47 : 115027 49 : 188519 51 : 308975 53 : 506415 55 : 830126 57 : 1360461 59 : 2229126 61 : 3652191 63 : 5983166 15353842 representatives in total. Sat Oct 14 20:25:06 2023: Inserted ≈ 5% of D-proof conclusions. [ 767692 of 15353842] (ETC: Sat Oct 14 20:25:14 2023 ; 7 s 824.52 ms remaining ; 8 s 236.34 ms total) Sat Oct 14 20:25:07 2023: Inserted ≈10% of D-proof conclusions. [ 1535384 of 15353842] (ETC: Sat Oct 14 20:25:14 2023 ; 7 s 506.44 ms remaining ; 8 s 340.49 ms total) Sat Oct 14 20:25:07 2023: Inserted ≈15% of D-proof conclusions. [ 2303076 of 15353842] (ETC: Sat Oct 14 20:25:15 2023 ; 7 s 283.46 ms remaining ; 8 s 568.78 ms total) Sat Oct 14 20:25:08 2023: Inserted ≈20% of D-proof conclusions. [ 3070768 of 15353842] (ETC: Sat Oct 14 20:25:16 2023 ; 7 s 687.73 ms remaining ; 9 s 609.66 ms total) Sat Oct 14 20:25:08 2023: Inserted ≈25% of D-proof conclusions. [ 3838460 of 15353842] (ETC: Sat Oct 14 20:25:16 2023 ; 7 s 200.71 ms remaining ; 9 s 600.95 ms total) Sat Oct 14 20:25:09 2023: Inserted ≈30% of D-proof conclusions. [ 4606152 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 7 s 316.91 ms remaining ; 10 s 452.72 ms total) Sat Oct 14 20:25:10 2023: Inserted ≈35% of D-proof conclusions. [ 5373844 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 6 s 922.99 ms remaining ; 10 s 650.75 ms total) Sat Oct 14 20:25:10 2023: Inserted ≈40% of D-proof conclusions. [ 6141536 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 6 s 405.23 ms remaining ; 10 s 675.38 ms total) Sat Oct 14 20:25:11 2023: Inserted ≈45% of D-proof conclusions. [ 6909228 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 5 s 769.02 ms remaining ; 10 s 489.13 ms total) Sat Oct 14 20:25:11 2023: Inserted ≈50% of D-proof conclusions. [ 7676921 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 5 s 271.78 ms remaining ; 10 s 543.55 ms total) Sat Oct 14 20:25:12 2023: Inserted ≈55% of D-proof conclusions. [ 8444613 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 4 s 797.57 ms remaining ; 10 s 661.26 ms total) Sat Oct 14 20:25:13 2023: Inserted ≈60% of D-proof conclusions. [ 9212305 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 4 s 375.07 ms remaining ; 10 s 937.69 ms total) Sat Oct 14 20:25:13 2023: Inserted ≈65% of D-proof conclusions. [ 9979997 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 3 s 836.69 ms remaining ; 10 s 961.98 ms total) Sat Oct 14 20:25:14 2023: Inserted ≈70% of D-proof conclusions. [10747689 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 3 s 285.69 ms remaining ; 10 s 952.32 ms total) Sat Oct 14 20:25:14 2023: Inserted ≈75% of D-proof conclusions. [11515381 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 2 s 740.79 ms remaining ; 10 s 963.18 ms total) Sat Oct 14 20:25:15 2023: Inserted ≈80% of D-proof conclusions. [12283073 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 2 s 189.68 ms remaining ; 10 s 948.38 ms total) Sat Oct 14 20:25:15 2023: Inserted ≈85% of D-proof conclusions. [13050765 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 1 s 649.44 ms remaining ; 10 s 996.27 ms total) Sat Oct 14 20:25:16 2023: Inserted ≈90% of D-proof conclusions. [13818457 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 1 s 113.25 ms remaining ; 11 s 132.49 ms total) Sat Oct 14 20:25:17 2023: Inserted ≈95% of D-proof conclusions. [14586149 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 566.97 ms remaining ; 11 s 339.41 ms total) Sat Oct 14 20:25:17 2023: Inserted 100% of D-proof conclusions. [15353842 of 15353842] (ETC: Sat Oct 14 20:25:17 2023 ; 0.00 ms remaining ; 11 s 306.69 ms total) 11306.89 ms (11 s 306.88 ms) total insertion duration. Estimated iteration count set to 222394969, based on entry 63:130626396 and last known pair (61:76725006, 63:130626396) with 130626396/76725006 ≈ 1.70253 and 130626396 * (130626396/76725006)^1 ≈ 222394969.01. Sat Oct 14 20:25:17 2023: Starting to generate D-proof representatives of length 65. Sat Oct 14 20:35:57 2023: Iterated ≈ 2% of D-proof candidates. [ 4447899 of approximately 222394969] (ETC: Sun Oct 15 05:18:28 2023 ; 8 h 42 min 30 s 640.55 ms remaining ; 8 h 53 min 10 s 449.48 ms total) Sat Oct 14 20:48:30 2023: Iterated ≈ 4% of D-proof candidates. [ 8895798 of approximately 222394969] (ETC: Sun Oct 15 06:05:42 2023 ; 9 h 17 min 11 s 328.12 ms remaining ; 9 h 40 min 24 s 300.00 ms total) Sat Oct 14 20:59:25 2023: Iterated ≈ 6% of D-proof candidates. [ 13343698 of approximately 222394969] (ETC: Sun Oct 15 05:54:06 2023 ; 8 h 54 min 40 s 885.72 ms remaining ; 9 h 28 min 48 s 601.81 ms total) Sat Oct 14 21:09:36 2023: Iterated ≈ 8% of D-proof candidates. [ 17791597 of approximately 222394969] (ETC: Sun Oct 15 05:39:10 2023 ; 8 h 29 min 34 s 419.36 ms remaining ; 9 h 13 min 53 s 64.43 ms total) Sat Oct 14 21:19:49 2023: Iterated ≈ 10% of D-proof candidates. [ 22239496 of approximately 222394969] (ETC: Sun Oct 15 05:30:34 2023 ; 8 h 10 min 44 s 790.86 ms remaining ; 9 h 5 min 16 s 434.14 ms total) Sat Oct 14 21:30:50 2023: Iterated ≈ 12% of D-proof candidates. [ 26687396 of approximately 222394969] (ETC: Sun Oct 15 05:31:28 2023 ; 8 h 38 s 307.64 ms remaining ; 9 h 6 min 10 s 804.09 ms total) Sat Oct 14 21:40:17 2023: Iterated ≈ 14% of D-proof candidates. [ 31135295 of approximately 222394969] (ETC: Sun Oct 15 05:20:54 2023 ; 7 h 40 min 37 s 428.36 ms remaining ; 8 h 55 min 36 s 544.49 ms total) Sat Oct 14 21:51:07 2023: Iterated ≈ 16% of D-proof candidates. [ 35583195 of approximately 222394969] (ETC: Sun Oct 15 05:21:42 2023 ; 7 h 30 min 35 s 143.22 ms remaining ; 8 h 56 min 24 s 694.30 ms total) Sat Oct 14 22:00:22 2023: Iterated ≈ 18% of D-proof candidates. [ 40031094 of approximately 222394969] (ETC: Sun Oct 15 05:13:27 2023 ; 7 h 13 min 5 s 756.38 ms remaining ; 8 h 48 min 9 s 946.73 ms total) Sat Oct 14 22:10:14 2023: Iterated ≈ 20% of D-proof candidates. [ 44478993 of approximately 222394969] (ETC: Sun Oct 15 05:10:01 2023 ; 6 h 59 min 47 s 48.96 ms remaining ; 8 h 44 min 43 s 811.06 ms total) Sat Oct 14 22:20:15 2023: Iterated ≈ 22% of D-proof candidates. [ 48926893 of approximately 222394969] (ETC: Sun Oct 15 05:07:52 2023 ; 6 h 47 min 36 s 305.54 ms remaining ; 8 h 42 min 34 s 237.83 ms total) Sat Oct 14 22:29:07 2023: Iterated ≈ 24% of D-proof candidates. [ 53374792 of approximately 222394969] (ETC: Sun Oct 15 05:01:13 2023 ; 6 h 32 min 6 s 84.67 ms remaining ; 8 h 35 min 55 s 374.47 ms total) Sat Oct 14 22:38:42 2023: Iterated ≈ 26% of D-proof candidates. [ 57822691 of approximately 222394969] (ETC: Sun Oct 15 04:58:23 2023 ; 6 h 19 min 41 s 24.83 ms remaining ; 8 h 33 min 5 s 168.52 ms total) Sat Oct 14 22:48:16 2023: Iterated ≈ 28% of D-proof candidates. [ 62270591 of approximately 222394969] (ETC: Sun Oct 15 04:55:55 2023 ; 6 h 7 min 39 s 72.14 ms remaining ; 8 h 30 min 37 s 600.14 ms total) Sat Oct 14 22:56:55 2023: Iterated ≈ 30% of D-proof candidates. [ 66718490 of approximately 222394969] (ETC: Sun Oct 15 04:50:41 2023 ; 5 h 53 min 46 s 778.72 ms remaining ; 8 h 25 min 23 s 969.46 ms total) Sat Oct 14 23:06:06 2023: Iterated ≈ 32% of D-proof candidates. [ 71166390 of approximately 222394969] (ETC: Sun Oct 15 04:47:48 2023 ; 5 h 41 min 42 s 698.97 ms remaining ; 8 h 22 min 31 s 27.88 ms total) Sat Oct 14 23:15:30 2023: Iterated ≈ 34% of D-proof candidates. [ 75614289 of approximately 222394969] (ETC: Sun Oct 15 04:45:54 2023 ; 5 h 30 min 23 s 862.20 ms remaining ; 8 h 20 min 36 s 154.75 ms total) Sat Oct 14 23:24:04 2023: Iterated ≈ 36% of D-proof candidates. [ 80062188 of approximately 222394969] (ETC: Sun Oct 15 04:41:55 2023 ; 5 h 17 min 50 s 182.93 ms remaining ; 8 h 16 min 37 s 160.66 ms total) Sat Oct 14 23:32:59 2023: Iterated ≈ 38% of D-proof candidates. [ 84510088 of approximately 222394969] (ETC: Sun Oct 15 04:39:14 2023 ; 5 h 6 min 14 s 696.94 ms remaining ; 8 h 13 min 56 s 607.92 ms total) Sat Oct 14 23:42:33 2023: Iterated ≈ 40% of D-proof candidates. [ 88957987 of approximately 222394969] (ETC: Sun Oct 15 04:38:26 2023 ; 4 h 55 min 53 s 310.71 ms remaining ; 8 h 13 min 8 s 851.04 ms total) Sat Oct 14 23:51:08 2023: Iterated ≈ 42% of D-proof candidates. [ 93405886 of approximately 222394969] (ETC: Sun Oct 15 04:35:23 2023 ; 4 h 44 min 15 s 162.37 ms remaining ; 8 h 10 min 5 s 452.13 ms total) Sat Oct 14 23:59:36 2023: Iterated ≈ 44% of D-proof candidates. [ 97853786 of approximately 222394969] (ETC: Sun Oct 15 04:32:22 2023 ; 4 h 32 min 45 s 586.52 ms remaining ; 8 h 7 min 4 s 261.56 ms total) Sun Oct 15 00:08:25 2023: Iterated ≈ 46% of D-proof candidates. [102301685 of approximately 222394969] (ETC: Sun Oct 15 04:30:21 2023 ; 4 h 21 min 56 s 93.16 ms remaining ; 8 h 5 min 3 s 876.04 ms total) Sun Oct 15 00:17:18 2023: Iterated ≈ 48% of D-proof candidates. [106749585 of approximately 222394969] (ETC: Sun Oct 15 04:28:38 2023 ; 4 h 11 min 20 s 422.54 ms remaining ; 8 h 3 min 20 s 812.54 ms total) Sun Oct 15 00:25:26 2023: Iterated ≈ 50% of D-proof candidates. [111197484 of approximately 222394969] (ETC: Sun Oct 15 04:25:36 2023 ; 4 h 9 s 70.08 ms remaining ; 8 h 18 s 140.03 ms total) Sun Oct 15 00:33:44 2023: Iterated ≈ 52% of D-proof candidates. [115645383 of approximately 222394969] (ETC: Sun Oct 15 04:23:04 2023 ; 3 h 49 min 19 s 879.19 ms remaining ; 7 h 57 min 46 s 414.75 ms total) Sun Oct 15 00:42:23 2023: Iterated ≈ 54% of D-proof candidates. [120093283 of approximately 222394969] (ETC: Sun Oct 15 04:21:24 2023 ; 3 h 39 min 761.13 ms remaining ; 7 h 56 min 6 s 871.95 ms total) Sun Oct 15 00:50:52 2023: Iterated ≈ 56% of D-proof candidates. [124541182 of approximately 222394969] (ETC: Sun Oct 15 04:19:32 2023 ; 3 h 28 min 39 s 922.20 ms remaining ; 7 h 54 min 14 s 368.44 ms total) Sun Oct 15 00:58:59 2023: Iterated ≈ 58% of D-proof candidates. [128989082 of approximately 222394969] (ETC: Sun Oct 15 04:17:11 2023 ; 3 h 18 min 11 s 854.90 ms remaining ; 7 h 51 min 53 s 940.22 ms total) Sun Oct 15 01:07:00 2023: Iterated ≈ 60% of D-proof candidates. [133436981 of approximately 222394969] (ETC: Sun Oct 15 04:14:48 2023 ; 3 h 7 min 48 s 171.33 ms remaining ; 7 h 49 min 30 s 428.20 ms total) Sun Oct 15 01:15:15 2023: Iterated ≈ 62% of D-proof candidates. [137884880 of approximately 222394969] (ETC: Sun Oct 15 04:12:58 2023 ; 2 h 57 min 43 s 215.35 ms remaining ; 7 h 47 min 41 s 92.77 ms total) Sun Oct 15 01:23:08 2023: Iterated ≈ 64% of D-proof candidates. [142332780 of approximately 222394969] (ETC: Sun Oct 15 04:10:41 2023 ; 2 h 47 min 32 s 442.06 ms remaining ; 7 h 45 min 23 s 450.11 ms total) Sun Oct 15 01:31:02 2023: Iterated ≈ 66% of D-proof candidates. [146780679 of approximately 222394969] (ETC: Sun Oct 15 04:08:32 2023 ; 2 h 37 min 30 s 327.85 ms remaining ; 7 h 43 min 15 s 81.71 ms total) Sun Oct 15 01:39:05 2023: Iterated ≈ 68% of D-proof candidates. [151228578 of approximately 222394969] (ETC: Sun Oct 15 04:06:45 2023 ; 2 h 27 min 39 s 905.43 ms remaining ; 7 h 41 min 27 s 204.10 ms total) Sun Oct 15 01:47:04 2023: Iterated ≈ 70% of D-proof candidates. [155676478 of approximately 222394969] (ETC: Sun Oct 15 04:04:59 2023 ; 2 h 17 min 54 s 474.67 ms remaining ; 7 h 39 min 41 s 582.11 ms total) Sun Oct 15 01:55:03 2023: Iterated ≈ 72% of D-proof candidates. [160124377 of approximately 222394969] (ETC: Sun Oct 15 04:03:17 2023 ; 2 h 8 min 14 s 222.91 ms remaining ; 7 h 37 min 59 s 367.22 ms total) Sun Oct 15 02:02:59 2023: Iterated ≈ 74% of D-proof candidates. [164572277 of approximately 222394969] (ETC: Sun Oct 15 04:01:37 2023 ; 1 h 58 min 38 s 776.63 ms remaining ; 7 h 36 min 19 s 910.07 ms total) Sun Oct 15 02:10:58 2023: Iterated ≈ 76% of D-proof candidates. [169020176 of approximately 222394969] (ETC: Sun Oct 15 04:00:07 2023 ; 1 h 49 min 9 s 568.40 ms remaining ; 7 h 34 min 49 s 868.11 ms total) Sun Oct 15 02:18:42 2023: Iterated ≈ 78% of D-proof candidates. [173468075 of approximately 222394969] (ETC: Sun Oct 15 03:58:23 2023 ; 1 h 39 min 40 s 906.21 ms remaining ; 7 h 33 min 5 s 936.88 ms total) Sun Oct 15 02:26:16 2023: Iterated ≈ 80% of D-proof candidates. [177915975 of approximately 222394969] (ETC: Sun Oct 15 03:56:31 2023 ; 1 h 30 min 14 s 740.11 ms remaining ; 7 h 31 min 13 s 700.41 ms total) Sun Oct 15 02:34:02 2023: Iterated ≈ 82% of D-proof candidates. [182363874 of approximately 222394969] (ETC: Sun Oct 15 03:54:59 2023 ; 1 h 20 min 56 s 716.57 ms remaining ; 7 h 29 min 41 s 758.31 ms total) Sun Oct 15 02:41:47 2023: Iterated ≈ 84% of D-proof candidates. [186811773 of approximately 222394969] (ETC: Sun Oct 15 03:53:30 2023 ; 1 h 11 min 42 s 739.13 ms remaining ; 7 h 28 min 12 s 118.85 ms total) Sun Oct 15 02:49:26 2023: Iterated ≈ 86% of D-proof candidates. [191259673 of approximately 222394969] (ETC: Sun Oct 15 03:51:59 2023 ; 1 h 2 min 32 s 177.58 ms remaining ; 7 h 26 min 41 s 268.14 ms total) Sun Oct 15 02:57:05 2023: Iterated ≈ 88% of D-proof candidates. [195707572 of approximately 222394969] (ETC: Sun Oct 15 03:50:31 2023 ; 53 min 25 s 587.45 ms remaining ; 7 h 25 min 13 s 228.04 ms total) Sun Oct 15 03:04:35 2023: Iterated ≈ 90% of D-proof candidates. [200155472 of approximately 222394969] (ETC: Sun Oct 15 03:48:57 2023 ; 44 min 21 s 984.68 ms remaining ; 7 h 23 min 39 s 846.70 ms total) Sun Oct 15 03:12:10 2023: Iterated ≈ 92% of D-proof candidates. [204603371 of approximately 222394969] (ETC: Sun Oct 15 03:47:33 2023 ; 35 min 22 s 840.99 ms remaining ; 7 h 22 min 15 s 511.66 ms total) Sun Oct 15 03:19:37 2023: Iterated ≈ 94% of D-proof candidates. [209051270 of approximately 222394969] (ETC: Sun Oct 15 03:46:04 2023 ; 26 min 26 s 795.18 ms remaining ; 7 h 20 min 46 s 584.63 ms total) Sun Oct 15 03:27:18 2023: Iterated ≈ 96% of D-proof candidates. [213499170 of approximately 222394969] (ETC: Sun Oct 15 03:44:53 2023 ; 17 min 35 s 22.66 ms remaining ; 7 h 19 min 35 s 565.84 ms total) Sun Oct 15 03:34:56 2023: Iterated ≈ 98% of D-proof candidates. [217947069 of approximately 222394969] (ETC: Sun Oct 15 03:43:42 2023 ; 8 min 46 s 91.47 ms remaining ; 7 h 18 min 24 s 570.07 ms total) 26189007.49 ms (7 h 16 min 29 s 7.49 ms) taken to collect 15025264 D-proofs of length 65. [iterated 222080338 condensed detachment proof strings] [Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 5 }, { 9, 12 }, { 11, 26 }, { 13, 58 }, { 15, 118 }, { 17, 242 }, { 19, 481 }, { 21, 930 }, { 23, 1740 }, { 25, 3236 }, { 27, 5963 }, { 29, 10842 }, { 31, 19546 }, { 33, 34926 }, { 35, 62034 }, { 37, 109464 }, { 39, 192165 }, { 41, 335910 }, { 43, 585246 }, { 45, 1016370 }, { 47, 1759100 }, { 49, 3036854 }, { 51, 5229155 }, { 53, 8983090 }, { 55, 15399435 }, { 57, 26347004 }, { 59, 44997806 }, { 61, 76725006 }, { 63, 130626396 }, { 65, 222080338 } } 89964.89 ms (1 min 29 s 964.89 ms) taken to filter and order new representative proofs. Found 15025264 representative, 20584319 redundant, and 186470755 invalid condensed detachment proof strings. lengths up to 65 ; amounts per length: {(1,1), (3,1), (5,2), (7,4), (9,7), (11,14), (13,23), (15,42), (17,72), (19,119), (21,180), (23,296), (25,493), (27,809), (29,1330), (31,2190), (33,3606), (35,5925), (37,9738), (39,15948), (41,26109), (43,42844), (45,70083), (47,115027), (49,188519), (51,308975), (53,506415), (55,830126), (57,1360461), (59,2229126), (61,3652191), (63,5983166), (65,15025264)} ; 15025264 new representative proofs (20584319 redundant, 186470755 invalid) Sun Oct 15 03:44:05 2023: Starting to write 15025264 entries to data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs65-unfiltered65+.txt. 31538.07 ms (31 s 538.07 ms) taken to print and save 9415171948 bytes of representative condensed detachment proof strings to data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs65-unfiltered65+.txt. Sun Oct 15 03:44:45 2023: Limited D-proof representative generator complete. [parallel ; 48 hardware thread contexts, limit: 65, unfiltered] Sun Oct 15 03:45:34 2023: Process terminated. [pid: 102266, tid:22823897167744]