( 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: 57.82111… h CPU utilization: 3700.55111… core-h ) Fri Nov 17 02:33:19 2023: Process started. [pid: 58784, tid:23272684255104] Tasks: 1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true) 2. generateDProofRepresentativeFiles(93, 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(93, false, true). Fri Nov 17 02:33:19 2023: Limited D-proof representative generator started. [parallel ; 64 hardware thread contexts, limit: 93, unfiltered] 0.01 ms taken to load initial representatives. 25.06 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:23272624006912] 18.17 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:23272621905664] 6.27 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:23272619804416] 14.85 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:23272617703168] 13.01 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:23272615601920] 15.35 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:23272347399936] 15.43 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:23272613500672] 13.79 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:23272611399424] 11.96 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:23272609298176] 21.54 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:23272607196928] 45.00 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:23272605095680] 16.76 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:23272602994432] 34.46 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:23272600893184] 32.18 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:23272598791936] 24.65 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:23272596690688] 23.72 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:23272594589440] 36.51 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:23272592488192] 32.65 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:23272590386944] 121.52 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:23272588285696] 187.37 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:23272586184448] 58.64 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:23272584083200] 162.76 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:23272581981952] 58.47 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:23272579880704] 55.03 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:23272577779456] 223.26 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:23272575678208] 331.91 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:23272573576960] 864.30 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:23272571475712] 785.87 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:23272569374464] 1051.18 ms (1 s 51.19 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:23272567273216] 1747.07 ms (1 s 747.07 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:23272565171968] 4695.66 ms (4 s 695.66 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:23272563070720] 7184.52 ms (7 s 184.52 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:23272560969472] 1944.85 ms (1 s 944.85 ms) taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:23272558868224] 2982.01 ms (2 s 982.01 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:23272556766976] 3986.57 ms (3 s 986.58 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:23272554665728] 5237.96 ms (5 s 237.96 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:23272552564480] 5633.79 ms (5 s 633.79 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:23272345298688] 6394.98 ms (6 s 394.98 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:23272343197440] 7164.92 ms (7 s 164.92 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:23272341096192] 7793.54 ms (7 s 793.54 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:23272338994944] 7878.85 ms (7 s 878.85 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. 50709.61 ms (50 s 709.61 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:23272338994944] 76069.51 ms (1 min 16 s 69.51 ms) taken to read 38726684 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs85-unfiltered83+.txt. [tid:23272341096192] 101081.50 ms (1 min 41 s 81.50 ms) taken to read 62716073 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs87-unfiltered83+.txt. [tid:23272343197440] 134101.63 ms (2 min 14 s 101.63 ms) taken to read 101227436 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs89-unfiltered83+.txt. [tid:23272345298688] 169464.36 ms (2 min 49 s 464.36 ms) taken to read 157874085 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs91-unfiltered83+.txt. [tid:23272552564480] 169496.59 ms (2 min 49 s 496.59 ms) additional read duration. Loaded 5 more representative collections of sizes: 83 : 22730041 85 : 38726684 87 : 62716073 89 : 101227436 91 : 157874085 403154030 representatives in total. Fri Nov 17 02:36:45 2023: Inserted ≈ 5% of D-proof conclusions. [ 20157701 of 403154030] (ETC: Fri Nov 17 02:45:43 2023 ; 8 min 58 s 434.40 ms remaining ; 9 min 26 s 773.05 ms total) Fri Nov 17 02:37:18 2023: Inserted ≈10% of D-proof conclusions. [ 40315403 of 403154030] (ETC: Fri Nov 17 02:46:36 2023 ; 9 min 17 s 310.43 ms remaining ; 10 min 19 s 233.81 ms total) Fri Nov 17 02:37:57 2023: Inserted ≈15% of D-proof conclusions. [ 60473104 of 403154030] (ETC: Fri Nov 17 02:47:25 2023 ; 9 min 28 s 37.35 ms remaining ; 11 min 8 s 279.24 ms total) Fri Nov 17 02:38:42 2023: Inserted ≈20% of D-proof conclusions. [ 80630806 of 403154030] (ETC: Fri Nov 17 02:48:23 2023 ; 9 min 41 s 392.08 ms remaining ; 12 min 6 s 740.10 ms total) Fri Nov 17 02:39:26 2023: Inserted ≈25% of D-proof conclusions. [100788507 of 403154030] (ETC: Fri Nov 17 02:48:53 2023 ; 9 min 27 s 568.74 ms remaining ; 12 min 36 s 758.32 ms total) Fri Nov 17 02:40:08 2023: Inserted ≈30% of D-proof conclusions. [120946209 of 403154030] (ETC: Fri Nov 17 02:49:09 2023 ; 9 min 775.06 ms remaining ; 12 min 52 s 535.80 ms total) Fri Nov 17 02:40:52 2023: Inserted ≈35% of D-proof conclusions. [141103910 of 403154030] (ETC: Fri Nov 17 02:49:25 2023 ; 8 min 32 s 541.98 ms remaining ; 13 min 8 s 526.12 ms total) Fri Nov 17 02:41:21 2023: Inserted ≈40% of D-proof conclusions. [161261612 of 403154030] (ETC: Fri Nov 17 02:48:57 2023 ; 7 min 36 s 309.19 ms remaining ; 12 min 40 s 515.33 ms total) Fri Nov 17 02:41:55 2023: Inserted ≈45% of D-proof conclusions. [181419313 of 403154030] (ETC: Fri Nov 17 02:48:49 2023 ; 6 min 53 s 870.31 ms remaining ; 12 min 32 s 491.47 ms total) Fri Nov 17 02:42:42 2023: Inserted ≈50% of D-proof conclusions. [201577015 of 403154030] (ETC: Fri Nov 17 02:49:07 2023 ; 6 min 25 s 257.62 ms remaining ; 12 min 50 s 515.24 ms total) Fri Nov 17 02:43:31 2023: Inserted ≈55% of D-proof conclusions. [221734716 of 403154030] (ETC: Fri Nov 17 02:49:26 2023 ; 5 min 55 s 309.76 ms remaining ; 13 min 9 s 577.23 ms total) Fri Nov 17 02:44:21 2023: Inserted ≈60% of D-proof conclusions. [241892418 of 403154030] (ETC: Fri Nov 17 02:49:44 2023 ; 5 min 22 s 899.16 ms remaining ; 13 min 27 s 247.90 ms total) Fri Nov 17 02:44:52 2023: Inserted ≈65% of D-proof conclusions. [262050119 of 403154030] (ETC: Fri Nov 17 02:49:29 2023 ; 4 min 37 s 342.45 ms remaining ; 13 min 12 s 407.00 ms total) Fri Nov 17 02:45:19 2023: Inserted ≈70% of D-proof conclusions. [282207821 of 403154030] (ETC: Fri Nov 17 02:49:11 2023 ; 3 min 52 s 422.37 ms remaining ; 12 min 54 s 741.22 ms total) Fri Nov 17 02:45:43 2023: Inserted ≈75% of D-proof conclusions. [302365522 of 403154030] (ETC: Fri Nov 17 02:48:52 2023 ; 3 min 8 s 970.93 ms remaining ; 12 min 35 s 883.73 ms total) Fri Nov 17 02:46:09 2023: Inserted ≈80% of D-proof conclusions. [322523224 of 403154030] (ETC: Fri Nov 17 02:48:38 2023 ; 2 min 28 s 226.61 ms remaining ; 12 min 21 s 133.07 ms total) Fri Nov 17 02:46:39 2023: Inserted ≈85% of D-proof conclusions. [342680925 of 403154030] (ETC: Fri Nov 17 02:48:29 2023 ; 1 min 49 s 873.26 ms remaining ; 12 min 12 s 488.38 ms total) Fri Nov 17 02:47:19 2023: Inserted ≈90% of D-proof conclusions. [362838627 of 403154030] (ETC: Fri Nov 17 02:48:33 2023 ; 1 min 13 s 634.31 ms remaining ; 12 min 16 s 343.08 ms total) Fri Nov 17 02:48:12 2023: Inserted ≈95% of D-proof conclusions. [382996328 of 403154030] (ETC: Fri Nov 17 02:48:50 2023 ; 37 s 663.10 ms remaining ; 12 min 33 s 262.03 ms total) Fri Nov 17 02:49:01 2023: Inserted 100% of D-proof conclusions. [403154030 of 403154030] (ETC: Fri Nov 17 02:49:01 2023 ; 0.00 ms remaining ; 12 min 44 s 906.95 ms total) 764908.30 ms (12 min 44 s 908.31 ms) total insertion duration. Known iteration count loaded from 93:2979484674. Fri Nov 17 02:49:01 2023: Starting to generate D-proof representatives of length 93. Fri Nov 17 04:44:01 2023: Iterated ≈ 2% of D-proof candidates. [ 59589693 of 2979484674] (ETC: Tue Nov 21 02:38:57 2023 ; 3 d 21 h 54 min 56 s 107.62 ms remaining ; 3 d 23 h 49 min 56 s 28.13 ms total) Fri Nov 17 06:09:02 2023: Iterated ≈ 4% of D-proof candidates. [ 119179386 of 2979484674] (ETC: Mon Nov 20 14:09:23 2023 ; 3 d 8 h 21 s 214.58 ms remaining ; 3 d 11 h 20 min 22 s 98.42 ms total) Fri Nov 17 07:47:09 2023: Iterated ≈ 6% of D-proof candidates. [ 178769080 of 2979484674] (ETC: Mon Nov 20 13:37:42 2023 ; 3 d 5 h 50 min 33 s 363.86 ms remaining ; 3 d 10 h 48 min 40 s 599.80 ms total) Fri Nov 17 09:20:27 2023: Iterated ≈ 8% of D-proof candidates. [ 238358773 of 2979484674] (ETC: Mon Nov 20 12:21:48 2023 ; 3 d 3 h 1 min 21 s 329.55 ms remaining ; 3 d 9 h 32 min 46 s 662.46 ms total) Fri Nov 17 10:37:57 2023: Iterated ≈10% of D-proof candidates. [ 297948467 of 2979484674] (ETC: Mon Nov 20 08:58:15 2023 ; 2 d 22 h 20 min 18 s 211.48 ms remaining ; 3 d 6 h 9 min 13 s 568.27 ms total) Fri Nov 17 12:25:06 2023: Iterated ≈12% of D-proof candidates. [ 357538160 of 2979484674] (ETC: Mon Nov 20 10:49:39 2023 ; 2 d 22 h 24 min 33 s 116.07 ms remaining ; 3 d 8 h 37 s 631.80 ms total) Fri Nov 17 13:53:35 2023: Iterated ≈14% of D-proof candidates. [ 417127854 of 2979484674] (ETC: Mon Nov 20 09:55:56 2023 ; 2 d 20 h 2 min 20 s 543.76 ms remaining ; 3 d 7 h 6 min 54 s 585.73 ms total) Fri Nov 17 15:26:22 2023: Iterated ≈16% of D-proof candidates. [ 476717547 of 2979484674] (ETC: Mon Nov 20 09:42:23 2023 ; 2 d 18 h 16 min 1 s 117.96 ms remaining ; 3 d 6 h 53 min 21 s 330.81 ms total) Fri Nov 17 16:50:40 2023: Iterated ≈18% of D-proof candidates. [ 536307241 of 2979484674] (ETC: Mon Nov 20 08:44:51 2023 ; 2 d 15 h 54 min 10 s 562.49 ms remaining ; 3 d 5 h 55 min 49 s 466.41 ms total) Fri Nov 17 18:19:05 2023: Iterated ≈20% of D-proof candidates. [ 595896934 of 2979484674] (ETC: Mon Nov 20 08:19:18 2023 ; 2 d 14 h 12 s 923.54 ms remaining ; 3 d 5 h 30 min 16 s 154.33 ms total) Fri Nov 17 19:49:21 2023: Iterated ≈22% of D-proof candidates. [ 655486628 of 2979484674] (ETC: Mon Nov 20 08:06:52 2023 ; 2 d 12 h 17 min 31 s 298.29 ms remaining ; 3 d 5 h 17 min 50 s 895.21 ms total) Fri Nov 17 21:12:49 2023: Iterated ≈24% of D-proof candidates. [ 715076321 of 2979484674] (ETC: Mon Nov 20 07:28:09 2023 ; 2 d 10 h 15 min 20 s 271.23 ms remaining ; 3 d 4 h 39 min 7 s 725.21 ms total) Fri Nov 17 22:25:42 2023: Iterated ≈26% of D-proof candidates. [ 774666015 of 2979484674] (ETC: Mon Nov 20 06:14:43 2023 ; 2 d 7 h 49 min 468.07 ms remaining ; 3 d 3 h 25 min 41 s 173.05 ms total) Fri Nov 17 23:45:06 2023: Iterated ≈28% of D-proof candidates. [ 834255708 of 2979484674] (ETC: Mon Nov 20 05:35:02 2023 ; 2 d 5 h 49 min 55 s 845.70 ms remaining ; 3 d 2 h 46 min 896.71 ms total) Sat Nov 18 01:03:04 2023: Iterated ≈30% of D-proof candidates. [ 893845402 of 2979484674] (ETC: Mon Nov 20 04:55:49 2023 ; 2 d 3 h 52 min 45 s 627.57 ms remaining ; 3 d 2 h 6 min 48 s 39.36 ms total) Sat Nov 18 02:14:16 2023: Iterated ≈32% of D-proof candidates. [ 953435095 of 2979484674] (ETC: Mon Nov 20 04:00:25 2023 ; 2 d 1 h 46 min 8 s 937.48 ms remaining ; 3 d 1 h 11 min 23 s 731.50 ms total) Sat Nov 18 03:16:08 2023: Iterated ≈34% of D-proof candidates. [1013024789 of 2979484674] (ETC: Mon Nov 20 02:44:03 2023 ; 1 d 23 h 27 min 55 s 102.40 ms remaining ; 2 d 23 h 55 min 1 s 670.29 ms total) Sat Nov 18 04:17:03 2023: Iterated ≈36% of D-proof candidates. [1072614482 of 2979484674] (ETC: Mon Nov 20 01:33:32 2023 ; 1 d 21 h 16 min 29 s 331.39 ms remaining ; 2 d 22 h 44 min 30 s 830.22 ms total) Sat Nov 18 05:21:09 2023: Iterated ≈38% of D-proof candidates. [1132204176 of 2979484674] (ETC: Mon Nov 20 00:38:50 2023 ; 1 d 19 h 17 min 40 s 643.02 ms remaining ; 2 d 21 h 49 min 48 s 133.89 ms total) Sat Nov 18 06:24:41 2023: Iterated ≈40% of D-proof candidates. [1191793869 of 2979484674] (ETC: Sun Nov 19 23:48:09 2023 ; 1 d 17 h 23 min 28 s 672.35 ms remaining ; 2 d 20 h 59 min 7 s 787.17 ms total) Sat Nov 18 07:22:37 2023: Iterated ≈42% of D-proof candidates. [1251383563 of 2979484674] (ETC: Sun Nov 19 22:49:01 2023 ; 1 d 15 h 26 min 23 s 562.21 ms remaining ; 2 d 19 h 59 min 59 s 245.17 ms total) Sat Nov 18 08:20:35 2023: Iterated ≈44% of D-proof candidates. [1310973256 of 2979484674] (ETC: Sun Nov 19 21:55:17 2023 ; 1 d 13 h 34 min 42 s 320.66 ms remaining ; 2 d 19 h 6 min 15 s 572.52 ms total) Sat Nov 18 09:19:21 2023: Iterated ≈46% of D-proof candidates. [1370562950 of 2979484674] (ETC: Sun Nov 19 21:08:00 2023 ; 1 d 11 h 48 min 38 s 637.36 ms remaining ; 2 d 18 h 18 min 58 s 217.33 ms total) Sat Nov 18 10:18:08 2023: Iterated ≈48% of D-proof candidates. [1430152643 of 2979484674] (ETC: Sun Nov 19 20:24:40 2023 ; 1 d 10 h 6 min 32 s 133.71 ms remaining ; 2 d 17 h 35 min 38 s 718.60 ms total) Sat Nov 18 11:16:20 2023: Iterated ≈50% of D-proof candidates. [1489742337 of 2979484674] (ETC: Sun Nov 19 19:43:38 2023 ; 1 d 8 h 27 min 18 s 297.94 ms remaining ; 2 d 16 h 54 min 36 s 595.88 ms total) Sat Nov 18 12:14:50 2023: Iterated ≈52% of D-proof candidates. [1549332030 of 2979484674] (ETC: Sun Nov 19 19:06:21 2023 ; 1 d 6 h 51 min 31 s 127.05 ms remaining ; 2 d 16 h 17 min 19 s 847.95 ms total) Sat Nov 18 13:13:17 2023: Iterated ≈54% of D-proof candidates. [1608921723 of 2979484674] (ETC: Sun Nov 19 18:31:44 2023 ; 1 d 5 h 18 min 26 s 950.28 ms remaining ; 2 d 15 h 42 min 42 s 935.23 ms total) Sat Nov 18 14:11:20 2023: Iterated ≈56% of D-proof candidates. [1668511417 of 2979484674] (ETC: Sun Nov 19 17:58:51 2023 ; 1 d 3 h 47 min 31 s 544.17 ms remaining ; 2 d 15 h 9 min 49 s 873.03 ms total) Sat Nov 18 15:08:20 2023: Iterated ≈58% of D-proof candidates. [1728101110 of 2979484674] (ETC: Sun Nov 19 17:26:27 2023 ; 1 d 2 h 18 min 7 s 291.78 ms remaining ; 2 d 14 h 37 min 25 s 932.65 ms total) Sat Nov 18 16:04:27 2023: Iterated ≈60% of D-proof candidates. [1787690804 of 2979484674] (ETC: Sun Nov 19 16:54:44 2023 ; 1 d 50 min 17 s 239.96 ms remaining ; 2 d 14 h 5 min 43 s 99.83 ms total) Sat Nov 18 17:00:21 2023: Iterated ≈62% of D-proof candidates. [1847280497 of 2979484674] (ETC: Sun Nov 19 16:24:42 2023 ; 23 h 24 min 21 s 465.41 ms remaining ; 2 d 13 h 35 min 40 s 698.28 ms total) Sat Nov 18 17:55:53 2023: Iterated ≈64% of D-proof candidates. [1906870191 of 2979484674] (ETC: Sun Nov 19 15:55:59 2023 ; 22 h 6 s 436.11 ms remaining ; 2 d 13 h 6 min 57 s 878.00 ms total) Sat Nov 18 18:51:36 2023: Iterated ≈66% of D-proof candidates. [1966459884 of 2979484674] (ETC: Sun Nov 19 15:29:18 2023 ; 20 h 37 min 41 s 644.02 ms remaining ; 2 d 12 h 40 min 16 s 599.89 ms total) Sat Nov 18 19:46:54 2023: Iterated ≈68% of D-proof candidates. [2026049578 of 2979484674] (ETC: Sun Nov 19 15:03:33 2023 ; 19 h 16 min 38 s 874.80 ms remaining ; 2 d 12 h 14 min 31 s 483.67 ms total) Sat Nov 18 20:42:36 2023: Iterated ≈70% of D-proof candidates. [2085639271 of 2979484674] (ETC: Sun Nov 19 14:39:50 2023 ; 17 h 57 min 14 s 613.91 ms remaining ; 2 d 11 h 50 min 48 s 712.86 ms total) Sat Nov 18 21:38:08 2023: Iterated ≈72% of D-proof candidates. [2145228965 of 2979484674] (ETC: Sun Nov 19 14:17:13 2023 ; 16 h 39 min 5 s 792.63 ms remaining ; 2 d 11 h 28 min 12 s 116.48 ms total) Sat Nov 18 22:33:57 2023: Iterated ≈74% of D-proof candidates. [2204818658 of 2979484674] (ETC: Sun Nov 19 13:56:13 2023 ; 15 h 22 min 16 s 136.85 ms remaining ; 2 d 11 h 7 min 11 s 295.35 ms total) Sat Nov 18 23:30:02 2023: Iterated ≈76% of D-proof candidates. [2264408352 of 2979484674] (ETC: Sun Nov 19 13:36:40 2023 ; 14 h 6 min 38 s 164.67 ms remaining ; 2 d 10 h 47 min 39 s 19.39 ms total) Sun Nov 19 00:26:10 2023: Iterated ≈78% of D-proof candidates. [2323998045 of 2979484674] (ETC: Sun Nov 19 13:18:10 2023 ; 12 h 52 min 783.33 ms remaining ; 2 d 10 h 29 min 9 s 14.93 ms total) Sun Nov 19 01:22:28 2023: Iterated ≈80% of D-proof candidates. [2383587739 of 2979484674] (ETC: Sun Nov 19 13:00:49 2023 ; 11 h 38 min 21 s 528.48 ms remaining ; 2 d 10 h 11 min 47 s 642.34 ms total) Sun Nov 19 02:18:52 2023: Iterated ≈82% of D-proof candidates. [2443177432 of 2979484674] (ETC: Sun Nov 19 12:44:26 2023 ; 10 h 25 min 34 s 440.98 ms remaining ; 2 d 9 h 55 min 24 s 671.85 ms total) Sun Nov 19 03:15:17 2023: Iterated ≈84% of D-proof candidates. [2502767126 of 2979484674] (ETC: Sun Nov 19 12:28:51 2023 ; 9 h 13 min 34 s 323.42 ms remaining ; 2 d 9 h 39 min 49 s 521.29 ms total) Sun Nov 19 04:11:43 2023: Iterated ≈86% of D-proof candidates. [2562356819 of 2979484674] (ETC: Sun Nov 19 12:14:01 2023 ; 8 h 2 min 17 s 957.70 ms remaining ; 2 d 9 h 24 min 59 s 697.57 ms total) Sun Nov 19 05:08:14 2023: Iterated ≈88% of D-proof candidates. [2621946513 of 2979484674] (ETC: Sun Nov 19 11:59:56 2023 ; 6 h 51 min 42 s 554.30 ms remaining ; 2 d 9 h 10 min 54 s 619.09 ms total) Sun Nov 19 06:04:30 2023: Iterated ≈90% of D-proof candidates. [2681536206 of 2979484674] (ETC: Sun Nov 19 11:46:13 2023 ; 5 h 41 min 43 s 180.59 ms remaining ; 2 d 8 h 57 min 11 s 805.48 ms total) Sun Nov 19 07:00:53 2023: Iterated ≈92% of D-proof candidates. [2741125900 of 2979484674] (ETC: Sun Nov 19 11:33:14 2023 ; 4 h 32 min 20 s 179.04 ms remaining ; 2 d 8 h 44 min 12 s 237.97 ms total) Sun Nov 19 07:57:02 2023: Iterated ≈94% of D-proof candidates. [2800715593 of 2979484674] (ETC: Sun Nov 19 11:20:32 2023 ; 3 h 23 min 29 s 420.00 ms remaining ; 2 d 8 h 31 min 30 s 332.76 ms total) Sun Nov 19 08:53:09 2023: Iterated ≈96% of D-proof candidates. [2860305287 of 2979484674] (ETC: Sun Nov 19 11:08:19 2023 ; 2 h 15 min 10 s 313.12 ms remaining ; 2 d 8 h 19 min 17 s 827.90 ms total) Sun Nov 19 09:49:18 2023: Iterated ≈98% of D-proof candidates. [2919894980 of 2979484674] (ETC: Sun Nov 19 10:56:39 2023 ; 1 h 7 min 21 s 153.07 ms remaining ; 2 d 8 h 7 min 37 s 651.88 ms total) Sun Nov 19 10:45:04 2023: Iterated 100% of D-proof candidates. [2979484674 of 2979484674] (ETC: Sun Nov 19 10:45:04 2023 ; 0.00 ms remaining ; 2 d 7 h 56 min 2 s 385.08 ms total) 201364582.70 ms (2 d 7 h 56 min 4 s 582.71 ms) taken to collect 251856137 D-proofs of length 93. [iterated 2979484674 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 }, { 91, 1817170079 }, { 93, 2979484674 } } 3292362.40 ms (54 min 52 s 362.40 ms) taken to filter and order new representative proofs. Found 251856137 representative, 722570631 redundant, and 2005057906 invalid condensed detachment proof strings. lengths up to 93 ; 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), (91,157874085), (93,251856137)} ; 251856137 new representative proofs (722570631 redundant, 2005057906 invalid) Sun Nov 19 11:58:01 2023: Starting to write 251856137 entries to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs93-unfiltered83+.txt. 444840.59 ms (7 min 24 s 840.59 ms) taken to print and save 112090394619 bytes of representative condensed detachment proof strings to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs93-unfiltered83+.txt. Sun Nov 19 12:10:58 2023: Limited D-proof representative generator complete. [parallel ; 64 hardware thread contexts, limit: 93, unfiltered] Sun Nov 19 12:22:35 2023: Process terminated. [pid: 58784, tid:23272684255104]