( This log file was generated by executing 'pmGenerator -c -n -s CCCpqCCCNrNsrtCCtpCsp --iterate -u' (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 MPI node — 2-socket Intel Xeon Platinum 8160 (Skylake), 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory — running Linux, Rocky 8.8. The job led to the following output: $ sacct --format="JobID,Partition,AllocCPUS,State,ExitCode,Elapsed,MaxRSS" JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS ------------ ---------- ---------- ---------- -------- ---------- ---------- 40363270 c18m_low 48 COMPLETED 0:0 00:05:16 40363270.ba+ 48 COMPLETED 0:0 00:05:16 35607860K 40363270.ex+ 48 COMPLETED 0:0 00:05:16 80K By 35607860 KiB = (35607860 / 1024^2) GiB = 33.958301544189453125 GiB, it used approximately 33.96 gibibytes of memory. ) Thu Oct 26 11:34:06 2023: Process started. [pid: 274050, tid:22714980550528] Tasks: 1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true) 2. countNextIterationAmount(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 countNextIterationAmount(false, true). Thu Oct 26 11:34:06 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.03 ms taken to load initial representatives. 18.80 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22714920302336] 22.90 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22714918201088] 20.66 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22714916099840] 2.93 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22714913998592] 3.00 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22714911897344] 8.92 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22714909796096] 12.86 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22714907694848] 14.85 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22714905593600] 8.17 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22714903492352] 22.88 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22714901391104] 26.84 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22714899289856] 15.79 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22714897188608] 16.04 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22714895087360] 26.88 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22714892986112] 21.76 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22714890884864] 24.14 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22714888783616] 36.79 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22714886682368] 39.84 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22714884581120] 60.86 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22714882479872] 32.01 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22714880378624] 62.68 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22714878277376] 36.02 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22714876176128] 60.20 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22713464780544] 75.08 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22713462679296] 100.77 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22713460578048] 159.46 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22713458476800] 298.03 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22713456375552] 508.02 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22713454274304] 1099.67 ms (1 s 99.67 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22713452173056] 2167.42 ms (2 s 167.42 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22713450071808] 4099.45 ms (4 s 99.45 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22713447970560] 9244.09 ms (9 s 244.09 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22713445869312] 792.84 ms taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22713443768064] 1205.67 ms (1 s 205.67 ms) taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22713441666816] 1652.96 ms (1 s 652.96 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22713439565568] 2125.71 ms (2 s 125.71 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22713437464320] 2818.34 ms (2 s 818.34 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22713435363072] 3442.79 ms (3 s 442.79 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22713433261824] 4426.33 ms (4 s 426.33 ms) taken to read 4409199 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. [tid:22713431160576] 5543.82 ms (5 s 543.82 ms) taken to read 6623647 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs81.txt. [tid:22713429059328] 9271.85 ms (9 s 271.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. 14003.71 ms (14 s 3.71 ms) taken to read 22730041 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs83-unfiltered83+.txt. [tid:22713429059328] 14005.36 ms (14 s 5.36 ms) additional read duration. Loaded 1 more representative collection of size: 83 : 22730041 42609752 representatives in total. Thu Oct 26 11:34:31 2023: Inserted ≈ 5% of D-proof conclusions. [ 2130487 of 42609752] (ETC: Thu Oct 26 11:35:03 2023 ; 31 s 798.98 ms remaining ; 33 s 472.61 ms total) Thu Oct 26 11:34:33 2023: Inserted ≈10% of D-proof conclusions. [ 4260975 of 42609752] (ETC: Thu Oct 26 11:35:04 2023 ; 30 s 699.60 ms remaining ; 34 s 110.67 ms total) Thu Oct 26 11:34:35 2023: Inserted ≈15% of D-proof conclusions. [ 6391462 of 42609752] (ETC: Thu Oct 26 11:35:04 2023 ; 29 s 500.35 ms remaining ; 34 s 706.30 ms total) Thu Oct 26 11:34:37 2023: Inserted ≈20% of D-proof conclusions. [ 8521950 of 42609752] (ETC: Thu Oct 26 11:35:04 2023 ; 27 s 765.29 ms remaining ; 34 s 706.61 ms total) Thu Oct 26 11:34:38 2023: Inserted ≈25% of D-proof conclusions. [10652438 of 42609752] (ETC: Thu Oct 26 11:35:04 2023 ; 26 s 126.38 ms remaining ; 34 s 835.17 ms total) Thu Oct 26 11:34:40 2023: Inserted ≈30% of D-proof conclusions. [12782925 of 42609752] (ETC: Thu Oct 26 11:35:05 2023 ; 24 s 748.79 ms remaining ; 35 s 355.41 ms total) Thu Oct 26 11:34:42 2023: Inserted ≈35% of D-proof conclusions. [14913413 of 42609752] (ETC: Thu Oct 26 11:35:05 2023 ; 23 s 15.00 ms remaining ; 35 s 407.69 ms total) Thu Oct 26 11:34:44 2023: Inserted ≈40% of D-proof conclusions. [17043900 of 42609752] (ETC: Thu Oct 26 11:35:05 2023 ; 21 s 354.17 ms remaining ; 35 s 590.29 ms total) Thu Oct 26 11:34:46 2023: Inserted ≈45% of D-proof conclusions. [19174388 of 42609752] (ETC: Thu Oct 26 11:35:06 2023 ; 19 s 738.91 ms remaining ; 35 s 888.92 ms total) Thu Oct 26 11:34:47 2023: Inserted ≈50% of D-proof conclusions. [21304876 of 42609752] (ETC: Thu Oct 26 11:35:05 2023 ; 17 s 584.98 ms remaining ; 35 s 169.97 ms total) Thu Oct 26 11:34:48 2023: Inserted ≈55% of D-proof conclusions. [23435363 of 42609752] (ETC: Thu Oct 26 11:35:04 2023 ; 15 s 318.95 ms remaining ; 34 s 42.11 ms total) Thu Oct 26 11:34:49 2023: Inserted ≈60% of D-proof conclusions. [25565851 of 42609752] (ETC: Thu Oct 26 11:35:03 2023 ; 13 s 187.33 ms remaining ; 32 s 968.32 ms total) Thu Oct 26 11:34:51 2023: Inserted ≈65% of D-proof conclusions. [27696338 of 42609752] (ETC: Thu Oct 26 11:35:02 2023 ; 11 s 335.71 ms remaining ; 32 s 387.75 ms total) Thu Oct 26 11:34:52 2023: Inserted ≈70% of D-proof conclusions. [29826826 of 42609752] (ETC: Thu Oct 26 11:35:02 2023 ; 9 s 625.95 ms remaining ; 32 s 86.50 ms total) Thu Oct 26 11:34:53 2023: Inserted ≈75% of D-proof conclusions. [31957314 of 42609752] (ETC: Thu Oct 26 11:35:01 2023 ; 7 s 912.18 ms remaining ; 31 s 648.71 ms total) Thu Oct 26 11:34:55 2023: Inserted ≈80% of D-proof conclusions. [34087801 of 42609752] (ETC: Thu Oct 26 11:35:01 2023 ; 6 s 309.84 ms remaining ; 31 s 549.21 ms total) Thu Oct 26 11:34:56 2023: Inserted ≈85% of D-proof conclusions. [36218289 of 42609752] (ETC: Thu Oct 26 11:35:01 2023 ; 4 s 690.04 ms remaining ; 31 s 266.96 ms total) Thu Oct 26 11:34:58 2023: Inserted ≈90% of D-proof conclusions. [38348776 of 42609752] (ETC: Thu Oct 26 11:35:01 2023 ; 3 s 111.18 ms remaining ; 31 s 111.76 ms total) Thu Oct 26 11:34:59 2023: Inserted ≈95% of D-proof conclusions. [40479264 of 42609752] (ETC: Thu Oct 26 11:35:01 2023 ; 1 s 556.01 ms remaining ; 31 s 120.26 ms total) Thu Oct 26 11:35:01 2023: Inserted 100% of D-proof conclusions. [42609752 of 42609752] (ETC: Thu Oct 26 11:35:01 2023 ; 0.00 ms remaining ; 31 s 559.91 ms total) 31560.27 ms (31 s 560.27 ms) total insertion duration. Thu Oct 26 11:35:01 2023: Starting to iterate D-proof candidates of length 85. 199529.46 ms (3 min 19 s 529.46 ms) taken to iterate 433296910 condensed detachment proof strings of length 85. [Copy] Next iteration count (unfiltered83+): { 85, 433296910 } Thu Oct 26 11:38:21 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Thu Oct 26 11:39:16 2023: Process terminated. [pid: 274050, tid:22714980550528]