( 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: 24.658333… h CPU utilization: 1578.1333… core-h ) Wed Nov 1 01:38:35 2023: Process started. [pid: 132528, tid:22749296859008] Tasks: 1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(79, 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(79, false, true). Wed Nov 1 01:38:35 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 79, unfiltered] 0.01 ms taken to load initial representatives. 17.72 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22749236610816] 26.74 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22749234509568] 22.90 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22749232408320] 16.08 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22749230307072] 14.59 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22749228205824] 22.66 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22749226104576] 10.72 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22749224003328] 31.99 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22749221902080] 17.15 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22749219800832] 20.62 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22749217699584] 18.82 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22749215598336] 5.16 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22749213497088] 26.61 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22749211395840] 31.54 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22749209294592] 17.41 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22749207193344] 47.10 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22749205092096] 60.91 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22749202990848] 62.55 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22749200889600] 46.51 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22749198788352] 107.33 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22749196687104] 145.59 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22749194585856] 96.67 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22749192484608] 109.82 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22749190383360] 288.08 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22749188282112] 434.37 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22749186180864] 797.16 ms taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22749184079616] 4368.35 ms (4 s 368.35 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22749181978368] 2473.55 ms (2 s 473.55 ms) taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22749179877120] 3021.72 ms (3 s 21.72 ms) taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22749177775872] 2886.67 ms (2 s 886.67 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22749175674624] 4294.08 ms (4 s 294.08 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22749173573376] 4556.69 ms (4 s 556.69 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22749171472128] 5718.01 ms (5 s 718.00 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22749169370880] 6804.17 ms (6 s 804.17 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22748696934144] 6888.20 ms (6 s 888.20 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. 20125.18 ms (20 s 125.18 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:22748696934144] 37695.68 ms (37 s 695.68 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:22749169370880] 54301.19 ms (54 s 301.19 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:22749171472128] 79640.00 ms (1 min 19 s 640.00 ms) taken to read 143296899 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. [tid:22749173573376] 79674.63 ms (1 min 19 s 674.63 ms) additional read duration. Loaded 4 more representative collections of sizes: 71 : 23150845 73 : 45156728 75 : 80141395 77 : 143296899 317049561 representatives in total. Wed Nov 1 01:40:21 2023: Inserted ≈ 5% of D-proof conclusions. [ 15852478 of 317049561] (ETC: Wed Nov 1 01:46:23 2023 ; 6 min 1 s 775.64 ms remaining ; 6 min 20 s 816.46 ms total) Wed Nov 1 01:40:36 2023: Inserted ≈10% of D-proof conclusions. [ 31704956 of 317049561] (ETC: Wed Nov 1 01:45:44 2023 ; 5 min 7 s 984.51 ms remaining ; 5 min 42 s 205.01 ms total) Wed Nov 1 01:40:48 2023: Inserted ≈15% of D-proof conclusions. [ 47557434 of 317049561] (ETC: Wed Nov 1 01:45:07 2023 ; 4 min 19 s 256.35 ms remaining ; 5 min 5 s 7.47 ms total) Wed Nov 1 01:41:01 2023: Inserted ≈20% of D-proof conclusions. [ 63409912 of 317049561] (ETC: Wed Nov 1 01:44:56 2023 ; 3 min 55 s 351.82 ms remaining ; 4 min 54 s 189.78 ms total) Wed Nov 1 01:41:15 2023: Inserted ≈25% of D-proof conclusions. [ 79262390 of 317049561] (ETC: Wed Nov 1 01:44:56 2023 ; 3 min 40 s 274.17 ms remaining ; 4 min 53 s 698.89 ms total) Wed Nov 1 01:41:29 2023: Inserted ≈30% of D-proof conclusions. [ 95114868 of 317049561] (ETC: Wed Nov 1 01:44:51 2023 ; 3 min 22 s 517.11 ms remaining ; 4 min 49 s 310.15 ms total) Wed Nov 1 01:41:44 2023: Inserted ≈35% of D-proof conclusions. [110967346 of 317049561] (ETC: Wed Nov 1 01:44:52 2023 ; 3 min 8 s 849.49 ms remaining ; 4 min 50 s 537.68 ms total) Wed Nov 1 01:41:59 2023: Inserted ≈40% of D-proof conclusions. [126819824 of 317049561] (ETC: Wed Nov 1 01:44:55 2023 ; 2 min 55 s 714.15 ms remaining ; 4 min 52 s 856.93 ms total) Wed Nov 1 01:42:16 2023: Inserted ≈45% of D-proof conclusions. [142672302 of 317049561] (ETC: Wed Nov 1 01:45:00 2023 ; 2 min 43 s 721.56 ms remaining ; 4 min 57 s 675.56 ms total) Wed Nov 1 01:42:34 2023: Inserted ≈50% of D-proof conclusions. [158524780 of 317049561] (ETC: Wed Nov 1 01:45:06 2023 ; 2 min 32 s 40.39 ms remaining ; 5 min 4 s 80.78 ms total) Wed Nov 1 01:42:52 2023: Inserted ≈55% of D-proof conclusions. [174377258 of 317049561] (ETC: Wed Nov 1 01:45:11 2023 ; 2 min 19 s 24.88 ms remaining ; 5 min 8 s 944.18 ms total) Wed Nov 1 01:43:05 2023: Inserted ≈60% of D-proof conclusions. [190229736 of 317049561] (ETC: Wed Nov 1 01:45:07 2023 ; 2 min 2 s 230.36 ms remaining ; 5 min 5 s 575.91 ms total) Wed Nov 1 01:43:20 2023: Inserted ≈65% of D-proof conclusions. [206082214 of 317049561] (ETC: Wed Nov 1 01:45:07 2023 ; 1 min 46 s 661.87 ms remaining ; 5 min 4 s 748.20 ms total) Wed Nov 1 01:43:36 2023: Inserted ≈70% of D-proof conclusions. [221934692 of 317049561] (ETC: Wed Nov 1 01:45:07 2023 ; 1 min 31 s 571.42 ms remaining ; 5 min 5 s 238.07 ms total) Wed Nov 1 01:43:50 2023: Inserted ≈75% of D-proof conclusions. [237787170 of 317049561] (ETC: Wed Nov 1 01:45:06 2023 ; 1 min 16 s 137.65 ms remaining ; 5 min 4 s 550.58 ms total) Wed Nov 1 01:44:06 2023: Inserted ≈80% of D-proof conclusions. [253639648 of 317049561] (ETC: Wed Nov 1 01:45:07 2023 ; 1 min 1 s 39.12 ms remaining ; 5 min 5 s 195.61 ms total) Wed Nov 1 01:44:22 2023: Inserted ≈85% of D-proof conclusions. [269492126 of 317049561] (ETC: Wed Nov 1 01:45:08 2023 ; 45 s 953.15 ms remaining ; 5 min 6 s 354.32 ms total) Wed Nov 1 01:44:38 2023: Inserted ≈90% of D-proof conclusions. [285344604 of 317049561] (ETC: Wed Nov 1 01:45:08 2023 ; 30 s 632.63 ms remaining ; 5 min 6 s 326.33 ms total) Wed Nov 1 01:44:55 2023: Inserted ≈95% of D-proof conclusions. [301197082 of 317049561] (ETC: Wed Nov 1 01:45:11 2023 ; 15 s 438.13 ms remaining ; 5 min 8 s 762.62 ms total) Wed Nov 1 01:45:14 2023: Inserted 100% of D-proof conclusions. [317049561 of 317049561] (ETC: Wed Nov 1 01:45:14 2023 ; 0.00 ms remaining ; 5 min 12 s 255.08 ms total) 312259.39 ms (5 min 12 s 259.39 ms) total insertion duration. Known iteration count loaded from 79:2091875434. Wed Nov 1 01:45:14 2023: Starting to generate D-proof representatives of length 79. Wed Nov 1 02:14:22 2023: Iterated ≈ 2% of D-proof candidates. [ 41837508 of 2091875434] (ETC: Thu Nov 2 02:02:07 2023 ; 23 h 47 min 44 s 66.45 ms remaining ; 1 d 16 min 52 s 312.67 ms total) Wed Nov 1 02:44:46 2023: Iterated ≈ 4% of D-proof candidates. [ 83675017 of 2091875434] (ETC: Thu Nov 2 02:33:39 2023 ; 23 h 48 min 52 s 893.62 ms remaining ; 1 d 48 min 25 s 97.51 ms total) Wed Nov 1 03:15:59 2023: Iterated ≈ 6% of D-proof candidates. [ 125512526 of 2091875434] (ETC: Thu Nov 2 02:57:35 2023 ; 23 h 41 min 36 s 540.87 ms remaining ; 1 d 1 h 12 min 21 s 0.93 ms total) Wed Nov 1 03:48:51 2023: Iterated ≈ 8% of D-proof candidates. [ 167350034 of 2091875434] (ETC: Thu Nov 2 03:30:20 2023 ; 23 h 41 min 29 s 336.18 ms remaining ; 1 d 1 h 45 min 5 s 800.16 ms total) Wed Nov 1 04:20:30 2023: Iterated ≈10% of D-proof candidates. [ 209187543 of 2091875434] (ETC: Thu Nov 2 03:37:48 2023 ; 23 h 17 min 18 s 622.48 ms remaining ; 1 d 1 h 52 min 34 s 24.96 ms total) Wed Nov 1 04:50:12 2023: Iterated ≈12% of D-proof candidates. [ 251025052 of 2091875434] (ETC: Thu Nov 2 03:26:39 2023 ; 22 h 36 min 26 s 866.73 ms remaining ; 1 d 1 h 41 min 25 s 75.83 ms total) Wed Nov 1 05:20:56 2023: Iterated ≈14% of D-proof candidates. [ 292862560 of 2091875434] (ETC: Thu Nov 2 03:25:56 2023 ; 22 h 4 min 59 s 944.19 ms remaining ; 1 d 1 h 40 min 41 s 795.53 ms total) Wed Nov 1 05:51:35 2023: Iterated ≈16% of D-proof candidates. [ 334700069 of 2091875434] (ETC: Thu Nov 2 03:24:54 2023 ; 21 h 33 min 19 s 215.33 ms remaining ; 1 d 1 h 39 min 40 s 18.23 ms total) Wed Nov 1 06:21:37 2023: Iterated ≈18% of D-proof candidates. [ 376537578 of 2091875434] (ETC: Thu Nov 2 03:20:39 2023 ; 20 h 59 min 2 s 125.64 ms remaining ; 1 d 1 h 35 min 24 s 543.45 ms total) Wed Nov 1 06:51:14 2023: Iterated ≈20% of D-proof candidates. [ 418375086 of 2091875434] (ETC: Thu Nov 2 03:15:15 2023 ; 20 h 24 min 784.12 ms remaining ; 1 d 1 h 30 min 980.11 ms total) Wed Nov 1 07:20:39 2023: Iterated ≈22% of D-proof candidates. [ 460212595 of 2091875434] (ETC: Thu Nov 2 03:09:48 2023 ; 19 h 49 min 9 s 926.72 ms remaining ; 1 d 1 h 24 min 34 s 265.00 ms total) Wed Nov 1 07:49:32 2023: Iterated ≈24% of D-proof candidates. [ 502050104 of 2091875434] (ETC: Thu Nov 2 03:03:07 2023 ; 19 h 13 min 34 s 969.67 ms remaining ; 1 d 1 h 17 min 52 s 328.50 ms total) Wed Nov 1 08:17:57 2023: Iterated ≈26% of D-proof candidates. [ 543887612 of 2091875434] (ETC: Thu Nov 2 02:55:42 2023 ; 18 h 37 min 44 s 656.29 ms remaining ; 1 d 1 h 10 min 27 s 913.85 ms total) Wed Nov 1 08:46:17 2023: Iterated ≈28% of D-proof candidates. [ 585725121 of 2091875434] (ETC: Thu Nov 2 02:48:59 2023 ; 18 h 2 min 42 s 107.55 ms remaining ; 1 d 1 h 3 min 45 s 149.34 ms total) Wed Nov 1 09:15:07 2023: Iterated ≈30% of D-proof candidates. [ 627562630 of 2091875434] (ETC: Thu Nov 2 02:44:51 2023 ; 17 h 29 min 44 s 80.85 ms remaining ; 1 d 59 min 37 s 258.35 ms total) Wed Nov 1 09:42:42 2023: Iterated ≈32% of D-proof candidates. [ 669400138 of 2091875434] (ETC: Thu Nov 2 02:37:18 2023 ; 16 h 54 min 36 s 5.41 ms remaining ; 1 d 52 min 3 s 537.31 ms total) Wed Nov 1 10:11:10 2023: Iterated ≈34% of D-proof candidates. [ 711237647 of 2091875434] (ETC: Thu Nov 2 02:33:15 2023 ; 16 h 22 min 5 s 629.83 ms remaining ; 1 d 48 min 1 s 257.28 ms total) Wed Nov 1 10:40:02 2023: Iterated ≈36% of D-proof candidates. [ 753075156 of 2091875434] (ETC: Thu Nov 2 02:30:48 2023 ; 15 h 50 min 45 s 772.41 ms remaining ; 1 d 45 min 34 s 19.38 ms total) Wed Nov 1 11:08:12 2023: Iterated ≈38% of D-proof candidates. [ 794912664 of 2091875434] (ETC: Thu Nov 2 02:26:43 2023 ; 15 h 18 min 31 s 46.15 ms remaining ; 1 d 41 min 28 s 784.05 ms total) Wed Nov 1 11:36:57 2023: Iterated ≈40% of D-proof candidates. [ 836750173 of 2091875434] (ETC: Thu Nov 2 02:24:31 2023 ; 14 h 47 min 34 s 203.96 ms remaining ; 1 d 39 min 17 s 6.56 ms total) Wed Nov 1 12:05:59 2023: Iterated ≈42% of D-proof candidates. [ 878587682 of 2091875434] (ETC: Thu Nov 2 02:23:12 2023 ; 14 h 17 min 12 s 926.45 ms remaining ; 1 d 37 min 57 s 459.38 ms total) Wed Nov 1 12:34:39 2023: Iterated ≈44% of D-proof candidates. [ 920425190 of 2091875434] (ETC: Thu Nov 2 02:21:11 2023 ; 13 h 46 min 31 s 732.85 ms remaining ; 1 d 35 min 56 s 665.74 ms total) Wed Nov 1 13:03:25 2023: Iterated ≈46% of D-proof candidates. [ 962262699 of 2091875434] (ETC: Thu Nov 2 02:19:33 2023 ; 13 h 16 min 7 s 804.75 ms remaining ; 1 d 34 min 18 s 897.64 ms total) Wed Nov 1 13:31:43 2023: Iterated ≈48% of D-proof candidates. [1004100208 of 2091875434] (ETC: Thu Nov 2 02:17:03 2023 ; 12 h 45 min 20 s 822.64 ms remaining ; 1 d 31 min 49 s 274.28 ms total) Wed Nov 1 13:59:35 2023: Iterated ≈50% of D-proof candidates. [1045937717 of 2091875434] (ETC: Thu Nov 2 02:13:55 2023 ; 12 h 14 min 20 s 542.98 ms remaining ; 1 d 28 min 41 s 85.95 ms total) Wed Nov 1 14:26:53 2023: Iterated ≈52% of D-proof candidates. [1087775225 of 2091875434] (ETC: Thu Nov 2 02:09:57 2023 ; 11 h 43 min 3 s 561.15 ms remaining ; 1 d 24 min 42 s 419.00 ms total) Wed Nov 1 14:54:13 2023: Iterated ≈54% of D-proof candidates. [1129612734 of 2091875434] (ETC: Thu Nov 2 02:06:19 2023 ; 11 h 12 min 5 s 709.94 ms remaining ; 1 d 21 min 4 s 586.78 ms total) Wed Nov 1 15:21:32 2023: Iterated ≈56% of D-proof candidates. [1171450243 of 2091875434] (ETC: Thu Nov 2 02:02:54 2023 ; 10 h 41 min 22 s 484.14 ms remaining ; 1 d 17 min 40 s 191.22 ms total) Wed Nov 1 15:48:41 2023: Iterated ≈58% of D-proof candidates. [1213287751 of 2091875434] (ETC: Thu Nov 2 01:59:28 2023 ; 10 h 10 min 46 s 517.76 ms remaining ; 1 d 14 min 13 s 613.63 ms total) Wed Nov 1 16:16:01 2023: Iterated ≈60% of D-proof candidates. [1255125260 of 2091875434] (ETC: Thu Nov 2 01:56:33 2023 ; 9 h 40 min 31 s 360.45 ms remaining ; 1 d 11 min 18 s 401.09 ms total) Wed Nov 1 16:43:08 2023: Iterated ≈62% of D-proof candidates. [1296962769 of 2091875434] (ETC: Thu Nov 2 01:53:28 2023 ; 9 h 10 min 19 s 623.64 ms remaining ; 1 d 8 min 13 s 746.42 ms total) Wed Nov 1 17:10:32 2023: Iterated ≈64% of D-proof candidates. [1338800277 of 2091875434] (ETC: Thu Nov 2 01:51:01 2023 ; 8 h 40 min 28 s 698.60 ms remaining ; 1 d 5 min 46 s 384.90 ms total) Wed Nov 1 17:37:37 2023: Iterated ≈66% of D-proof candidates. [1380637786 of 2091875434] (ETC: Thu Nov 2 01:48:14 2023 ; 8 h 10 min 37 s 245.29 ms remaining ; 1 d 3 min 133.16 ms total) Wed Nov 1 18:04:50 2023: Iterated ≈68% of D-proof candidates. [1422475295 of 2091875434] (ETC: Thu Nov 2 01:45:49 2023 ; 7 h 40 min 58 s 994.80 ms remaining ; 1 d 34 s 358.73 ms total) Wed Nov 1 18:31:38 2023: Iterated ≈70% of D-proof candidates. [1464312803 of 2091875434] (ETC: Thu Nov 2 01:42:57 2023 ; 7 h 11 min 18 s 694.39 ms remaining ; 23 h 57 min 42 s 314.53 ms total) Wed Nov 1 18:58:36 2023: Iterated ≈72% of D-proof candidates. [1506150312 of 2091875434] (ETC: Thu Nov 2 01:40:27 2023 ; 6 h 41 min 51 s 651.65 ms remaining ; 23 h 55 min 13 s 41.53 ms total) Wed Nov 1 19:25:09 2023: Iterated ≈74% of D-proof candidates. [1547987821 of 2091875434] (ETC: Thu Nov 2 01:37:34 2023 ; 6 h 12 min 24 s 234.43 ms remaining ; 23 h 52 min 19 s 363.19 ms total) Wed Nov 1 19:51:59 2023: Iterated ≈76% of D-proof candidates. [1589825329 of 2091875434] (ETC: Thu Nov 2 01:35:10 2023 ; 5 h 43 min 11 s 6.21 ms remaining ; 23 h 49 min 55 s 859.07 ms total) Wed Nov 1 20:18:41 2023: Iterated ≈78% of D-proof candidates. [1631662838 of 2091875434] (ETC: Thu Nov 2 01:32:43 2023 ; 5 h 14 min 2 s 830.13 ms remaining ; 23 h 47 min 29 s 227.75 ms total) Wed Nov 1 20:45:29 2023: Iterated ≈80% of D-proof candidates. [1673500347 of 2091875434] (ETC: Thu Nov 2 01:30:33 2023 ; 4 h 45 min 3 s 705.47 ms remaining ; 23 h 45 min 18 s 527.30 ms total) Wed Nov 1 21:12:08 2023: Iterated ≈82% of D-proof candidates. [1715337855 of 2091875434] (ETC: Thu Nov 2 01:28:17 2023 ; 4 h 16 min 8 s 822.34 ms remaining ; 23 h 43 min 2 s 346.12 ms total) Wed Nov 1 21:38:43 2023: Iterated ≈84% of D-proof candidates. [1757175364 of 2091875434] (ETC: Thu Nov 2 01:26:03 2023 ; 3 h 47 min 19 s 765.36 ms remaining ; 23 h 40 min 48 s 533.33 ms total) Wed Nov 1 22:05:10 2023: Iterated ≈86% of D-proof candidates. [1799012873 of 2091875434] (ETC: Thu Nov 2 01:23:46 2023 ; 3 h 18 min 35 s 642.71 ms remaining ; 23 h 38 min 31 s 733.59 ms total) Wed Nov 1 22:31:40 2023: Iterated ≈88% of D-proof candidates. [1840850381 of 2091875434] (ETC: Thu Nov 2 01:21:38 2023 ; 2 h 49 min 58 s 86.63 ms remaining ; 23 h 36 min 24 s 54.97 ms total) Wed Nov 1 22:58:05 2023: Iterated ≈90% of D-proof candidates. [1882687890 of 2091875434] (ETC: Thu Nov 2 01:19:30 2023 ; 2 h 21 min 25 s 587.11 ms remaining ; 23 h 34 min 15 s 870.87 ms total) Wed Nov 1 23:24:30 2023: Iterated ≈92% of D-proof candidates. [1924525399 of 2091875434] (ETC: Thu Nov 2 01:17:29 2023 ; 1 h 52 min 58 s 792.10 ms remaining ; 23 h 32 min 14 s 901.14 ms total) Wed Nov 1 23:50:53 2023: Iterated ≈94% of D-proof candidates. [1966362907 of 2091875434] (ETC: Thu Nov 2 01:15:30 2023 ; 1 h 24 min 36 s 963.92 ms remaining ; 23 h 30 min 16 s 64.73 ms total) Thu Nov 2 00:17:17 2023: Iterated ≈96% of D-proof candidates. [2008200416 of 2091875434] (ETC: Thu Nov 2 01:13:37 2023 ; 56 min 20 s 122.67 ms remaining ; 23 h 28 min 23 s 66.08 ms total) Thu Nov 2 00:43:36 2023: Iterated ≈98% of D-proof candidates. [2050037925 of 2091875434] (ETC: Thu Nov 2 01:11:43 2023 ; 28 min 7 s 783.11 ms remaining ; 23 h 26 min 29 s 154.87 ms total) Thu Nov 2 01:09:43 2023: Iterated 100% of D-proof candidates. [2091875434 of 2091875434] (ETC: Thu Nov 2 01:09:43 2023 ; 0.00 ms remaining ; 23 h 24 min 28 s 418.92 ms total) 84271688.36 ms (23 h 24 min 31 s 688.36 ms) taken to collect 263540491 D-proofs of length 79. [iterated 2091875434 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 }, { 79, 2091875434 } } 2705956.91 ms (45 min 5 s 956.91 ms) taken to filter and order new representative proofs. Found 263540491 representative, 1062776779 redundant, and 765558164 invalid condensed detachment proof strings. lengths up to 79 ; 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), (79,263540491)} ; 263540491 new representative proofs (1062776779 redundant, 765558164 invalid) Thu Nov 2 02:03:05 2023: Starting to write 263540491 entries to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs79-unfiltered71+.txt. 281122.13 ms (4 min 41 s 122.13 ms) taken to print and save 56177510817 bytes of representative condensed detachment proof strings to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs79-unfiltered71+.txt. Thu Nov 2 02:12:48 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 79, unfiltered] Thu Nov 2 02:18:05 2023: Process terminated. [pid: 132528, tid:22749296859008]