( This log file was generated by 'pmGenerator 1.2.3' (master branch), compiled by 'oneAPI DPC++/C++ Compiler 2024.2.0 (2024.2.0.20240602)'. 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 9.6. Wall-clock time: 52.82666… h CPU utilization: 3380.90666… core-h ) Fri May 29 07:07:07 2026: Process started. [pid: 411393, tid:22696871438144] Fri May 29 07:07:07 2026: Process started. [pid: 411394, tid:22759917545280] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50") 2. mpi_filterDProofRepresentativeFile(85, true) [Rank 0 ; pid: 411393 ; 2 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50"). Loaded 1 custom axioms. [SHA-512/224 hash: 97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146] (1) CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) Selected extracted proof system at "data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/". (1) 1 - CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) [Rank 1 ; pid: 411394 ; 2 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50"), silently. [Rank 0 ; pid: 411393 ; 2 processes] Calling mpi_filterDProofRepresentativeFile(85, true). Fri May 29 07:07:08 2026: MPI-based D-proof representative filter started. [rank 0 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] [Rank 1 ; pid: 411394 ; 2 processes] Calling mpi_filterDProofRepresentativeFile(85, true). Fri May 29 07:07:08 2026: MPI-based D-proof representative filter started. [rank 1 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 0.00 ms taken to load initial representatives. 0.01 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs3.txt. [tid:22696594126400] 0.50 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs5.txt. [tid:22696592025152] 0.22 ms taken to read 3 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs7.txt. [tid:22696589923904] 6.56 ms taken to read 8 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs9.txt. [tid:22696587822656] 0.36 ms taken to read 14 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs11.txt. [tid:22696585721408] 0.77 ms taken to read 21 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs13.txt. [tid:22696583620160] 3.85 ms taken to read 31 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs15.txt. [tid:22696581518912] 7.38 ms taken to read 42 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs17.txt. [tid:22696579417664] 1.06 ms taken to read 64 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs19.txt. [tid:22696577316416] 0.96 ms taken to read 93 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs21.txt. [tid:22696575215168] 6.81 ms taken to read 126 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs23.txt. [tid:22696573113920] 0.27 ms taken to read 177 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs25.txt. [tid:22696571012672] 3.33 ms taken to read 235 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs27.txt. [tid:22696568911424] 12.40 ms taken to read 327 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs29.txt. [tid:22696566810176] 20.64 ms taken to read 422 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs31.txt. [tid:22696564708928] 11.85 ms taken to read 591 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs33.txt. [tid:22696562607680] 6.25 ms taken to read 767 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs35.txt. [tid:22696560506432] 15.84 ms taken to read 1020 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs37.txt. [tid:22696558405184] 52.14 ms taken to read 1381 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs39.txt. [tid:22696556303936] 14.67 ms taken to read 1778 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs41.txt. [tid:22694245897792] 5.68 ms taken to read 2392 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs43.txt. [tid:22694243796544] 27.87 ms taken to read 3132 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs45.txt. [tid:22694241695296] 18.99 ms taken to read 4236 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs47.txt. [tid:22694239594048] 65.13 ms taken to read 5546 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs49.txt. [tid:22694237492800] 45.45 ms taken to read 7333 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs51.txt. [tid:22694235391552] 52.45 ms taken to read 9554 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs53.txt. [tid:22694233290304] 33.82 ms taken to read 12655 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs55.txt. [tid:22694231189056] 47.74 ms taken to read 16465 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs57.txt. [tid:22694229087808] 35.77 ms taken to read 21698 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs59.txt. [tid:22694226986560] 60.13 ms taken to read 28493 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs61.txt. [tid:22694224885312] 62.44 ms taken to read 37358 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs63.txt. [tid:22694222784064] 54.25 ms taken to read 49422 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs65.txt. [tid:22694220682816] 116.51 ms taken to read 64895 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs67.txt. [tid:22694218581568] 177.31 ms taken to read 85553 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs69.txt. [tid:22694216480320] 198.89 ms taken to read 112796 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs71.txt. [tid:22694214379072] 209.40 ms taken to read 148709 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs73.txt. [tid:22694212277824] 293.43 ms taken to read 196242 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs75.txt. [tid:22694210176576] 291.28 ms taken to read 257029 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs77.txt. [tid:22694208075328] 337.71 ms taken to read 337065 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs79.txt. [tid:22692191270464] 398.88 ms taken to read 438138 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs81.txt. [tid:22692189169216] 391.92 ms taken to read 569886 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs83.txt. [tid:22692187067968] 501.28 ms total read duration. Loaded 42 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 8 11 : 14 13 : 21 15 : 31 17 : 42 19 : 64 21 : 93 23 : 126 25 : 177 27 : 235 29 : 327 31 : 422 33 : 591 35 : 767 37 : 1020 39 : 1381 41 : 1778 43 : 2392 45 : 3132 47 : 4236 49 : 5546 51 : 7333 53 : 9554 55 : 12655 57 : 16465 59 : 21698 61 : 28493 63 : 37358 65 : 49422 67 : 64895 69 : 85553 71 : 112796 73 : 148709 75 : 196242 77 : 257029 79 : 337065 81 : 438138 83 : 569886 2415700 representatives in total. 2226.15 ms (2 s 226.15 ms) taken to read 5979512 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs85-unfiltered85+.txt. [tid:22692187067968] 2229.58 ms (2 s 229.58 ms) additional read duration. Loaded 1 more representative collection of size: 85 : 5979512 8395212 representatives in total. Fri May 29 07:07:11 2026: Representative collections were initialized successfully on all ranks. Could not estimate removal count since there are no known entries yet. Fri May 29 07:07:11 2026: Inserted ≈ 5% of D-proof conclusions. [ 419760 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 985.76 ms remaining ; 1 s 37.64 ms total) Fri May 29 07:07:11 2026: Inserted ≈10% of D-proof conclusions. [ 839521 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 886.93 ms remaining ; 985.48 ms total) Fri May 29 07:07:11 2026: Inserted ≈15% of D-proof conclusions. [1259281 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 845.40 ms remaining ; 994.59 ms total) Fri May 29 07:07:11 2026: Inserted ≈20% of D-proof conclusions. [1679042 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 779.49 ms remaining ; 974.37 ms total) Fri May 29 07:07:11 2026: Inserted ≈25% of D-proof conclusions. [2098803 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 726.27 ms remaining ; 968.36 ms total) Fri May 29 07:07:11 2026: Inserted ≈30% of D-proof conclusions. [2518563 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 711.88 ms remaining ; 1 s 16.98 ms total) Fri May 29 07:07:11 2026: Inserted ≈35% of D-proof conclusions. [2938324 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 684.71 ms remaining ; 1 s 53.40 ms total) Fri May 29 07:07:11 2026: Inserted ≈40% of D-proof conclusions. [3358084 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 646.62 ms remaining ; 1 s 77.71 ms total) Fri May 29 07:07:11 2026: Inserted ≈45% of D-proof conclusions. [3777845 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 604.44 ms remaining ; 1 s 98.98 ms total) Fri May 29 07:07:11 2026: Inserted ≈50% of D-proof conclusions. [4197606 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 551.93 ms remaining ; 1 s 103.85 ms total) Fri May 29 07:07:11 2026: Inserted ≈55% of D-proof conclusions. [4617366 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 522.13 ms remaining ; 1 s 160.28 ms total) Fri May 29 07:07:12 2026: Inserted ≈60% of D-proof conclusions. [5037127 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 469.70 ms remaining ; 1 s 174.25 ms total) Fri May 29 07:07:12 2026: Inserted ≈65% of D-proof conclusions. [5456887 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 411.83 ms remaining ; 1 s 176.67 ms total) Fri May 29 07:07:12 2026: Inserted ≈70% of D-proof conclusions. [5876648 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 351.74 ms remaining ; 1 s 172.45 ms total) Fri May 29 07:07:12 2026: Inserted ≈75% of D-proof conclusions. [6296409 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 294.00 ms remaining ; 1 s 176.00 ms total) Fri May 29 07:07:12 2026: Inserted ≈80% of D-proof conclusions. [6716169 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 235.19 ms remaining ; 1 s 175.93 ms total) Fri May 29 07:07:12 2026: Inserted ≈85% of D-proof conclusions. [7135930 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 176.10 ms remaining ; 1 s 174.01 ms total) Fri May 29 07:07:12 2026: Inserted ≈90% of D-proof conclusions. [7555690 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 117.49 ms remaining ; 1 s 174.88 ms total) Fri May 29 07:07:12 2026: Inserted ≈95% of D-proof conclusions. [7975451 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 58.67 ms remaining ; 1 s 173.38 ms total) Fri May 29 07:07:12 2026: Inserted 100% of D-proof conclusions. [8395212 of 8395212] (ETC: Fri May 29 07:07:12 2026 ; 0.00 ms remaining ; 1 s 229.94 ms total) 1229.99 ms (1 s 229.99 ms) total insertion duration. Reservable workloads: { 0:[1993171, 2989755], 1:[4982927, 5979511] } [Rank 1] Workload transfer approved. Starting to work on 0:[2952846, 2977452]. [Rank 1] Workload transfer approved. Starting to work on 0:[2977453, 2985654]. [Rank 1] Workload transfer approved. Starting to work on 0:[2985655, 2988388]. [Rank 1] Workload transfer approved. Starting to work on 0:[2988389, 2989300]. [Rank 1] Workload transfer approved. Starting to work on 0:[2989301, 2989755]. Fri May 29 14:35:26 2026: MPI-based D-proof representative filter complete. [rank 1 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 26945569.89 ms (7 h 29 min 5 s 569.89 ms) taken to detect 5243732 conclusions for which there are more general variants proven in lower or equal amounts of steps. Found 735780 representative and 5243732 redundant condensed detachment proof strings. [Copy] Removal count: { 85, 5243732 } 126.11 ms taken to filter and order new representative proofs. Fri May 29 14:36:18 2026: Starting to write 735780 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs85.txt. 269.54 ms taken to print and save 107174904 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs85.txt. Fri May 29 14:36:18 2026: MPI-based D-proof representative filter complete. [rank 0 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] Fri May 29 14:36:22 2026: Process terminated. [pid: 411393, tid:22696871438144] Fri May 29 14:36:22 2026: Process terminated. [pid: 411394, tid:22759917545280] Fri May 29 14:36:22 2026: Process started. [pid: 65195, tid:22765052614464] Fri May 29 14:36:22 2026: Process started. [pid: 65194, tid:22748687619904] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50") 2. mpi_filterDProofRepresentativeFile(87, true) [Rank 0 ; pid: 65194 ; 2 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50"). Loaded 1 custom axioms. [SHA-512/224 hash: 97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146] (1) CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) Selected extracted proof system at "data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/". (1) 1 - CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) [Rank 1 ; pid: 65195 ; 2 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50"), silently. [Rank 0 ; pid: 65194 ; 2 processes] Calling mpi_filterDProofRepresentativeFile(87, true). Fri May 29 14:36:23 2026: MPI-based D-proof representative filter started. [rank 0 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 0.00 ms taken to load initial representatives. [Rank 1 ; pid: 65195 ; 2 processes] Calling mpi_filterDProofRepresentativeFile(87, true). Fri May 29 14:36:23 2026: MPI-based D-proof representative filter started. [rank 1 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 5.05 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs3.txt. [tid:22748414752320] 8.11 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs5.txt. [tid:22748412651072] 10.92 ms taken to read 3 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs7.txt. [tid:22748410549824] 24.52 ms taken to read 8 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs9.txt. [tid:22748408448576] 13.80 ms taken to read 14 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs11.txt. [tid:22748406347328] 17.74 ms taken to read 21 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs13.txt. [tid:22748404246080] 10.46 ms taken to read 31 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs15.txt. [tid:22748402144832] 13.90 ms taken to read 42 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs17.txt. [tid:22748400043584] 2.62 ms taken to read 64 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs19.txt. [tid:22748397942336] 11.33 ms taken to read 93 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs21.txt. [tid:22748395841088] 9.10 ms taken to read 126 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs23.txt. [tid:22748393739840] 19.34 ms taken to read 177 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs25.txt. [tid:22748391638592] 16.15 ms taken to read 235 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs27.txt. [tid:22748389537344] 2.32 ms taken to read 327 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs29.txt. [tid:22748387436096] 18.70 ms taken to read 422 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs31.txt. [tid:22748385334848] 27.03 ms taken to read 591 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs33.txt. [tid:22748383233600] 13.01 ms taken to read 767 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs35.txt. [tid:22748381132352] 37.15 ms taken to read 1020 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs37.txt. [tid:22748379031104] 23.47 ms taken to read 1381 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs39.txt. [tid:22748376929856] 24.96 ms taken to read 1778 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs41.txt. [tid:22748374828608] 24.43 ms taken to read 2392 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs43.txt. [tid:22748372727360] 32.85 ms taken to read 3132 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs45.txt. [tid:22748370626112] 31.67 ms taken to read 4236 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs47.txt. [tid:22748368524864] 36.11 ms taken to read 5546 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs49.txt. [tid:22748366423616] 34.06 ms taken to read 7333 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs51.txt. [tid:22748364322368] 28.68 ms taken to read 9554 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs53.txt. [tid:22746053940800] 50.90 ms taken to read 12655 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs55.txt. [tid:22746051839552] 37.34 ms taken to read 16465 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs57.txt. [tid:22746049738304] 36.34 ms taken to read 21698 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs59.txt. [tid:22746047637056] 74.09 ms taken to read 28493 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs61.txt. [tid:22746045535808] 240.82 ms taken to read 37358 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs63.txt. [tid:22746043434560] 69.32 ms taken to read 49422 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs65.txt. [tid:22746041333312] 172.55 ms taken to read 64895 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs67.txt. [tid:22746039232064] 98.94 ms taken to read 85553 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs69.txt. [tid:22746037130816] 139.50 ms taken to read 112796 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs71.txt. [tid:22746035029568] 230.74 ms taken to read 148709 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs73.txt. [tid:22746032928320] 277.80 ms taken to read 196242 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs75.txt. [tid:22746030827072] 266.00 ms taken to read 257029 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs77.txt. [tid:22746028725824] 306.83 ms taken to read 337065 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs79.txt. [tid:22746026624576] 385.54 ms taken to read 438138 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs81.txt. [tid:22746024523328] 405.72 ms taken to read 569886 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs83.txt. [tid:22746022422080] 194.01 ms taken to read 735780 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs85.txt. [tid:22746020320832] 475.61 ms total read duration. Loaded 43 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 8 11 : 14 13 : 21 15 : 31 17 : 42 19 : 64 21 : 93 23 : 126 25 : 177 27 : 235 29 : 327 31 : 422 33 : 591 35 : 767 37 : 1020 39 : 1381 41 : 1778 43 : 2392 45 : 3132 47 : 4236 49 : 5546 51 : 7333 53 : 9554 55 : 12655 57 : 16465 59 : 21698 61 : 28493 63 : 37358 65 : 49422 67 : 64895 69 : 85553 71 : 112796 73 : 148709 75 : 196242 77 : 257029 79 : 337065 81 : 438138 83 : 569886 85 : 735780 3151480 representatives in total. 3490.09 ms (3 s 490.09 ms) taken to read 11805896 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs87-unfiltered87+.txt. [tid:22746020320832] 3491.09 ms (3 s 491.09 ms) additional read duration. Loaded 1 more representative collection of size: 87 : 11805896 14957376 representatives in total. Fri May 29 14:36:27 2026: Representative collections were initialized successfully on all ranks. Could not estimate removal count since there are no relevant entries yet. Fri May 29 14:36:27 2026: Inserted ≈ 5% of D-proof conclusions. [ 747868 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 1 s 659.61 ms remaining ; 1 s 746.96 ms total) Fri May 29 14:36:27 2026: Inserted ≈10% of D-proof conclusions. [ 1495737 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 1 s 719.81 ms remaining ; 1 s 910.90 ms total) Fri May 29 14:36:27 2026: Inserted ≈15% of D-proof conclusions. [ 2243606 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 1 s 697.39 ms remaining ; 1 s 996.93 ms total) Fri May 29 14:36:28 2026: Inserted ≈20% of D-proof conclusions. [ 2991475 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 1 s 573.34 ms remaining ; 1 s 966.67 ms total) Fri May 29 14:36:28 2026: Inserted ≈25% of D-proof conclusions. [ 3739344 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 1 s 472.00 ms remaining ; 1 s 962.67 ms total) Fri May 29 14:36:28 2026: Inserted ≈30% of D-proof conclusions. [ 4487212 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 1 s 390.40 ms remaining ; 1 s 986.28 ms total) Fri May 29 14:36:28 2026: Inserted ≈35% of D-proof conclusions. [ 5235081 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 1 s 263.84 ms remaining ; 1 s 944.37 ms total) Fri May 29 14:36:28 2026: Inserted ≈40% of D-proof conclusions. [ 5982950 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 1 s 155.87 ms remaining ; 1 s 926.45 ms total) Fri May 29 14:36:28 2026: Inserted ≈45% of D-proof conclusions. [ 6730819 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 1 s 54.16 ms remaining ; 1 s 916.65 ms total) Fri May 29 14:36:28 2026: Inserted ≈50% of D-proof conclusions. [ 7478688 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 959.64 ms remaining ; 1 s 919.27 ms total) Fri May 29 14:36:28 2026: Inserted ≈55% of D-proof conclusions. [ 8226556 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 857.25 ms remaining ; 1 s 905.00 ms total) Fri May 29 14:36:28 2026: Inserted ≈60% of D-proof conclusions. [ 8974425 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 777.24 ms remaining ; 1 s 943.09 ms total) Fri May 29 14:36:28 2026: Inserted ≈65% of D-proof conclusions. [ 9722294 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 684.27 ms remaining ; 1 s 955.07 ms total) Fri May 29 14:36:28 2026: Inserted ≈70% of D-proof conclusions. [10470163 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 586.23 ms remaining ; 1 s 954.11 ms total) Fri May 29 14:36:29 2026: Inserted ≈75% of D-proof conclusions. [11218032 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 488.01 ms remaining ; 1 s 952.04 ms total) Fri May 29 14:36:29 2026: Inserted ≈80% of D-proof conclusions. [11965900 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 391.67 ms remaining ; 1 s 958.34 ms total) Fri May 29 14:36:29 2026: Inserted ≈85% of D-proof conclusions. [12713769 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 295.11 ms remaining ; 1 s 967.37 ms total) Fri May 29 14:36:29 2026: Inserted ≈90% of D-proof conclusions. [13461638 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 197.23 ms remaining ; 1 s 972.33 ms total) Fri May 29 14:36:29 2026: Inserted ≈95% of D-proof conclusions. [14209507 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 98.78 ms remaining ; 1 s 975.68 ms total) Fri May 29 14:36:29 2026: Inserted 100% of D-proof conclusions. [14957376 of 14957376] (ETC: Fri May 29 14:36:29 2026 ; 0.00 ms remaining ; 1 s 974.41 ms total) 1974.72 ms (1 s 974.72 ms) total insertion duration. Reservable workloads: { 0:[3935299, 5902947], 1:[9838247, 11805895] } [Rank 1] Workload transfer approved. Starting to work on 0:[5830073, 5878656]. [Rank 1] Workload transfer approved. Starting to work on 0:[5878657, 5894850]. [Rank 1] Workload transfer approved. Starting to work on 0:[5894851, 5900248]. [Rank 1] Workload transfer approved. Starting to work on 0:[5900249, 5902048]. [Rank 1] Workload transfer approved. Starting to work on 0:[5902049, 5902947]. Sat May 30 07:13:06 2026: MPI-based D-proof representative filter complete. [rank 1 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 59980577.69 ms (16 h 39 min 40 s 577.69 ms) taken to detect 10857903 conclusions for which there are more general variants proven in lower or equal amounts of steps. Found 947993 representative and 10857903 redundant condensed detachment proof strings. [Copy] Removal count: { 87, 10857903 } 206.75 ms taken to filter and order new representative proofs. Sat May 30 07:16:10 2026: Starting to write 947993 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs87.txt. 290.54 ms taken to print and save 140445968 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs87.txt. Sat May 30 07:16:10 2026: MPI-based D-proof representative filter complete. [rank 0 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] Sat May 30 07:16:18 2026: Process terminated. [pid: 65194, tid:22748687619904] Sat May 30 07:16:18 2026: Process terminated. [pid: 65195, tid:22765052614464] Sat May 30 07:16:19 2026: Process started. [pid: 461452, tid:22391288448832] Sat May 30 07:16:19 2026: Process started. [pid: 461451, tid:22366707791680] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50") 2. mpi_filterDProofRepresentativeFile(89, true) [Rank 0 ; pid: 461451 ; 2 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50"). Loaded 1 custom axioms. [SHA-512/224 hash: 97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146] (1) CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) Selected extracted proof system at "data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/". (1) 1 - CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) [Rank 1 ; pid: 461452 ; 2 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50"), silently. [Rank 0 ; pid: 461451 ; 2 processes] Calling mpi_filterDProofRepresentativeFile(89, true). Sat May 30 07:16:19 2026: MPI-based D-proof representative filter started. [rank 0 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 0.00 ms taken to load initial representatives. [Rank 1 ; pid: 461452 ; 2 processes] Calling mpi_filterDProofRepresentativeFile(89, true). Sat May 30 07:16:19 2026: MPI-based D-proof representative filter started. [rank 1 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 8.19 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs3.txt. [tid:22366431098432] 5.91 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs5.txt. [tid:22366428997184] 10.91 ms taken to read 3 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs7.txt. [tid:22366426895936] 16.77 ms taken to read 8 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs9.txt. [tid:22366424794688] 10.84 ms taken to read 14 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs11.txt. [tid:22366422693440] 9.03 ms taken to read 21 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs13.txt. [tid:22366420592192] 18.68 ms taken to read 31 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs15.txt. [tid:22366418490944] 8.69 ms taken to read 42 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs17.txt. [tid:22366416389696] 8.76 ms taken to read 64 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs19.txt. [tid:22366414288448] 15.62 ms taken to read 93 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs21.txt. [tid:22366412187200] 9.92 ms taken to read 126 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs23.txt. [tid:22366410085952] 18.86 ms taken to read 177 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs25.txt. [tid:22366407984704] 24.23 ms taken to read 235 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs27.txt. [tid:22366405883456] 12.86 ms taken to read 327 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs29.txt. [tid:22366403782208] 26.74 ms taken to read 422 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs31.txt. [tid:22366401680960] 23.43 ms taken to read 591 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs33.txt. [tid:22366399579712] 26.66 ms taken to read 767 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs35.txt. [tid:22366397478464] 22.12 ms taken to read 1020 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs37.txt. [tid:22366395377216] 29.22 ms taken to read 1381 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs39.txt. [tid:22366393275968] 18.55 ms taken to read 1778 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs41.txt. [tid:22366391174720] 24.11 ms taken to read 2392 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs43.txt. [tid:22366389073472] 29.70 ms taken to read 3132 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs45.txt. [tid:22366386972224] 27.38 ms taken to read 4236 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs47.txt. [tid:22366384870976] 93.51 ms taken to read 5546 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs49.txt. [tid:22366382769728] 51.15 ms taken to read 7333 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs51.txt. [tid:22366380668480] 46.36 ms taken to read 9554 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs53.txt. [tid:22364070286912] 42.41 ms taken to read 12655 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs55.txt. [tid:22364068185664] 34.71 ms taken to read 16465 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs57.txt. [tid:22364066084416] 56.19 ms taken to read 21698 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs59.txt. [tid:22364063983168] 138.91 ms taken to read 28493 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs61.txt. [tid:22364061881920] 153.41 ms taken to read 37358 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs63.txt. [tid:22364059780672] 94.07 ms taken to read 49422 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs65.txt. [tid:22364057679424] 136.55 ms taken to read 64895 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs67.txt. [tid:22364055578176] 101.88 ms taken to read 85553 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs69.txt. [tid:22364053476928] 185.94 ms taken to read 112796 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs71.txt. [tid:22364051375680] 224.47 ms taken to read 148709 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs73.txt. [tid:22364049274432] 322.99 ms taken to read 196242 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs75.txt. [tid:22364047173184] 319.14 ms taken to read 257029 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs77.txt. [tid:22364045071936] 320.46 ms taken to read 337065 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs79.txt. [tid:22364042970688] 432.22 ms taken to read 438138 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs81.txt. [tid:22364040869440] 436.73 ms taken to read 569886 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs83.txt. [tid:22364038768192] 542.63 ms taken to read 735780 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs85.txt. [tid:22364036666944] 247.11 ms taken to read 947993 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs87.txt. [tid:22364034565696] 614.29 ms total read duration. Loaded 44 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 8 11 : 14 13 : 21 15 : 31 17 : 42 19 : 64 21 : 93 23 : 126 25 : 177 27 : 235 29 : 327 31 : 422 33 : 591 35 : 767 37 : 1020 39 : 1381 41 : 1778 43 : 2392 45 : 3132 47 : 4236 49 : 5546 51 : 7333 53 : 9554 55 : 12655 57 : 16465 59 : 21698 61 : 28493 63 : 37358 65 : 49422 67 : 64895 69 : 85553 71 : 112796 73 : 148709 75 : 196242 77 : 257029 79 : 337065 81 : 438138 83 : 569886 85 : 735780 87 : 947993 4099473 representatives in total. 5128.91 ms (5 s 128.91 ms) taken to read 16345345 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs89-unfiltered89+.txt. [tid:22364034565696] 5130.63 ms (5 s 130.63 ms) additional read duration. Loaded 1 more representative collection of size: 89 : 16345345 20444818 representatives in total. Sat May 30 07:16:25 2026: Representative collections were initialized successfully on all ranks. Estimated removal count set to 22482853, based on entry 87:10857903 and last known pair (85:5243732, 87:10857903) with 10857903/5243732 ≈ 2.07064 and 10857903 * (10857903/5243732)^1 ≈ 22482853.35. Sat May 30 07:16:25 2026: Inserted ≈ 5% of D-proof conclusions. [ 1022240 of 20444818] (ETC: Sat May 30 07:16:27 2026 ; 2 s 125.74 ms remaining ; 2 s 237.62 ms total) Sat May 30 07:16:25 2026: Inserted ≈10% of D-proof conclusions. [ 2044481 of 20444818] (ETC: Sat May 30 07:16:27 2026 ; 2 s 74.10 ms remaining ; 2 s 304.56 ms total) Sat May 30 07:16:25 2026: Inserted ≈15% of D-proof conclusions. [ 3066722 of 20444818] (ETC: Sat May 30 07:16:27 2026 ; 1 s 990.40 ms remaining ; 2 s 341.65 ms total) Sat May 30 07:16:26 2026: Inserted ≈20% of D-proof conclusions. [ 4088963 of 20444818] (ETC: Sat May 30 07:16:27 2026 ; 1 s 877.30 ms remaining ; 2 s 346.62 ms total) Sat May 30 07:16:26 2026: Inserted ≈25% of D-proof conclusions. [ 5111204 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 1 s 814.31 ms remaining ; 2 s 419.08 ms total) Sat May 30 07:16:26 2026: Inserted ≈30% of D-proof conclusions. [ 6133445 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 1 s 751.06 ms remaining ; 2 s 501.51 ms total) Sat May 30 07:16:26 2026: Inserted ≈35% of D-proof conclusions. [ 7155686 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 1 s 636.29 ms remaining ; 2 s 517.37 ms total) Sat May 30 07:16:26 2026: Inserted ≈40% of D-proof conclusions. [ 8177927 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 1 s 519.46 ms remaining ; 2 s 532.44 ms total) Sat May 30 07:16:26 2026: Inserted ≈45% of D-proof conclusions. [ 9200168 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 1 s 418.99 ms remaining ; 2 s 579.98 ms total) Sat May 30 07:16:26 2026: Inserted ≈50% of D-proof conclusions. [10222409 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 1 s 291.08 ms remaining ; 2 s 582.16 ms total) Sat May 30 07:16:27 2026: Inserted ≈55% of D-proof conclusions. [11244649 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 1 s 164.48 ms remaining ; 2 s 587.73 ms total) Sat May 30 07:16:27 2026: Inserted ≈60% of D-proof conclusions. [12266890 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 1 s 36.56 ms remaining ; 2 s 591.40 ms total) Sat May 30 07:16:27 2026: Inserted ≈65% of D-proof conclusions. [13289131 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 905.63 ms remaining ; 2 s 587.53 ms total) Sat May 30 07:16:27 2026: Inserted ≈70% of D-proof conclusions. [14311372 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 776.11 ms remaining ; 2 s 587.02 ms total) Sat May 30 07:16:27 2026: Inserted ≈75% of D-proof conclusions. [15333613 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 648.08 ms remaining ; 2 s 592.30 ms total) Sat May 30 07:16:27 2026: Inserted ≈80% of D-proof conclusions. [16355854 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 521.96 ms remaining ; 2 s 609.79 ms total) Sat May 30 07:16:27 2026: Inserted ≈85% of D-proof conclusions. [17378095 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 397.73 ms remaining ; 2 s 651.55 ms total) Sat May 30 07:16:27 2026: Inserted ≈90% of D-proof conclusions. [18400336 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 264.72 ms remaining ; 2 s 647.25 ms total) Sat May 30 07:16:28 2026: Inserted ≈95% of D-proof conclusions. [19422577 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 132.22 ms remaining ; 2 s 644.49 ms total) Sat May 30 07:16:28 2026: Inserted 100% of D-proof conclusions. [20444818 of 20444818] (ETC: Sat May 30 07:16:28 2026 ; 0.00 ms remaining ; 2 s 636.43 ms total) 2636.74 ms (2 s 636.74 ms) total insertion duration. Reservable workloads: { 0:[5448448, 8172671], 1:[13621121, 16345344] } Sat May 30 08:07:27 2026: Removed ≈ 2% of redundant conclusions. [ 449657 of approximately 22482853] (ETC: Mon Jun 1 01:45:19 2026 ; 1 d 17 h 37 min 51 s 697.35 ms remaining ; 1 d 18 h 28 min 50 s 303.01 ms total) Sat May 30 08:57:49 2026: Removed ≈ 4% of redundant conclusions. [ 899314 of approximately 22482853] (ETC: Mon Jun 1 01:29:43 2026 ; 1 d 16 h 31 min 54 s 366.82 ms remaining ; 1 d 18 h 13 min 14 s 131.26 ms total) Sat May 30 09:47:14 2026: Removed ≈ 6% of redundant conclusions. [ 1348971 of approximately 22482853] (ETC: Mon Jun 1 01:09:10 2026 ; 1 d 15 h 21 min 55 s 680.01 ms remaining ; 1 d 17 h 52 min 41 s 360.43 ms total) Sat May 30 10:35:37 2026: Removed ≈ 8% of redundant conclusions. [ 1798628 of approximately 22482853] (ETC: Mon Jun 1 00:45:43 2026 ; 1 d 14 h 10 min 6 s 106.36 ms remaining ; 1 d 17 h 29 min 14 s 461.70 ms total) Sat May 30 11:23:36 2026: Removed ≈ 10% of redundant conclusions. [ 2248285 of approximately 22482853] (ETC: Mon Jun 1 00:27:42 2026 ; 1 d 13 h 4 min 5 s 582.17 ms remaining ; 1 d 17 h 11 min 12 s 866.88 ms total) Sat May 30 12:11:24 2026: Removed ≈ 12% of redundant conclusions. [ 2697942 of approximately 22482853] (ETC: Mon Jun 1 00:14:09 2026 ; 1 d 12 h 2 min 44 s 795.94 ms remaining ; 1 d 16 h 57 min 39 s 992.70 ms total) Sat May 30 12:59:30 2026: Removed ≈ 14% of redundant conclusions. [ 3147599 of approximately 22482853] (ETC: Mon Jun 1 00:06:39 2026 ; 1 d 11 h 7 min 9 s 2.56 ms remaining ; 1 d 16 h 50 min 10 s 464.89 ms total) Sat May 30 13:47:35 2026: Removed ≈ 16% of redundant conclusions. [ 3597256 of approximately 22482853] (ETC: Mon Jun 1 00:00:51 2026 ; 1 d 10 h 13 min 16 s 487.49 ms remaining ; 1 d 16 h 44 min 22 s 481.38 ms total) Sat May 30 14:35:16 2026: Removed ≈ 18% of redundant conclusions. [ 4046913 of approximately 22482853] (ETC: Sun May 31 23:54:10 2026 ; 1 d 9 h 18 min 54 s 277.83 ms remaining ; 1 d 16 h 37 min 41 s 310.14 ms total) Sat May 30 15:23:12 2026: Removed ≈ 20% of redundant conclusions. [ 4496570 of approximately 22482853] (ETC: Sun May 31 23:50:04 2026 ; 1 d 8 h 26 min 52 s 280.44 ms remaining ; 1 d 16 h 33 min 35 s 345.67 ms total) Sat May 30 16:11:08 2026: Removed ≈ 22% of redundant conclusions. [ 4946227 of approximately 22482853] (ETC: Sun May 31 23:46:45 2026 ; 1 d 7 h 35 min 36 s 344.51 ms remaining ; 1 d 16 h 30 min 15 s 820.81 ms total) Sat May 30 16:58:59 2026: Removed ≈ 24% of redundant conclusions. [ 5395884 of approximately 22482853] (ETC: Sun May 31 23:43:36 2026 ; 1 d 6 h 44 min 36 s 615.56 ms remaining ; 1 d 16 h 27 min 7 s 119.60 ms total) Sat May 30 17:47:11 2026: Removed ≈ 26% of redundant conclusions. [ 5845541 of approximately 22482853] (ETC: Sun May 31 23:42:17 2026 ; 1 d 5 h 55 min 5 s 416.10 ms remaining ; 1 d 16 h 25 min 47 s 852.77 ms total) Sat May 30 18:35:21 2026: Removed ≈ 28% of redundant conclusions. [ 6295198 of approximately 22482853] (ETC: Sun May 31 23:41:00 2026 ; 1 d 5 h 5 min 39 s 392.53 ms remaining ; 1 d 16 h 24 min 31 s 370.97 ms total) Sat May 30 19:23:02 2026: Removed ≈ 30% of redundant conclusions. [ 6744855 of approximately 22482853] (ETC: Sun May 31 23:38:20 2026 ; 1 d 4 h 15 min 17 s 791.40 ms remaining ; 1 d 16 h 21 min 51 s 122.27 ms total) Sat May 30 20:11:17 2026: Removed ≈ 32% of redundant conclusions. [ 7194512 of approximately 22482853] (ETC: Sun May 31 23:37:44 2026 ; 1 d 3 h 26 min 27 s 87.36 ms remaining ; 1 d 16 h 21 min 15 s 119.35 ms total) Sat May 30 20:59:23 2026: Removed ≈ 34% of redundant conclusions. [ 7644170 of approximately 22482853] (ETC: Sun May 31 23:36:47 2026 ; 1 d 2 h 37 min 24 s 82.48 ms remaining ; 1 d 16 h 20 min 18 s 306.59 ms total) Sat May 30 21:47:18 2026: Removed ≈ 36% of redundant conclusions. [ 8093827 of approximately 22482853] (ETC: Sun May 31 23:35:27 2026 ; 1 d 1 h 48 min 8 s 176.34 ms remaining ; 1 d 16 h 18 min 57 s 774.72 ms total) Sat May 30 22:35:30 2026: Removed ≈ 38% of redundant conclusions. [ 8543484 of approximately 22482853] (ETC: Sun May 31 23:34:56 2026 ; 1 d 59 min 26 s 659.43 ms remaining ; 1 d 16 h 18 min 27 s 513.76 ms total) Sat May 30 23:24:10 2026: Removed ≈ 40% of redundant conclusions. [ 8993141 of approximately 22482853] (ETC: Sun May 31 23:35:41 2026 ; 1 d 11 min 31 s 531.29 ms remaining ; 1 d 16 h 19 min 12 s 550.00 ms total) Sun May 31 00:13:05 2026: Removed ≈ 42% of redundant conclusions. [ 9442798 of approximately 22482853] (ETC: Sun May 31 23:36:58 2026 ; 23 h 23 min 52 s 830.72 ms remaining ; 1 d 16 h 20 min 29 s 15.59 ms total) Sun May 31 01:01:57 2026: Removed ≈ 44% of redundant conclusions. [ 9892455 of approximately 22482853] (ETC: Sun May 31 23:38:00 2026 ; 22 h 36 min 3 s 246.01 ms remaining ; 1 d 16 h 21 min 31 s 507.04 ms total) Sun May 31 01:50:26 2026: Removed ≈ 46% of redundant conclusions. [10342112 of approximately 22482853] (ETC: Sun May 31 23:38:07 2026 ; 21 h 47 min 40 s 904.36 ms remaining ; 1 d 16 h 21 min 37 s 966.49 ms total) Sun May 31 02:37:45 2026: Removed ≈ 48% of redundant conclusions. [10791769 of approximately 22482853] (ETC: Sun May 31 23:35:48 2026 ; 20 h 58 min 2 s 841.84 ms remaining ; 1 d 16 h 19 min 19 s 305.77 ms total) Sun May 31 03:26:25 2026: Removed ≈ 50% of redundant conclusions. [11241426 of approximately 22482853] (ETC: Sun May 31 23:36:22 2026 ; 20 h 9 min 56 s 694.88 ms remaining ; 1 d 16 h 19 min 53 s 383.31 ms total) Sun May 31 04:14:53 2026: Removed ≈ 52% of redundant conclusions. [11691083 of approximately 22482853] (ETC: Sun May 31 23:36:30 2026 ; 19 h 21 min 36 s 422.59 ms remaining ; 1 d 16 h 20 min 872.86 ms total) Sun May 31 05:04:02 2026: Removed ≈ 54% of redundant conclusions. [12140740 of approximately 22482853] (ETC: Sun May 31 23:37:53 2026 ; 18 h 33 min 50 s 919.44 ms remaining ; 1 d 16 h 21 min 24 s 598.76 ms total) Sun May 31 05:53:03 2026: Removed ≈ 56% of redundant conclusions. [12590397 of approximately 22482853] (ETC: Sun May 31 23:38:56 2026 ; 17 h 45 min 52 s 908.12 ms remaining ; 1 d 16 h 22 min 27 s 508.45 ms total) Sun May 31 06:41:43 2026: Removed ≈ 58% of redundant conclusions. [13040054 of approximately 22482853] (ETC: Sun May 31 23:39:18 2026 ; 16 h 57 min 35 s 219.34 ms remaining ; 1 d 16 h 22 min 49 s 558.47 ms total) Sun May 31 07:30:13 2026: Removed ≈ 60% of redundant conclusions. [13489711 of approximately 22482853] (ETC: Sun May 31 23:39:23 2026 ; 16 h 9 min 9 s 683.81 ms remaining ; 1 d 16 h 22 min 54 s 196.59 ms total) Sun May 31 08:18:00 2026: Removed ≈ 62% of redundant conclusions. [13939368 of approximately 22482853] (ETC: Sun May 31 23:38:17 2026 ; 15 h 20 min 16 s 993.50 ms remaining ; 1 d 16 h 21 min 47 s 863.01 ms total) Sun May 31 09:06:46 2026: Removed ≈ 64% of redundant conclusions. [14389025 of approximately 22482853] (ETC: Sun May 31 23:38:48 2026 ; 14 h 32 min 2 s 225.01 ms remaining ; 1 d 16 h 22 min 19 s 497.40 ms total) Sun May 31 09:55:06 2026: Removed ≈ 66% of redundant conclusions. [14838682 of approximately 22482853] (ETC: Sun May 31 23:38:38 2026 ; 13 h 43 min 31 s 907.70 ms remaining ; 1 d 16 h 22 min 9 s 121.66 ms total) [Rank 1] Workload transfer approved. Starting to work on 0:[8139040, 8161461]. [Rank 1] Workload transfer approved. Starting to work on 0:[8161462, 8168935]. [Rank 1] Workload transfer approved. Starting to work on 0:[8168936, 8171426]. [Rank 1] Workload transfer approved. Starting to work on 0:[8171427, 8172256]. [Rank 1] Workload transfer approved. Starting to work on 0:[8172257, 8172671]. Sun May 31 10:24:35 2026: MPI-based D-proof representative filter complete. [rank 1 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 97970880.57 ms (1 d 3 h 12 min 50 s 880.57 ms) taken to detect 15132824 conclusions for which there are more general variants proven in lower or equal amounts of steps. Found 1212521 representative and 15132824 redundant condensed detachment proof strings. [Copy] Removal count: { 89, 15132824 } 215.08 ms taken to filter and order new representative proofs. Sun May 31 10:29:19 2026: Starting to write 1212521 entries to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs89.txt. 370.03 ms taken to print and save 182558589 bytes of representative condensed detachment proof strings to data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs89.txt. Sun May 31 10:29:20 2026: MPI-based D-proof representative filter complete. [rank 0 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] Sun May 31 10:29:30 2026: Process terminated. [pid: 461452, tid:22391288448832] Sun May 31 10:29:30 2026: Process terminated. [pid: 461451, tid:22366707791680] Sun May 31 10:29:30 2026: Process started. [pid: 59733, tid:22497708341056] Sun May 31 10:29:30 2026: Process started. [pid: 59732, tid:23075322816320] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50") 2. mpi_filterDProofRepresentativeFile(91, true) [Rank 0 ; pid: 59732 ; 2 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50"). Loaded 1 custom axioms. [SHA-512/224 hash: 97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146] (1) CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) Selected extracted proof system at "data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/". (1) 1 - CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) [Rank 1 ; pid: 59733 ; 2 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp", true, 0, true, "l50"), silently. [Rank 0 ; pid: 59732 ; 2 processes] Calling mpi_filterDProofRepresentativeFile(91, true). Sun May 31 10:29:31 2026: MPI-based D-proof representative filter started. [rank 0 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 0.00 ms taken to load initial representatives. [Rank 1 ; pid: 59733 ; 2 processes] Calling mpi_filterDProofRepresentativeFile(91, true). Sun May 31 10:29:31 2026: MPI-based D-proof representative filter started. [rank 1 on "nco04.hpc.itc.rwth-aachen.de" ; 2 processes ; 64 local hardware thread contexts] 16.82 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs3.txt. [tid:23075046176320] 6.00 ms taken to read 1 condensed detachment proof and conclusion from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs5.txt. [tid:23075044075072] 9.03 ms taken to read 3 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs7.txt. [tid:23075041973824] 9.89 ms taken to read 8 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs9.txt. [tid:23075039872576] 11.23 ms taken to read 14 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs11.txt. [tid:23075037771328] 11.05 ms taken to read 21 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs13.txt. [tid:23075035670080] 4.30 ms taken to read 31 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs15.txt. [tid:23075033568832] 5.46 ms taken to read 42 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs17.txt. [tid:23075031467584] 20.06 ms taken to read 64 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs19.txt. [tid:23075029366336] 16.64 ms taken to read 93 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs21.txt. [tid:23075027265088] 9.35 ms taken to read 126 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs23.txt. [tid:23075025163840] 8.64 ms taken to read 177 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs25.txt. [tid:23075023062592] 29.88 ms taken to read 235 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs27.txt. [tid:23075020961344] 6.07 ms taken to read 327 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs29.txt. [tid:23075018860096] 32.18 ms taken to read 422 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs31.txt. [tid:23075016758848] 19.50 ms taken to read 591 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs33.txt. [tid:23075014657600] 12.56 ms taken to read 767 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs35.txt. [tid:23075012556352] 25.96 ms taken to read 1020 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs37.txt. [tid:23075010455104] 251.82 ms taken to read 1381 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs39.txt. [tid:23075008353856] 34.35 ms taken to read 1778 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs41.txt. [tid:23075006252608] 26.48 ms taken to read 2392 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs43.txt. [tid:23075004151360] 30.37 ms taken to read 3132 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs45.txt. [tid:23075002050112] 42.32 ms taken to read 4236 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs47.txt. [tid:23074999948864] 146.21 ms taken to read 5546 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs49.txt. [tid:23074997847616] 39.77 ms taken to read 7333 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs51.txt. [tid:23074995746368] 27.52 ms taken to read 9554 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs53.txt. [tid:23074993645120] 36.81 ms taken to read 12655 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs55.txt. [tid:23074991543872] 63.22 ms taken to read 16465 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs57.txt. [tid:23074989442624] 45.55 ms taken to read 21698 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs59.txt. [tid:23074987341376] 204.11 ms taken to read 28493 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs61.txt. [tid:23074985240128] 188.52 ms taken to read 37358 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs63.txt. [tid:23074983138880] 147.36 ms taken to read 49422 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs65.txt. [tid:23072672781888] 147.13 ms taken to read 64895 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs67.txt. [tid:23072670680640] 85.00 ms taken to read 85553 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs69.txt. [tid:23072668579392] 215.80 ms taken to read 112796 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs71.txt. [tid:23072666478144] 201.73 ms taken to read 148709 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs73.txt. [tid:23072664376896] 290.43 ms taken to read 196242 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs75.txt. [tid:23072662275648] 298.07 ms taken to read 257029 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs77.txt. [tid:23072660174400] 342.31 ms taken to read 337065 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs79.txt. [tid:23072658073152] 446.10 ms taken to read 438138 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs81.txt. [tid:23072655971904] 626.62 ms taken to read 569886 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs83.txt. [tid:23072653870656] 575.25 ms taken to read 735780 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs85.txt. [tid:23072651769408] 710.92 ms taken to read 947993 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs87.txt. [tid:23072649668160] 396.84 ms taken to read 1212521 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs89.txt. [tid:23072647566912] 785.00 ms total read duration. Loaded 45 representative collections of sizes: 1 : 1 3 : 1 5 : 1 7 : 3 9 : 8 11 : 14 13 : 21 15 : 31 17 : 42 19 : 64 21 : 93 23 : 126 25 : 177 27 : 235 29 : 327 31 : 422 33 : 591 35 : 767 37 : 1020 39 : 1381 41 : 1778 43 : 2392 45 : 3132 47 : 4236 49 : 5546 51 : 7333 53 : 9554 55 : 12655 57 : 16465 59 : 21698 61 : 28493 63 : 37358 65 : 49422 67 : 64895 69 : 85553 71 : 112796 73 : 148709 75 : 196242 77 : 257029 79 : 337065 81 : 438138 83 : 569886 85 : 735780 87 : 947993 89 : 1212521 5311994 representatives in total. 6069.53 ms (6 s 69.53 ms) taken to read 19429840 condensed detachment proofs and conclusions from data/97553789db1645226627da044ed0a2e6a9cfd5963d66a8a44e121146/extraction-l50/dProofs-withConclusions/dProofs91-unfiltered91+.txt. [tid:23072647566912] 6071.28 ms (6 s 71.28 ms) additional read duration. Loaded 1 more representative collection of size: 91 : 19429840 24741834 representatives in total. Sun May 31 10:29:38 2026: Representative collections were initialized successfully on all ranks. Estimated removal count set to 21090846, based on entry 89:15132824 and last known pair (87:10857903, 89:15132824) with 15132824/10857903 ≈ 1.39372 and 15132824 * (15132824/10857903)^1 ≈ 21090846.20. Sun May 31 10:29:38 2026: Inserted ≈ 5% of D-proof conclusions. [ 1237091 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 2 s 852.19 ms remaining ; 3 s 2.30 ms total) Sun May 31 10:29:38 2026: Inserted ≈10% of D-proof conclusions. [ 2474183 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 2 s 639.12 ms remaining ; 2 s 932.36 ms total) Sun May 31 10:29:38 2026: Inserted ≈15% of D-proof conclusions. [ 3711275 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 2 s 514.71 ms remaining ; 2 s 958.49 ms total) Sun May 31 10:29:39 2026: Inserted ≈20% of D-proof conclusions. [ 4948366 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 2 s 429.26 ms remaining ; 3 s 36.58 ms total) Sun May 31 10:29:39 2026: Inserted ≈25% of D-proof conclusions. [ 6185458 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 2 s 327.42 ms remaining ; 3 s 103.22 ms total) Sun May 31 10:29:39 2026: Inserted ≈30% of D-proof conclusions. [ 7422550 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 2 s 152.89 ms remaining ; 3 s 75.56 ms total) Sun May 31 10:29:39 2026: Inserted ≈35% of D-proof conclusions. [ 8659641 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 2 s 31.90 ms remaining ; 3 s 126.00 ms total) Sun May 31 10:29:39 2026: Inserted ≈40% of D-proof conclusions. [ 9896733 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 1 s 889.44 ms remaining ; 3 s 149.06 ms total) Sun May 31 10:29:39 2026: Inserted ≈45% of D-proof conclusions. [11133825 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 1 s 742.13 ms remaining ; 3 s 167.52 ms total) Sun May 31 10:29:40 2026: Inserted ≈50% of D-proof conclusions. [12370917 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 1 s 584.71 ms remaining ; 3 s 169.42 ms total) Sun May 31 10:29:40 2026: Inserted ≈55% of D-proof conclusions. [13608008 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 1 s 430.28 ms remaining ; 3 s 178.40 ms total) Sun May 31 10:29:40 2026: Inserted ≈60% of D-proof conclusions. [14845100 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 1 s 269.56 ms remaining ; 3 s 173.91 ms total) Sun May 31 10:29:40 2026: Inserted ≈65% of D-proof conclusions. [16082192 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 1 s 108.75 ms remaining ; 3 s 167.85 ms total) Sun May 31 10:29:40 2026: Inserted ≈70% of D-proof conclusions. [17319283 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 959.76 ms remaining ; 3 s 199.19 ms total) Sun May 31 10:29:40 2026: Inserted ≈75% of D-proof conclusions. [18556375 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 801.31 ms remaining ; 3 s 205.25 ms total) Sun May 31 10:29:41 2026: Inserted ≈80% of D-proof conclusions. [19793467 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 642.84 ms remaining ; 3 s 214.20 ms total) Sun May 31 10:29:41 2026: Inserted ≈85% of D-proof conclusions. [21030558 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 481.36 ms remaining ; 3 s 209.10 ms total) Sun May 31 10:29:41 2026: Inserted ≈90% of D-proof conclusions. [22267650 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 320.02 ms remaining ; 3 s 200.21 ms total) Sun May 31 10:29:41 2026: Inserted ≈95% of D-proof conclusions. [23504742 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 159.92 ms remaining ; 3 s 198.45 ms total) Sun May 31 10:29:41 2026: Inserted 100% of D-proof conclusions. [24741834 of 24741834] (ETC: Sun May 31 10:29:41 2026 ; 0.00 ms remaining ; 3 s 198.72 ms total) 3199.01 ms (3 s 199.01 ms) total insertion duration. Reservable workloads: { 0:[6476614, 9714919], 1:[16191534, 19429839] } Sun May 31 11:33:08 2026: Removed ≈ 2% of redundant conclusions. [ 421816 of approximately 21090846] (ETC: Tue Jun 2 15:21:12 2026 ; 2 d 3 h 48 min 4 s 53.34 ms remaining ; 2 d 4 h 51 min 29 s 841.88 ms total) srun: Job step aborted: Waiting up to 92 seconds for job step to finish. [2026-05-31T11:56:43.227] error: *** STEP 677647.3 ON nco04 CANCELLED AT 2026-05-31T11:56:43 DUE to SIGNAL Terminated *** [2026-05-31T11:56:43.228] error: *** JOB 677647 ON nco04 CANCELLED AT 2026-05-31T11:56:43 DUE to SIGNAL Terminated ***