( 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 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40412741 c18m_low 48 COMPLETED 0:0 00:24:11 40412741.ba+ 48 COMPLETED 0:0 00:24:11 43271180K 40412741.ex+ 48 COMPLETED 0:0 00:24:11 80K By 43271180 KiB = (43271180 / 1024^2) GiB = 41.266613006591796875 GiB, it used approximately 41.27 gibibytes of memory. ) Fri Oct 27 21:53:35 2023: Process started. [pid: 132716, tid:23202666489728] 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 Oct 27 21:53:35 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 28.51 ms taken to read 6 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs2.txt. [tid:23202067625728] 11.00 ms taken to read 17 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs3.txt. [tid:23202065524480] 11.97 ms taken to read 28 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs4.txt. [tid:23202063423232] 13.93 ms taken to read 56 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs5.txt. [tid:23202061321984] 17.09 ms taken to read 89 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs6.txt. [tid:23202059220736] 27.04 ms taken to read 203 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs7.txt. [tid:23202057119488] 21.49 ms taken to read 325 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs8.txt. [tid:23202055018240] 30.65 ms taken to read 666 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs9.txt. [tid:23202052916992] 15.75 ms taken to read 1174 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs10.txt. [tid:23202050815744] 12.06 ms taken to read 2340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs11.txt. [tid:23202048714496] 113.89 ms taken to read 4106 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs12.txt. [tid:23202046613248] 40.45 ms taken to read 8396 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs13.txt. [tid:23202044512000] 60.27 ms taken to read 15153 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs14.txt. [tid:23202042410752] 72.48 ms taken to read 30340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs15.txt. [tid:23202040309504] 110.25 ms taken to read 56725 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs16.txt. [tid:23202038208256] 229.01 ms taken to read 113539 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs17.txt. [tid:23202036107008] 646.06 ms taken to read 214468 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs18.txt. [tid:23202034005760] 2313.72 ms (2 s 313.72 ms) taken to read 431896 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs19.txt. [tid:23202031904512] 7762.43 ms (7 s 762.43 ms) taken to read 829754 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs20.txt. [tid:23202029803264] 1008.49 ms (1 s 8.49 ms) taken to read 1666562 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs21.txt. [tid:23202027702016] 1661.44 ms (1 s 661.44 ms) taken to read 3250922 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs22.txt. [tid:23202025600768] 2744.53 ms (2 s 744.53 ms) taken to read 6547739 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs23.txt. [tid:23202023499520] 4331.69 ms (4 s 331.69 ms) taken to read 12887201 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs24.txt. [tid:23202021398272] 7777.38 ms (7 s 777.38 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. 13205.74 ms (13 s 205.74 ms) taken to read 28743307 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs25-unfiltered25+.txt. [tid:23202021398272] 21746.45 ms (21 s 746.46 ms) taken to read 59305631 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs26-unfiltered25+.txt. [tid:23202023499520] 21748.77 ms (21 s 748.77 ms) additional read duration. Loaded 2 more representative collections of sizes: 25 : 28743307 26 : 59305631 114110649 representatives in total. Fri Oct 27 21:54:07 2023: Inserted ≈ 5% of D-proof conclusions. [ 5705532 of 114110649] (ETC: Fri Oct 27 21:54:47 2023 ; 40 s 386.25 ms remaining ; 42 s 511.84 ms total) Fri Oct 27 21:54:09 2023: Inserted ≈10% of D-proof conclusions. [ 11411064 of 114110649] (ETC: Fri Oct 27 21:54:46 2023 ; 37 s 70.36 ms remaining ; 41 s 189.29 ms total) Fri Oct 27 21:54:11 2023: Inserted ≈15% of D-proof conclusions. [ 17116597 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 34 s 406.75 ms remaining ; 40 s 478.53 ms total) Fri Oct 27 21:54:13 2023: Inserted ≈20% of D-proof conclusions. [ 22822129 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 32 s 522.62 ms remaining ; 40 s 653.28 ms total) Fri Oct 27 21:54:15 2023: Inserted ≈25% of D-proof conclusions. [ 28527662 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 30 s 210.74 ms remaining ; 40 s 280.99 ms total) Fri Oct 27 21:54:17 2023: Inserted ≈30% of D-proof conclusions. [ 34233194 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 28 s 121.76 ms remaining ; 40 s 173.95 ms total) Fri Oct 27 21:54:19 2023: Inserted ≈35% of D-proof conclusions. [ 39938727 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 26 s 342.81 ms remaining ; 40 s 527.41 ms total) Fri Oct 27 21:54:21 2023: Inserted ≈40% of D-proof conclusions. [ 45644259 of 114110649] (ETC: Fri Oct 27 21:54:46 2023 ; 24 s 401.32 ms remaining ; 40 s 668.87 ms total) Fri Oct 27 21:54:23 2023: Inserted ≈45% of D-proof conclusions. [ 51349792 of 114110649] (ETC: Fri Oct 27 21:54:46 2023 ; 22 s 508.82 ms remaining ; 40 s 925.12 ms total) Fri Oct 27 21:54:25 2023: Inserted ≈50% of D-proof conclusions. [ 57055324 of 114110649] (ETC: Fri Oct 27 21:54:46 2023 ; 20 s 380.33 ms remaining ; 40 s 760.66 ms total) Fri Oct 27 21:54:27 2023: Inserted ≈55% of D-proof conclusions. [ 62760856 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 18 s 188.37 ms remaining ; 40 s 418.59 ms total) Fri Oct 27 21:54:29 2023: Inserted ≈60% of D-proof conclusions. [ 68466389 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 16 s 178.62 ms remaining ; 40 s 446.54 ms total) Fri Oct 27 21:54:31 2023: Inserted ≈65% of D-proof conclusions. [ 74171921 of 114110649] (ETC: Fri Oct 27 21:54:46 2023 ; 14 s 237.30 ms remaining ; 40 s 678.00 ms total) Fri Oct 27 21:54:33 2023: Inserted ≈70% of D-proof conclusions. [ 79877454 of 114110649] (ETC: Fri Oct 27 21:54:46 2023 ; 12 s 232.05 ms remaining ; 40 s 773.50 ms total) Fri Oct 27 21:54:35 2023: Inserted ≈75% of D-proof conclusions. [ 85582986 of 114110649] (ETC: Fri Oct 27 21:54:46 2023 ; 10 s 199.13 ms remaining ; 40 s 796.50 ms total) Fri Oct 27 21:54:37 2023: Inserted ≈80% of D-proof conclusions. [ 91288519 of 114110649] (ETC: Fri Oct 27 21:54:46 2023 ; 8 s 153.96 ms remaining ; 40 s 769.82 ms total) Fri Oct 27 21:54:39 2023: Inserted ≈85% of D-proof conclusions. [ 96994051 of 114110649] (ETC: Fri Oct 27 21:54:46 2023 ; 6 s 108.76 ms remaining ; 40 s 725.08 ms total) Fri Oct 27 21:54:41 2023: Inserted ≈90% of D-proof conclusions. [102699584 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 4 s 60.17 ms remaining ; 40 s 601.68 ms total) Fri Oct 27 21:54:43 2023: Inserted ≈95% of D-proof conclusions. [108405116 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 2 s 23.47 ms remaining ; 40 s 469.48 ms total) Fri Oct 27 21:54:45 2023: Inserted 100% of D-proof conclusions. [114110649 of 114110649] (ETC: Fri Oct 27 21:54:45 2023 ; 0.00 ms remaining ; 40 s 396.25 ms total) 40396.43 ms (40 s 396.43 ms) total insertion duration. Fri Oct 27 21:54:45 2023: Starting to iterate D-proof candidates of length 27. 1291042.77 ms (21 min 31 s 42.77 ms) taken to iterate 2233996317 condensed detachment proof strings of length 27. [Copy] Next iteration count (unfiltered25+): { 27, 2233996317 } Fri Oct 27 22:16:16 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Fri Oct 27 22:17:39 2023: Process terminated. [pid: 132716, tid:23202666489728]