( 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: 80.210555… h CPU utilization: 5133.47555… core-h ) Tue Nov 7 18:17:58 2023: Process started. [pid: 161614, tid:22757254178688] Tasks: 1. resetRepresentativesFor("CpCCNqCCNrsCptCCtqCrq", true, 0, true) 2. generateDProofRepresentativeFiles(73, 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(73, false, true). Tue Nov 7 18:17:58 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 73, unfiltered] 0.01 ms taken to load initial representatives. 10.46 ms taken to read 1 condensed detachment proof and conclusion from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs3.txt. [tid:22757193930496] 25.57 ms taken to read 2 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs5.txt. [tid:22757191829248] 19.48 ms taken to read 4 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs7.txt. [tid:22757189728000] 9.86 ms taken to read 7 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs9.txt. [tid:22757187626752] 21.76 ms taken to read 14 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs11.txt. [tid:22757185525504] 23.02 ms taken to read 23 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs13.txt. [tid:22756951324416] 16.52 ms taken to read 42 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs15.txt. [tid:22757183424256] 22.32 ms taken to read 72 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs17.txt. [tid:22757181323008] 28.78 ms taken to read 119 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs19.txt. [tid:22757179221760] 22.56 ms taken to read 180 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs21.txt. [tid:22757177120512] 20.75 ms taken to read 296 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs23.txt. [tid:22757175019264] 70.77 ms taken to read 493 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs25.txt. [tid:22757172918016] 31.15 ms taken to read 809 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs27.txt. [tid:22757170816768] 161.45 ms taken to read 1330 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs29.txt. [tid:22757168715520] 38.05 ms taken to read 2190 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs31.txt. [tid:22757166614272] 46.64 ms taken to read 3606 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs33.txt. [tid:22757164513024] 54.49 ms taken to read 5925 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs35.txt. [tid:22757162411776] 107.46 ms taken to read 9738 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs37.txt. [tid:22757160310528] 181.52 ms taken to read 15948 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs39.txt. [tid:22757158209280] 467.17 ms taken to read 26109 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs41.txt. [tid:22757156108032] 640.52 ms taken to read 42844 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs43.txt. [tid:22756949223168] 1004.59 ms (1 s 4.59 ms) taken to read 70083 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs45.txt. [tid:22756947121920] 5273.72 ms (5 s 273.73 ms) taken to read 115027 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs47.txt. [tid:22756945020672] 1974.84 ms (1 s 974.84 ms) taken to read 188519 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs49.txt. [tid:22756942919424] 2662.22 ms (2 s 662.22 ms) taken to read 308975 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs51.txt. [tid:22756940818176] 4192.26 ms (4 s 192.26 ms) taken to read 506415 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs53.txt. [tid:22756938716928] 5160.98 ms (5 s 160.98 ms) taken to read 830126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs55.txt. [tid:22756936615680] 6067.49 ms (6 s 67.49 ms) taken to read 1360461 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs57.txt. [tid:22756934514432] 6985.25 ms (6 s 985.25 ms) taken to read 2229126 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs59.txt. [tid:22756932413184] 8636.50 ms (8 s 636.50 ms) taken to read 3652191 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs61.txt. [tid:22756930311936] 9913.64 ms (9 s 913.64 ms) taken to read 5983166 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs63.txt. [tid:22756928210688] 9988.34 ms (9 s 988.34 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. 35890.90 ms (35 s 890.90 ms) taken to read 15025264 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs65-unfiltered65+.txt. [tid:22756928210688] 70286.00 ms (1 min 10 s 286.00 ms) taken to read 32295163 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs67-unfiltered65+.txt. [tid:22756930311936] 118023.64 ms (1 min 58 s 23.64 ms) taken to read 63892072 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs69-unfiltered65+.txt. [tid:22756932413184] 173989.55 ms (2 min 53 s 989.55 ms) taken to read 123578255 condensed detachment proofs and conclusions from data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs71-unfiltered65+.txt. [tid:22756934514432] 174013.36 ms (2 min 54 s 13.36 ms) additional read duration. Loaded 4 more representative collections of sizes: 65 : 15025264 67 : 32295163 69 : 63892072 71 : 123578255 250144596 representatives in total. Tue Nov 7 18:21:32 2023: Inserted ≈ 5% of D-proof conclusions. [ 12507229 of 250144596] (ETC: Tue Nov 7 18:31:00 2023 ; 9 min 28 s 622.27 ms remaining ; 9 min 58 s 549.76 ms total) Tue Nov 7 18:22:00 2023: Inserted ≈10% of D-proof conclusions. [ 25014459 of 250144596] (ETC: Tue Nov 7 18:30:48 2023 ; 8 min 47 s 603.28 ms remaining ; 9 min 46 s 225.86 ms total) Tue Nov 7 18:22:28 2023: Inserted ≈15% of D-proof conclusions. [ 37521689 of 250144596] (ETC: Tue Nov 7 18:30:39 2023 ; 8 min 10 s 641.16 ms remaining ; 9 min 37 s 224.89 ms total) Tue Nov 7 18:22:54 2023: Inserted ≈20% of D-proof conclusions. [ 50028919 of 250144596] (ETC: Tue Nov 7 18:30:22 2023 ; 7 min 27 s 733.09 ms remaining ; 9 min 19 s 666.36 ms total) Tue Nov 7 18:23:32 2023: Inserted ≈25% of D-proof conclusions. [ 62536149 of 250144596] (ETC: Tue Nov 7 18:31:01 2023 ; 7 min 29 s 23.19 ms remaining ; 9 min 58 s 697.58 ms total) Tue Nov 7 18:24:06 2023: Inserted ≈30% of D-proof conclusions. [ 75043378 of 250144596] (ETC: Tue Nov 7 18:31:15 2023 ; 7 min 9 s 360.64 ms remaining ; 10 min 13 s 372.35 ms total) Tue Nov 7 18:24:42 2023: Inserted ≈35% of D-proof conclusions. [ 87550608 of 250144596] (ETC: Tue Nov 7 18:31:30 2023 ; 6 min 48 s 613.45 ms remaining ; 10 min 28 s 636.07 ms total) Tue Nov 7 18:25:18 2023: Inserted ≈40% of D-proof conclusions. [100057838 of 250144596] (ETC: Tue Nov 7 18:31:43 2023 ; 6 min 24 s 962.44 ms remaining ; 10 min 41 s 604.06 ms total) Tue Nov 7 18:25:55 2023: Inserted ≈45% of D-proof conclusions. [112565068 of 250144596] (ETC: Tue Nov 7 18:31:54 2023 ; 5 min 58 s 603.82 ms remaining ; 10 min 52 s 6.94 ms total) Tue Nov 7 18:26:32 2023: Inserted ≈50% of D-proof conclusions. [125072298 of 250144596] (ETC: Tue Nov 7 18:32:03 2023 ; 5 min 30 s 657.56 ms remaining ; 11 min 1 s 315.12 ms total) Tue Nov 7 18:27:04 2023: Inserted ≈55% of D-proof conclusions. [137579527 of 250144596] (ETC: Tue Nov 7 18:32:01 2023 ; 4 min 56 s 539.48 ms remaining ; 10 min 58 s 976.62 ms total) Tue Nov 7 18:27:33 2023: Inserted ≈60% of D-proof conclusions. [150086757 of 250144596] (ETC: Tue Nov 7 18:31:53 2023 ; 4 min 20 s 483.72 ms remaining ; 10 min 51 s 209.30 ms total) Tue Nov 7 18:28:03 2023: Inserted ≈65% of D-proof conclusions. [162593987 of 250144596] (ETC: Tue Nov 7 18:31:49 2023 ; 3 min 46 s 572.69 ms remaining ; 10 min 47 s 350.53 ms total) Tue Nov 7 18:28:34 2023: Inserted ≈70% of D-proof conclusions. [175101217 of 250144596] (ETC: Tue Nov 7 18:31:48 2023 ; 3 min 13 s 906.36 ms remaining ; 10 min 46 s 354.52 ms total) Tue Nov 7 18:29:11 2023: Inserted ≈75% of D-proof conclusions. [187608447 of 250144596] (ETC: Tue Nov 7 18:31:54 2023 ; 2 min 43 s 129.77 ms remaining ; 10 min 52 s 519.06 ms total) Tue Nov 7 18:29:50 2023: Inserted ≈80% of D-proof conclusions. [200115676 of 250144596] (ETC: Tue Nov 7 18:32:01 2023 ; 2 min 11 s 928.14 ms remaining ; 10 min 59 s 640.69 ms total) Tue Nov 7 18:30:39 2023: Inserted ≈85% of D-proof conclusions. [212622906 of 250144596] (ETC: Tue Nov 7 18:32:21 2023 ; 1 min 41 s 887.53 ms remaining ; 11 min 19 s 250.21 ms total) Tue Nov 7 18:31:28 2023: Inserted ≈90% of D-proof conclusions. [225130136 of 250144596] (ETC: Tue Nov 7 18:32:37 2023 ; 1 min 9 s 564.85 ms remaining ; 11 min 35 s 648.45 ms total) Tue Nov 7 18:32:24 2023: Inserted ≈95% of D-proof conclusions. [237637366 of 250144596] (ETC: Tue Nov 7 18:33:00 2023 ; 35 s 888.76 ms remaining ; 11 min 57 s 775.11 ms total) Tue Nov 7 18:33:26 2023: Inserted 100% of D-proof conclusions. [250144596 of 250144596] (ETC: Tue Nov 7 18:33:26 2023 ; 0.00 ms remaining ; 12 min 23 s 675.22 ms total) 743676.87 ms (12 min 23 s 676.87 ms) total insertion duration. Known iteration count loaded from 73:2175612424. Tue Nov 7 18:33:26 2023: Starting to generate D-proof representatives of length 73. Tue Nov 7 20:53:43 2023: Iterated ≈ 2% of D-proof candidates. [ 43512248 of 2175612424] (ETC: Sun Nov 12 15:27:40 2023 ; 4 d 18 h 33 min 57 s 326.79 ms remaining ; 4 d 20 h 54 min 14 s 414.99 ms total) Tue Nov 7 23:25:10 2023: Iterated ≈ 4% of D-proof candidates. [ 87024496 of 2175612424] (ETC: Sun Nov 12 20:07:00 2023 ; 4 d 20 h 41 min 50 s 165.62 ms remaining ; 5 d 1 h 33 min 34 s 755.65 ms total) Wed Nov 8 01:44:19 2023: Iterated ≈ 6% of D-proof candidates. [ 130536745 of 2175612424] (ETC: Sun Nov 12 18:14:56 2023 ; 4 d 16 h 30 min 37 s 482.14 ms remaining ; 4 d 23 h 41 min 30 s 938.35 ms total) Wed Nov 8 04:58:03 2023: Iterated ≈ 8% of D-proof candidates. [ 174048993 of 2175612424] (ETC: Mon Nov 13 04:41:12 2023 ; 4 d 23 h 43 min 8 s 941.22 ms remaining ; 5 d 10 h 7 min 46 s 240.24 ms total) Wed Nov 8 07:44:36 2023: Iterated ≈10% of D-proof candidates. [ 217561242 of 2175612424] (ETC: Mon Nov 13 06:25:06 2023 ; 4 d 22 h 40 min 30 s 721.57 ms remaining ; 5 d 11 h 51 min 40 s 801.64 ms total) Wed Nov 8 09:58:42 2023: Iterated ≈12% of D-proof candidates. [ 261073490 of 2175612424] (ETC: Mon Nov 13 03:04:06 2023 ; 4 d 17 h 5 min 23 s 342.46 ms remaining ; 5 d 8 h 30 min 40 s 161.68 ms total) Wed Nov 8 12:00:53 2023: Iterated ≈14% of D-proof candidates. [ 304585739 of 2175612424] (ETC: Sun Nov 12 23:15:15 2023 ; 4 d 11 h 14 min 22 s 220.03 ms remaining ; 5 d 4 h 41 min 49 s 558.09 ms total) Wed Nov 8 14:10:55 2023: Iterated ≈16% of D-proof candidates. [ 348097987 of 2175612424] (ETC: Sun Nov 12 21:12:43 2023 ; 4 d 7 h 1 min 48 s 380.63 ms remaining ; 5 d 2 h 39 min 17 s 595.78 ms total) Wed Nov 8 16:04:40 2023: Iterated ≈18% of D-proof candidates. [ 391610236 of 2175612424] (ETC: Sun Nov 12 18:06:56 2023 ; 4 d 2 h 2 min 16 s 907.08 ms remaining ; 4 d 23 h 33 min 30 s 862.22 ms total) Wed Nov 8 18:15:38 2023: Iterated ≈20% of D-proof candidates. [ 435122484 of 2175612424] (ETC: Sun Nov 12 17:04:29 2023 ; 3 d 22 h 48 min 50 s 933.60 ms remaining ; 4 d 22 h 31 min 3 s 666.81 ms total) Wed Nov 8 20:11:48 2023: Iterated ≈22% of D-proof candidates. [ 478634733 of 2175612424] (ETC: Sun Nov 12 15:06:03 2023 ; 3 d 18 h 54 min 14 s 747.65 ms remaining ; 4 d 20 h 32 min 37 s 368.71 ms total) Wed Nov 8 21:59:05 2023: Iterated ≈24% of D-proof candidates. [ 522146981 of 2175612424] (ETC: Sun Nov 12 12:50:19 2023 ; 3 d 14 h 51 min 14 s 444.40 ms remaining ; 4 d 18 h 16 min 53 s 742.44 ms total) Wed Nov 8 23:46:10 2023: Iterated ≈26% of D-proof candidates. [ 565659230 of 2175612424] (ETC: Sun Nov 12 10:54:44 2023 ; 3 d 11 h 8 min 34 s 283.80 ms remaining ; 4 d 16 h 21 min 18 s 761.83 ms total) Thu Nov 9 01:28:31 2023: Iterated ≈28% of D-proof candidates. [ 609171478 of 2175612424] (ETC: Sun Nov 12 08:58:43 2023 ; 3 d 7 h 30 min 12 s 654.82 ms remaining ; 4 d 14 h 25 min 17 s 575.95 ms total) Thu Nov 9 03:08:51 2023: Iterated ≈30% of D-proof candidates. [ 652683727 of 2175612424] (ETC: Sun Nov 12 07:11:30 2023 ; 3 d 4 h 2 min 39 s 243.92 ms remaining ; 4 d 12 h 38 min 4 s 634.13 ms total) Thu Nov 9 04:45:32 2023: Iterated ≈32% of D-proof candidates. [ 696195975 of 2175612424] (ETC: Sun Nov 12 05:26:17 2023 ; 3 d 40 min 44 s 352.86 ms remaining ; 4 d 10 h 52 min 51 s 106.97 ms total) Thu Nov 9 06:21:57 2023: Iterated ≈34% of D-proof candidates. [ 739708224 of 2175612424] (ETC: Sun Nov 12 03:52:37 2023 ; 2 d 21 h 30 min 39 s 883.60 ms remaining ; 4 d 9 h 19 min 11 s 338.75 ms total) Thu Nov 9 07:53:49 2023: Iterated ≈36% of D-proof candidates. [ 783220472 of 2175612424] (ETC: Sun Nov 12 02:16:45 2023 ; 2 d 18 h 22 min 55 s 342.89 ms remaining ; 4 d 7 h 43 min 18 s 973.09 ms total) Thu Nov 9 09:24:53 2023: Iterated ≈38% of D-proof candidates. [ 826732721 of 2175612424] (ETC: Sun Nov 12 00:48:50 2023 ; 2 d 15 h 23 min 57 s 350.19 ms remaining ; 4 d 6 h 15 min 24 s 758.34 ms total) Thu Nov 9 10:55:53 2023: Iterated ≈40% of D-proof candidates. [ 870244969 of 2175612424] (ETC: Sat Nov 11 23:29:34 2023 ; 2 d 12 h 33 min 41 s 11.95 ms remaining ; 4 d 4 h 56 min 8 s 353.08 ms total) Thu Nov 9 12:22:17 2023: Iterated ≈42% of D-proof candidates. [ 913757218 of 2175612424] (ETC: Sat Nov 11 22:06:53 2023 ; 2 d 9 h 44 min 36 s 462.22 ms remaining ; 4 d 3 h 33 min 27 s 693.45 ms total) Thu Nov 9 13:52:46 2023: Iterated ≈44% of D-proof candidates. [ 957269466 of 2175612424] (ETC: Sat Nov 11 21:01:02 2023 ; 2 d 7 h 8 min 15 s 407.56 ms remaining ; 4 d 2 h 27 min 36 s 84.77 ms total) Thu Nov 9 15:17:03 2023: Iterated ≈46% of D-proof candidates. [1000781715 of 2175612424] (ETC: Sat Nov 11 19:47:24 2023 ; 2 d 4 h 30 min 20 s 996.69 ms remaining ; 4 d 1 h 13 min 58 s 882.75 ms total) Thu Nov 9 16:43:16 2023: Iterated ≈48% of D-proof candidates. [1044293963 of 2175612424] (ETC: Sat Nov 11 18:43:56 2023 ; 2 d 2 h 39 s 843.09 ms remaining ; 4 d 10 min 30 s 467.33 ms total) Thu Nov 9 18:09:21 2023: Iterated ≈50% of D-proof candidates. [1087806212 of 2175612424] (ETC: Sat Nov 11 17:45:16 2023 ; 1 d 23 h 35 min 55 s 356.15 ms remaining ; 3 d 23 h 11 min 50 s 712.30 ms total) Thu Nov 9 19:30:00 2023: Iterated ≈52% of D-proof candidates. [1131318460 of 2175612424] (ETC: Sat Nov 11 16:40:41 2023 ; 1 d 21 h 10 min 40 s 891.67 ms remaining ; 3 d 22 h 7 min 15 s 190.82 ms total) Thu Nov 9 20:54:46 2023: Iterated ≈54% of D-proof candidates. [1174830708 of 2175612424] (ETC: Sat Nov 11 15:48:30 2023 ; 1 d 18 h 53 min 44 s 252.79 ms remaining ; 3 d 21 h 15 min 4 s 897.05 ms total) Thu Nov 9 22:14:10 2023: Iterated ≈56% of D-proof candidates. [1218342957 of 2175612424] (ETC: Sat Nov 11 14:50:28 2023 ; 1 d 16 h 36 min 17 s 970.96 ms remaining ; 3 d 20 h 17 min 2 s 661.13 ms total) Thu Nov 9 23:31:52 2023: Iterated ≈58% of D-proof candidates. [1261855205 of 2175612424] (ETC: Sat Nov 11 13:53:30 2023 ; 1 d 14 h 21 min 37 s 668.07 ms remaining ; 3 d 19 h 20 min 3 s 971.26 ms total) Fri Nov 10 00:53:09 2023: Iterated ≈60% of D-proof candidates. [1305367454 of 2175612424] (ETC: Sat Nov 11 13:06:18 2023 ; 1 d 12 h 13 min 8 s 888.15 ms remaining ; 3 d 18 h 32 min 52 s 220.23 ms total) Fri Nov 10 02:07:50 2023: Iterated ≈62% of D-proof candidates. [1348879702 of 2175612424] (ETC: Sat Nov 11 12:11:31 2023 ; 1 d 10 h 3 min 40 s 330.34 ms remaining ; 3 d 17 h 38 min 5 s 79.50 ms total) Fri Nov 10 03:24:58 2023: Iterated ≈64% of D-proof candidates. [1392391951 of 2175612424] (ETC: Sat Nov 11 11:23:57 2023 ; 1 d 7 h 58 min 59 s 302.49 ms remaining ; 3 d 16 h 50 min 31 s 395.65 ms total) Fri Nov 10 04:40:42 2023: Iterated ≈66% of D-proof candidates. [1435904199 of 2175612424] (ETC: Sat Nov 11 10:37:10 2023 ; 1 d 5 h 56 min 28 s 370.95 ms remaining ; 3 d 16 h 3 min 44 s 620.09 ms total) Fri Nov 10 05:54:22 2023: Iterated ≈68% of D-proof candidates. [1479416448 of 2175612424] (ETC: Sat Nov 11 09:50:07 2023 ; 1 d 3 h 55 min 44 s 322.01 ms remaining ; 3 d 15 h 16 min 41 s 6.13 ms total) Fri Nov 10 07:10:09 2023: Iterated ≈70% of D-proof candidates. [1522928696 of 2175612424] (ETC: Sat Nov 11 09:08:44 2023 ; 1 d 1 h 58 min 35 s 610.24 ms remaining ; 3 d 14 h 35 min 18 s 700.43 ms total) Fri Nov 10 08:23:00 2023: Iterated ≈72% of D-proof candidates. [1566440945 of 2175612424] (ETC: Sat Nov 11 08:25:37 2023 ; 1 d 2 min 36 s 798.74 ms remaining ; 3 d 13 h 52 min 11 s 423.93 ms total) Fri Nov 10 09:35:40 2023: Iterated ≈74% of D-proof candidates. [1609953193 of 2175612424] (ETC: Sat Nov 11 07:44:34 2023 ; 22 h 8 min 53 s 779.27 ms remaining ; 3 d 13 h 11 min 8 s 381.40 ms total) Fri Nov 10 10:47:57 2023: Iterated ≈76% of D-proof candidates. [1653465442 of 2175612424] (ETC: Sat Nov 11 07:05:10 2023 ; 20 h 17 min 13 s 184.33 ms remaining ; 3 d 12 h 31 min 44 s 934.56 ms total) Fri Nov 10 11:59:08 2023: Iterated ≈78% of D-proof candidates. [1696977690 of 2175612424] (ETC: Sat Nov 11 06:26:23 2023 ; 18 h 27 min 15 s 69.10 ms remaining ; 3 d 11 h 52 min 57 s 586.38 ms total) Fri Nov 10 13:11:20 2023: Iterated ≈80% of D-proof candidates. [1740489939 of 2175612424] (ETC: Sat Nov 11 05:50:49 2023 ; 16 h 39 min 28 s 716.59 ms remaining ; 3 d 11 h 17 min 23 s 582.80 ms total) Fri Nov 10 14:22:05 2023: Iterated ≈82% of D-proof candidates. [1784002187 of 2175612424] (ETC: Sat Nov 11 05:15:12 2023 ; 14 h 53 min 7 s 84.08 ms remaining ; 3 d 10 h 41 min 46 s 22.17 ms total) Fri Nov 10 15:32:22 2023: Iterated ≈84% of D-proof candidates. [1827514436 of 2175612424] (ETC: Sat Nov 11 04:40:44 2023 ; 13 h 8 min 22 s 167.68 ms remaining ; 3 d 10 h 7 min 18 s 547.86 ms total) Fri Nov 10 16:41:56 2023: Iterated ≈86% of D-proof candidates. [1871026684 of 2175612424] (ETC: Sat Nov 11 04:07:02 2023 ; 11 h 25 min 6 s 351.65 ms remaining ; 3 d 9 h 33 min 36 s 796.86 ms total) Fri Nov 10 17:51:53 2023: Iterated ≈88% of D-proof candidates. [1914538933 of 2175612424] (ETC: Sat Nov 11 03:35:18 2023 ; 9 h 43 min 25 s 504.54 ms remaining ; 3 d 9 h 1 min 52 s 537.68 ms total) Fri Nov 10 19:01:32 2023: Iterated ≈90% of D-proof candidates. [1958051181 of 2175612424] (ETC: Sat Nov 11 03:04:39 2023 ; 8 h 3 min 7 s 347.12 ms remaining ; 3 d 8 h 31 min 13 s 470.39 ms total) Fri Nov 10 20:10:34 2023: Iterated ≈92% of D-proof candidates. [2001563430 of 2175612424] (ETC: Sat Nov 11 02:34:40 2023 ; 6 h 24 min 5 s 979.95 ms remaining ; 3 d 8 h 1 min 14 s 749.23 ms total) Fri Nov 10 21:19:38 2023: Iterated ≈94% of D-proof candidates. [2045075678 of 2175612424] (ETC: Sat Nov 11 02:05:59 2023 ; 4 h 46 min 21 s 229.75 ms remaining ; 3 d 7 h 32 min 33 s 827.88 ms total) Fri Nov 10 22:27:50 2023: Iterated ≈96% of D-proof candidates. [2088587927 of 2175612424] (ETC: Sat Nov 11 01:37:36 2023 ; 3 h 9 min 46 s 14.30 ms remaining ; 3 d 7 h 4 min 10 s 357.45 ms total) Fri Nov 10 23:35:35 2023: Iterated ≈98% of D-proof candidates. [2132100175 of 2175612424] (ETC: Sat Nov 11 01:09:55 2023 ; 1 h 34 min 19 s 792.46 ms remaining ; 3 d 6 h 36 min 29 s 619.60 ms total) Sat Nov 11 00:43:05 2023: Iterated 100% of D-proof candidates. [2175612424 of 2175612424] (ETC: Sat Nov 11 00:43:05 2023 ; 0.00 ms remaining ; 3 d 6 h 9 min 39 s 931.50 ms total) 281383853.11 ms (3 d 6 h 9 min 43 s 853.11 ms) taken to collect 241257616 D-proofs of length 73. [iterated 2175612424 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 }, { 73, 2175612424 } } 3483432.75 ms (58 min 3 s 432.75 ms) taken to filter and order new representative proofs. Found 241257616 representative, 224738206 redundant, and 1709616602 invalid condensed detachment proof strings. lengths up to 73 ; 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), (73,241257616)} ; 241257616 new representative proofs (224738206 redundant, 1709616602 invalid) Sat Nov 11 01:56:51 2023: Starting to write 241257616 entries to data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs73-unfiltered65+.txt. 918034.41 ms (15 min 18 s 34.41 ms) taken to print and save 220718480631 bytes of representative condensed detachment proof strings to data/0df075acc552c62513b49b6ed674bfcde1c1b018e532c665be229314/dProofs-withConclusions/dProofs73-unfiltered65+.txt. Sat Nov 11 02:18:53 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 73, unfiltered] Sat Nov 11 02:30:36 2023: Process terminated. [pid: 161614, tid:22757254178688]