( This log file was generated by executing 'pmGenerator -c -n -s CCCCCpqCNrNsrtCCtpCsp --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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40400313 c18m_low 48 COMPLETED 0:0 00:31:54 40400313.ba+ 48 COMPLETED 0:0 00:31:54 190238488K 40400313.ex+ 48 COMPLETED 0:0 00:31:54 80K By 190238488 KiB = (190238488 / 1024^2) GiB = 181.42555999755859375 GiB, it used approximately 181.43 gibibytes of memory. ) Fri Oct 27 05:34:32 2023: Process started. [pid: 228064, tid:23037665621888] Tasks: 1. resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CCCCCpqCNrNsrtCCtpCsp", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed] (1) CCCCC0.1CN2N3.2.4CC4.0C3.0 - CCCCCpqCNrNsrtCCtpCsp - ((((0\imply1)\imply(\not2\imply\not3))\imply2)\imply4)\imply((4\imply0)\imply(3\imply0)) [Main] Calling countNextIterationAmount(false, true). Fri Oct 27 05:34:32 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.02 ms taken to load initial representatives. 7.78 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:23037605373696] 17.99 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:23037603272448] 21.79 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:23037399267072] 20.09 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:23037397165824] 17.61 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:23037395064576] 21.71 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:23037130831616] 23.06 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:23037392963328] 16.02 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:23037390862080] 22.33 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:23037388760832] 17.44 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:23037386659584] 24.33 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:23037384558336] 14.11 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:23037382457088] 28.81 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:23037380355840] 28.20 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:23037378254592] 22.29 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:23037376153344] 32.18 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:23037374052096] 58.01 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:23037371950848] 31.36 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:23037369849600] 53.88 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:23037367748352] 48.83 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:23037365647104] 60.72 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:23037363545856] 108.49 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:23037361444608] 187.31 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:23037359343360] 348.26 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:23037357242112] 853.57 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:23037355140864] 2065.11 ms (2 s 65.11 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:23037353039616] 5386.14 ms (5 s 386.14 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:23037350938368] 629.52 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:23037348837120] 991.88 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:23037346735872] 1427.99 ms (1 s 427.99 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:23037344634624] 2061.30 ms (2 s 61.30 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:23037342533376] 2769.20 ms (2 s 769.20 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:23037340432128] 4217.29 ms (4 s 217.29 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:23037338330880] 5712.35 ms (5 s 712.35 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:23037336229632] 5734.26 ms (5 s 734.26 ms) total read duration. Loaded 35 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 7 11 : 10 13 : 13 15 : 19 17 : 37 19 : 56 21 : 87 23 : 140 25 : 227 27 : 369 29 : 579 31 : 918 33 : 1499 35 : 2408 37 : 3881 39 : 6254 41 : 10109 43 : 16460 45 : 26753 47 : 43360 49 : 70709 51 : 115604 53 : 188634 55 : 308241 57 : 504870 59 : 827701 61 : 1357539 63 : 2227822 65 : 3660735 67 : 6021110 69 : 9907537 25303694 representatives in total. 15159.64 ms (15 s 159.64 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:23037336229632] 31424.66 ms (31 s 424.66 ms) taken to read 45156728 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs73-unfiltered71+.txt. [tid:23037338330880] 53664.14 ms (53 s 664.14 ms) taken to read 80141395 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs75-unfiltered71+.txt. [tid:23037340432128] 89596.62 ms (1 min 29 s 596.62 ms) taken to read 143296899 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs77-unfiltered71+.txt. [tid:23037342533376] 89609.23 ms (1 min 29 s 609.23 ms) additional read duration. Loaded 4 more representative collections of sizes: 71 : 23150845 73 : 45156728 75 : 80141395 77 : 143296899 317049561 representatives in total. Fri Oct 27 05:36:15 2023: Inserted ≈ 5% of D-proof conclusions. [ 15852478 of 317049561] (ETC: Fri Oct 27 05:38:46 2023 ; 2 min 30 s 443.65 ms remaining ; 2 min 38 s 361.74 ms total) Fri Oct 27 05:36:23 2023: Inserted ≈10% of D-proof conclusions. [ 31704956 of 317049561] (ETC: Fri Oct 27 05:38:48 2023 ; 2 min 24 s 284.95 ms remaining ; 2 min 40 s 316.61 ms total) Fri Oct 27 05:36:32 2023: Inserted ≈15% of D-proof conclusions. [ 47557434 of 317049561] (ETC: Fri Oct 27 05:38:52 2023 ; 2 min 20 s 142.32 ms remaining ; 2 min 44 s 873.31 ms total) Fri Oct 27 05:36:41 2023: Inserted ≈20% of D-proof conclusions. [ 63409912 of 317049561] (ETC: Fri Oct 27 05:38:54 2023 ; 2 min 13 s 175.29 ms remaining ; 2 min 46 s 469.12 ms total) Fri Oct 27 05:36:50 2023: Inserted ≈25% of D-proof conclusions. [ 79262390 of 317049561] (ETC: Fri Oct 27 05:38:57 2023 ; 2 min 6 s 870.38 ms remaining ; 2 min 49 s 160.51 ms total) Fri Oct 27 05:36:58 2023: Inserted ≈30% of D-proof conclusions. [ 95114868 of 317049561] (ETC: Fri Oct 27 05:38:58 2023 ; 1 min 59 s 217.01 ms remaining ; 2 min 50 s 310.02 ms total) Fri Oct 27 05:37:08 2023: Inserted ≈35% of D-proof conclusions. [110967346 of 317049561] (ETC: Fri Oct 27 05:39:00 2023 ; 1 min 52 s 395.67 ms remaining ; 2 min 52 s 916.41 ms total) Fri Oct 27 05:37:17 2023: Inserted ≈40% of D-proof conclusions. [126819824 of 317049561] (ETC: Fri Oct 27 05:39:02 2023 ; 1 min 44 s 737.87 ms remaining ; 2 min 54 s 563.11 ms total) Fri Oct 27 05:37:27 2023: Inserted ≈45% of D-proof conclusions. [142672302 of 317049561] (ETC: Fri Oct 27 05:39:04 2023 ; 1 min 37 s 369.25 ms remaining ; 2 min 57 s 35.00 ms total) Fri Oct 27 05:37:36 2023: Inserted ≈50% of D-proof conclusions. [158524780 of 317049561] (ETC: Fri Oct 27 05:39:04 2023 ; 1 min 28 s 279.36 ms remaining ; 2 min 56 s 558.72 ms total) Fri Oct 27 05:37:44 2023: Inserted ≈55% of D-proof conclusions. [174377258 of 317049561] (ETC: Fri Oct 27 05:39:03 2023 ; 1 min 19 s 198.27 ms remaining ; 2 min 55 s 996.15 ms total) Fri Oct 27 05:37:52 2023: Inserted ≈60% of D-proof conclusions. [190229736 of 317049561] (ETC: Fri Oct 27 05:39:01 2023 ; 1 min 9 s 570.16 ms remaining ; 2 min 53 s 925.39 ms total) Fri Oct 27 05:37:59 2023: Inserted ≈65% of D-proof conclusions. [206082214 of 317049561] (ETC: Fri Oct 27 05:39:00 2023 ; 1 min 356.69 ms remaining ; 2 min 52 s 447.67 ms total) Fri Oct 27 05:38:07 2023: Inserted ≈70% of D-proof conclusions. [221934692 of 317049561] (ETC: Fri Oct 27 05:38:59 2023 ; 51 s 355.40 ms remaining ; 2 min 51 s 184.68 ms total) Fri Oct 27 05:38:15 2023: Inserted ≈75% of D-proof conclusions. [237787170 of 317049561] (ETC: Fri Oct 27 05:38:57 2023 ; 42 s 495.78 ms remaining ; 2 min 49 s 983.12 ms total) Fri Oct 27 05:38:22 2023: Inserted ≈80% of D-proof conclusions. [253639648 of 317049561] (ETC: Fri Oct 27 05:38:56 2023 ; 33 s 651.38 ms remaining ; 2 min 48 s 256.91 ms total) Fri Oct 27 05:38:30 2023: Inserted ≈85% of D-proof conclusions. [269492126 of 317049561] (ETC: Fri Oct 27 05:38:55 2023 ; 25 s 207.55 ms remaining ; 2 min 48 s 50.36 ms total) Fri Oct 27 05:38:39 2023: Inserted ≈90% of D-proof conclusions. [285344604 of 317049561] (ETC: Fri Oct 27 05:38:56 2023 ; 16 s 847.05 ms remaining ; 2 min 48 s 470.54 ms total) Fri Oct 27 05:38:46 2023: Inserted ≈95% of D-proof conclusions. [301197082 of 317049561] (ETC: Fri Oct 27 05:38:54 2023 ; 8 s 349.49 ms remaining ; 2 min 46 s 989.74 ms total) Fri Oct 27 05:38:52 2023: Inserted 100% of D-proof conclusions. [317049561 of 317049561] (ETC: Fri Oct 27 05:38:52 2023 ; 0.00 ms remaining ; 2 min 44 s 889.31 ms total) 164891.07 ms (2 min 44 s 891.07 ms) total insertion duration. Fri Oct 27 05:38:52 2023: Starting to iterate D-proof candidates of length 79. 1159324.62 ms (19 min 19 s 324.62 ms) taken to iterate 2091875434 condensed detachment proof strings of length 79. [Copy] Next iteration count (unfiltered71+): { 79, 2091875434 } Fri Oct 27 05:58:12 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Fri Oct 27 06:06:06 2023: Process terminated. [pid: 228064, tid:23037665621888]