( 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: 18.21888… h CPU utilization: 1166.00888… core-h ) Tue Nov 14 14:43:09 2023: Process started. [pid: 14356, tid:22360061020032] Tasks: 1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(89, false, true) [Main] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69] (1) CCC0.1CCCN2N3.2.4CC4.0C3.0 - CCCpqCCCNrNsrtCCtpCsp - ((0\imply1)\imply(((\not2\imply\not3)\imply2)\imply4))\imply((4\imply0)\imply(3\imply0)) [Main] Calling generateDProofRepresentativeFiles(89, false, true). Tue Nov 14 14:43:09 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 89, unfiltered] 0.01 ms taken to load initial representatives. 14.81 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22360000771840] 19.25 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22359998670592] 26.79 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22359996569344] 10.38 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22359994468096] 16.86 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22359992366848] 27.56 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22359990265600] 17.70 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22359988164352] 15.27 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22359986063104] 23.99 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22359983961856] 9.12 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22359981860608] 22.63 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22359979759360] 19.34 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22359977658112] 27.92 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22359975556864] 31.91 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22359973455616] 26.84 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22359971354368] 27.67 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22359969253120] 33.08 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22359967151872] 20.89 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22359965050624] 35.96 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22359962949376] 23.71 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22359960848128] 48.94 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22359958746880] 51.04 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22359956645632] 58.77 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22359954544384] 61.38 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22359952443136] 80.72 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22359950341888] 77.58 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22359948240640] 767.52 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22359946139392] 642.73 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22359944038144] 996.49 ms taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22359941936896] 2183.92 ms (2 s 183.92 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22359939835648] 5240.87 ms (5 s 240.87 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22359937734400] 7752.52 ms (7 s 752.52 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22358861543168] 2697.08 ms (2 s 697.08 ms) taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22358859441920] 3581.26 ms (3 s 581.26 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22358857340672] 4603.20 ms (4 s 603.20 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22358855239424] 6166.12 ms (6 s 166.12 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22358853138176] 6968.59 ms (6 s 968.59 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22358851036928] 7799.41 ms (7 s 799.41 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22358848935680] 8981.16 ms (8 s 981.16 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:22358846834432] 9770.53 ms (9 s 770.53 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:22358844733184] 9888.96 ms (9 s 888.96 ms) total read duration. Loaded 41 representative collections of sizes: 1 : 1 3 : 1 5 : 2 7 : 3 9 : 6 11 : 7 13 : 12 15 : 15 17 : 23 19 : 36 21 : 61 23 : 99 25 : 152 27 : 214 29 : 299 31 : 400 33 : 560 35 : 797 37 : 1162 39 : 1706 41 : 2502 43 : 3673 45 : 5333 47 : 7756 49 : 11285 51 : 16457 53 : 24156 55 : 35569 57 : 52769 59 : 78319 61 : 116867 63 : 174207 65 : 260535 67 : 389264 69 : 582969 71 : 872258 73 : 1307863 75 : 1959086 77 : 2940441 79 : 4409199 81 : 6623647 19879711 representatives in total. 22443.31 ms (22 s 443.31 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:22358844733184] 35203.24 ms (35 s 203.24 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:22358846834432] 46215.54 ms (46 s 215.54 ms) taken to read 62716073 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt. [tid:22358848935680] 46242.39 ms (46 s 242.39 ms) additional read duration. Loaded 3 more representative collections of sizes: 83 : 22730041 85 : 38726684 87 : 62716073 144052509 representatives in total. Tue Nov 14 14:44:16 2023: Inserted ≈ 5% of D-proof conclusions. [ 7202625 of 144052509] (ETC: Tue Nov 14 14:47:41 2023 ; 3 min 25 s 129.64 ms remaining ; 3 min 35 s 925.93 ms total) Tue Nov 14 14:44:26 2023: Inserted ≈10% of D-proof conclusions. [ 14405250 of 144052509] (ETC: Tue Nov 14 14:47:37 2023 ; 3 min 11 s 68.55 ms remaining ; 3 min 32 s 298.38 ms total) Tue Nov 14 14:44:38 2023: Inserted ≈15% of D-proof conclusions. [ 21607876 of 144052509] (ETC: Tue Nov 14 14:47:44 2023 ; 3 min 5 s 910.11 ms remaining ; 3 min 38 s 717.77 ms total) Tue Nov 14 14:44:45 2023: Inserted ≈20% of D-proof conclusions. [ 28810501 of 144052509] (ETC: Tue Nov 14 14:47:27 2023 ; 2 min 41 s 820.38 ms remaining ; 3 min 22 s 275.48 ms total) Tue Nov 14 14:44:54 2023: Inserted ≈25% of D-proof conclusions. [ 36013127 of 144052509] (ETC: Tue Nov 14 14:47:19 2023 ; 2 min 25 s 607.06 ms remaining ; 3 min 14 s 142.74 ms total) Tue Nov 14 14:45:02 2023: Inserted ≈30% of D-proof conclusions. [ 43215752 of 144052509] (ETC: Tue Nov 14 14:47:15 2023 ; 2 min 12 s 915.14 ms remaining ; 3 min 9 s 878.77 ms total) Tue Nov 14 14:45:09 2023: Inserted ≈35% of D-proof conclusions. [ 50418378 of 144052509] (ETC: Tue Nov 14 14:47:08 2023 ; 1 min 59 s 3.07 ms remaining ; 3 min 3 s 81.65 ms total) Tue Nov 14 14:45:17 2023: Inserted ≈40% of D-proof conclusions. [ 57621003 of 144052509] (ETC: Tue Nov 14 14:47:05 2023 ; 1 min 47 s 753.05 ms remaining ; 2 min 59 s 588.42 ms total) Tue Nov 14 14:45:25 2023: Inserted ≈45% of D-proof conclusions. [ 64823629 of 144052509] (ETC: Tue Nov 14 14:47:04 2023 ; 1 min 38 s 192.13 ms remaining ; 2 min 58 s 531.15 ms total) Tue Nov 14 14:45:35 2023: Inserted ≈50% of D-proof conclusions. [ 72026254 of 144052509] (ETC: Tue Nov 14 14:47:04 2023 ; 1 min 29 s 663.84 ms remaining ; 2 min 59 s 327.67 ms total) Tue Nov 14 14:45:44 2023: Inserted ≈55% of D-proof conclusions. [ 79228879 of 144052509] (ETC: Tue Nov 14 14:47:06 2023 ; 1 min 21 s 227.99 ms remaining ; 3 min 506.65 ms total) Tue Nov 14 14:45:53 2023: Inserted ≈60% of D-proof conclusions. [ 86431505 of 144052509] (ETC: Tue Nov 14 14:47:05 2023 ; 1 min 12 s 153.82 ms remaining ; 3 min 384.55 ms total) Tue Nov 14 14:46:03 2023: Inserted ≈65% of D-proof conclusions. [ 93634130 of 144052509] (ETC: Tue Nov 14 14:47:07 2023 ; 1 min 3 s 534.59 ms remaining ; 3 min 1 s 527.40 ms total) Tue Nov 14 14:46:13 2023: Inserted ≈70% of D-proof conclusions. [100836756 of 144052509] (ETC: Tue Nov 14 14:47:07 2023 ; 54 s 722.09 ms remaining ; 3 min 2 s 406.96 ms total) Tue Nov 14 14:46:23 2023: Inserted ≈75% of D-proof conclusions. [108039381 of 144052509] (ETC: Tue Nov 14 14:47:09 2023 ; 45 s 991.45 ms remaining ; 3 min 3 s 965.81 ms total) Tue Nov 14 14:46:34 2023: Inserted ≈80% of D-proof conclusions. [115242007 of 144052509] (ETC: Tue Nov 14 14:47:11 2023 ; 37 s 202.58 ms remaining ; 3 min 6 s 12.88 ms total) Tue Nov 14 14:46:44 2023: Inserted ≈85% of D-proof conclusions. [122444632 of 144052509] (ETC: Tue Nov 14 14:47:12 2023 ; 28 s 95.38 ms remaining ; 3 min 7 s 302.50 ms total) Tue Nov 14 14:46:54 2023: Inserted ≈90% of D-proof conclusions. [129647258 of 144052509] (ETC: Tue Nov 14 14:47:13 2023 ; 18 s 802.22 ms remaining ; 3 min 8 s 22.20 ms total) Tue Nov 14 14:47:05 2023: Inserted ≈95% of D-proof conclusions. [136849883 of 144052509] (ETC: Tue Nov 14 14:47:14 2023 ; 9 s 448.37 ms remaining ; 3 min 8 s 967.47 ms total) Tue Nov 14 14:47:16 2023: Inserted 100% of D-proof conclusions. [144052509 of 144052509] (ETC: Tue Nov 14 14:47:16 2023 ; 0.00 ms remaining ; 3 min 10 s 497.34 ms total) 190498.77 ms (3 min 10 s 498.77 ms) total insertion duration. Known iteration count loaded from 89:1120159490. Tue Nov 14 14:47:16 2023: Starting to generate D-proof representatives of length 89. Tue Nov 14 15:16:25 2023: Iterated ≈ 2% of D-proof candidates. [ 22403189 of 1120159490] (ETC: Wed Nov 15 15:05:23 2023 ; 23 h 48 min 58 s 88.97 ms remaining ; 1 d 18 min 7 s 845.82 ms total) Tue Nov 14 15:40:43 2023: Iterated ≈ 4% of D-proof candidates. [ 44806379 of 1120159490] (ETC: Wed Nov 15 13:03:42 2023 ; 21 h 22 min 59 s 283.55 ms remaining ; 22 h 16 min 26 s 753.65 ms total) Tue Nov 14 16:06:19 2023: Iterated ≈ 6% of D-proof candidates. [ 67209569 of 1120159490] (ETC: Wed Nov 15 12:45:00 2023 ; 20 h 38 min 40 s 994.86 ms remaining ; 21 h 57 min 44 s 888.12 ms total) Tue Nov 14 16:34:17 2023: Iterated ≈ 8% of D-proof candidates. [ 89612759 of 1120159490] (ETC: Wed Nov 15 13:04:58 2023 ; 20 h 30 min 41 s 498.55 ms remaining ; 22 h 17 min 42 s 498.40 ms total) Tue Nov 14 16:57:31 2023: Iterated ≈10% of D-proof candidates. [ 112015949 of 1120159490] (ETC: Wed Nov 15 12:29:55 2023 ; 19 h 32 min 23 s 417.97 ms remaining ; 21 h 42 min 39 s 353.30 ms total) Tue Nov 14 17:22:34 2023: Iterated ≈12% of D-proof candidates. [ 134419138 of 1120159490] (ETC: Wed Nov 15 12:21:26 2023 ; 18 h 58 min 52 s 317.69 ms remaining ; 21 h 34 min 10 s 360.95 ms total) Tue Nov 14 17:47:53 2023: Iterated ≈14% of D-proof candidates. [ 156822328 of 1120159490] (ETC: Wed Nov 15 12:17:29 2023 ; 18 h 29 min 35 s 636.89 ms remaining ; 21 h 30 min 13 s 531.22 ms total) Tue Nov 14 18:10:46 2023: Iterated ≈16% of D-proof candidates. [ 179225518 of 1120159490] (ETC: Wed Nov 15 11:59:13 2023 ; 17 h 48 min 26 s 656.98 ms remaining ; 21 h 11 min 57 s 448.75 ms total) Tue Nov 14 18:30:56 2023: Iterated ≈18% of D-proof candidates. [ 201628708 of 1120159490] (ETC: Wed Nov 15 11:29:54 2023 ; 16 h 58 min 58 s 268.79 ms remaining ; 20 h 42 min 38 s 864.36 ms total) Tue Nov 14 18:53:02 2023: Iterated ≈20% of D-proof candidates. [ 224031898 of 1120159490] (ETC: Wed Nov 15 11:16:06 2023 ; 16 h 23 min 4 s 300.97 ms remaining ; 20 h 28 min 50 s 376.22 ms total) Tue Nov 14 19:15:23 2023: Iterated ≈22% of D-proof candidates. [ 246435087 of 1120159490] (ETC: Wed Nov 15 11:05:59 2023 ; 15 h 50 min 36 s 574.18 ms remaining ; 20 h 18 min 43 s 812.99 ms total) Tue Nov 14 19:37:11 2023: Iterated ≈24% of D-proof candidates. [ 268838277 of 1120159490] (ETC: Wed Nov 15 10:55:17 2023 ; 15 h 18 min 5 s 769.36 ms remaining ; 20 h 8 min 1 s 275.43 ms total) Tue Nov 14 19:57:26 2023: Iterated ≈26% of D-proof candidates. [ 291241467 of 1120159490] (ETC: Wed Nov 15 10:40:16 2023 ; 14 h 42 min 49 s 297.68 ms remaining ; 19 h 53 min 131.97 ms total) Tue Nov 14 20:18:20 2023: Iterated ≈28% of D-proof candidates. [ 313644657 of 1120159490] (ETC: Wed Nov 15 10:29:39 2023 ; 14 h 11 min 19 s 235.78 ms remaining ; 19 h 42 min 23 s 383.02 ms total) Tue Nov 14 20:38:41 2023: Iterated ≈30% of D-proof candidates. [ 336047847 of 1120159490] (ETC: Wed Nov 15 10:18:39 2023 ; 13 h 39 min 58 s 706.09 ms remaining ; 19 h 31 min 23 s 865.85 ms total) Tue Nov 14 20:59:21 2023: Iterated ≈32% of D-proof candidates. [ 358451036 of 1120159490] (ETC: Wed Nov 15 10:10:01 2023 ; 13 h 10 min 40 s 800.30 ms remaining ; 19 h 22 min 45 s 882.72 ms total) Tue Nov 14 21:19:48 2023: Iterated ≈34% of D-proof candidates. [ 380854226 of 1120159490] (ETC: Wed Nov 15 10:01:47 2023 ; 12 h 41 min 59 s 454.83 ms remaining ; 19 h 14 min 31 s 901.20 ms total) Tue Nov 14 21:40:00 2023: Iterated ≈36% of D-proof candidates. [ 403257416 of 1120159490] (ETC: Wed Nov 15 09:53:47 2023 ; 12 h 13 min 46 s 510.82 ms remaining ; 19 h 6 min 31 s 423.12 ms total) Tue Nov 14 22:00:31 2023: Iterated ≈38% of D-proof candidates. [ 425660606 of 1120159490] (ETC: Wed Nov 15 09:47:24 2023 ; 11 h 46 min 53 s 524.77 ms remaining ; 19 h 8 s 910.90 ms total) Tue Nov 14 22:21:04 2023: Iterated ≈40% of D-proof candidates. [ 448063796 of 1120159490] (ETC: Wed Nov 15 09:41:46 2023 ; 11 h 20 min 42 s 31.83 ms remaining ; 18 h 54 min 30 s 53.05 ms total) Tue Nov 14 22:41:31 2023: Iterated ≈42% of D-proof candidates. [ 470466985 of 1120159490] (ETC: Wed Nov 15 09:36:27 2023 ; 10 h 54 min 55 s 985.49 ms remaining ; 18 h 49 min 11 s 699.03 ms total) Tue Nov 14 23:02:07 2023: Iterated ≈44% of D-proof candidates. [ 492870175 of 1120159490] (ETC: Wed Nov 15 09:31:55 2023 ; 10 h 29 min 48 s 593.12 ms remaining ; 18 h 44 min 39 s 630.51 ms total) Tue Nov 14 23:22:35 2023: Iterated ≈46% of D-proof candidates. [ 515273365 of 1120159490] (ETC: Wed Nov 15 09:27:31 2023 ; 10 h 4 min 56 s 257.16 ms remaining ; 18 h 40 min 15 s 291.00 ms total) Tue Nov 14 23:42:56 2023: Iterated ≈48% of D-proof candidates. [ 537676555 of 1120159490] (ETC: Wed Nov 15 09:23:14 2023 ; 9 h 40 min 18 s 537.16 ms remaining ; 18 h 35 min 58 s 725.28 ms total) Wed Nov 15 00:03:10 2023: Iterated ≈50% of D-proof candidates. [ 560079745 of 1120159490] (ETC: Wed Nov 15 09:19:05 2023 ; 9 h 15 min 54 s 551.37 ms remaining ; 18 h 31 min 49 s 102.75 ms total) Wed Nov 15 00:23:21 2023: Iterated ≈52% of D-proof candidates. [ 582482934 of 1120159490] (ETC: Wed Nov 15 09:15:07 2023 ; 8 h 51 min 46 s 324.35 ms remaining ; 18 h 27 min 51 s 508.97 ms total) Wed Nov 15 00:43:28 2023: Iterated ≈54% of D-proof candidates. [ 604886124 of 1120159490] (ETC: Wed Nov 15 09:11:21 2023 ; 8 h 27 min 52 s 789.73 ms remaining ; 18 h 24 min 5 s 195.00 ms total) Wed Nov 15 01:03:38 2023: Iterated ≈56% of D-proof candidates. [ 627289314 of 1120159490] (ETC: Wed Nov 15 09:07:55 2023 ; 8 h 4 min 17 s 393.66 ms remaining ; 18 h 20 min 39 s 530.98 ms total) Wed Nov 15 01:23:43 2023: Iterated ≈58% of D-proof candidates. [ 649692504 of 1120159490] (ETC: Wed Nov 15 09:04:37 2023 ; 7 h 40 min 53 s 261.61 ms remaining ; 18 h 17 min 21 s 99.03 ms total) Wed Nov 15 01:43:47 2023: Iterated ≈60% of D-proof candidates. [ 672095694 of 1120159490] (ETC: Wed Nov 15 09:01:28 2023 ; 7 h 17 min 40 s 941.00 ms remaining ; 18 h 14 min 12 s 352.50 ms total) Wed Nov 15 02:03:51 2023: Iterated ≈62% of D-proof candidates. [ 694498883 of 1120159490] (ETC: Wed Nov 15 08:58:32 2023 ; 6 h 54 min 41 s 175.05 ms remaining ; 18 h 11 min 16 s 776.34 ms total) Wed Nov 15 02:23:56 2023: Iterated ≈64% of D-proof candidates. [ 716902073 of 1120159490] (ETC: Wed Nov 15 08:55:49 2023 ; 6 h 31 min 52 s 728.07 ms remaining ; 18 h 8 min 33 s 133.44 ms total) Wed Nov 15 02:43:55 2023: Iterated ≈66% of D-proof candidates. [ 739305263 of 1120159490] (ETC: Wed Nov 15 08:53:06 2023 ; 6 h 9 min 11 s 125.00 ms remaining ; 18 h 5 min 50 s 367.58 ms total) Wed Nov 15 03:03:55 2023: Iterated ≈68% of D-proof candidates. [ 761708453 of 1120159490] (ETC: Wed Nov 15 08:50:35 2023 ; 5 h 46 min 39 s 761.15 ms remaining ; 18 h 3 min 19 s 253.55 ms total) Wed Nov 15 03:23:56 2023: Iterated ≈70% of D-proof candidates. [ 784111643 of 1120159490] (ETC: Wed Nov 15 08:48:14 2023 ; 5 h 24 min 17 s 473.12 ms remaining ; 18 h 58 s 243.72 ms total) Wed Nov 15 03:44:15 2023: Iterated ≈72% of D-proof candidates. [ 806514832 of 1120159490] (ETC: Wed Nov 15 08:46:24 2023 ; 5 h 2 min 9 s 658.92 ms remaining ; 17 h 59 min 8 s 781.71 ms total) Wed Nov 15 04:04:22 2023: Iterated ≈74% of D-proof candidates. [ 828918022 of 1120159490] (ETC: Wed Nov 15 08:44:26 2023 ; 4 h 40 min 3 s 976.89 ms remaining ; 17 h 57 min 10 s 680.22 ms total) Wed Nov 15 04:24:49 2023: Iterated ≈76% of D-proof candidates. [ 851321212 of 1120159490] (ETC: Wed Nov 15 08:42:59 2023 ; 4 h 18 min 10 s 448.63 ms remaining ; 17 h 55 min 43 s 535.87 ms total) Wed Nov 15 04:45:07 2023: Iterated ≈78% of D-proof candidates. [ 873724402 of 1120159490] (ETC: Wed Nov 15 08:41:26 2023 ; 3 h 56 min 19 s 31.09 ms remaining ; 17 h 54 min 10 s 141.27 ms total) Wed Nov 15 05:05:30 2023: Iterated ≈80% of D-proof candidates. [ 896127592 of 1120159490] (ETC: Wed Nov 15 08:40:04 2023 ; 3 h 34 min 33 s 724.96 ms remaining ; 17 h 52 min 48 s 624.79 ms total) Wed Nov 15 05:25:53 2023: Iterated ≈82% of D-proof candidates. [ 918530781 of 1120159490] (ETC: Wed Nov 15 08:38:45 2023 ; 3 h 12 min 52 s 152.11 ms remaining ; 17 h 51 min 29 s 733.70 ms total) Wed Nov 15 05:46:17 2023: Iterated ≈84% of D-proof candidates. [ 940933971 of 1120159490] (ETC: Wed Nov 15 08:37:32 2023 ; 2 h 51 min 14 s 569.61 ms remaining ; 17 h 50 min 16 s 59.87 ms total) Wed Nov 15 06:06:43 2023: Iterated ≈86% of D-proof candidates. [ 963337161 of 1120159490] (ETC: Wed Nov 15 08:36:24 2023 ; 2 h 29 min 40 s 760.82 ms remaining ; 17 h 49 min 8 s 291.40 ms total) Wed Nov 15 06:27:12 2023: Iterated ≈88% of D-proof candidates. [ 985740351 of 1120159490] (ETC: Wed Nov 15 08:35:22 2023 ; 2 h 8 min 10 s 385.03 ms remaining ; 17 h 48 min 6 s 541.85 ms total) Wed Nov 15 06:47:34 2023: Iterated ≈90% of D-proof candidates. [1008143541 of 1120159490] (ETC: Wed Nov 15 08:34:16 2023 ; 1 h 46 min 42 s 41.80 ms remaining ; 17 h 47 min 418.06 ms total) Wed Nov 15 07:07:55 2023: Iterated ≈92% of D-proof candidates. [1030546730 of 1120159490] (ETC: Wed Nov 15 08:33:11 2023 ; 1 h 25 min 16 s 446.65 ms remaining ; 17 h 45 min 55 s 582.60 ms total) Wed Nov 15 07:28:12 2023: Iterated ≈94% of D-proof candidates. [1052949920 of 1120159490] (ETC: Wed Nov 15 08:32:06 2023 ; 1 h 3 min 53 s 414.81 ms remaining ; 17 h 44 min 50 s 246.36 ms total) Wed Nov 15 07:48:32 2023: Iterated ≈96% of D-proof candidates. [1075353110 of 1120159490] (ETC: Wed Nov 15 08:31:05 2023 ; 42 min 33 s 173.95 ms remaining ; 17 h 43 min 49 s 348.19 ms total) Wed Nov 15 08:08:37 2023: Iterated ≈98% of D-proof candidates. [1097756300 of 1120159490] (ETC: Wed Nov 15 08:29:52 2023 ; 21 min 15 s 126.38 ms remaining ; 17 h 42 min 36 s 318.43 ms total) Wed Nov 15 08:28:47 2023: Iterated 100% of D-proof candidates. [1120159490 of 1120159490] (ETC: Wed Nov 15 08:28:47 2023 ; 0.00 ms remaining ; 17 h 41 min 30 s 997.85 ms total) 63692386.37 ms (17 h 41 min 32 s 386.37 ms) taken to collect 101227436 D-proofs of length 89. [iterated 1120159490 condensed detachment proof strings] [Copy] Custom iteration counts: { { 1, 1 }, { 3, 1 }, { 5, 2 }, { 7, 5 }, { 9, 10 }, { 11, 22 }, { 13, 38 }, { 15, 71 }, { 17, 118 }, { 19, 202 }, { 21, 334 }, { 23, 569 }, { 25, 950 }, { 27, 1592 }, { 29, 2608 }, { 31, 4241 }, { 33, 6762 }, { 35, 10683 }, { 37, 16666 }, { 39, 25862 }, { 41, 39912 }, { 43, 61603 }, { 45, 94986 }, { 47, 146305 }, { 49, 224682 }, { 51, 343672 }, { 53, 523454 }, { 55, 794596 }, { 57, 1203760 }, { 59, 1822563 }, { 61, 2759474 }, { 63, 4180702 }, { 65, 6335388 }, { 67, 9603788 }, { 69, 14556142 }, { 71, 22063703 }, { 73, 33439008 }, { 75, 50690848 }, { 77, 76854816 }, { 79, 116576814 }, { 81, 176882404 }, { 83, 268514198 }, { 85, 433296910 }, { 87, 692467431 }, { 89, 1120159490 } } 995951.22 ms (16 min 35 s 951.22 ms) taken to filter and order new representative proofs. Found 101227436 representative, 259950010 redundant, and 758982044 invalid condensed detachment proof strings. lengths up to 89 ; amounts per length: {(1,1), (3,1), (5,2), (7,3), (9,6), (11,7), (13,12), (15,15), (17,23), (19,36), (21,61), (23,99), (25,152), (27,214), (29,299), (31,400), (33,560), (35,797), (37,1162), (39,1706), (41,2502), (43,3673), (45,5333), (47,7756), (49,11285), (51,16457), (53,24156), (55,35569), (57,52769), (59,78319), (61,116867), (63,174207), (65,260535), (67,389264), (69,582969), (71,872258), (73,1307863), (75,1959086), (77,2940441), (79,4409199), (81,6623647), (83,22730041), (85,38726684), (87,62716073), (89,101227436)} ; 101227436 new representative proofs (259950010 redundant, 758982044 invalid) Wed Nov 15 08:49:03 2023: Starting to write 101227436 entries to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs89-unfiltered83+.txt. 155542.89 ms (2 min 35 s 542.89 ms) taken to print and save 42757203285 bytes of representative condensed detachment proof strings to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs89-unfiltered83+.txt. Wed Nov 15 08:53:22 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 89, unfiltered] Wed Nov 15 08:56:17 2023: Process terminated. [pid: 14356, tid:22360061020032]