( 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 60 CLAIX-2023 MPI (small) nodes — 2-socket Intel Xeon Platinum 8468 (Sapphire Rapids) each, 48 cores each (96 cores total per node), 2.1 GHz, 3.8 GHz turbo mode, 256 GiB main memory each — running Linux, Rocky 9.6. Initialization and completion messages with rank numbers have been grouped and sorted for better readability. Wall-clock time: 3.0052777… h CPU utilization: 17310.4 core-h ) Wed May 27 11:26:22 2026: Process started. [pid: 192079, tid:22971732338496] Wed May 27 11:26:22 2026: Process started. [pid: 471905, tid:22836145325888] Wed May 27 11:26:22 2026: Process started. [pid: 445336, tid:23415661631296] Wed May 27 11:26:22 2026: Process started. [pid: 465472, tid:23407832545088] Wed May 27 11:26:22 2026: Process started. [pid: 64538, tid:22581304309568] Wed May 27 11:26:22 2026: Process started. [pid: 62647, tid:23212363347776] Wed May 27 11:26:22 2026: Process started. [pid: 497788, tid:23074471597888] Wed May 27 11:26:22 2026: Process started. [pid: 148746, tid:23105974847296] Wed May 27 11:26:22 2026: Process started. [pid: 82636, tid:22671244744512] Wed May 27 11:26:22 2026: Process started. [pid: 259355, tid:23064122001216] Wed May 27 11:26:22 2026: Process started. [pid: 308870, tid:22532565313344] Wed May 27 11:26:22 2026: Process started. [pid: 306798, tid:22500854232896] Wed May 27 11:26:22 2026: Process started. [pid: 333762, tid:22777525540672] Wed May 27 11:26:22 2026: Process started. [pid: 357447, tid:22730884736832] Wed May 27 11:26:22 2026: Process started. [pid: 194820, tid:22595603355456] Wed May 27 11:26:22 2026: Process started. [pid: 177339, tid:22670266541888] Wed May 27 11:26:22 2026: Process started. [pid: 329160, tid:22851718575936] Wed May 27 11:26:22 2026: Process started. [pid: 211164, tid:22685043099456] Wed May 27 11:26:22 2026: Process started. [pid: 510506, tid:23435859040064] Wed May 27 11:26:22 2026: Process started. [pid: 85445, tid:22507493599040] Wed May 27 11:26:22 2026: Process started. [pid: 192359, tid:23020153050944] Wed May 27 11:26:22 2026: Process started. [pid: 242053, tid:22754416789312] Wed May 27 11:26:22 2026: Process started. [pid: 68392, tid:22701044557632] Wed May 27 11:26:22 2026: Process started. [pid: 468489, tid:23332397877056] Wed May 27 11:26:22 2026: Process started. [pid: 277788, tid:22380893255488] Wed May 27 11:26:22 2026: Process started. [pid: 144799, tid:23166106789696] Wed May 27 11:26:22 2026: Process started. [pid: 319152, tid:22528117147456] Wed May 27 11:26:22 2026: Process started. [pid: 20769, tid:22683440625472] Wed May 27 11:26:22 2026: Process started. [pid: 306270, tid:23397369894720] Wed May 27 11:26:22 2026: Process started. [pid: 33341, tid:22545377056576] Wed May 27 11:26:22 2026: Process started. [pid: 200421, tid:22392660305728] Wed May 27 11:26:22 2026: Process started. [pid: 202637, tid:22555229353792] Wed May 27 11:26:22 2026: Process started. [pid: 190557, tid:22792100808512] Wed May 27 11:26:22 2026: Process started. [pid: 368611, tid:23269152233280] Wed May 27 11:26:22 2026: Process started. [pid: 370544, tid:22792286033728] Wed May 27 11:26:22 2026: Process started. [pid: 35626, tid:23321925957440] Wed May 27 11:26:22 2026: Process started. [pid: 441798, tid:22634782824256] Wed May 27 11:26:22 2026: Process started. [pid: 82413, tid:22637892388672] Wed May 27 11:26:22 2026: Process started. [pid: 203002, tid:23107243792192] Wed May 27 11:26:22 2026: Process started. [pid: 14839, tid:22944205371200] Wed May 27 11:26:22 2026: Process started. [pid: 198407, tid:22790379091776] Wed May 27 11:26:22 2026: Process started. [pid: 14347, tid:22874380195648] Wed May 27 11:26:22 2026: Process started. [pid: 412632, tid:22417817372480] Wed May 27 11:26:22 2026: Process started. [pid: 382868, tid:22536080172864] Wed May 27 11:26:22 2026: Process started. [pid: 32602, tid:23419598763840] Wed May 27 11:26:22 2026: Process started. [pid: 138714, tid:22655049541440] Wed May 27 11:26:22 2026: Process started. [pid: 493949, tid:22471013734208] Wed May 27 11:26:22 2026: Process started. [pid: 336539, tid:23356773332800] Wed May 27 11:26:22 2026: Process started. [pid: 222428, tid:22844546508608] Wed May 27 11:26:22 2026: Process started. [pid: 242364, tid:23247545284416] Wed May 27 11:26:22 2026: Process started. [pid: 410435, tid:23363590874944] Wed May 27 11:26:22 2026: Process started. [pid: 452511, tid:22852064212800] Wed May 27 11:26:22 2026: Process started. [pid: 614, tid:22658079733568] Wed May 27 11:26:22 2026: Process started. [pid: 108160, tid:23420245473088] Wed May 27 11:26:22 2026: Process started. [pid: 215538, tid:22857974089536] Wed May 27 11:26:22 2026: Process started. [pid: 139652, tid:22486660564800] Wed May 27 11:26:22 2026: Process started. [pid: 227269, tid:23252522219328] Wed May 27 11:26:22 2026: Process started. [pid: 218643, tid:23231993034560] Wed May 27 11:26:22 2026: Process started. [pid: 458635, tid:22981983397696] Wed May 27 11:26:23 2026: Process started. [pid: 385718, tid:23317994788672] Tasks: 1. resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true) 2. mpi_filterDProofRepresentativeFile(81, true) [Rank 0 ; pid: 385718 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true). Loaded 2 custom axioms. [SHA-512/224 hash: d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9] (1) CCC0.1.2CC2.0C3.0 - CCCpqrCCrpCsp - ((0\imply1)\imply2)\imply((2\imply0)\imply(3\imply0)) (2) CO0 - COp - \bot\imply0 [Rank 1 ; pid: 468489 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 2 ; pid: 412632 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 3 ; pid: 333762 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 4 ; pid: 441798 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 5 ; pid: 329160 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 6 ; pid: 85445 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 7 ; pid: 319152 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 8 ; pid: 357447 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 9 ; pid: 471905 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 10 ; pid: 148746 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 11 ; pid: 465472 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 12 ; pid: 144799 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 13 ; pid: 202637 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 14 ; pid: 64538 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 15 ; pid: 277788 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 16 ; pid: 493949 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 17 ; pid: 308870 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 18 ; pid: 82636 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 19 ; pid: 410435 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 20 ; pid: 215538 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 21 ; pid: 306270 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 22 ; pid: 32602 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 23 ; pid: 194820 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 24 ; pid: 20769 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 25 ; pid: 510506 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 26 ; pid: 35626 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 27 ; pid: 138714 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 28 ; pid: 198407 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 29 ; pid: 445336 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 30 ; pid: 192079 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 31 ; pid: 139652 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 32 ; pid: 192359 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 33 ; pid: 306798 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 34 ; pid: 200421 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 35 ; pid: 452511 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 36 ; pid: 177339 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 37 ; pid: 458635 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 38 ; pid: 259355 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 39 ; pid: 368611 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 40 ; pid: 336539 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 41 ; pid: 211164 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 42 ; pid: 382868 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 43 ; pid: 68392 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 44 ; pid: 203002 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 45 ; pid: 497788 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 46 ; pid: 190557 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 47 ; pid: 14347 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 48 ; pid: 242053 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 49 ; pid: 82413 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 50 ; pid: 218643 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 51 ; pid: 370544 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 52 ; pid: 108160 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 53 ; pid: 62647 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 54 ; pid: 33341 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 55 ; pid: 14839 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 56 ; pid: 614 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 57 ; pid: 222428 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 58 ; pid: 242364 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 59 ; pid: 227269 ; 60 processes] Calling resetRepresentativesFor("CCCpqrCCrpCsp,COp", true, 0, true), silently. [Rank 0 ; pid: 385718 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 1 ; pid: 468489 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 2 ; pid: 412632 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 3 ; pid: 333762 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 4 ; pid: 441798 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 5 ; pid: 329160 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 6 ; pid: 85445 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 7 ; pid: 319152 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 8 ; pid: 357447 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 9 ; pid: 471905 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 10 ; pid: 148746 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 11 ; pid: 465472 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 12 ; pid: 144799 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 13 ; pid: 202637 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 14 ; pid: 64538 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 15 ; pid: 277788 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 16 ; pid: 493949 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 17 ; pid: 308870 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 18 ; pid: 82636 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 19 ; pid: 410435 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 20 ; pid: 215538 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 21 ; pid: 306270 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 22 ; pid: 32602 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 23 ; pid: 194820 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 24 ; pid: 20769 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 25 ; pid: 510506 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 26 ; pid: 35626 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 27 ; pid: 138714 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 28 ; pid: 198407 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 29 ; pid: 445336 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 30 ; pid: 192079 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 31 ; pid: 139652 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 32 ; pid: 192359 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 33 ; pid: 306798 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 34 ; pid: 200421 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 35 ; pid: 452511 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 36 ; pid: 177339 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 37 ; pid: 458635 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 38 ; pid: 259355 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 39 ; pid: 368611 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 40 ; pid: 336539 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 41 ; pid: 211164 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 42 ; pid: 382868 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 43 ; pid: 68392 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 44 ; pid: 203002 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 45 ; pid: 497788 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 46 ; pid: 190557 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 47 ; pid: 14347 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 48 ; pid: 242053 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 49 ; pid: 82413 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 50 ; pid: 218643 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 51 ; pid: 370544 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 52 ; pid: 108160 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 53 ; pid: 62647 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 54 ; pid: 33341 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 55 ; pid: 14839 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 56 ; pid: 614 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 57 ; pid: 222428 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 58 ; pid: 242364 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). [Rank 59 ; pid: 227269 ; 60 processes] Calling mpi_filterDProofRepresentativeFile(81, true). Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 0 on "n23m0009.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 1 on "n23m0024.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 2 on "n23m0026.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 3 on "n23m0030.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 4 on "n23m0040.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 5 on "n23m0042.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 6 on "n23m0045.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 7 on "n23m0046.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 8 on "n23m0050.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 9 on "n23m0055.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 10 on "n23m0056.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 11 on "n23m0058.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 12 on "n23m0068.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 13 on "n23m0070.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 14 on "n23m0076.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 15 on "n23m0078.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 16 on "n23m0093.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 17 on "n23m0096.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 18 on "n23m0100.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 19 on "n23m0124.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 20 on "n23m0140.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 21 on "n23m0147.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 22 on "n23m0170.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 23 on "n23m0176.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 24 on "n23m0180.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 25 on "n23m0182.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 26 on "n23m0183.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 27 on "n23m0184.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 28 on "n23m0185.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 29 on "n23m0190.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 30 on "n23m0195.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 31 on "n23m0196.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 32 on "n23m0205.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 33 on "n23m0212.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 34 on "n23m0215.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 35 on "n23m0216.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 36 on "n23m0238.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 37 on "n23m0242.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 38 on "n23m0244.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 39 on "n23m0245.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 40 on "n23m0246.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 41 on "n23m0249.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 42 on "n23m0251.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 43 on "n23m0252.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 44 on "n23m0254.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 45 on "n23m0256.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 46 on "n23m0260.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 47 on "n23m0261.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 48 on "n23m0263.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 49 on "n23m0264.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 50 on "n23m0296.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 51 on "n23m0303.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 52 on "n23m0312.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 53 on "n23m0314.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 54 on "n23m0318.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 55 on "n23m0320.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 56 on "n23m0322.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 57 on "n23m0341.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 58 on "r23m0075.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 11:26:24 2026: MPI-based D-proof representative filter started. [rank 59 on "r23m0143.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] 0.00 ms taken to load initial representatives. 9.62 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs3.txt. [tid:23317582943808] 11.03 ms taken to read 1 condensed detachment proof and conclusion from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs5.txt. [tid:23317448689216] 8.51 ms taken to read 3 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs7.txt. [tid:23316693771840] 5.19 ms taken to read 8 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs9.txt. [tid:23316827989568] 6.75 ms taken to read 15 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs11.txt. [tid:23316825888320] 6.02 ms taken to read 22 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs13.txt. [tid:23316823787072] 11.84 ms taken to read 33 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs15.txt. [tid:23316821685824] 7.83 ms taken to read 45 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs17.txt. [tid:23316819584576] 5.70 ms taken to read 69 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs19.txt. [tid:23316817483328] 4.00 ms taken to read 101 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs21.txt. [tid:23316815382080] 27.61 ms taken to read 140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs23.txt. [tid:23316813280832] 33.11 ms taken to read 205 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs25.txt. [tid:23316811179584] 26.10 ms taken to read 280 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs27.txt. [tid:23316809078336] 14.12 ms taken to read 404 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs29.txt. [tid:23316806977088] 29.11 ms taken to read 568 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs31.txt. [tid:23316804875840] 16.66 ms taken to read 809 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs33.txt. [tid:23316802774592] 22.60 ms taken to read 1140 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs35.txt. [tid:23316800673344] 28.73 ms taken to read 1614 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs37.txt. [tid:23316798572096] 21.94 ms taken to read 2278 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs39.txt. [tid:23316796470848] 17.39 ms taken to read 3217 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs41.txt. [tid:23316794369600] 19.93 ms taken to read 4529 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs43.txt. [tid:23316792268352] 21.68 ms taken to read 6426 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs45.txt. [tid:23316790167104] 24.56 ms taken to read 9042 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs47.txt. [tid:23316788065856] 29.37 ms taken to read 12829 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs49.txt. [tid:23316785964608] 33.16 ms taken to read 18076 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs51.txt. [tid:23316783863360] 45.57 ms taken to read 25667 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs53.txt. [tid:23316781762112] 100.60 ms taken to read 36224 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs55.txt. [tid:23316779660864] 57.18 ms taken to read 51530 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs57.txt. [tid:23316777559616] 94.34 ms taken to read 72889 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs59.txt. [tid:23316706358848] 96.56 ms taken to read 103901 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs61.txt. [tid:23316704257600] 178.61 ms taken to read 147416 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs63.txt. [tid:23316702156352] 210.46 ms taken to read 210360 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs65.txt. [tid:23316700055104] 229.75 ms taken to read 299183 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs67.txt. [tid:23316697953856] 283.34 ms taken to read 427694 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs69.txt. [tid:23316691670592] 359.10 ms taken to read 609264 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs71.txt. [tid:23316689569344] 515.74 ms taken to read 872065 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs73.txt. [tid:23316687468096] 668.28 ms taken to read 1244628 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs75.txt. [tid:23316685366848] 782.61 ms taken to read 1782980 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs77.txt. [tid:23316683265600] 1392.52 ms (1 s 392.52 ms) taken to read 2547752 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs79.txt. [tid:23316681164352] 1422.21 ms (1 s 422.21 ms) total read duration. Loaded 40 representative collections of sizes: 1 : 2 3 : 1 5 : 1 7 : 3 9 : 8 11 : 15 13 : 22 15 : 33 17 : 45 19 : 69 21 : 101 23 : 140 25 : 205 27 : 280 29 : 404 31 : 568 33 : 809 35 : 1140 37 : 1614 39 : 2278 41 : 3217 43 : 4529 45 : 6426 47 : 9042 49 : 12829 51 : 18076 53 : 25667 55 : 36224 57 : 51530 59 : 72889 61 : 103901 63 : 147416 65 : 210360 67 : 299183 69 : 427694 71 : 609264 73 : 872065 75 : 1244628 77 : 1782980 79 : 2547752 8493410 representatives in total. 10296.48 ms (10 s 296.48 ms) taken to read 35197393 condensed detachment proofs and conclusions from data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs81-unfiltered81+.txt. [tid:23316681164352] 10297.87 ms (10 s 297.87 ms) additional read duration. Loaded 1 more representative collection of size: 81 : 35197393 43690803 representatives in total. Wed May 27 11:26:40 2026: Representative collections were initialized successfully on all ranks. Estimated removal count set to 31611427, based on entry 79:21730511 and last known pair (77:14938114, 79:21730511) with 21730511/14938114 ≈ 1.4547 and 21730511 * (21730511/14938114)^1 ≈ 31611427.54. Wed May 27 11:26:41 2026: Inserted ≈ 5% of D-proof conclusions. [ 2184540 of 43690803] (ETC: Wed May 27 11:26:58 2026 ; 17 s 705.40 ms remaining ; 18 s 637.26 ms total) Wed May 27 11:26:41 2026: Inserted ≈10% of D-proof conclusions. [ 4369080 of 43690803] (ETC: Wed May 27 11:26:58 2026 ; 16 s 582.33 ms remaining ; 18 s 424.81 ms total) Wed May 27 11:26:42 2026: Inserted ≈15% of D-proof conclusions. [ 6553620 of 43690803] (ETC: Wed May 27 11:26:58 2026 ; 15 s 769.09 ms remaining ; 18 s 551.87 ms total) Wed May 27 11:26:43 2026: Inserted ≈20% of D-proof conclusions. [ 8738160 of 43690803] (ETC: Wed May 27 11:26:58 2026 ; 14 s 853.35 ms remaining ; 18 s 566.69 ms total) Wed May 27 11:26:44 2026: Inserted ≈25% of D-proof conclusions. [10922700 of 43690803] (ETC: Wed May 27 11:26:56 2026 ; 12 s 372.38 ms remaining ; 16 s 496.50 ms total) Wed May 27 11:26:44 2026: Inserted ≈30% of D-proof conclusions. [13107240 of 43690803] (ETC: Wed May 27 11:26:55 2026 ; 10 s 614.45 ms remaining ; 15 s 163.49 ms total) Wed May 27 11:26:45 2026: Inserted ≈35% of D-proof conclusions. [15291781 of 43690803] (ETC: Wed May 27 11:26:54 2026 ; 9 s 251.69 ms remaining ; 14 s 233.36 ms total) Wed May 27 11:26:45 2026: Inserted ≈40% of D-proof conclusions. [17476321 of 43690803] (ETC: Wed May 27 11:26:53 2026 ; 8 s 140.23 ms remaining ; 13 s 567.06 ms total) Wed May 27 11:26:45 2026: Inserted ≈45% of D-proof conclusions. [19660861 of 43690803] (ETC: Wed May 27 11:26:53 2026 ; 7 s 159.58 ms remaining ; 13 s 17.41 ms total) Wed May 27 11:26:46 2026: Inserted ≈50% of D-proof conclusions. [21845401 of 43690803] (ETC: Wed May 27 11:26:52 2026 ; 6 s 282.76 ms remaining ; 12 s 565.53 ms total) Wed May 27 11:26:46 2026: Inserted ≈55% of D-proof conclusions. [24029941 of 43690803] (ETC: Wed May 27 11:26:52 2026 ; 5 s 491.02 ms remaining ; 12 s 202.26 ms total) Wed May 27 11:26:47 2026: Inserted ≈60% of D-proof conclusions. [26214481 of 43690803] (ETC: Wed May 27 11:26:52 2026 ; 4 s 758.59 ms remaining ; 11 s 896.47 ms total) Wed May 27 11:26:47 2026: Inserted ≈65% of D-proof conclusions. [28399021 of 43690803] (ETC: Wed May 27 11:26:51 2026 ; 4 s 104.90 ms remaining ; 11 s 728.29 ms total) Wed May 27 11:26:48 2026: Inserted ≈70% of D-proof conclusions. [30583562 of 43690803] (ETC: Wed May 27 11:26:51 2026 ; 3 s 490.43 ms remaining ; 11 s 634.77 ms total) Wed May 27 11:26:48 2026: Inserted ≈75% of D-proof conclusions. [32768102 of 43690803] (ETC: Wed May 27 11:26:51 2026 ; 2 s 893.11 ms remaining ; 11 s 572.42 ms total) Wed May 27 11:26:49 2026: Inserted ≈80% of D-proof conclusions. [34952642 of 43690803] (ETC: Wed May 27 11:26:51 2026 ; 2 s 315.99 ms remaining ; 11 s 579.95 ms total) Wed May 27 11:26:49 2026: Inserted ≈85% of D-proof conclusions. [37137182 of 43690803] (ETC: Wed May 27 11:26:51 2026 ; 1 s 732.84 ms remaining ; 11 s 552.26 ms total) Wed May 27 11:26:50 2026: Inserted ≈90% of D-proof conclusions. [39321722 of 43690803] (ETC: Wed May 27 11:26:51 2026 ; 1 s 142.94 ms remaining ; 11 s 429.39 ms total) Wed May 27 11:26:50 2026: Inserted ≈95% of D-proof conclusions. [41506262 of 43690803] (ETC: Wed May 27 11:26:51 2026 ; 562.18 ms remaining ; 11 s 243.51 ms total) Wed May 27 11:26:51 2026: Inserted 100% of D-proof conclusions. [43690803 of 43690803] (ETC: Wed May 27 11:26:51 2026 ; 0.00 ms remaining ; 11 s 81.27 ms total) 11081.70 ms (11 s 81.70 ms) total insertion duration. Reservable workloads: { 0:[391082, 586622], 1:[977705, 1173245], 2:[1564328, 1759868], 3:[2150951, 2346491], 4:[2737575, 2933115], 5:[3324198, 3519738], 6:[3910821, 4106361], 7:[4497444, 4692984], 8:[5084067, 5279607], 9:[5670691, 5866231], 10:[6257314, 6452854], 11:[6843937, 7039477], 12:[7430560, 7626100], 13:[8017184, 8212724], 14:[8603807, 8799347], 15:[9190430, 9385970], 16:[9777053, 9972593], 17:[10363676, 10559216], 18:[10950300, 11145840], 19:[11536923, 11732463], 20:[12123546, 12319086], 21:[12710169, 12905709], 22:[13296792, 13492332], 23:[13883416, 14078956], 24:[14470039, 14665579], 25:[15056662, 15252202], 26:[15643285, 15838825], 27:[16229909, 16425449], 28:[16816532, 17012072], 29:[17403155, 17598695], 30:[17989778, 18185318], 31:[18576401, 18771941], 32:[19163025, 19358565], 33:[19749648, 19945188], 34:[20336271, 20531811], 35:[20922894, 21118434], 36:[21509518, 21705058], 37:[22096141, 22291681], 38:[22682764, 22878304], 39:[23269387, 23464927], 40:[23856010, 24051550], 41:[24442634, 24638174], 42:[25029257, 25224797], 43:[25615880, 25811420], 44:[26202503, 26398043], 45:[26789126, 26984666], 46:[27375750, 27571290], 47:[27962373, 28157913], 48:[28548996, 28744536], 49:[29135619, 29331159], 50:[29722243, 29917783], 51:[30308866, 30504406], 52:[30895489, 31091029], 53:[31482112, 31677652], 54:[32068735, 32264275], 55:[32655359, 32850899], 56:[33241982, 33437522], 57:[33828605, 34024145], 58:[34415228, 34610768], 59:[35001852, 35197392] } Wed May 27 11:30:26 2026: Removed ≈ 2% of redundant conclusions. [ 632228 of approximately 31611427] (ETC: Wed May 27 14:23:59 2026 ; 2 h 53 min 32 s 908.96 ms remaining ; 2 h 57 min 5 s 417.13 ms total) Wed May 27 11:33:59 2026: Removed ≈ 4% of redundant conclusions. [ 1264457 of approximately 31611427] (ETC: Wed May 27 14:24:26 2026 ; 2 h 50 min 26 s 668.06 ms remaining ; 2 h 57 min 32 s 779.20 ms total) Wed May 27 11:37:34 2026: Removed ≈ 6% of redundant conclusions. [ 1896685 of approximately 31611427] (ETC: Wed May 27 14:24:49 2026 ; 2 h 47 min 15 s 584.47 ms remaining ; 2 h 57 min 56 s 153.47 ms total) Wed May 27 11:41:10 2026: Removed ≈ 8% of redundant conclusions. [ 2528914 of approximately 31611427] (ETC: Wed May 27 14:25:22 2026 ; 2 h 44 min 12 s 203.46 ms remaining ; 2 h 58 min 28 s 916.74 ms total) Wed May 27 11:44:44 2026: Removed ≈ 10% of redundant conclusions. [ 3161142 of approximately 31611427] (ETC: Wed May 27 14:25:23 2026 ; 2 h 40 min 38 s 704.47 ms remaining ; 2 h 58 min 29 s 671.37 ms total) Wed May 27 11:48:19 2026: Removed ≈ 12% of redundant conclusions. [ 3793371 of approximately 31611427] (ETC: Wed May 27 14:25:26 2026 ; 2 h 37 min 7 s 492.77 ms remaining ; 2 h 58 min 33 s 59.88 ms total) Wed May 27 11:51:54 2026: Removed ≈ 14% of redundant conclusions. [ 4425599 of approximately 31611427] (ETC: Wed May 27 14:25:32 2026 ; 2 h 33 min 38 s 340.47 ms remaining ; 2 h 58 min 39 s 0.24 ms total) Wed May 27 11:55:28 2026: Removed ≈ 16% of redundant conclusions. [ 5057828 of approximately 31611427] (ETC: Wed May 27 14:25:29 2026 ; 2 h 30 min 1 s 634.41 ms remaining ; 2 h 58 min 36 s 231.31 ms total) Wed May 27 11:59:02 2026: Removed ≈ 18% of redundant conclusions. [ 5690056 of approximately 31611427] (ETC: Wed May 27 14:25:29 2026 ; 2 h 26 min 27 s 103.94 ms remaining ; 2 h 58 min 35 s 980.06 ms total) Wed May 27 12:02:38 2026: Removed ≈ 20% of redundant conclusions. [ 6322285 of approximately 31611427] (ETC: Wed May 27 14:25:37 2026 ; 2 h 22 min 58 s 817.35 ms remaining ; 2 h 58 min 43 s 521.52 ms total) Wed May 27 12:06:12 2026: Removed ≈ 22% of redundant conclusions. [ 6954513 of approximately 31611427] (ETC: Wed May 27 14:25:38 2026 ; 2 h 19 min 25 s 45.90 ms remaining ; 2 h 58 min 44 s 417.41 ms total) Wed May 27 12:09:48 2026: Removed ≈ 24% of redundant conclusions. [ 7586742 of approximately 31611427] (ETC: Wed May 27 14:25:42 2026 ; 2 h 15 min 53 s 663.77 ms remaining ; 2 h 58 min 48 s 504.75 ms total) Wed May 27 12:13:23 2026: Removed ≈ 26% of redundant conclusions. [ 8218971 of approximately 31611427] (ETC: Wed May 27 14:25:45 2026 ; 2 h 12 min 21 s 788.70 ms remaining ; 2 h 58 min 52 s 146.88 ms total) Wed May 27 12:16:58 2026: Removed ≈ 28% of redundant conclusions. [ 8851199 of approximately 31611427] (ETC: Wed May 27 14:25:45 2026 ; 2 h 8 min 47 s 84.60 ms remaining ; 2 h 58 min 52 s 61.68 ms total) Wed May 27 12:20:34 2026: Removed ≈ 30% of redundant conclusions. [ 9483428 of approximately 31611427] (ETC: Wed May 27 14:25:49 2026 ; 2 h 5 min 15 s 255.39 ms remaining ; 2 h 58 min 56 s 79.09 ms total) Wed May 27 12:24:10 2026: Removed ≈ 32% of redundant conclusions. [10115656 of approximately 31611427] (ETC: Wed May 27 14:25:52 2026 ; 2 h 1 min 42 s 674.13 ms remaining ; 2 h 58 min 59 s 226.34 ms total) Wed May 27 12:27:46 2026: Removed ≈ 34% of redundant conclusions. [10747885 of approximately 31611427] (ETC: Wed May 27 14:25:58 2026 ; 1 h 58 min 11 s 919.81 ms remaining ; 2 h 59 min 5 s 332.96 ms total) Wed May 27 12:31:22 2026: Removed ≈ 36% of redundant conclusions. [11380113 of approximately 31611427] (ETC: Wed May 27 14:26:01 2026 ; 1 h 54 min 38 s 652.06 ms remaining ; 2 h 59 min 7 s 893.46 ms total) Wed May 27 12:34:57 2026: Removed ≈ 38% of redundant conclusions. [12012342 of approximately 31611427] (ETC: Wed May 27 14:25:59 2026 ; 1 h 51 min 2 s 583.43 ms remaining ; 2 h 59 min 6 s 102.17 ms total) Wed May 27 12:38:33 2026: Removed ≈ 40% of redundant conclusions. [12644570 of approximately 31611427] (ETC: Wed May 27 14:26:02 2026 ; 1 h 47 min 29 s 259.34 ms remaining ; 2 h 59 min 8 s 765.11 ms total) Wed May 27 12:42:08 2026: Removed ≈ 42% of redundant conclusions. [13276799 of approximately 31611427] (ETC: Wed May 27 14:26:02 2026 ; 1 h 43 min 54 s 441.66 ms remaining ; 2 h 59 min 9 s 37.15 ms total) Wed May 27 12:45:43 2026: Removed ≈ 44% of redundant conclusions. [13909027 of approximately 31611427] (ETC: Wed May 27 14:26:03 2026 ; 1 h 40 min 19 s 693.53 ms remaining ; 2 h 59 min 9 s 452.21 ms total) Wed May 27 12:49:19 2026: Removed ≈ 46% of redundant conclusions. [14541256 of approximately 31611427] (ETC: Wed May 27 14:26:05 2026 ; 1 h 36 min 46 s 65.76 ms remaining ; 2 h 59 min 11 s 973.37 ms total) Wed May 27 12:52:54 2026: Removed ≈ 48% of redundant conclusions. [15173484 of approximately 31611427] (ETC: Wed May 27 14:26:05 2026 ; 1 h 33 min 10 s 848.21 ms remaining ; 2 h 59 min 11 s 630.55 ms total) Wed May 27 12:56:30 2026: Removed ≈ 50% of redundant conclusions. [15805713 of approximately 31611427] (ETC: Wed May 27 14:26:06 2026 ; 1 h 29 min 36 s 653.86 ms remaining ; 2 h 59 min 13 s 307.39 ms total) Wed May 27 13:00:06 2026: Removed ≈ 52% of redundant conclusions. [16437942 of approximately 31611427] (ETC: Wed May 27 14:26:08 2026 ; 1 h 26 min 2 s 314.05 ms remaining ; 2 h 59 min 14 s 820.91 ms total) Wed May 27 13:03:40 2026: Removed ≈ 54% of redundant conclusions. [17070170 of approximately 31611427] (ETC: Wed May 27 14:26:07 2026 ; 1 h 22 min 26 s 794.31 ms remaining ; 2 h 59 min 13 s 900.24 ms total) Wed May 27 13:07:15 2026: Removed ≈ 56% of redundant conclusions. [17702399 of approximately 31611427] (ETC: Wed May 27 14:26:07 2026 ; 1 h 18 min 51 s 858.82 ms remaining ; 2 h 59 min 14 s 224.49 ms total) Wed May 27 13:10:51 2026: Removed ≈ 58% of redundant conclusions. [18334627 of approximately 31611427] (ETC: Wed May 27 14:26:07 2026 ; 1 h 15 min 16 s 839.91 ms remaining ; 2 h 59 min 14 s 380.20 ms total) Wed May 27 13:14:26 2026: Removed ≈ 60% of redundant conclusions. [18966856 of approximately 31611427] (ETC: Wed May 27 14:26:08 2026 ; 1 h 11 min 41 s 847.39 ms remaining ; 2 h 59 min 14 s 618.30 ms total) Wed May 27 13:18:01 2026: Removed ≈ 62% of redundant conclusions. [19599084 of approximately 31611427] (ETC: Wed May 27 14:26:08 2026 ; 1 h 8 min 6 s 779.85 ms remaining ; 2 h 59 min 14 s 683.15 ms total) Wed May 27 13:21:36 2026: Removed ≈ 64% of redundant conclusions. [20231313 of approximately 31611427] (ETC: Wed May 27 14:26:07 2026 ; 1 h 4 min 31 s 401.42 ms remaining ; 2 h 59 min 13 s 892.56 ms total) Wed May 27 13:25:10 2026: Removed ≈ 66% of redundant conclusions. [20863541 of approximately 31611427] (ETC: Wed May 27 14:26:06 2026 ; 1 h 55 s 907.49 ms remaining ; 2 h 59 min 12 s 668.28 ms total) Wed May 27 13:29:09 2026: Removed ≈ 68% of redundant conclusions. [21495770 of approximately 31611427] (ETC: Wed May 27 14:26:40 2026 ; 57 min 31 s 972.96 ms remaining ; 2 h 59 min 47 s 415.10 ms total) Wed May 27 13:32:40 2026: Removed ≈ 70% of redundant conclusions. [22127998 of approximately 31611427] (ETC: Wed May 27 14:26:34 2026 ; 53 min 54 s 211.01 ms remaining ; 2 h 59 min 40 s 702.36 ms total) Wed May 27 13:36:11 2026: Removed ≈ 72% of redundant conclusions. [22760227 of approximately 31611427] (ETC: Wed May 27 14:26:28 2026 ; 50 min 16 s 968.97 ms remaining ; 2 h 59 min 34 s 888.65 ms total) Wed May 27 13:39:41 2026: Removed ≈ 74% of redundant conclusions. [23392455 of approximately 31611427] (ETC: Wed May 27 14:26:20 2026 ; 46 min 39 s 465.40 ms remaining ; 2 h 59 min 27 s 173.33 ms total) Wed May 27 13:43:10 2026: Removed ≈ 76% of redundant conclusions. [24024684 of approximately 31611427] (ETC: Wed May 27 14:26:12 2026 ; 43 min 2 s 215.94 ms remaining ; 2 h 59 min 19 s 232.36 ms total) Wed May 27 13:46:41 2026: Removed ≈ 78% of redundant conclusions. [24656913 of approximately 31611427] (ETC: Wed May 27 14:26:06 2026 ; 39 min 25 s 723.79 ms remaining ; 2 h 59 min 13 s 289.88 ms total) Wed May 27 13:50:09 2026: Removed ≈ 80% of redundant conclusions. [25289141 of approximately 31611427] (ETC: Wed May 27 14:25:58 2026 ; 35 min 48 s 994.26 ms remaining ; 2 h 59 min 4 s 970.27 ms total) Wed May 27 13:53:38 2026: Removed ≈ 82% of redundant conclusions. [25921370 of approximately 31611427] (ETC: Wed May 27 14:25:51 2026 ; 32 min 12 s 783.49 ms remaining ; 2 h 58 min 57 s 685.77 ms total) Wed May 27 13:57:06 2026: Removed ≈ 84% of redundant conclusions. [26553598 of approximately 31611427] (ETC: Wed May 27 14:25:43 2026 ; 28 min 36 s 832.54 ms remaining ; 2 h 58 min 50 s 201.91 ms total) Wed May 27 14:00:35 2026: Removed ≈ 86% of redundant conclusions. [27185827 of approximately 31611427] (ETC: Wed May 27 14:25:36 2026 ; 25 min 1 s 231.00 ms remaining ; 2 h 58 min 43 s 78.08 ms total) Wed May 27 14:04:02 2026: Removed ≈ 88% of redundant conclusions. [27818055 of approximately 31611427] (ETC: Wed May 27 14:25:28 2026 ; 21 min 25 s 815.36 ms remaining ; 2 h 58 min 35 s 125.84 ms total) Wed May 27 14:07:47 2026: Removed ≈ 90% of redundant conclusions. [28450284 of approximately 31611427] (ETC: Wed May 27 14:25:39 2026 ; 17 min 52 s 625.40 ms remaining ; 2 h 58 min 46 s 252.94 ms total) Wed May 27 14:11:12 2026: Removed ≈ 92% of redundant conclusions. [29082512 of approximately 31611427] (ETC: Wed May 27 14:25:30 2026 ; 14 min 17 s 336.17 ms remaining ; 2 h 58 min 36 s 698.55 ms total) Wed May 27 14:14:38 2026: Removed ≈ 94% of redundant conclusions. [29714741 of approximately 31611427] (ETC: Wed May 27 14:25:21 2026 ; 10 min 42 s 455.49 ms remaining ; 2 h 58 min 27 s 589.41 ms total) [Rank 14] Workload transfer approved. Starting to work on 0:[564897, 579380]. Wed May 27 14:18:07 2026: Removed ≈ 96% of redundant conclusions. [30346969 of approximately 31611427] (ETC: Wed May 27 14:25:15 2026 ; 7 min 8 s 78.44 ms remaining ; 2 h 58 min 21 s 953.09 ms total) [Rank 52] Workload transfer approved. Starting to work on 1:[1151520, 1166003]. [Rank 56] Workload transfer approved. Starting to work on 2:[1738143, 1752626]. [Rank 2] Workload transfer approved. Starting to work on 3:[2339250, 2344077]. [Rank 48] Workload transfer approved. Starting to work on 4:[2925874, 2930701]. [Rank 14] Workload transfer approved. Starting to work on 5:[3512497, 3517324]. Wed May 27 14:21:48 2026: Removed ≈ 98% of redundant conclusions. [30979198 of approximately 31611427] (ETC: Wed May 27 14:25:22 2026 ; 3 min 34 s 173.10 ms remaining ; 2 h 58 min 28 s 647.24 ms total) [Rank 52] Workload transfer approved. Starting to work on 7:[4685743, 4690570]. [Rank 2] Workload transfer approved. Starting to work on 8:[5272366, 5277193]. [Rank 56] Workload transfer approved. Starting to work on 9:[5858990, 5863817]. [Rank 0] Workload transfer approved. Starting to work on 10:[6445613, 6450440]. [Rank 1] Workload transfer approved. Starting to work on 11:[7032236, 7037063]. [Rank 14] Workload transfer approved. Starting to work on 12:[7618859, 7623686]. [Rank 50] Workload transfer approved. Starting to work on 13:[8205483, 8210310]. [Rank 48] Workload transfer approved. Starting to work on 16:[9965352, 9970179]. [Rank 49] Workload transfer approved. Starting to work on 17:[10551975, 10556802]. [Rank 7] Workload transfer approved. Starting to work on 18:[11138599, 11143426]. [Rank 52] Workload transfer approved. Starting to work on 23:[14071715, 14076542]. [Rank 2] Workload transfer approved. Starting to work on 25:[15244961, 15249788]. [Rank 56] Workload transfer approved. Starting to work on 30:[18178077, 18182904]. [Rank 15] Workload transfer approved. Starting to work on 37:[22284440, 22289267]. [Rank 4] Workload transfer approved. Starting to work on 40:[24044309, 24049136]. [Rank 10] Workload transfer approved. Starting to work on 45:[26977425, 26982252]. [Rank 29] Workload transfer approved. Starting to work on 59:[35190151, 35194978]. [Rank 1] Workload transfer approved. Starting to work on 3:[2344078, 2345687]. [Rank 41] Workload transfer approved. Starting to work on 5:[3517325, 3518934]. [Rank 8] Workload transfer approved. Starting to work on 11:[7037064, 7038673]. [Rank 0] Workload transfer approved. Starting to work on 12:[7623687, 7625296]. [Rank 39] Workload transfer approved. Starting to work on 13:[8210311, 8211920]. [Rank 14] Workload transfer approved. Starting to work on 18:[11143427, 11145036]. [Rank 9] Workload transfer approved. Starting to work on 19:[11730050, 11731659]. [Rank 6] Workload transfer approved. Starting to work on 22:[13489919, 13491528]. [Rank 57] Workload transfer approved. Starting to work on 25:[15249789, 15251398]. [Rank 43] Workload transfer approved. Starting to work on 27:[16423036, 16424645]. [Rank 23] Workload transfer approved. Starting to work on 32:[19356152, 19357761]. [Rank 51] Workload transfer approved. Starting to work on 34:[20529398, 20531007]. [Rank 41] Workload transfer approved. Starting to work on 38:[22875891, 22877500]. [Rank 1] Workload transfer approved. Starting to work on 47:[28155500, 28157109]. [Rank 49] Workload transfer approved. Starting to work on 53:[31675239, 31676848]. [Rank 28] Workload transfer approved. Starting to work on 54:[32261862, 32263471]. [Rank 55] Workload transfer approved. Starting to work on 58:[34608355, 34609964]. [Rank 36] Workload transfer approved. Starting to work on 59:[35194979, 35196588]. [Rank 8] Workload transfer approved. Starting to work on 3:[2345688, 2346491]. [Rank 48] Workload transfer approved. Starting to work on 12:[7625297, 7626100]. [Rank 50] Workload transfer approved. Starting to work on 19:[11731660, 11732463]. [Rank 13] Workload transfer approved. Starting to work on 26:[15838022, 15838825]. [Rank 3] Workload transfer approved. Starting to work on 27:[16424646, 16425449]. [Rank 24] Workload transfer approved. Starting to work on 30:[18184515, 18185318]. [Rank 39] Workload transfer approved. Starting to work on 32:[19357762, 19358565]. [Rank 7] Workload transfer approved. Starting to work on 33:[19944385, 19945188]. [Rank 27] Workload transfer approved. Starting to work on 34:[20531008, 20531811]. [Rank 22] Workload transfer approved. Starting to work on 37:[22290878, 22291681]. [Rank 31] Workload transfer approved. Starting to work on 38:[22877501, 22878304]. [Rank 46] Workload transfer approved. Starting to work on 40:[24050747, 24051550]. [Rank 34] Workload transfer approved. Starting to work on 42:[25223994, 25224797]. [Rank 19] Workload transfer approved. Starting to work on 44:[26397240, 26398043]. [Rank 0] Workload transfer approved. Starting to work on 45:[26983863, 26984666]. [Rank 21] Workload transfer approved. Starting to work on 53:[31676849, 31677652]. [Rank 5] Workload transfer approved. Starting to work on 58:[34609965, 34610768]. 10752863.73 ms (2 h 59 min 12 s 863.73 ms) taken to detect 31544132 conclusions for which there are more general variants proven in lower or equal amounts of steps. Found 3653261 representative and 31544132 redundant condensed detachment proof strings. [Copy] Removal count: { 81, 31544132 } Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 1 on "n23m0024.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 2 on "n23m0026.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 3 on "n23m0030.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 4 on "n23m0040.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 5 on "n23m0042.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 6 on "n23m0045.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 7 on "n23m0046.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 8 on "n23m0050.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 9 on "n23m0055.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 10 on "n23m0056.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 11 on "n23m0058.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 12 on "n23m0068.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 13 on "n23m0070.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 14 on "n23m0076.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 15 on "n23m0078.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 16 on "n23m0093.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 17 on "n23m0096.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 18 on "n23m0100.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 19 on "n23m0124.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 20 on "n23m0140.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 21 on "n23m0147.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 22 on "n23m0170.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 23 on "n23m0176.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 24 on "n23m0180.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 25 on "n23m0182.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 26 on "n23m0183.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 27 on "n23m0184.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 28 on "n23m0185.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 29 on "n23m0190.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 30 on "n23m0195.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 31 on "n23m0196.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 32 on "n23m0205.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 33 on "n23m0212.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 34 on "n23m0215.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 35 on "n23m0216.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 36 on "n23m0238.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 37 on "n23m0242.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 38 on "n23m0244.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 39 on "n23m0245.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 40 on "n23m0246.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 41 on "n23m0249.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 42 on "n23m0251.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 43 on "n23m0252.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 44 on "n23m0254.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 45 on "n23m0256.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 46 on "n23m0260.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 47 on "n23m0261.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 48 on "n23m0263.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 49 on "n23m0264.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 50 on "n23m0296.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 51 on "n23m0303.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 52 on "n23m0312.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 53 on "n23m0314.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 54 on "n23m0318.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 55 on "n23m0320.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 56 on "n23m0322.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 57 on "n23m0341.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 58 on "r23m0075.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:05 2026: MPI-based D-proof representative filter complete. [rank 59 on "r23m0143.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] 726.44 ms taken to filter and order new representative proofs. Wed May 27 14:26:05 2026: Starting to write 3653261 entries to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs81.txt. 1141.75 ms (1 s 141.75 ms) taken to print and save 810545237 bytes of representative condensed detachment proof strings to data/d099134db97a750df3c662fb6ffa88c2d84bc409e4109a48410d25f9/dProofs-withConclusions/dProofs81.txt. Wed May 27 14:26:06 2026: MPI-based D-proof representative filter complete. [rank 0 on "n23m0009.hpc.itc.rwth-aachen.de" ; 60 processes ; 96 local hardware thread contexts] Wed May 27 14:26:41 2026: Process terminated. [pid: 33341, tid:22545377056576] Wed May 27 14:26:41 2026: Process terminated. [pid: 468489, tid:23332397877056] Wed May 27 14:26:41 2026: Process terminated. [pid: 211164, tid:22685043099456] Wed May 27 14:26:41 2026: Process terminated. [pid: 368611, tid:23269152233280] Wed May 27 14:26:41 2026: Process terminated. [pid: 20769, tid:22683440625472] Wed May 27 14:26:41 2026: Process terminated. [pid: 412632, tid:22417817372480] Wed May 27 14:26:41 2026: Process terminated. [pid: 242053, tid:22754416789312] Wed May 27 14:26:41 2026: Process terminated. [pid: 329160, tid:22851718575936] Wed May 27 14:26:41 2026: Process terminated. [pid: 452511, tid:22852064212800] Wed May 27 14:26:41 2026: Process terminated. [pid: 82413, tid:22637892388672] Wed May 27 14:26:41 2026: Process terminated. [pid: 441798, tid:22634782824256] Wed May 27 14:26:41 2026: Process terminated. [pid: 357447, tid:22730884736832] Wed May 27 14:26:41 2026: Process terminated. [pid: 215538, tid:22857974089536] Wed May 27 14:26:41 2026: Process terminated. [pid: 333762, tid:22777525540672] Wed May 27 14:26:41 2026: Process terminated. [pid: 139652, tid:22486660564800] Wed May 27 14:26:41 2026: Process terminated. [pid: 222428, tid:22844546508608] Wed May 27 14:26:41 2026: Process terminated. [pid: 138714, tid:22655049541440] Wed May 27 14:26:41 2026: Process terminated. [pid: 14839, tid:22944205371200] Wed May 27 14:26:41 2026: Process terminated. [pid: 32602, tid:23419598763840] Wed May 27 14:26:41 2026: Process terminated. [pid: 68392, tid:22701044557632] Wed May 27 14:26:41 2026: Process terminated. [pid: 410435, tid:23363590874944] Wed May 27 14:26:41 2026: Process terminated. [pid: 14347, tid:22874380195648] Wed May 27 14:26:41 2026: Process terminated. [pid: 277788, tid:22380893255488] Wed May 27 14:26:41 2026: Process terminated. [pid: 190557, tid:22792100808512] Wed May 27 14:26:41 2026: Process terminated. [pid: 306798, tid:22500854232896] Wed May 27 14:26:41 2026: Process terminated. [pid: 319152, tid:22528117147456] Wed May 27 14:26:41 2026: Process terminated. [pid: 614, tid:22658079733568] Wed May 27 14:26:41 2026: Process terminated. [pid: 218643, tid:23231993034560] Wed May 27 14:26:41 2026: Process terminated. [pid: 306270, tid:23397369894720] Wed May 27 14:26:41 2026: Process terminated. [pid: 203002, tid:23107243792192] Wed May 27 14:26:41 2026: Process terminated. [pid: 144799, tid:23166106789696] Wed May 27 14:26:41 2026: Process terminated. [pid: 198407, tid:22790379091776] Wed May 27 14:26:41 2026: Process terminated. [pid: 177339, tid:22670266541888] Wed May 27 14:26:41 2026: Process terminated. [pid: 382868, tid:22536080172864] Wed May 27 14:26:41 2026: Process terminated. [pid: 200421, tid:22392660305728] Wed May 27 14:26:41 2026: Process terminated. [pid: 108160, tid:23420245473088] Wed May 27 14:26:41 2026: Process terminated. [pid: 35626, tid:23321925957440] Wed May 27 14:26:41 2026: Process terminated. [pid: 385718, tid:23317994788672] Wed May 27 14:26:41 2026: Process terminated. [pid: 194820, tid:22595603355456] Wed May 27 14:26:41 2026: Process terminated. [pid: 85445, tid:22507493599040] Wed May 27 14:26:41 2026: Process terminated. [pid: 192359, tid:23020153050944] Wed May 27 14:26:41 2026: Process terminated. [pid: 370544, tid:22792286033728] Wed May 27 14:26:41 2026: Process terminated. [pid: 259355, tid:23064122001216] Wed May 27 14:26:41 2026: Process terminated. [pid: 227269, tid:23252522219328] Wed May 27 14:26:41 2026: Process terminated. [pid: 148746, tid:23105974847296] Wed May 27 14:26:41 2026: Process terminated. [pid: 242364, tid:23247545284416] Wed May 27 14:26:41 2026: Process terminated. [pid: 64538, tid:22581304309568] Wed May 27 14:26:41 2026: Process terminated. [pid: 497788, tid:23074471597888] Wed May 27 14:26:41 2026: Process terminated. [pid: 493949, tid:22471013734208] Wed May 27 14:26:41 2026: Process terminated. [pid: 510506, tid:23435859040064] Wed May 27 14:26:41 2026: Process terminated. [pid: 202637, tid:22555229353792] Wed May 27 14:26:41 2026: Process terminated. [pid: 458635, tid:22981983397696] Wed May 27 14:26:41 2026: Process terminated. [pid: 308870, tid:22532565313344] Wed May 27 14:26:41 2026: Process terminated. [pid: 62647, tid:23212363347776] Wed May 27 14:26:41 2026: Process terminated. [pid: 465472, tid:23407832545088] Wed May 27 14:26:41 2026: Process terminated. [pid: 82636, tid:22671244744512] Wed May 27 14:26:41 2026: Process terminated. [pid: 192079, tid:22971732338496] Wed May 27 14:26:41 2026: Process terminated. [pid: 445336, tid:23415661631296] Wed May 27 14:26:41 2026: Process terminated. [pid: 471905, tid:22836145325888] Wed May 27 14:26:41 2026: Process terminated. [pid: 336539, tid:23356773332800]