( 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-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 ------------ ---------- ---------- ---------- -------- ---------- ---------- 40493687 optane_low 64 COMPLETED 0:0 00:40:13 40493687.ba+ 64 COMPLETED 0:0 00:40:13 784353372K 40493687.ex+ 64 COMPLETED 0:0 00:40:13 4K By 784353372 KiB = (784353372 / 1024^2) GiB = 748.017665863037109375 GiB, it used approximately 748.02 gibibytes of memory. ) Thu Nov 2 07:23:15 2023: Process started. [pid: 222253, tid:22818804762496] 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). Thu Nov 2 07:23:15 2023: Next iteration amount counter started. [parallel ; 64 hardware thread contexts, unfiltered] 0.01 ms taken to load initial representatives. 27.00 ms taken to read 1 condensed detachment proof and conclusion from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs3.txt. [tid:22818744514304] 20.18 ms taken to read 2 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs5.txt. [tid:22818742413056] 20.61 ms taken to read 5 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs7.txt. [tid:22818740311808] 22.43 ms taken to read 10 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs9.txt. [tid:22818738210560] 9.69 ms taken to read 24 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs11.txt. [tid:22818736109312] 20.24 ms taken to read 57 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs13.txt. [tid:22818734008064] 35.44 ms taken to read 137 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs15.txt. [tid:22818731906816] 25.95 ms taken to read 339 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs17.txt. [tid:22818729805568] 67.93 ms taken to read 854 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs19.txt. [tid:22818727704320] 53.61 ms taken to read 2171 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs21.txt. [tid:22818725603072] 163.82 ms taken to read 5583 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs23.txt. [tid:22818723501824] 235.99 ms taken to read 14478 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs25.txt. [tid:22818721400576] 2307.56 ms (2 s 307.56 ms) taken to read 37874 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs27.txt. [tid:22818719299328] 1684.17 ms (1 s 684.17 ms) taken to read 99756 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs29.txt. [tid:22818717198080] 2190.12 ms (2 s 190.12 ms) taken to read 264466 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs31.txt. [tid:22818715096832] 3950.70 ms (3 s 950.71 ms) taken to read 705026 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs33.txt. [tid:22818712995584] 7133.51 ms (7 s 133.51 ms) taken to read 1888450 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs35.txt. [tid:22818710894336] 13626.82 ms (13 s 626.82 ms) taken to read 5081180 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs37.txt. [tid:22818708793088] 13668.20 ms (13 s 668.20 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. 72418.64 ms (1 min 12 s 418.64 ms) taken to read 13863883 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs39-unfiltered39+.txt. [tid:22818708793088] 174251.54 ms (2 min 54 s 251.53 ms) taken to read 37699564 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs41-unfiltered39+.txt. [tid:22818710894336] 333157.69 ms (5 min 33 s 157.69 ms) taken to read 102797921 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs43-unfiltered39+.txt. [tid:22818712995584] 333165.38 ms (5 min 33 s 165.38 ms) additional read duration. Loaded 3 more representative collections of sizes: 39 : 13863883 41 : 37699564 43 : 102797921 162461782 representatives in total. Thu Nov 2 07:29:59 2023: Inserted ≈ 5% of D-proof conclusions. [ 8123089 of 162461782] (ETC: Thu Nov 2 07:47:46 2023 ; 17 min 47 s 594.03 ms remaining ; 18 min 43 s 783.19 ms total) Thu Nov 2 07:30:54 2023: Inserted ≈10% of D-proof conclusions. [ 16246178 of 162461782] (ETC: Thu Nov 2 07:47:39 2023 ; 16 min 45 s 317.99 ms remaining ; 18 min 37 s 19.98 ms total) Thu Nov 2 07:31:58 2023: Inserted ≈15% of D-proof conclusions. [ 24369267 of 162461782] (ETC: Thu Nov 2 07:48:31 2023 ; 16 min 33 s 393.00 ms remaining ; 19 min 28 s 697.65 ms total) Thu Nov 2 07:32:57 2023: Inserted ≈20% of D-proof conclusions. [ 32492356 of 162461782] (ETC: Thu Nov 2 07:48:38 2023 ; 15 min 40 s 453.04 ms remaining ; 19 min 35 s 566.29 ms total) Thu Nov 2 07:34:03 2023: Inserted ≈25% of D-proof conclusions. [ 40615445 of 162461782] (ETC: Thu Nov 2 07:49:05 2023 ; 15 min 2 s 123.39 ms remaining ; 20 min 2 s 831.18 ms total) Thu Nov 2 07:35:11 2023: Inserted ≈30% of D-proof conclusions. [ 48738534 of 162461782] (ETC: Thu Nov 2 07:49:32 2023 ; 14 min 20 s 514.94 ms remaining ; 20 min 29 s 307.06 ms total) Thu Nov 2 07:36:25 2023: Inserted ≈35% of D-proof conclusions. [ 56861623 of 162461782] (ETC: Thu Nov 2 07:50:08 2023 ; 13 min 42 s 639.38 ms remaining ; 21 min 5 s 599.04 ms total) Thu Nov 2 07:37:31 2023: Inserted ≈40% of D-proof conclusions. [ 64984712 of 162461782] (ETC: Thu Nov 2 07:50:14 2023 ; 12 min 42 s 888.91 ms remaining ; 21 min 11 s 481.50 ms total) Thu Nov 2 07:38:21 2023: Inserted ≈45% of D-proof conclusions. [ 73107801 of 162461782] (ETC: Thu Nov 2 07:49:44 2023 ; 11 min 22 s 682.18 ms remaining ; 20 min 41 s 240.32 ms total) Thu Nov 2 07:39:13 2023: Inserted ≈50% of D-proof conclusions. [ 81230891 of 162461782] (ETC: Thu Nov 2 07:49:24 2023 ; 10 min 10 s 621.60 ms remaining ; 20 min 21 s 243.20 ms total) Thu Nov 2 07:40:09 2023: Inserted ≈55% of D-proof conclusions. [ 89353980 of 162461782] (ETC: Thu Nov 2 07:49:15 2023 ; 9 min 5 s 625.77 ms remaining ; 20 min 12 s 501.71 ms total) Thu Nov 2 07:41:04 2023: Inserted ≈60% of D-proof conclusions. [ 97477069 of 162461782] (ETC: Thu Nov 2 07:49:05 2023 ; 8 min 1 s 179.37 ms remaining ; 20 min 2 s 948.43 ms total) Thu Nov 2 07:42:05 2023: Inserted ≈65% of D-proof conclusions. [105600158 of 162461782] (ETC: Thu Nov 2 07:49:07 2023 ; 7 min 1 s 564.80 ms remaining ; 20 min 4 s 470.84 ms total) Thu Nov 2 07:43:04 2023: Inserted ≈70% of D-proof conclusions. [113723247 of 162461782] (ETC: Thu Nov 2 07:49:04 2023 ; 6 min 627.82 ms remaining ; 20 min 2 s 92.73 ms total) Thu Nov 2 07:44:03 2023: Inserted ≈75% of D-proof conclusions. [121846336 of 162461782] (ETC: Thu Nov 2 07:49:03 2023 ; 5 min 252.47 ms remaining ; 20 min 1 s 9.85 ms total) Thu Nov 2 07:45:06 2023: Inserted ≈80% of D-proof conclusions. [129969425 of 162461782] (ETC: Thu Nov 2 07:49:07 2023 ; 4 min 1 s 0.50 ms remaining ; 20 min 5 s 2.48 ms total) Thu Nov 2 07:46:08 2023: Inserted ≈85% of D-proof conclusions. [138092514 of 162461782] (ETC: Thu Nov 2 07:49:09 2023 ; 3 min 1 s 7.93 ms remaining ; 20 min 6 s 719.47 ms total) Thu Nov 2 07:47:20 2023: Inserted ≈90% of D-proof conclusions. [146215603 of 162461782] (ETC: Thu Nov 2 07:49:22 2023 ; 2 min 1 s 967.29 ms remaining ; 20 min 19 s 672.83 ms total) Thu Nov 2 07:48:36 2023: Inserted ≈95% of D-proof conclusions. [154338692 of 162461782] (ETC: Thu Nov 2 07:49:37 2023 ; 1 min 1 s 747.85 ms remaining ; 20 min 34 s 956.80 ms total) Thu Nov 2 07:49:59 2023: Inserted 100% of D-proof conclusions. [162461782 of 162461782] (ETC: Thu Nov 2 07:49:59 2023 ; 0.00 ms remaining ; 20 min 56 s 757.10 ms total) 1256757.58 ms (20 min 56 s 757.58 ms) total insertion duration. Thu Nov 2 07:49:59 2023: Starting to iterate D-proof candidates of length 45. 508302.21 ms (8 min 28 s 302.21 ms) taken to iterate 591003200 condensed detachment proof strings of length 45. [Copy] Next iteration count (unfiltered39+): { 45, 591003200 } Thu Nov 2 07:58:27 2023: Next iteration amount counter complete. [parallel ; 64 hardware thread contexts, unfiltered] Thu Nov 2 08:02:49 2023: Process terminated. [pid: 222253, tid:22818804762496]