( 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: 45.2525 h CPU utilization: 2896.16 core-h ) Thu Nov 2 03:34:57 2023: Process started. [pid: 52115, tid:22642132342656] Tasks: 1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(81, 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(81, false, true). Thu Nov 2 03:34:57 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 81, unfiltered] 0.01 ms taken to load initial representatives. 10.31 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:22642072094464] 14.82 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:22642069993216] 7.79 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:22642067891968] 15.29 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:22642065790720] 20.19 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:22642063689472] 17.01 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:22641993840384] 12.03 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:22641991739136] 13.58 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:22641989637888] 11.87 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:22641987536640] 7.28 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:22641985435392] 22.97 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:22641983334144] 21.38 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:22641981232896] 36.90 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:22641979131648] 16.81 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:22641977030400] 20.95 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:22641974929152] 28.77 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:22641972827904] 47.29 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:22641970726656] 43.59 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:22641968625408] 49.78 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:22641966524160] 45.37 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:22641964422912] 119.53 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:22641962321664] 257.22 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:22641960220416] 310.59 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:22641958119168] 347.20 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:22641956017920] 1044.56 ms (1 s 44.56 ms) taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:22641953916672] 2141.10 ms (2 s 141.10 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:22641951815424] 4514.42 ms (4 s 514.42 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:22641949714176] 552.50 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:22641947612928] 1237.92 ms (1 s 237.92 ms) taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:22641945511680] 3141.40 ms (3 s 141.40 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:22641943410432] 4143.27 ms (4 s 143.27 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:22641941309184] 4512.02 ms (4 s 512.02 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:22641939207936] 5409.05 ms (5 s 409.05 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:22641937106688] 6529.23 ms (6 s 529.23 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:22641935005440] 6605.48 ms (6 s 605.48 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. 32083.31 ms (32 s 83.31 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:22641935005440] 56115.88 ms (56 s 115.88 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:22641937106688] 75528.68 ms (1 min 15 s 528.68 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:22641939207936] 102787.09 ms (1 min 42 s 787.09 ms) taken to read 143296899 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. [tid:22641941309184] 148053.05 ms (2 min 28 s 53.05 ms) taken to read 263540491 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs79-unfiltered71+.txt. [tid:22641943410432] 148195.85 ms (2 min 28 s 195.85 ms) additional read duration. Loaded 5 more representative collections of sizes: 71 : 23150845 73 : 45156728 75 : 80141395 77 : 143296899 79 : 263540491 580590052 representatives in total. Thu Nov 2 03:38:12 2023: Inserted ≈ 5% of D-proof conclusions. [ 29029502 of 580590052] (ETC: Thu Nov 2 03:50:49 2023 ; 12 min 37 s 156.12 ms remaining ; 13 min 17 s 6.44 ms total) Thu Nov 2 03:38:53 2023: Inserted ≈10% of D-proof conclusions. [ 58059005 of 580590052] (ETC: Thu Nov 2 03:50:59 2023 ; 12 min 6 s 253.37 ms remaining ; 13 min 26 s 948.19 ms total) Thu Nov 2 03:39:37 2023: Inserted ≈15% of D-proof conclusions. [ 87088507 of 580590052] (ETC: Thu Nov 2 03:51:26 2023 ; 11 min 48 s 476.18 ms remaining ; 13 min 53 s 501.39 ms total) Thu Nov 2 03:40:19 2023: Inserted ≈20% of D-proof conclusions. [116118010 of 580590052] (ETC: Thu Nov 2 03:51:25 2023 ; 11 min 6 s 228.45 ms remaining ; 13 min 52 s 785.57 ms total) Thu Nov 2 03:41:00 2023: Inserted ≈25% of D-proof conclusions. [145147513 of 580590052] (ETC: Thu Nov 2 03:51:25 2023 ; 10 min 24 s 921.24 ms remaining ; 13 min 53 s 228.32 ms total) Thu Nov 2 03:41:44 2023: Inserted ≈30% of D-proof conclusions. [174177015 of 580590052] (ETC: Thu Nov 2 03:51:32 2023 ; 9 min 47 s 716.53 ms remaining ; 13 min 59 s 595.04 ms total) Thu Nov 2 03:42:32 2023: Inserted ≈35% of D-proof conclusions. [203206518 of 580590052] (ETC: Thu Nov 2 03:51:50 2023 ; 9 min 17 s 791.44 ms remaining ; 14 min 18 s 140.68 ms total) Thu Nov 2 03:43:19 2023: Inserted ≈40% of D-proof conclusions. [232236020 of 580590052] (ETC: Thu Nov 2 03:52:00 2023 ; 8 min 40 s 974.03 ms remaining ; 14 min 28 s 290.05 ms total) Thu Nov 2 03:44:05 2023: Inserted ≈45% of D-proof conclusions. [261265523 of 580590052] (ETC: Thu Nov 2 03:52:06 2023 ; 8 min 560.09 ms remaining ; 14 min 33 s 745.63 ms total) Thu Nov 2 03:44:49 2023: Inserted ≈50% of D-proof conclusions. [290295026 of 580590052] (ETC: Thu Nov 2 03:52:06 2023 ; 7 min 16 s 957.38 ms remaining ; 14 min 33 s 914.77 ms total) Thu Nov 2 03:45:31 2023: Inserted ≈55% of D-proof conclusions. [319324528 of 580590052] (ETC: Thu Nov 2 03:52:02 2023 ; 6 min 31 s 515.00 ms remaining ; 14 min 30 s 33.34 ms total) Thu Nov 2 03:46:07 2023: Inserted ≈60% of D-proof conclusions. [348354031 of 580590052] (ETC: Thu Nov 2 03:51:50 2023 ; 5 min 43 s 262.95 ms remaining ; 14 min 18 s 157.38 ms total) Thu Nov 2 03:46:44 2023: Inserted ≈65% of D-proof conclusions. [377383533 of 580590052] (ETC: Thu Nov 2 03:51:42 2023 ; 4 min 57 s 363.41 ms remaining ; 14 min 9 s 609.75 ms total) Thu Nov 2 03:47:23 2023: Inserted ≈70% of D-proof conclusions. [406413036 of 580590052] (ETC: Thu Nov 2 03:51:36 2023 ; 4 min 13 s 202.52 ms remaining ; 14 min 4 s 8.41 ms total) Thu Nov 2 03:48:02 2023: Inserted ≈75% of D-proof conclusions. [435442539 of 580590052] (ETC: Thu Nov 2 03:51:33 2023 ; 3 min 30 s 123.52 ms remaining ; 14 min 494.08 ms total) Thu Nov 2 03:48:44 2023: Inserted ≈80% of D-proof conclusions. [464472041 of 580590052] (ETC: Thu Nov 2 03:51:32 2023 ; 2 min 47 s 992.56 ms remaining ; 13 min 59 s 962.79 ms total) Thu Nov 2 03:49:28 2023: Inserted ≈85% of D-proof conclusions. [493501544 of 580590052] (ETC: Thu Nov 2 03:51:35 2023 ; 2 min 6 s 400.34 ms remaining ; 14 min 2 s 668.93 ms total) Thu Nov 2 03:50:13 2023: Inserted ≈90% of D-proof conclusions. [522531046 of 580590052] (ETC: Thu Nov 2 03:51:37 2023 ; 1 min 24 s 492.84 ms remaining ; 14 min 4 s 928.34 ms total) Thu Nov 2 03:51:00 2023: Inserted ≈95% of D-proof conclusions. [551560549 of 580590052] (ETC: Thu Nov 2 03:51:42 2023 ; 42 s 516.97 ms remaining ; 14 min 10 s 339.39 ms total) Thu Nov 2 03:51:47 2023: Inserted 100% of D-proof conclusions. [580590052 of 580590052] (ETC: Thu Nov 2 03:51:47 2023 ; 0.00 ms remaining ; 14 min 14 s 595.31 ms total) 854596.71 ms (14 min 14 s 596.71 ms) total insertion duration. Known iteration count loaded from 81:3720990150. Thu Nov 2 03:51:47 2023: Starting to generate D-proof representatives of length 81. Thu Nov 2 04:50:24 2023: Iterated ≈ 2% of D-proof candidates. [ 74419803 of 3720990150] (ETC: Sat Nov 4 04:42:32 2023 ; 1 d 23 h 52 min 8 s 274.34 ms remaining ; 2 d 50 min 45 s 177.90 ms total) Thu Nov 2 05:48:10 2023: Iterated ≈ 4% of D-proof candidates. [ 148839606 of 3720990150] (ETC: Sat Nov 4 04:21:24 2023 ; 1 d 22 h 33 min 13 s 956.46 ms remaining ; 2 d 29 min 37 s 37.98 ms total) Thu Nov 2 06:43:29 2023: Iterated ≈ 6% of D-proof candidates. [ 223259409 of 3720990150] (ETC: Sat Nov 4 03:33:28 2023 ; 1 d 20 h 49 min 59 s 447.55 ms remaining ; 1 d 23 h 41 min 41 s 539.95 ms total) Thu Nov 2 07:43:02 2023: Iterated ≈ 8% of D-proof candidates. [ 297679212 of 3720990150] (ETC: Sat Nov 4 04:02:22 2023 ; 1 d 20 h 19 min 20 s 734.74 ms remaining ; 2 d 10 min 35 s 581.24 ms total) Thu Nov 2 08:40:32 2023: Iterated ≈10% of D-proof candidates. [ 372099015 of 3720990150] (ETC: Sat Nov 4 03:59:20 2023 ; 1 d 19 h 18 min 47 s 651.17 ms remaining ; 2 d 7 min 32 s 945.74 ms total) Thu Nov 2 09:34:21 2023: Iterated ≈12% of D-proof candidates. [ 446518818 of 3720990150] (ETC: Sat Nov 4 03:26:30 2023 ; 1 d 17 h 52 min 9 s 689.01 ms remaining ; 1 d 23 h 34 min 43 s 737.51 ms total) Thu Nov 2 10:29:41 2023: Iterated ≈14% of D-proof candidates. [ 520938621 of 3720990150] (ETC: Sat Nov 4 03:13:55 2023 ; 1 d 16 h 44 min 14 s 452.33 ms remaining ; 1 d 23 h 22 min 8 s 432.94 ms total) Thu Nov 2 11:25:21 2023: Iterated ≈16% of D-proof candidates. [ 595358424 of 3720990150] (ETC: Sat Nov 4 03:06:34 2023 ; 1 d 15 h 41 min 13 s 177.10 ms remaining ; 1 d 23 h 14 min 47 s 115.59 ms total) Thu Nov 2 12:19:30 2023: Iterated ≈18% of D-proof candidates. [ 669778227 of 3720990150] (ETC: Sat Nov 4 02:52:25 2023 ; 1 d 14 h 32 min 55 s 331.64 ms remaining ; 1 d 23 h 38 s 209.32 ms total) Thu Nov 2 13:13:02 2023: Iterated ≈20% of D-proof candidates. [ 744198030 of 3720990150] (ETC: Sat Nov 4 02:38:05 2023 ; 1 d 13 h 25 min 2 s 521.88 ms remaining ; 1 d 22 h 46 min 18 s 152.35 ms total) Thu Nov 2 14:05:57 2023: Iterated ≈22% of D-proof candidates. [ 818617833 of 3720990150] (ETC: Sat Nov 4 02:23:28 2023 ; 1 d 12 h 17 min 31 s 86.87 ms remaining ; 1 d 22 h 31 min 41 s 393.42 ms total) Thu Nov 2 14:58:35 2023: Iterated ≈24% of D-proof candidates. [ 893037636 of 3720990150] (ETC: Sat Nov 4 02:10:07 2023 ; 1 d 11 h 11 min 32 s 584.53 ms remaining ; 1 d 22 h 18 min 20 s 769.12 ms total) Thu Nov 2 15:50:27 2023: Iterated ≈26% of D-proof candidates. [ 967457439 of 3720990150] (ETC: Sat Nov 4 01:55:52 2023 ; 1 d 10 h 5 min 25 s 452.55 ms remaining ; 1 d 22 h 4 min 5 s 206.15 ms total) Thu Nov 2 16:42:01 2023: Iterated ≈28% of D-proof candidates. [1041877242 of 3720990150] (ETC: Sat Nov 4 01:42:37 2023 ; 1 d 9 h 36 s 407.80 ms remaining ; 1 d 21 h 50 min 50 s 566.39 ms total) Thu Nov 2 17:33:52 2023: Iterated ≈30% of D-proof candidates. [1116297045 of 3720990150] (ETC: Sat Nov 4 01:32:04 2023 ; 1 d 7 h 58 min 12 s 364.30 ms remaining ; 1 d 21 h 40 min 17 s 663.28 ms total) Thu Nov 2 18:25:21 2023: Iterated ≈32% of D-proof candidates. [1190716848 of 3720990150] (ETC: Sat Nov 4 01:21:43 2023 ; 1 d 6 h 56 min 21 s 221.68 ms remaining ; 1 d 21 h 29 min 55 s 914.24 ms total) Thu Nov 2 19:16:38 2023: Iterated ≈34% of D-proof candidates. [1265136651 of 3720990150] (ETC: Sat Nov 4 01:11:56 2023 ; 1 d 5 h 55 min 17 s 937.27 ms remaining ; 1 d 21 h 20 min 8 s 995.86 ms total) Thu Nov 2 20:08:18 2023: Iterated ≈36% of D-proof candidates. [1339556454 of 3720990150] (ETC: Sat Nov 4 01:04:20 2023 ; 1 d 4 h 56 min 1 s 904.96 ms remaining ; 1 d 21 h 12 min 32 s 976.50 ms total) Thu Nov 2 20:59:51 2023: Iterated ≈38% of D-proof candidates. [1413976257 of 3720990150] (ETC: Sat Nov 4 00:57:13 2023 ; 1 d 3 h 57 min 22 s 128.97 ms remaining ; 1 d 21 h 5 min 26 s 14.47 ms total) Thu Nov 2 21:51:07 2023: Iterated ≈40% of D-proof candidates. [1488396060 of 3720990150] (ETC: Sat Nov 4 00:50:08 2023 ; 1 d 2 h 59 min 951.84 ms remaining ; 1 d 20 h 58 min 21 s 586.39 ms total) Thu Nov 2 22:43:38 2023: Iterated ≈42% of D-proof candidates. [1562815863 of 3720990150] (ETC: Sat Nov 4 00:46:41 2023 ; 1 d 2 h 3 min 2 s 419.82 ms remaining ; 1 d 20 h 54 min 53 s 827.27 ms total) Thu Nov 2 23:34:40 2023: Iterated ≈44% of D-proof candidates. [1637235666 of 3720990150] (ETC: Sat Nov 4 00:40:10 2023 ; 1 d 1 h 5 min 29 s 608.10 ms remaining ; 1 d 20 h 48 min 22 s 871.60 ms total) Fri Nov 3 00:26:27 2023: Iterated ≈46% of D-proof candidates. [1711655469 of 3720990150] (ETC: Sat Nov 4 00:35:50 2023 ; 1 d 9 min 23 s 550.46 ms remaining ; 1 d 20 h 44 min 3 s 611.97 ms total) Fri Nov 3 01:17:42 2023: Iterated ≈48% of D-proof candidates. [1786075272 of 3720990150] (ETC: Sat Nov 4 00:30:46 2023 ; 23 h 13 min 4 s 550.34 ms remaining ; 1 d 20 h 38 min 59 s 519.88 ms total) Fri Nov 3 02:08:30 2023: Iterated ≈50% of D-proof candidates. [1860495075 of 3720990150] (ETC: Sat Nov 4 00:25:13 2023 ; 22 h 16 min 43 s 270.50 ms remaining ; 1 d 20 h 33 min 26 s 540.99 ms total) Fri Nov 3 02:58:58 2023: Iterated ≈52% of D-proof candidates. [1934914878 of 3720990150] (ETC: Sat Nov 4 00:19:26 2023 ; 21 h 20 min 28 s 559.67 ms remaining ; 1 d 20 h 27 min 39 s 499.32 ms total) Fri Nov 3 03:49:02 2023: Iterated ≈54% of D-proof candidates. [2009334681 of 3720990150] (ETC: Sat Nov 4 00:13:22 2023 ; 20 h 24 min 19 s 879.39 ms remaining ; 1 d 20 h 21 min 35 s 389.97 ms total) Fri Nov 3 04:38:31 2023: Iterated ≈56% of D-proof candidates. [2083754484 of 3720990150] (ETC: Sat Nov 4 00:06:41 2023 ; 19 h 28 min 9 s 277.84 ms remaining ; 1 d 20 h 14 min 53 s 813.27 ms total) Fri Nov 3 05:27:56 2023: Iterated ≈58% of D-proof candidates. [2158174287 of 3720990150] (ETC: Sat Nov 4 00:00:20 2023 ; 18 h 32 min 23 s 584.73 ms remaining ; 1 d 20 h 8 min 33 s 296.97 ms total) Fri Nov 3 06:16:53 2023: Iterated ≈60% of D-proof candidates. [2232594090 of 3720990150] (ETC: Fri Nov 3 23:53:37 2023 ; 17 h 36 min 43 s 971.76 ms remaining ; 1 d 20 h 1 min 49 s 929.39 ms total) Fri Nov 3 07:05:57 2023: Iterated ≈62% of D-proof candidates. [2307013893 of 3720990150] (ETC: Fri Nov 3 23:47:33 2023 ; 16 h 41 min 35 s 495.05 ms remaining ; 1 d 19 h 55 min 46 s 39.60 ms total) Fri Nov 3 07:54:58 2023: Iterated ≈64% of D-proof candidates. [2381433696 of 3720990150] (ETC: Fri Nov 3 23:41:46 2023 ; 15 h 46 min 47 s 624.62 ms remaining ; 1 d 19 h 49 min 58 s 957.29 ms total) Fri Nov 3 08:43:55 2023: Iterated ≈66% of D-proof candidates. [2455853499 of 3720990150] (ETC: Fri Nov 3 23:36:13 2023 ; 14 h 52 min 18 s 686.05 ms remaining ; 1 d 19 h 44 min 26 s 723.67 ms total) Fri Nov 3 09:32:34 2023: Iterated ≈68% of D-proof candidates. [2530273302 of 3720990150] (ETC: Fri Nov 3 23:30:36 2023 ; 13 h 58 min 1 s 270.64 ms remaining ; 1 d 19 h 38 min 48 s 970.75 ms total) Fri Nov 3 10:21:02 2023: Iterated ≈70% of D-proof candidates. [2604693105 of 3720990150] (ETC: Fri Nov 3 23:25:00 2023 ; 13 h 3 min 57 s 967.90 ms remaining ; 1 d 19 h 33 min 13 s 226.33 ms total) Fri Nov 3 11:09:45 2023: Iterated ≈72% of D-proof candidates. [2679112908 of 3720990150] (ETC: Fri Nov 3 23:20:04 2023 ; 12 h 10 min 19 s 344.16 ms remaining ; 1 d 19 h 28 min 17 s 657.73 ms total) Fri Nov 3 11:58:20 2023: Iterated ≈74% of D-proof candidates. [2753532711 of 3720990150] (ETC: Fri Nov 3 23:15:14 2023 ; 11 h 16 min 53 s 919.58 ms remaining ; 1 d 19 h 23 min 27 s 383.00 ms total) Fri Nov 3 12:46:27 2023: Iterated ≈76% of D-proof candidates. [2827952514 of 3720990150] (ETC: Fri Nov 3 23:10:01 2023 ; 10 h 23 min 34 s 735.13 ms remaining ; 1 d 19 h 18 min 14 s 729.71 ms total) Fri Nov 3 13:34:36 2023: Iterated ≈78% of D-proof candidates. [2902372317 of 3720990150] (ETC: Fri Nov 3 23:05:08 2023 ; 9 h 30 min 32 s 360.25 ms remaining ; 1 d 19 h 13 min 21 s 637.48 ms total) Fri Nov 3 14:22:32 2023: Iterated ≈80% of D-proof candidates. [2976792120 of 3720990150] (ETC: Fri Nov 3 23:00:14 2023 ; 8 h 37 min 41 s 413.87 ms remaining ; 1 d 19 h 8 min 27 s 69.36 ms total) Fri Nov 3 15:10:10 2023: Iterated ≈82% of D-proof candidates. [3051211923 of 3720990150] (ETC: Fri Nov 3 22:55:11 2023 ; 7 h 45 min 749.77 ms remaining ; 1 d 19 h 3 min 24 s 165.41 ms total) Fri Nov 3 15:58:02 2023: Iterated ≈84% of D-proof candidates. [3125631726 of 3720990150] (ETC: Fri Nov 3 22:50:39 2023 ; 6 h 52 min 37 s 123.51 ms remaining ; 1 d 18 h 58 min 52 s 21.92 ms total) Fri Nov 3 16:45:54 2023: Iterated ≈86% of D-proof candidates. [3200051529 of 3720990150] (ETC: Fri Nov 3 22:46:20 2023 ; 6 h 26 s 317.60 ms remaining ; 1 d 18 h 54 min 33 s 697.11 ms total) Fri Nov 3 17:33:48 2023: Iterated ≈88% of D-proof candidates. [3274471332 of 3720990150] (ETC: Fri Nov 3 22:42:15 2023 ; 5 h 8 min 27 s 381.63 ms remaining ; 1 d 18 h 50 min 28 s 180.23 ms total) Fri Nov 3 18:21:26 2023: Iterated ≈90% of D-proof candidates. [3348891135 of 3720990150] (ETC: Fri Nov 3 22:38:04 2023 ; 4 h 16 min 37 s 688.50 ms remaining ; 1 d 18 h 46 min 16 s 885.05 ms total) Fri Nov 3 19:09:19 2023: Iterated ≈92% of D-proof candidates. [3423310938 of 3720990150] (ETC: Fri Nov 3 22:34:19 2023 ; 3 h 25 min 214.65 ms remaining ; 1 d 18 h 42 min 32 s 683.14 ms total) Fri Nov 3 19:58:25 2023: Iterated ≈94% of D-proof candidates. [3497730741 of 3720990150] (ETC: Fri Nov 3 22:32:01 2023 ; 2 h 33 min 36 s 882.35 ms remaining ; 1 d 18 h 40 min 14 s 705.89 ms total) Fri Nov 3 20:45:44 2023: Iterated ≈96% of D-proof candidates. [3572150544 of 3720990150] (ETC: Fri Nov 3 22:27:59 2023 ; 1 h 42 min 14 s 902.23 ms remaining ; 1 d 18 h 36 min 12 s 555.73 ms total) Fri Nov 3 21:33:10 2023: Iterated ≈98% of D-proof candidates. [3646570347 of 3720990150] (ETC: Fri Nov 3 22:24:13 2023 ; 51 min 2 s 929.93 ms remaining ; 1 d 18 h 32 min 26 s 496.69 ms total) Fri Nov 3 22:20:39 2023: Iterated 100% of D-proof candidates. [3720990150 of 3720990150] (ETC: Fri Nov 3 22:20:39 2023 ; 0.00 ms remaining ; 1 d 18 h 28 min 52 s 627.09 ms total) 152938545.89 ms (1 d 18 h 28 min 58 s 545.89 ms) taken to collect 489824924 D-proofs of length 81. [iterated 3720990150 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 }, { 81, 3720990150 } } 5192605.75 ms (1 h 26 min 32 s 605.75 ms) taken to filter and order new representative proofs. Found 489824924 representative, 1861962719 redundant, and 1369202507 invalid condensed detachment proof strings. lengths up to 81 ; 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), (81,489824924)} ; 489824924 new representative proofs (1861962719 redundant, 1369202507 invalid) Sat Nov 4 00:10:32 2023: Starting to write 489824924 entries to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs81-unfiltered71+.txt. 695441.12 ms (11 min 35 s 441.12 ms) taken to print and save 108323290318 bytes of representative condensed detachment proof strings to data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs81-unfiltered71+.txt. Sat Nov 4 00:35:32 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 81, unfiltered] Sat Nov 4 00:50:06 2023: Process terminated. [pid: 52115, tid:22642132342656]