( 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: 39.175 h CPU utilization: 2507.2 core-h ) Thu Nov 2 11:05:48 2023: Process started. [pid: 83516, tid:22404950038400] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true) 2. generateDProofRepresentativeFiles(71, 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(71, false, true). Thu Nov 2 11:05:48 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 71, unfiltered] 0.01 ms taken to load initial representatives. 16.96 ms taken to read 1 condensed detachment proof and conclusion from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs3.txt. [tid:22404889790208] 11.78 ms taken to read 2 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs5.txt. [tid:22404887688960] 5.17 ms taken to read 4 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs7.txt. [tid:22404885587712] 12.66 ms taken to read 7 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs9.txt. [tid:22404883486464] 18.31 ms taken to read 14 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs11.txt. [tid:22404881385216] 13.61 ms taken to read 23 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs13.txt. [tid:22404879283968] 15.54 ms taken to read 42 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs15.txt. [tid:22404877182720] 11.00 ms taken to read 72 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs17.txt. [tid:22404875081472] 25.46 ms taken to read 119 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs19.txt. [tid:22404872980224] 31.25 ms taken to read 180 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs21.txt. [tid:22404870878976] 21.96 ms taken to read 296 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs23.txt. [tid:22404868777728] 36.92 ms taken to read 493 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs25.txt. [tid:22404866676480] 92.17 ms taken to read 809 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs27.txt. [tid:22404864575232] 34.12 ms taken to read 1330 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs29.txt. [tid:22404862473984] 33.85 ms taken to read 2190 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs31.txt. [tid:22404860372736] 47.33 ms taken to read 3606 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs33.txt. [tid:22404858271488] 141.73 ms taken to read 5925 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs35.txt. [tid:22404856170240] 129.94 ms taken to read 9738 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs37.txt. [tid:22404854068992] 686.80 ms taken to read 15948 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs39.txt. [tid:22404851967744] 153.82 ms taken to read 26109 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs41.txt. [tid:22404849866496] 2441.47 ms (2 s 441.47 ms) taken to read 42844 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs43.txt. [tid:22404847765248] 2677.80 ms (2 s 677.80 ms) taken to read 70083 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs45.txt. [tid:22404845664000] 4765.15 ms (4 s 765.15 ms) taken to read 115027 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs47.txt. [tid:22404843562752] 2844.91 ms (2 s 844.91 ms) taken to read 188519 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs49.txt. [tid:22404841461504] 1260.84 ms (1 s 260.84 ms) taken to read 308975 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs51.txt. [tid:22404839360256] 2301.22 ms (2 s 301.22 ms) taken to read 506415 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs53.txt. [tid:22404837259008] 3980.09 ms (3 s 980.10 ms) taken to read 830126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs55.txt. [tid:22404835157760] 4802.57 ms (4 s 802.57 ms) taken to read 1360461 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs57.txt. [tid:22403690264320] 5999.07 ms (5 s 999.07 ms) taken to read 2229126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs59.txt. [tid:22403688163072] 7200.79 ms (7 s 200.79 ms) taken to read 3652191 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs61.txt. [tid:22403686061824] 8545.37 ms (8 s 545.37 ms) taken to read 5983166 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs63.txt. [tid:22403683960576] 8623.88 ms (8 s 623.88 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. 25325.74 ms (25 s 325.74 ms) taken to read 15025264 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs65-unfiltered65+.txt. [tid:22403683960576] 48867.57 ms (48 s 867.57 ms) taken to read 32295163 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs67-unfiltered65+.txt. [tid:22403686061824] 73785.63 ms (1 min 13 s 785.63 ms) taken to read 63892072 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs69-unfiltered65+.txt. [tid:22403688163072] 73812.22 ms (1 min 13 s 812.22 ms) additional read duration. Loaded 3 more representative collections of sizes: 65 : 15025264 67 : 32295163 69 : 63892072 126566341 representatives in total. Thu Nov 2 11:07:21 2023: Inserted ≈ 5% of D-proof conclusions. [ 6328317 of 126566341] (ETC: Thu Nov 2 11:10:47 2023 ; 3 min 25 s 779.58 ms remaining ; 3 min 36 s 610.08 ms total) Thu Nov 2 11:07:33 2023: Inserted ≈10% of D-proof conclusions. [ 12656634 of 126566341] (ETC: Thu Nov 2 11:10:58 2023 ; 3 min 24 s 339.30 ms remaining ; 3 min 47 s 43.67 ms total) Thu Nov 2 11:07:44 2023: Inserted ≈15% of D-proof conclusions. [ 18984951 of 126566341] (ETC: Thu Nov 2 11:10:51 2023 ; 3 min 7 s 150.91 ms remaining ; 3 min 40 s 177.53 ms total) Thu Nov 2 11:07:54 2023: Inserted ≈20% of D-proof conclusions. [ 25313268 of 126566341] (ETC: Thu Nov 2 11:10:48 2023 ; 2 min 53 s 889.70 ms remaining ; 3 min 37 s 362.12 ms total) Thu Nov 2 11:08:06 2023: Inserted ≈25% of D-proof conclusions. [ 31641585 of 126566341] (ETC: Thu Nov 2 11:10:53 2023 ; 2 min 46 s 720.36 ms remaining ; 3 min 42 s 293.81 ms total) Thu Nov 2 11:08:18 2023: Inserted ≈30% of D-proof conclusions. [ 37969902 of 126566341] (ETC: Thu Nov 2 11:10:56 2023 ; 2 min 37 s 523.76 ms remaining ; 3 min 45 s 33.95 ms total) Thu Nov 2 11:08:31 2023: Inserted ≈35% of D-proof conclusions. [ 44298219 of 126566341] (ETC: Thu Nov 2 11:11:00 2023 ; 2 min 29 s 77.00 ms remaining ; 3 min 49 s 349.23 ms total) Thu Nov 2 11:08:46 2023: Inserted ≈40% of D-proof conclusions. [ 50626536 of 126566341] (ETC: Thu Nov 2 11:11:08 2023 ; 2 min 22 s 544.51 ms remaining ; 3 min 57 s 574.19 ms total) Thu Nov 2 11:09:02 2023: Inserted ≈45% of D-proof conclusions. [ 56954853 of 126566341] (ETC: Thu Nov 2 11:11:18 2023 ; 2 min 16 s 165.76 ms remaining ; 4 min 7 s 574.11 ms total) Thu Nov 2 11:09:17 2023: Inserted ≈50% of D-proof conclusions. [ 63283170 of 126566341] (ETC: Thu Nov 2 11:11:24 2023 ; 2 min 6 s 655.88 ms remaining ; 4 min 13 s 311.76 ms total) Thu Nov 2 11:09:31 2023: Inserted ≈55% of D-proof conclusions. [ 69611487 of 126566341] (ETC: Thu Nov 2 11:11:27 2023 ; 1 min 55 s 216.49 ms remaining ; 4 min 16 s 36.65 ms total) Thu Nov 2 11:09:45 2023: Inserted ≈60% of D-proof conclusions. [ 75939804 of 126566341] (ETC: Thu Nov 2 11:11:28 2023 ; 1 min 42 s 984.40 ms remaining ; 4 min 17 s 461.00 ms total) Thu Nov 2 11:09:59 2023: Inserted ≈65% of D-proof conclusions. [ 82268121 of 126566341] (ETC: Thu Nov 2 11:11:30 2023 ; 1 min 30 s 907.94 ms remaining ; 4 min 19 s 736.97 ms total) Thu Nov 2 11:10:14 2023: Inserted ≈70% of D-proof conclusions. [ 88596438 of 126566341] (ETC: Thu Nov 2 11:11:32 2023 ; 1 min 18 s 437.44 ms remaining ; 4 min 21 s 458.14 ms total) Thu Nov 2 11:10:27 2023: Inserted ≈75% of D-proof conclusions. [ 94924755 of 126566341] (ETC: Thu Nov 2 11:11:33 2023 ; 1 min 5 s 494.06 ms remaining ; 4 min 21 s 976.23 ms total) Thu Nov 2 11:10:40 2023: Inserted ≈80% of D-proof conclusions. [101253072 of 126566341] (ETC: Thu Nov 2 11:11:33 2023 ; 52 s 451.15 ms remaining ; 4 min 22 s 255.75 ms total) Thu Nov 2 11:10:52 2023: Inserted ≈85% of D-proof conclusions. [107581389 of 126566341] (ETC: Thu Nov 2 11:11:32 2023 ; 39 s 131.36 ms remaining ; 4 min 20 s 875.71 ms total) Thu Nov 2 11:11:06 2023: Inserted ≈90% of D-proof conclusions. [113909706 of 126566341] (ETC: Thu Nov 2 11:11:32 2023 ; 26 s 146.49 ms remaining ; 4 min 21 s 464.84 ms total) Thu Nov 2 11:11:20 2023: Inserted ≈95% of D-proof conclusions. [120238023 of 126566341] (ETC: Thu Nov 2 11:11:33 2023 ; 13 s 123.95 ms remaining ; 4 min 22 s 478.88 ms total) Thu Nov 2 11:11:34 2023: Inserted 100% of D-proof conclusions. [126566341 of 126566341] (ETC: Thu Nov 2 11:11:34 2023 ; 0.00 ms remaining ; 4 min 23 s 289.50 ms total) 263289.79 ms (4 min 23 s 289.79 ms) total insertion duration. Known iteration count loaded from 71:1211683171. Thu Nov 2 11:11:34 2023: Starting to generate D-proof representatives of length 71. Thu Nov 2 12:12:16 2023: Iterated ≈ 2% of D-proof candidates. [ 24233663 of 1211683171] (ETC: Sat Nov 4 13:46:24 2023 ; 2 d 1 h 34 min 8 s 199.82 ms remaining ; 2 d 2 h 34 min 49 s 999.75 ms total) Thu Nov 2 13:22:19 2023: Iterated ≈ 4% of D-proof candidates. [ 48467326 of 1211683171] (ETC: Sat Nov 4 17:40:22 2023 ; 2 d 4 h 18 min 3 s 73.22 ms remaining ; 2 d 6 h 28 min 48 s 201.12 ms total) Thu Nov 2 14:36:56 2023: Iterated ≈ 6% of D-proof candidates. [ 72700990 of 1211683171] (ETC: Sat Nov 4 20:14:23 2023 ; 2 d 5 h 37 min 26 s 756.61 ms remaining ; 2 d 9 h 2 min 48 s 889.97 ms total) Thu Nov 2 16:04:05 2023: Iterated ≈ 8% of D-proof candidates. [ 96934653 of 1211683171] (ETC: Sun Nov 5 00:08:05 2023 ; 2 d 8 h 3 min 59 s 867.91 ms remaining ; 2 d 12 h 56 min 31 s 160.64 ms total) Thu Nov 2 17:10:11 2023: Iterated ≈10% of D-proof candidates. [ 121168317 of 1211683171] (ETC: Sat Nov 4 22:57:49 2023 ; 2 d 5 h 47 min 37 s 426.77 ms remaining ; 2 d 11 h 46 min 14 s 918.62 ms total) Thu Nov 2 18:15:04 2023: Iterated ≈12% of D-proof candidates. [ 145401980 of 1211683171] (ETC: Sat Nov 4 22:00:42 2023 ; 2 d 3 h 45 min 38 s 312.47 ms remaining ; 2 d 10 h 49 min 8 s 82.25 ms total) Thu Nov 2 19:11:35 2023: Iterated ≈14% of D-proof candidates. [ 169635643 of 1211683171] (ETC: Sat Nov 4 20:20:19 2023 ; 2 d 1 h 8 min 43 s 462.39 ms remaining ; 2 d 9 h 8 min 44 s 956.08 ms total) Thu Nov 2 20:09:15 2023: Iterated ≈16% of D-proof candidates. [ 193869307 of 1211683171] (ETC: Sat Nov 4 19:12:06 2023 ; 1 d 23 h 2 min 50 s 621.68 ms remaining ; 2 d 8 h 31 s 692.40 ms total) Thu Nov 2 21:07:58 2023: Iterated ≈18% of D-proof candidates. [ 218102970 of 1211683171] (ETC: Sat Nov 4 18:24:55 2023 ; 1 d 21 h 16 min 56 s 632.88 ms remaining ; 2 d 7 h 13 min 20 s 771.65 ms total) Thu Nov 2 22:04:29 2023: Iterated ≈20% of D-proof candidates. [ 242336634 of 1211683171] (ETC: Sat Nov 4 17:36:10 2023 ; 1 d 19 h 31 min 40 s 564.84 ms remaining ; 2 d 6 h 24 min 35 s 706.01 ms total) Thu Nov 2 22:56:16 2023: Iterated ≈22% of D-proof candidates. [ 266570297 of 1211683171] (ETC: Sat Nov 4 16:34:44 2023 ; 1 d 17 h 38 min 28 s 182.15 ms remaining ; 2 d 5 h 23 min 9 s 976.99 ms total) Thu Nov 2 23:50:27 2023: Iterated ≈24% of D-proof candidates. [ 290803961 of 1211683171] (ETC: Sat Nov 4 15:53:34 2023 ; 1 d 16 h 3 min 7 s 214.97 ms remaining ; 2 d 4 h 42 min 19.69 ms total) Fri Nov 3 00:38:20 2023: Iterated ≈26% of D-proof candidates. [ 315037624 of 1211683171] (ETC: Sat Nov 4 14:54:31 2023 ; 1 d 14 h 16 min 10 s 877.71 ms remaining ; 2 d 3 h 42 min 56 s 861.68 ms total) Fri Nov 3 01:31:00 2023: Iterated ≈28% of D-proof candidates. [ 339271287 of 1211683171] (ETC: Sat Nov 4 14:20:58 2023 ; 1 d 12 h 49 min 57 s 899.58 ms remaining ; 2 d 3 h 9 min 23 s 749.22 ms total) Fri Nov 3 02:16:53 2023: Iterated ≈30% of D-proof candidates. [ 363504951 of 1211683171] (ETC: Sat Nov 4 13:29:18 2023 ; 1 d 11 h 12 min 24 s 500.81 ms remaining ; 2 d 2 h 17 min 43 s 572.53 ms total) Fri Nov 3 03:06:39 2023: Iterated ≈32% of D-proof candidates. [ 387738614 of 1211683171] (ETC: Sat Nov 4 12:56:12 2023 ; 1 d 9 h 49 min 32 s 931.17 ms remaining ; 2 d 1 h 44 min 37 s 839.80 ms total) Fri Nov 3 03:51:54 2023: Iterated ≈34% of D-proof candidates. [ 411972278 of 1211683171] (ETC: Sat Nov 4 12:13:43 2023 ; 1 d 8 h 21 min 49 s 155.28 ms remaining ; 2 d 1 h 2 min 9 s 23.12 ms total) Fri Nov 3 04:37:12 2023: Iterated ≈36% of D-proof candidates. [ 436205941 of 1211683171] (ETC: Sat Nov 4 11:36:07 2023 ; 1 d 6 h 58 min 54 s 799.80 ms remaining ; 2 d 24 min 33 s 124.55 ms total) Fri Nov 3 05:25:38 2023: Iterated ≈38% of D-proof candidates. [ 460439604 of 1211683171] (ETC: Sat Nov 4 11:10:41 2023 ; 1 d 5 h 45 min 3 s 33.84 ms remaining ; 1 d 23 h 59 min 6 s 828.54 ms total) Fri Nov 3 06:08:22 2023: Iterated ≈40% of D-proof candidates. [ 484673268 of 1211683171] (ETC: Sat Nov 4 10:33:34 2023 ; 1 d 4 h 25 min 12 s 332.58 ms remaining ; 1 d 23 h 22 min 554.21 ms total) Fri Nov 3 06:54:05 2023: Iterated ≈42% of D-proof candidates. [ 508906931 of 1211683171] (ETC: Sat Nov 4 10:07:05 2023 ; 1 d 3 h 13 min 280.02 ms remaining ; 1 d 22 h 55 min 31 s 517.07 ms total) Fri Nov 3 07:38:48 2023: Iterated ≈44% of D-proof candidates. [ 533140595 of 1211683171] (ETC: Sat Nov 4 09:40:44 2023 ; 1 d 2 h 1 min 55 s 797.36 ms remaining ; 1 d 22 h 29 min 9 s 638.09 ms total) Fri Nov 3 08:20:33 2023: Iterated ≈46% of D-proof candidates. [ 557374258 of 1211683171] (ETC: Sat Nov 4 09:10:13 2023 ; 1 d 49 min 40 s 231.96 ms remaining ; 1 d 21 h 58 min 38 s 947.90 ms total) Fri Nov 3 09:05:26 2023: Iterated ≈48% of D-proof candidates. [ 581607922 of 1211683171] (ETC: Sat Nov 4 08:48:48 2023 ; 23 h 43 min 21 s 842.55 ms remaining ; 1 d 21 h 37 min 14 s 312.57 ms total) Fri Nov 3 09:48:21 2023: Iterated ≈50% of D-proof candidates. [ 605841585 of 1211683171] (ETC: Sat Nov 4 08:25:07 2023 ; 22 h 36 min 46 s 730.94 ms remaining ; 1 d 21 h 13 min 33 s 461.75 ms total) Fri Nov 3 10:29:14 2023: Iterated ≈52% of D-proof candidates. [ 630075248 of 1211683171] (ETC: Sat Nov 4 07:59:23 2023 ; 21 h 30 min 9 s 12.97 ms remaining ; 1 d 20 h 47 min 48 s 776.76 ms total) Fri Nov 3 11:12:10 2023: Iterated ≈54% of D-proof candidates. [ 654308912 of 1211683171] (ETC: Sat Nov 4 07:39:21 2023 ; 20 h 27 min 10 s 838.57 ms remaining ; 1 d 20 h 27 min 47 s 40.28 ms total) Fri Nov 3 11:53:35 2023: Iterated ≈56% of D-proof candidates. [ 678542575 of 1211683171] (ETC: Sat Nov 4 07:18:02 2023 ; 19 h 24 min 26 s 627.64 ms remaining ; 1 d 20 h 6 min 27 s 789.86 ms total) Fri Nov 3 12:33:09 2023: Iterated ≈58% of D-proof candidates. [ 702776239 of 1211683171] (ETC: Sat Nov 4 06:55:00 2023 ; 18 h 21 min 50 s 420.03 ms remaining ; 1 d 19 h 43 min 25 s 761.92 ms total) Fri Nov 3 13:14:22 2023: Iterated ≈60% of D-proof candidates. [ 727009902 of 1211683171] (ETC: Sat Nov 4 06:36:14 2023 ; 17 h 21 min 52 s 186.62 ms remaining ; 1 d 19 h 24 min 40 s 466.37 ms total) Fri Nov 3 13:53:42 2023: Iterated ≈62% of D-proof candidates. [ 751243566 of 1211683171] (ETC: Sat Nov 4 06:15:40 2023 ; 16 h 21 min 57 s 473.44 ms remaining ; 1 d 19 h 4 min 5 s 982.72 ms total) Fri Nov 3 14:32:19 2023: Iterated ≈64% of D-proof candidates. [ 775477229 of 1211683171] (ETC: Sat Nov 4 05:55:14 2023 ; 15 h 22 min 55 s 358.56 ms remaining ; 1 d 18 h 43 min 40 s 440.29 ms total) Fri Nov 3 15:12:34 2023: Iterated ≈66% of D-proof candidates. [ 799710892 of 1211683171] (ETC: Sat Nov 4 05:38:31 2023 ; 14 h 25 min 57 s 956.79 ms remaining ; 1 d 18 h 26 min 57 s 519.65 ms total) Fri Nov 3 15:50:17 2023: Iterated ≈68% of D-proof candidates. [ 823944556 of 1211683171] (ETC: Sat Nov 4 05:19:05 2023 ; 13 h 28 min 48 s 416.65 ms remaining ; 1 d 18 h 7 min 31 s 301.92 ms total) Fri Nov 3 16:28:14 2023: Iterated ≈70% of D-proof candidates. [ 848178219 of 1211683171] (ETC: Sat Nov 4 05:01:06 2023 ; 12 h 32 min 51 s 505.27 ms remaining ; 1 d 17 h 49 min 31 s 683.94 ms total) Fri Nov 3 17:07:24 2023: Iterated ≈72% of D-proof candidates. [ 872411883 of 1211683171] (ETC: Sat Nov 4 04:45:46 2023 ; 11 h 38 min 22 s 701.33 ms remaining ; 1 d 17 h 34 min 12 s 504.71 ms total) Fri Nov 3 17:44:20 2023: Iterated ≈74% of D-proof candidates. [ 896645546 of 1211683171] (ETC: Sat Nov 4 04:28:17 2023 ; 10 h 43 min 56 s 713.62 ms remaining ; 1 d 17 h 16 min 42 s 744.44 ms total) Fri Nov 3 18:21:48 2023: Iterated ≈76% of D-proof candidates. [ 920879209 of 1211683171] (ETC: Sat Nov 4 04:12:24 2023 ; 9 h 50 min 36 s 8.93 ms remaining ; 1 d 17 h 50 s 36.71 ms total) Fri Nov 3 18:59:29 2023: Iterated ≈78% of D-proof candidates. [ 945112873 of 1211683171] (ETC: Sat Nov 4 03:57:37 2023 ; 8 h 58 min 7 s 841.15 ms remaining ; 1 d 16 h 46 min 2 s 914.12 ms total) Fri Nov 3 19:36:09 2023: Iterated ≈80% of D-proof candidates. [ 969346536 of 1211683171] (ETC: Sat Nov 4 03:42:17 2023 ; 8 h 6 min 8 s 689.57 ms remaining ; 1 d 16 h 30 min 43 s 447.36 ms total) Fri Nov 3 20:12:50 2023: Iterated ≈82% of D-proof candidates. [ 993580200 of 1211683171] (ETC: Sat Nov 4 03:27:44 2023 ; 7 h 14 min 54 s 701.87 ms remaining ; 1 d 16 h 16 min 10 s 565.78 ms total) Fri Nov 3 20:49:46 2023: Iterated ≈84% of D-proof candidates. [1017813863 of 1211683171] (ETC: Sat Nov 4 03:14:11 2023 ; 6 h 24 min 25 s 169.18 ms remaining ; 1 d 16 h 2 min 37 s 306.92 ms total) Fri Nov 3 21:26:15 2023: Iterated ≈86% of D-proof candidates. [1042047527 of 1211683171] (ETC: Sat Nov 4 03:00:44 2023 ; 5 h 34 min 29 s 12.48 ms remaining ; 1 d 15 h 49 min 10 s 89.11 ms total) Fri Nov 3 22:02:30 2023: Iterated ≈88% of D-proof candidates. [1066281190 of 1211683171] (ETC: Sat Nov 4 02:47:37 2023 ; 4 h 45 min 7 s 587.47 ms remaining ; 1 d 15 h 36 min 3 s 228.47 ms total) Fri Nov 3 22:38:55 2023: Iterated ≈90% of D-proof candidates. [1090514853 of 1211683171] (ETC: Sat Nov 4 02:35:17 2023 ; 3 h 56 min 22 s 309.76 ms remaining ; 1 d 15 h 23 min 43 s 96.55 ms total) Fri Nov 3 23:14:59 2023: Iterated ≈92% of D-proof candidates. [1114748517 of 1211683171] (ETC: Sat Nov 4 02:23:06 2023 ; 3 h 8 min 7 s 354.36 ms remaining ; 1 d 15 h 11 min 31 s 929.08 ms total) Fri Nov 3 23:51:09 2023: Iterated ≈94% of D-proof candidates. [1138982180 of 1211683171] (ETC: Sat Nov 4 02:11:33 2023 ; 2 h 20 min 23 s 967.55 ms remaining ; 1 d 14 h 59 min 59 s 457.78 ms total) Sat Nov 4 00:27:07 2023: Iterated ≈96% of D-proof candidates. [1163215844 of 1211683171] (ETC: Sat Nov 4 02:00:15 2023 ; 1 h 33 min 8 s 857.63 ms remaining ; 1 d 14 h 48 min 41 s 440.35 ms total) Sat Nov 4 01:03:00 2023: Iterated ≈98% of D-proof candidates. [1187449507 of 1211683171] (ETC: Sat Nov 4 01:49:21 2023 ; 46 min 21 s 344.22 ms remaining ; 1 d 14 h 37 min 47 s 207.54 ms total) Sat Nov 4 01:37:53 2023: Iterated 100% of D-proof candidates. [1211683171 of 1211683171] (ETC: Sat Nov 4 01:37:53 2023 ; 0.00 ms remaining ; 1 d 14 h 26 min 18 s 714.85 ms total) 138380222.37 ms (1 d 14 h 26 min 20 s 222.37 ms) taken to collect 123578255 D-proofs of length 71. [iterated 1211683171 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 }, { 67, 387519448 }, { 69, 682368918 }, { 71, 1211683171 } } 1280411.74 ms (21 min 20 s 411.74 ms) taken to filter and order new representative proofs. Found 123578255 representative, 123145619 redundant, and 964959297 invalid condensed detachment proof strings. lengths up to 71 ; 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), (67,32295163), (69,63892072), (71,123578255)} ; 123578255 new representative proofs (123145619 redundant, 964959297 invalid) Sat Nov 4 02:03:36 2023: Starting to write 123578255 entries to data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs71-unfiltered65+.txt. 334209.51 ms (5 min 34 s 209.51 ms) taken to print and save 103402476250 bytes of representative condensed detachment proof strings to data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs71-unfiltered65+.txt. Sat Nov 4 02:10:57 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 71, unfiltered] Sat Nov 4 02:16:18 2023: Process terminated. [pid: 83516, tid:22404950038400]