( This log file was generated by executing 'pmGenerator -c -n -s CpCCqCprCCNrCCNstqCsr --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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 39801022 c18m_low 48 COMPLETED 0:0 00:01:47 39801022.ba+ 48 COMPLETED 0:0 00:01:47 28120984K 39801022.ex+ 48 COMPLETED 0:0 00:01:47 80K By 28120984 KiB = (28120984 / 1024^2) GiB = 26.81826019287109375 GiB, it used approximately 26.82 gibibytes of memory. ) Mon Oct 9 07:24:14 2023: Process started. [pid: 35094, tid:22462652753792] Tasks: 1. resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true) 2. countNextIterationAmount(false, true) [Main] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff] (1) C0CC1C0.2CCN2CCN3.4.1C3.2 - CpCCqCprCCNrCCNstqCsr - 0\imply((1\imply(0\imply2))\imply((\not2\imply((\not3\imply4)\imply1))\imply(3\imply2))) [Main] Calling countNextIterationAmount(false, true). Mon Oct 9 07:24:14 2023: Next iteration amount counter started. [parallel ; 48 hardware thread contexts, unfiltered] 0.04 ms taken to load initial representatives. 21.03 ms taken to read 1 condensed detachment proof and conclusion from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs3.txt. [tid:22462592505600] 15.05 ms taken to read 2 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs5.txt. [tid:22462590404352] 23.06 ms taken to read 5 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs7.txt. [tid:22462588303104] 14.84 ms taken to read 10 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs9.txt. [tid:22462586201856] 21.03 ms taken to read 24 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs11.txt. [tid:22462584100608] 32.20 ms taken to read 57 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs13.txt. [tid:22462581999360] 29.32 ms taken to read 137 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs15.txt. [tid:22462579898112] 24.52 ms taken to read 339 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs17.txt. [tid:22462577796864] 53.57 ms taken to read 854 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs19.txt. [tid:22462575695616] 63.28 ms taken to read 2171 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs21.txt. [tid:22462573594368] 102.60 ms taken to read 5583 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs23.txt. [tid:22462571493120] 551.52 ms taken to read 14478 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs25.txt. [tid:22462569391872] 3641.27 ms (3 s 641.26 ms) taken to read 37874 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs27.txt. [tid:22462567290624] 293.70 ms taken to read 99756 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs29.txt. [tid:22462565189376] 979.97 ms taken to read 264466 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs31.txt. [tid:22462563088128] 2673.12 ms (2 s 673.12 ms) taken to read 705026 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs33.txt. [tid:22462560986880] 5791.39 ms (5 s 791.39 ms) taken to read 1888450 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs35.txt. [tid:22462558885632] 13450.79 ms (13 s 450.79 ms) taken to read 5081180 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs37.txt. [tid:22462556784384] 13464.14 ms (13 s 464.14 ms) total read duration. Loaded 19 representative collections of sizes: 1 : 1 3 : 1 5 : 2 7 : 5 9 : 10 11 : 24 13 : 57 15 : 137 17 : 339 19 : 854 21 : 2171 23 : 5583 25 : 14478 27 : 37874 29 : 99756 31 : 264466 33 : 705026 35 : 1888450 37 : 5081180 8100414 representatives in total. Mon Oct 9 07:24:29 2023: Inserted ≈ 5% of D-proof conclusions. [ 405020 of 8100414] (ETC: Mon Oct 9 07:24:54 2023 ; 24 s 727.06 ms remaining ; 26 s 28.48 ms total) Mon Oct 9 07:24:30 2023: Inserted ≈10% of D-proof conclusions. [ 810041 of 8100414] (ETC: Mon Oct 9 07:24:55 2023 ; 24 s 445.09 ms remaining ; 27 s 161.21 ms total) Mon Oct 9 07:24:32 2023: Inserted ≈15% of D-proof conclusions. [1215062 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 25 s 378.08 ms remaining ; 29 s 856.56 ms total) Mon Oct 9 07:24:34 2023: Inserted ≈20% of D-proof conclusions. [1620082 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 24 s 29.34 ms remaining ; 30 s 36.67 ms total) Mon Oct 9 07:24:35 2023: Inserted ≈25% of D-proof conclusions. [2025103 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 23 s 53.27 ms remaining ; 30 s 737.70 ms total) Mon Oct 9 07:24:37 2023: Inserted ≈30% of D-proof conclusions. [2430124 of 8100414] (ETC: Mon Oct 9 07:24:59 2023 ; 22 s 182.90 ms remaining ; 31 s 689.86 ms total) Mon Oct 9 07:24:39 2023: Inserted ≈35% of D-proof conclusions. [2835144 of 8100414] (ETC: Mon Oct 9 07:25:00 2023 ; 21 s 2.77 ms remaining ; 32 s 311.95 ms total) Mon Oct 9 07:24:40 2023: Inserted ≈40% of D-proof conclusions. [3240165 of 8100414] (ETC: Mon Oct 9 07:25:00 2023 ; 19 s 286.24 ms remaining ; 32 s 143.73 ms total) Mon Oct 9 07:24:42 2023: Inserted ≈45% of D-proof conclusions. [3645186 of 8100414] (ETC: Mon Oct 9 07:24:59 2023 ; 17 s 74.59 ms remaining ; 31 s 44.72 ms total) Mon Oct 9 07:24:43 2023: Inserted ≈50% of D-proof conclusions. [4050207 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 15 s 200.89 ms remaining ; 30 s 401.79 ms total) Mon Oct 9 07:24:44 2023: Inserted ≈55% of D-proof conclusions. [4455227 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 13 s 474.59 ms remaining ; 29 s 943.53 ms total) Mon Oct 9 07:24:45 2023: Inserted ≈60% of D-proof conclusions. [4860248 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 11 s 855.61 ms remaining ; 29 s 639.03 ms total) Mon Oct 9 07:24:47 2023: Inserted ≈65% of D-proof conclusions. [5265269 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 10 s 317.20 ms remaining ; 29 s 477.72 ms total) Mon Oct 9 07:24:48 2023: Inserted ≈70% of D-proof conclusions. [5670289 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 8 s 756.34 ms remaining ; 29 s 187.78 ms total) Mon Oct 9 07:24:49 2023: Inserted ≈75% of D-proof conclusions. [6075310 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 7 s 289.26 ms remaining ; 29 s 157.05 ms total) Mon Oct 9 07:24:51 2023: Inserted ≈80% of D-proof conclusions. [6480331 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 5 s 858.50 ms remaining ; 29 s 292.49 ms total) Mon Oct 9 07:24:53 2023: Inserted ≈85% of D-proof conclusions. [6885351 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 4 s 415.00 ms remaining ; 29 s 433.35 ms total) Mon Oct 9 07:24:54 2023: Inserted ≈90% of D-proof conclusions. [7290372 of 8100414] (ETC: Mon Oct 9 07:24:57 2023 ; 2 s 979.57 ms remaining ; 29 s 795.68 ms total) Mon Oct 9 07:24:56 2023: Inserted ≈95% of D-proof conclusions. [7695393 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 1 s 500.66 ms remaining ; 30 s 13.14 ms total) Mon Oct 9 07:24:58 2023: Inserted 100% of D-proof conclusions. [8100414 of 8100414] (ETC: Mon Oct 9 07:24:58 2023 ; 0.00 ms remaining ; 30 s 698.91 ms total) 30699.14 ms (30 s 699.14 ms) total insertion duration. Mon Oct 9 07:24:58 2023: Starting to iterate D-proof candidates of length 39. 31507.42 ms (31 s 507.42 ms) taken to iterate 28598584 condensed detachment proof strings of length 39. [Copy] Next iteration count (filtered): { 39, 28598584 } Mon Oct 9 07:25:30 2023: Next iteration amount counter complete. [parallel ; 48 hardware thread contexts, unfiltered] Mon Oct 9 07:25:56 2023: Process terminated. [pid: 35094, tid:22462652753792]