( 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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40424813 c18m_low 48 COMPLETED 0:0 00:49:37 40424813.ba+ 48 COMPLETED 0:0 00:49:37 93403380K 40424813.ex+ 48 COMPLETED 0:0 00:49:37 0 By 93403380 KiB = (93403380 / 1024^2) GiB = 89.076404571533203125 GiB, it used approximately 89.08 gibibytes of memory. ) Sat Oct 28 13:49:43 2023: Process started. [pid: 37540, tid:22852221302656] 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). Sat Oct 28 13:49:43 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 16.56 ms taken to read 6 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs2.txt. [tid:22851607299840] 20.54 ms taken to read 17 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs3.txt. [tid:22851605198592] 20.39 ms taken to read 28 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs4.txt. [tid:22851603097344] 27.52 ms taken to read 56 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs5.txt. [tid:22851600996096] 24.93 ms taken to read 89 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs6.txt. [tid:22851598894848] 11.80 ms taken to read 203 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs7.txt. [tid:22851596793600] 26.30 ms taken to read 325 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs8.txt. [tid:22851594692352] 15.58 ms taken to read 666 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs9.txt. [tid:22851592591104] 29.61 ms taken to read 1174 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs10.txt. [tid:22851590489856] 27.56 ms taken to read 2340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs11.txt. [tid:22851588388608] 45.63 ms taken to read 4106 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs12.txt. [tid:22851586287360] 57.20 ms taken to read 8396 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs13.txt. [tid:22851584186112] 40.44 ms taken to read 15153 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs14.txt. [tid:22851582084864] 61.06 ms taken to read 30340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs15.txt. [tid:22851579983616] 102.95 ms taken to read 56725 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs16.txt. [tid:22851577882368] 223.70 ms taken to read 113539 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs17.txt. [tid:22850501080832] 680.09 ms taken to read 214468 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs18.txt. [tid:22850498979584] 2360.75 ms (2 s 360.75 ms) taken to read 431896 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs19.txt. [tid:22850496878336] 7880.24 ms (7 s 880.24 ms) taken to read 829754 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs20.txt. [tid:22850494777088] 1300.96 ms (1 s 300.96 ms) taken to read 1666562 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs21.txt. [tid:22850492675840] 1796.62 ms (1 s 796.62 ms) taken to read 3250922 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs22.txt. [tid:22850490574592] 2766.59 ms (2 s 766.59 ms) taken to read 6547739 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs23.txt. [tid:22850488473344] 4374.19 ms (4 s 374.19 ms) taken to read 12887201 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs24.txt. [tid:22850486372096] 7896.57 ms (7 s 896.57 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. 14434.65 ms (14 s 434.65 ms) taken to read 28743307 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs25-unfiltered25+.txt. [tid:22850486372096] 25649.76 ms (25 s 649.76 ms) taken to read 59305631 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs26-unfiltered25+.txt. [tid:22850488473344] 47902.51 ms (47 s 902.51 ms) taken to read 128588180 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs27-unfiltered25+.txt. [tid:22850490574592] 47909.41 ms (47 s 909.41 ms) additional read duration. Loaded 3 more representative collections of sizes: 25 : 28743307 26 : 59305631 27 : 128588180 242698829 representatives in total. Sat Oct 28 13:50:43 2023: Inserted ≈ 5% of D-proof conclusions. [ 12134941 of 242698829] (ETC: Sat Oct 28 13:52:02 2023 ; 1 min 18 s 798.13 ms remaining ; 1 min 22 s 945.40 ms total) Sat Oct 28 13:50:48 2023: Inserted ≈10% of D-proof conclusions. [ 24269882 of 242698829] (ETC: Sat Oct 28 13:52:04 2023 ; 1 min 16 s 660.69 ms remaining ; 1 min 25 s 178.54 ms total) Sat Oct 28 13:50:53 2023: Inserted ≈15% of D-proof conclusions. [ 36404824 of 242698829] (ETC: Sat Oct 28 13:52:08 2023 ; 1 min 15 s 812.59 ms remaining ; 1 min 29 s 191.29 ms total) Sat Oct 28 13:50:57 2023: Inserted ≈20% of D-proof conclusions. [ 48539765 of 242698829] (ETC: Sat Oct 28 13:52:09 2023 ; 1 min 11 s 794.05 ms remaining ; 1 min 29 s 742.56 ms total) Sat Oct 28 13:51:02 2023: Inserted ≈25% of D-proof conclusions. [ 60674707 of 242698829] (ETC: Sat Oct 28 13:52:09 2023 ; 1 min 7 s 607.36 ms remaining ; 1 min 30 s 143.14 ms total) Sat Oct 28 13:51:06 2023: Inserted ≈30% of D-proof conclusions. [ 72809648 of 242698829] (ETC: Sat Oct 28 13:52:10 2023 ; 1 min 3 s 722.84 ms remaining ; 1 min 31 s 32.63 ms total) Sat Oct 28 13:51:11 2023: Inserted ≈35% of D-proof conclusions. [ 84944590 of 242698829] (ETC: Sat Oct 28 13:52:11 2023 ; 59 s 508.02 ms remaining ; 1 min 31 s 550.80 ms total) Sat Oct 28 13:51:16 2023: Inserted ≈40% of D-proof conclusions. [ 97079531 of 242698829] (ETC: Sat Oct 28 13:52:11 2023 ; 55 s 29.80 ms remaining ; 1 min 31 s 716.33 ms total) Sat Oct 28 13:51:20 2023: Inserted ≈45% of D-proof conclusions. [109214473 of 242698829] (ETC: Sat Oct 28 13:52:11 2023 ; 50 s 473.96 ms remaining ; 1 min 31 s 770.84 ms total) Sat Oct 28 13:51:25 2023: Inserted ≈50% of D-proof conclusions. [121349414 of 242698829] (ETC: Sat Oct 28 13:52:10 2023 ; 45 s 627.24 ms remaining ; 1 min 31 s 254.49 ms total) Sat Oct 28 13:51:29 2023: Inserted ≈55% of D-proof conclusions. [133484355 of 242698829] (ETC: Sat Oct 28 13:52:10 2023 ; 40 s 712.91 ms remaining ; 1 min 30 s 473.13 ms total) Sat Oct 28 13:51:34 2023: Inserted ≈60% of D-proof conclusions. [145619297 of 242698829] (ETC: Sat Oct 28 13:52:10 2023 ; 36 s 352.12 ms remaining ; 1 min 30 s 880.29 ms total) Sat Oct 28 13:51:38 2023: Inserted ≈65% of D-proof conclusions. [157754238 of 242698829] (ETC: Sat Oct 28 13:52:10 2023 ; 31 s 823.07 ms remaining ; 1 min 30 s 923.07 ms total) Sat Oct 28 13:51:43 2023: Inserted ≈70% of D-proof conclusions. [169889180 of 242698829] (ETC: Sat Oct 28 13:52:10 2023 ; 27 s 258.92 ms remaining ; 1 min 30 s 863.07 ms total) Sat Oct 28 13:51:47 2023: Inserted ≈75% of D-proof conclusions. [182024121 of 242698829] (ETC: Sat Oct 28 13:52:10 2023 ; 22 s 663.60 ms remaining ; 1 min 30 s 654.38 ms total) Sat Oct 28 13:51:51 2023: Inserted ≈80% of D-proof conclusions. [194159063 of 242698829] (ETC: Sat Oct 28 13:52:09 2023 ; 18 s 73.17 ms remaining ; 1 min 30 s 365.84 ms total) Sat Oct 28 13:51:56 2023: Inserted ≈85% of D-proof conclusions. [206294004 of 242698829] (ETC: Sat Oct 28 13:52:09 2023 ; 13 s 515.74 ms remaining ; 1 min 30 s 104.94 ms total) Sat Oct 28 13:52:00 2023: Inserted ≈90% of D-proof conclusions. [218428946 of 242698829] (ETC: Sat Oct 28 13:52:09 2023 ; 8 s 983.56 ms remaining ; 1 min 29 s 835.62 ms total) Sat Oct 28 13:52:04 2023: Inserted ≈95% of D-proof conclusions. [230563887 of 242698829] (ETC: Sat Oct 28 13:52:09 2023 ; 4 s 486.14 ms remaining ; 1 min 29 s 722.81 ms total) Sat Oct 28 13:52:08 2023: Inserted 100% of D-proof conclusions. [242698829 of 242698829] (ETC: Sat Oct 28 13:52:08 2023 ; 0.00 ms remaining ; 1 min 29 s 304.06 ms total) 89305.01 ms (1 min 29 s 305.01 ms) total insertion duration. Sat Oct 28 13:52:08 2023: Starting to iterate D-proof candidates of length 28. 2578837.81 ms (42 min 58 s 837.81 ms) taken to iterate 4589712682 condensed detachment proof strings of length 28. [Copy] Next iteration count (unfiltered25+): { 28, 4589712682 } Sat Oct 28 14:35:07 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Sat Oct 28 14:39:11 2023: Process terminated. [pid: 37540, tid:22852221302656]