( This log file was generated by executing 'pmGenerator -c -N -1 -n -s CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp --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-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. The job led to the following output: $ sacct --format="JobID,Partition,AllocCPUS,State,ExitCode,Elapsed,MaxRSS" JobID Partition AllocCPUS State ExitCode Elapsed MaxRSS ------------ ---------- ---------- ---------- -------- ---------- ---------- 40824221 optane_low 64 COMPLETED 0:0 01:29:54 40824221.ba+ 64 COMPLETED 0:0 01:29:54 199289840K 40824221.ex+ 64 COMPLETED 0:0 01:29:54 76K By 199289840 KiB = (199289840 / 1024^2) GiB = 190.0576019287109375 GiB, it used approximately 190.06 gibibytes of memory. ) Fri Nov 17 08:43:56 2023: Process started. [pid: 267675, tid:23071569139584] Tasks: 1. resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true). Loaded 6 custom axioms. [SHA-512/224 hash: d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f] (1) C0C1.0 - CpCqp - 0\imply(1\imply0) (2) CC0C1.2CC0.1C0.2 - CCpCqrCCpqCpr - (0\imply(1\imply2))\imply((0\imply1)\imply(0\imply2)) (3) CCN0N1C1.0 - CCNpNqCqp - (\not0\imply\not1)\imply(1\imply0) (4) CL0.0 - CLpp - \nece0\imply0 (5) CLC0.1CL0L1 - CLCpqCLpLq - \nece(0\imply1)\imply(\nece0\imply\nece1) (6) CNLN0LNLN0 - CNLNpLNLNp - \not\nece\not0\imply\nece\not\nece\not0 Supports necessitation steps. [Main] Calling countNextIterationAmount(false, true). Fri Nov 17 08:43:56 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 10.88 ms taken to read 6 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs2.txt. [tid:23071381477120] 17.07 ms taken to read 17 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs3.txt. [tid:23071379375872] 19.23 ms taken to read 28 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs4.txt. [tid:23071377274624] 22.94 ms taken to read 56 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs5.txt. [tid:23071375173376] 20.20 ms taken to read 89 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs6.txt. [tid:23071373072128] 16.91 ms taken to read 203 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs7.txt. [tid:23071370970880] 30.44 ms taken to read 325 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs8.txt. [tid:23071368869632] 30.17 ms taken to read 666 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs9.txt. [tid:23071366768384] 13.69 ms taken to read 1174 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs10.txt. [tid:23071364667136] 16.82 ms taken to read 2340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs11.txt. [tid:23071362565888] 33.19 ms taken to read 4106 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs12.txt. [tid:23071360464640] 42.56 ms taken to read 8396 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs13.txt. [tid:23071020807936] 47.00 ms taken to read 15153 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs14.txt. [tid:23071018706688] 53.59 ms taken to read 30340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs15.txt. [tid:23071016605440] 160.55 ms taken to read 56725 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs16.txt. [tid:23071014504192] 410.03 ms taken to read 113539 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs17.txt. [tid:23071012402944] 578.37 ms taken to read 214468 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs18.txt. [tid:23071010301696] 1979.72 ms (1 s 979.72 ms) taken to read 431896 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs19.txt. [tid:23071008200448] 4979.12 ms (4 s 979.12 ms) taken to read 829754 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs20.txt. [tid:23071006099200] 1898.30 ms (1 s 898.30 ms) taken to read 1666562 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs21.txt. [tid:23071003997952] 2799.43 ms (2 s 799.43 ms) taken to read 3250922 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs22.txt. [tid:23071001896704] 3651.76 ms (3 s 651.76 ms) taken to read 6547739 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs23.txt. [tid:23070999795456] 5070.74 ms (5 s 70.74 ms) taken to read 12887201 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs24.txt. [tid:23070997694208] 5126.57 ms (5 s 126.58 ms) total read duration. Loaded 24 representative collections of sizes: 1 : 6 2 : 6 3 : 17 4 : 28 5 : 56 6 : 89 7 : 203 8 : 325 9 : 666 10 : 1174 11 : 2340 12 : 4106 13 : 8396 14 : 15153 15 : 30340 16 : 56725 17 : 113539 18 : 214468 19 : 431896 20 : 829754 21 : 1666562 22 : 3250922 23 : 6547739 24 : 12887201 26061711 representatives in total. 15592.96 ms (15 s 592.96 ms) taken to read 28743307 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs25-unfiltered25+.txt. [tid:23070997694208] 35019.15 ms (35 s 19.15 ms) taken to read 59305631 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs26-unfiltered25+.txt. [tid:23070999795456] 68803.65 ms (1 min 8 s 803.65 ms) taken to read 128588180 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs27-unfiltered25+.txt. [tid:23071001896704] 107887.67 ms (1 min 47 s 887.67 ms) taken to read 268614600 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs28-unfiltered25+.txt. [tid:23071003997952] 107896.73 ms (1 min 47 s 896.73 ms) additional read duration. Loaded 4 more representative collections of sizes: 25 : 28743307 26 : 59305631 27 : 128588180 28 : 268614600 511313429 representatives in total. Fri Nov 17 08:46:11 2023: Inserted ≈ 5% of D-proof conclusions. [ 25565671 of 511313429] (ETC: Fri Nov 17 08:53:09 2023 ; 6 min 58 s 211.76 ms remaining ; 7 min 20 s 222.91 ms total) Fri Nov 17 08:46:35 2023: Inserted ≈10% of D-proof conclusions. [ 51131342 of 511313429] (ETC: Fri Nov 17 08:53:28 2023 ; 6 min 52 s 664.56 ms remaining ; 7 min 38 s 516.18 ms total) Fri Nov 17 08:47:00 2023: Inserted ≈15% of D-proof conclusions. [ 76697014 of 511313429] (ETC: Fri Nov 17 08:53:43 2023 ; 6 min 43 s 70.95 ms remaining ; 7 min 54 s 201.12 ms total) Fri Nov 17 08:47:24 2023: Inserted ≈20% of D-proof conclusions. [102262685 of 511313429] (ETC: Fri Nov 17 08:53:46 2023 ; 6 min 21 s 141.96 ms remaining ; 7 min 56 s 427.44 ms total) Fri Nov 17 08:47:44 2023: Inserted ≈25% of D-proof conclusions. [127828357 of 511313429] (ETC: Fri Nov 17 08:53:30 2023 ; 5 min 45 s 736.44 ms remaining ; 7 min 40 s 981.92 ms total) Fri Nov 17 08:48:04 2023: Inserted ≈30% of D-proof conclusions. [153394028 of 511313429] (ETC: Fri Nov 17 08:53:17 2023 ; 5 min 13 s 733.93 ms remaining ; 7 min 28 s 191.32 ms total) Fri Nov 17 08:48:22 2023: Inserted ≈35% of D-proof conclusions. [178959700 of 511313429] (ETC: Fri Nov 17 08:53:07 2023 ; 4 min 44 s 561.01 ms remaining ; 7 min 17 s 786.17 ms total) Fri Nov 17 08:48:40 2023: Inserted ≈40% of D-proof conclusions. [204525371 of 511313429] (ETC: Fri Nov 17 08:52:56 2023 ; 4 min 15 s 957.46 ms remaining ; 7 min 6 s 595.77 ms total) Fri Nov 17 08:48:57 2023: Inserted ≈45% of D-proof conclusions. [230091043 of 511313429] (ETC: Fri Nov 17 08:52:47 2023 ; 3 min 49 s 620.46 ms remaining ; 6 min 57 s 491.75 ms total) Fri Nov 17 08:49:18 2023: Inserted ≈50% of D-proof conclusions. [255656714 of 511313429] (ETC: Fri Nov 17 08:52:47 2023 ; 3 min 28 s 807.42 ms remaining ; 6 min 57 s 614.84 ms total) Fri Nov 17 08:49:36 2023: Inserted ≈55% of D-proof conclusions. [281222385 of 511313429] (ETC: Fri Nov 17 08:52:42 2023 ; 3 min 5 s 621.40 ms remaining ; 6 min 52 s 492.00 ms total) Fri Nov 17 08:49:54 2023: Inserted ≈60% of D-proof conclusions. [306788057 of 511313429] (ETC: Fri Nov 17 08:52:37 2023 ; 2 min 42 s 973.68 ms remaining ; 6 min 47 s 434.21 ms total) Fri Nov 17 08:50:11 2023: Inserted ≈65% of D-proof conclusions. [332353728 of 511313429] (ETC: Fri Nov 17 08:52:33 2023 ; 2 min 21 s 164.94 ms remaining ; 6 min 43 s 328.41 ms total) Fri Nov 17 08:50:29 2023: Inserted ≈70% of D-proof conclusions. [357919400 of 511313429] (ETC: Fri Nov 17 08:52:29 2023 ; 1 min 59 s 879.96 ms remaining ; 6 min 39 s 599.85 ms total) Fri Nov 17 08:50:47 2023: Inserted ≈75% of D-proof conclusions. [383485071 of 511313429] (ETC: Fri Nov 17 08:52:26 2023 ; 1 min 39 s 149.90 ms remaining ; 6 min 36 s 599.59 ms total) Fri Nov 17 08:51:04 2023: Inserted ≈80% of D-proof conclusions. [409050743 of 511313429] (ETC: Fri Nov 17 08:52:23 2023 ; 1 min 18 s 812.72 ms remaining ; 6 min 34 s 63.62 ms total) Fri Nov 17 08:51:23 2023: Inserted ≈85% of D-proof conclusions. [434616414 of 511313429] (ETC: Fri Nov 17 08:52:22 2023 ; 58 s 896.75 ms remaining ; 6 min 32 s 645.03 ms total) Fri Nov 17 08:51:42 2023: Inserted ≈90% of D-proof conclusions. [460182086 of 511313429] (ETC: Fri Nov 17 08:52:21 2023 ; 39 s 176.86 ms remaining ; 6 min 31 s 768.59 ms total) Fri Nov 17 08:52:04 2023: Inserted ≈95% of D-proof conclusions. [485747757 of 511313429] (ETC: Fri Nov 17 08:52:24 2023 ; 19 s 745.21 ms remaining ; 6 min 34 s 904.09 ms total) Fri Nov 17 08:52:30 2023: Inserted 100% of D-proof conclusions. [511313429 of 511313429] (ETC: Fri Nov 17 08:52:30 2023 ; 0.00 ms remaining ; 6 min 40 s 783.42 ms total) 400783.64 ms (6 min 40 s 783.64 ms) total insertion duration. Fri Nov 17 08:52:30 2023: Starting to iterate D-proof candidates of length 29. 4390702.74 ms (1 h 13 min 10 s 702.74 ms) taken to iterate 9565398427 condensed detachment proof strings of length 29. [Copy] Next iteration count (unfiltered25+): { 29, 9565398427 } Fri Nov 17 10:05:52 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Fri Nov 17 10:13:38 2023: Process terminated. [pid: 267675, tid:23071569139584]