( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40411943 c18m_low 48 COMPLETED 0:0 00:12:15 40411943.ba+ 48 COMPLETED 0:0 00:12:15 20445708K 40411943.ex+ 48 COMPLETED 0:0 00:12:15 12K By 20445708 KiB = (20445708 / 1024^2) GiB = 19.498546600341796875 GiB, it used approximately 19.50 gibibytes of memory. ) Fri Oct 27 14:57:36 2023: Process started. [pid: 11251, tid:22717911299968] 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 14:57:36 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.03 ms taken to load initial representatives. 22.14 ms taken to read 6 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs2.txt. [tid:22717712516864] 20.94 ms taken to read 17 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs3.txt. [tid:22717710415616] 9.59 ms taken to read 28 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs4.txt. [tid:22717708314368] 16.06 ms taken to read 56 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs5.txt. [tid:22717706213120] 16.46 ms taken to read 89 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs6.txt. [tid:22717704111872] 23.31 ms taken to read 203 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs7.txt. [tid:22717702010624] 27.63 ms taken to read 325 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs8.txt. [tid:22717699909376] 27.95 ms taken to read 666 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs9.txt. [tid:22717697808128] 29.21 ms taken to read 1174 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs10.txt. [tid:22717695706880] 18.23 ms taken to read 2340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs11.txt. [tid:22716686006016] 49.52 ms taken to read 4106 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs12.txt. [tid:22716551788288] 27.86 ms taken to read 8396 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs13.txt. [tid:22716683904768] 40.49 ms taken to read 15153 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs14.txt. [tid:22716681803520] 64.84 ms taken to read 30340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs15.txt. [tid:22716679702272] 99.06 ms taken to read 56725 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs16.txt. [tid:22716677601024] 229.01 ms taken to read 113539 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs17.txt. [tid:22716675499776] 641.74 ms taken to read 214468 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs18.txt. [tid:22716673398528] 2222.95 ms (2 s 222.95 ms) taken to read 431896 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs19.txt. [tid:22716671297280] 7979.10 ms (7 s 979.10 ms) taken to read 829754 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs20.txt. [tid:22716669196032] 1069.02 ms (1 s 69.02 ms) taken to read 1666562 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs21.txt. [tid:22716667094784] 1979.21 ms (1 s 979.21 ms) taken to read 3250922 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs22.txt. [tid:22716664993536] 3442.33 ms (3 s 442.33 ms) taken to read 6547739 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs23.txt. [tid:22716662892288] 5284.95 ms (5 s 284.94 ms) taken to read 12887201 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs24.txt. [tid:22716660791040] 7995.53 ms (7 s 995.53 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. 7626.16 ms (7 s 626.16 ms) taken to read 28743307 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs25-unfiltered25+.txt. [tid:22716660791040] 7630.54 ms (7 s 630.54 ms) additional read duration. Loaded 1 more representative collection of size: 25 : 28743307 54805018 representatives in total. Fri Oct 27 14:57:53 2023: Inserted ≈ 5% of D-proof conclusions. [ 2740250 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 21 s 303.43 ms remaining ; 22 s 424.67 ms total) Fri Oct 27 14:57:54 2023: Inserted ≈10% of D-proof conclusions. [ 5480501 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 20 s 575.95 ms remaining ; 22 s 862.16 ms total) Fri Oct 27 14:57:55 2023: Inserted ≈15% of D-proof conclusions. [ 8220752 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 18 s 895.21 ms remaining ; 22 s 229.66 ms total) Fri Oct 27 14:57:56 2023: Inserted ≈20% of D-proof conclusions. [10961003 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 18 s 251.15 ms remaining ; 22 s 813.94 ms total) Fri Oct 27 14:57:57 2023: Inserted ≈25% of D-proof conclusions. [13701254 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 16 s 906.45 ms remaining ; 22 s 541.93 ms total) Fri Oct 27 14:57:58 2023: Inserted ≈30% of D-proof conclusions. [16441505 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 15 s 582.80 ms remaining ; 22 s 261.14 ms total) Fri Oct 27 14:57:59 2023: Inserted ≈35% of D-proof conclusions. [19181756 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 14 s 734.84 ms remaining ; 22 s 668.98 ms total) Fri Oct 27 14:58:01 2023: Inserted ≈40% of D-proof conclusions. [21922007 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 13 s 683.82 ms remaining ; 22 s 806.36 ms total) Fri Oct 27 14:58:02 2023: Inserted ≈45% of D-proof conclusions. [24662258 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 12 s 598.85 ms remaining ; 22 s 907.00 ms total) Fri Oct 27 14:58:03 2023: Inserted ≈50% of D-proof conclusions. [27402509 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 11 s 341.88 ms remaining ; 22 s 683.75 ms total) Fri Oct 27 14:58:04 2023: Inserted ≈55% of D-proof conclusions. [30142759 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 10 s 200.90 ms remaining ; 22 s 668.66 ms total) Fri Oct 27 14:58:05 2023: Inserted ≈60% of D-proof conclusions. [32883010 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 9 s 93.34 ms remaining ; 22 s 733.34 ms total) Fri Oct 27 14:58:06 2023: Inserted ≈65% of D-proof conclusions. [35623261 of 54805018] (ETC: Fri Oct 27 14:58:14 2023 ; 8 s 61.84 ms remaining ; 23 s 33.82 ms total) Fri Oct 27 14:58:08 2023: Inserted ≈70% of D-proof conclusions. [38363512 of 54805018] (ETC: Fri Oct 27 14:58:15 2023 ; 6 s 940.45 ms remaining ; 23 s 134.84 ms total) Fri Oct 27 14:58:09 2023: Inserted ≈75% of D-proof conclusions. [41103763 of 54805018] (ETC: Fri Oct 27 14:58:15 2023 ; 5 s 795.79 ms remaining ; 23 s 183.16 ms total) Fri Oct 27 14:58:10 2023: Inserted ≈80% of D-proof conclusions. [43844014 of 54805018] (ETC: Fri Oct 27 14:58:15 2023 ; 4 s 636.59 ms remaining ; 23 s 182.94 ms total) Fri Oct 27 14:58:11 2023: Inserted ≈85% of D-proof conclusions. [46584265 of 54805018] (ETC: Fri Oct 27 14:58:15 2023 ; 3 s 472.97 ms remaining ; 23 s 153.13 ms total) Fri Oct 27 14:58:12 2023: Inserted ≈90% of D-proof conclusions. [49324516 of 54805018] (ETC: Fri Oct 27 14:58:15 2023 ; 2 s 311.06 ms remaining ; 23 s 110.56 ms total) Fri Oct 27 14:58:13 2023: Inserted ≈95% of D-proof conclusions. [52064767 of 54805018] (ETC: Fri Oct 27 14:58:15 2023 ; 1 s 154.89 ms remaining ; 23 s 97.88 ms total) Fri Oct 27 14:58:15 2023: Inserted 100% of D-proof conclusions. [54805018 of 54805018] (ETC: Fri Oct 27 14:58:15 2023 ; 0.00 ms remaining ; 23 s 72.75 ms total) 23072.91 ms (23 s 72.91 ms) total insertion duration. Fri Oct 27 14:58:15 2023: Starting to iterate D-proof candidates of length 26. 629071.96 ms (10 min 29 s 71.96 ms) taken to iterate 1083165713 condensed detachment proof strings of length 26. [Copy] Next iteration count (unfiltered25+): { 26, 1083165713 } Fri Oct 27 15:08:44 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Fri Oct 27 15:09:24 2023: Process terminated. [pid: 11251, tid:22717911299968]