( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 39699862 c18m 48 COMPLETED 0:0 00:05:30 39699862.ba+ 48 COMPLETED 0:0 00:05:30 26282436K 39699862.ex+ 48 COMPLETED 0:0 00:05:30 0 By 26282436 KiB = (26282436 / 1024^2) GiB = 25.064884185791015625 GiB, it used approximately 25.06 gibibytes of memory. ) Wed Oct 4 07:43:10 2023: Process started. [pid: 209238, tid:23174865581952] 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). Wed Oct 4 07:43:10 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.02 ms taken to load initial representatives. 17.50 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs3.txt. [tid:23174805333760] 17.38 ms taken to read 1 condensed detachment proof and conclusion from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs5.txt. [tid:23174803232512] 23.30 ms taken to read 3 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs7.txt. [tid:23174801131264] 25.59 ms taken to read 7 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs9.txt. [tid:23174799030016] 20.53 ms taken to read 10 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs11.txt. [tid:23174796928768] 18.21 ms taken to read 13 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs13.txt. [tid:23174794827520] 19.89 ms taken to read 19 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs15.txt. [tid:23174792726272] 7.56 ms taken to read 37 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs17.txt. [tid:23174790625024] 16.63 ms taken to read 56 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs19.txt. [tid:23174788523776] 17.32 ms taken to read 87 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs21.txt. [tid:23174786422528] 14.55 ms taken to read 140 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs23.txt. [tid:23174784321280] 20.34 ms taken to read 227 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs25.txt. [tid:23174782220032] 31.10 ms taken to read 369 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs27.txt. [tid:23174780118784] 30.13 ms taken to read 579 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs29.txt. [tid:23174778017536] 29.00 ms taken to read 918 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs31.txt. [tid:23174775916288] 64.96 ms taken to read 1499 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs33.txt. [tid:23174773815040] 45.65 ms taken to read 2408 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs35.txt. [tid:23173630260992] 41.87 ms taken to read 3881 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs37.txt. [tid:23173628159744] 52.08 ms taken to read 6254 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs39.txt. [tid:23173496043264] 51.93 ms taken to read 10109 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs41.txt. [tid:23173626058496] 85.74 ms taken to read 16460 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs43.txt. [tid:23173623957248] 92.64 ms taken to read 26753 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs45.txt. [tid:23173621856000] 183.80 ms taken to read 43360 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs47.txt. [tid:23173619754752] 383.25 ms taken to read 70709 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs49.txt. [tid:23173617653504] 863.54 ms taken to read 115604 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs51.txt. [tid:23173615552256] 2166.37 ms (2 s 166.37 ms) taken to read 188634 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs53.txt. [tid:23173613451008] 5134.28 ms (5 s 134.28 ms) taken to read 308241 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs55.txt. [tid:23173611349760] 539.11 ms taken to read 504870 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs57.txt. [tid:23173609248512] 850.62 ms taken to read 827701 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs59.txt. [tid:23173607147264] 1415.47 ms (1 s 415.47 ms) taken to read 1357539 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs61.txt. [tid:23173605046016] 1976.76 ms (1 s 976.76 ms) taken to read 2227822 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs63.txt. [tid:23173602944768] 2545.83 ms (2 s 545.83 ms) taken to read 3660735 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs65.txt. [tid:23173600843520] 3627.11 ms (3 s 627.11 ms) taken to read 6021110 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs67.txt. [tid:23173598742272] 5094.80 ms (5 s 94.80 ms) taken to read 9907537 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs69.txt. [tid:23173596641024] 5157.35 ms (5 s 157.35 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. 8844.87 ms (8 s 844.87 ms) taken to read 23150845 condensed detachment proofs and conclusions from data/478804cd4793bc7f87041d99326aff4595662146d8a68175dda22bed/dProofs-withConclusions/dProofs71-unfiltered71+.txt. [tid:23173596641024] 8847.31 ms (8 s 847.31 ms) additional read duration. Loaded 1 more representative collection of size: 71 : 23150845 48454539 representatives in total. Wed Oct 4 07:43:25 2023: Inserted ≈ 5% of D-proof conclusions. [ 2422726 of 48454539] (ETC: Wed Oct 4 07:43:37 2023 ; 12 s 354.58 ms remaining ; 13 s 4.83 ms total) Wed Oct 4 07:43:26 2023: Inserted ≈10% of D-proof conclusions. [ 4845453 of 48454539] (ETC: Wed Oct 4 07:43:38 2023 ; 12 s 312.10 ms remaining ; 13 s 680.11 ms total) Wed Oct 4 07:43:26 2023: Inserted ≈15% of D-proof conclusions. [ 7268180 of 48454539] (ETC: Wed Oct 4 07:43:38 2023 ; 11 s 783.08 ms remaining ; 13 s 862.44 ms total) Wed Oct 4 07:43:27 2023: Inserted ≈20% of D-proof conclusions. [ 9690907 of 48454539] (ETC: Wed Oct 4 07:43:39 2023 ; 11 s 848.72 ms remaining ; 14 s 810.90 ms total) Wed Oct 4 07:43:28 2023: Inserted ≈25% of D-proof conclusions. [12113634 of 48454539] (ETC: Wed Oct 4 07:43:40 2023 ; 11 s 905.55 ms remaining ; 15 s 874.07 ms total) Wed Oct 4 07:43:29 2023: Inserted ≈30% of D-proof conclusions. [14536361 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 11 s 778.24 ms remaining ; 16 s 826.06 ms total) Wed Oct 4 07:43:30 2023: Inserted ≈35% of D-proof conclusions. [16959088 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 11 s 168.46 ms remaining ; 17 s 182.25 ms total) Wed Oct 4 07:43:31 2023: Inserted ≈40% of D-proof conclusions. [19381815 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 10 s 362.54 ms remaining ; 17 s 270.91 ms total) Wed Oct 4 07:43:32 2023: Inserted ≈45% of D-proof conclusions. [21804542 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 9 s 561.40 ms remaining ; 17 s 384.36 ms total) Wed Oct 4 07:43:33 2023: Inserted ≈50% of D-proof conclusions. [24227269 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 8 s 780.24 ms remaining ; 17 s 560.48 ms total) Wed Oct 4 07:43:34 2023: Inserted ≈55% of D-proof conclusions. [26649996 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 7 s 897.59 ms remaining ; 17 s 550.19 ms total) Wed Oct 4 07:43:35 2023: Inserted ≈60% of D-proof conclusions. [29072723 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 7 s 34.40 ms remaining ; 17 s 586.00 ms total) Wed Oct 4 07:43:36 2023: Inserted ≈65% of D-proof conclusions. [31495450 of 48454539] (ETC: Wed Oct 4 07:43:42 2023 ; 6 s 95.96 ms remaining ; 17 s 417.02 ms total) Wed Oct 4 07:43:36 2023: Inserted ≈70% of D-proof conclusions. [33918177 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 5 s 180.73 ms remaining ; 17 s 269.11 ms total) Wed Oct 4 07:43:37 2023: Inserted ≈75% of D-proof conclusions. [36340904 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 4 s 275.97 ms remaining ; 17 s 103.87 ms total) Wed Oct 4 07:43:38 2023: Inserted ≈80% of D-proof conclusions. [38763631 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 3 s 395.47 ms remaining ; 16 s 977.37 ms total) Wed Oct 4 07:43:39 2023: Inserted ≈85% of D-proof conclusions. [41186358 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 2 s 543.46 ms remaining ; 16 s 956.42 ms total) Wed Oct 4 07:43:39 2023: Inserted ≈90% of D-proof conclusions. [43609085 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 1 s 685.09 ms remaining ; 16 s 850.90 ms total) Wed Oct 4 07:43:40 2023: Inserted ≈95% of D-proof conclusions. [46031812 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 837.09 ms remaining ; 16 s 741.80 ms total) Wed Oct 4 07:43:41 2023: Inserted 100% of D-proof conclusions. [48454539 of 48454539] (ETC: Wed Oct 4 07:43:41 2023 ; 0.00 ms remaining ; 16 s 611.68 ms total) 16611.87 ms (16 s 611.87 ms) total insertion duration. Wed Oct 4 07:43:41 2023: Starting to iterate D-proof candidates of length 73. 247928.78 ms (4 min 7 s 928.78 ms) taken to iterate 397509772 condensed detachment proof strings of length 73. [Copy] Next iteration count (unfiltered71+): { 73, 397509772 } Wed Oct 4 07:47:49 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Wed Oct 4 07:48:35 2023: Process terminated. [pid: 209238, tid:23174865581952]