( This log file was generated by 'pmGenerator 1.2' (master branch), compiled by 'Intel(R) oneAPI DPC++/C++ Compiler 2022.1.0 (2022.1.0.20220316)'. The run was executed on 72 CLAIX-2018 MPI nodes — 2-socket Intel Xeon Platinum 8160 (Skylake) each, 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory each — running Linux, Rocky 8.8. Initialization and completion messages with rank numbers have been grouped and sorted for better readability. Wall-clock time: 3.326111… h CPU utilization: 11495.04 core-h ) Fri Oct 27 06:34:43 2023: Process started. [pid: 197576, tid:22375951521664] Fri Oct 27 06:34:43 2023: Process started. [pid: 108798, tid:23092767803264] Fri Oct 27 06:34:43 2023: Process started. [pid: 110102, tid:22769206597504] Fri Oct 27 06:34:43 2023: Process started. [pid: 90596, tid:23378356860800] Fri Oct 27 06:34:43 2023: Process started. [pid: 178986, tid:22843087759232] Fri Oct 27 06:34:43 2023: Process started. [pid: 263665, tid:22848938645376] Fri Oct 27 06:34:43 2023: Process started. [pid: 124323, tid:22843799517056] Fri Oct 27 06:34:43 2023: Process started. [pid: 2433, tid:23128085718912] Fri Oct 27 06:34:43 2023: Process started. [pid: 36779, tid:23184168441728] Fri Oct 27 06:34:43 2023: Process started. [pid: 43719, tid:22947466860416] Fri Oct 27 06:34:43 2023: Process started. [pid: 232688, tid:22561912452992] Fri Oct 27 06:34:43 2023: Process started. [pid: 127202, tid:22954551646080] Fri Oct 27 06:34:43 2023: Process started. [pid: 187523, tid:23315005351808] Fri Oct 27 06:34:43 2023: Process started. [pid: 271884, tid:23080020006784] Fri Oct 27 06:34:43 2023: Process started. [pid: 20232, tid:22596695283584] Fri Oct 27 06:34:43 2023: Process started. [pid: 11858, tid:23186030139264] Fri Oct 27 06:34:43 2023: Process started. [pid: 202907, tid:23141182240640] Fri Oct 27 06:34:43 2023: Process started. [pid: 98365, tid:22465365833600] Fri Oct 27 06:34:43 2023: Process started. [pid: 264831, tid:22830988916608] Fri Oct 27 06:34:43 2023: Process started. [pid: 80470, tid:22386371372928] Fri Oct 27 06:34:43 2023: Process started. [pid: 185115, tid:22601236178816] Fri Oct 27 06:34:44 2023: Process started. [pid: 44470, tid:22632355481472] Fri Oct 27 06:34:44 2023: Process started. [pid: 68765, tid:22450204813184] Fri Oct 27 06:34:44 2023: Process started. [pid: 229215, tid:22994335106944] Fri Oct 27 06:34:44 2023: Process started. [pid: 148156, tid:22809531279232] Fri Oct 27 06:34:44 2023: Process started. [pid: 136681, tid:23438505510784] Fri Oct 27 06:34:44 2023: Process started. [pid: 70972, tid:22538402772864] Fri Oct 27 06:34:44 2023: Process started. [pid: 160001, tid:22991548471168] Fri Oct 27 06:34:44 2023: Process started. [pid: 221896, tid:23410194192256] Fri Oct 27 06:34:44 2023: Process started. [pid: 21026, tid:22688141846400] Fri Oct 27 06:34:44 2023: Process started. [pid: 210940, tid:23149081790336] Fri Oct 27 06:34:44 2023: Process started. [pid: 70919, tid:23350307731328] Fri Oct 27 06:34:44 2023: Process started. [pid: 275597, tid:22583170742144] Fri Oct 27 06:34:44 2023: Process started. [pid: 260097, tid:23035240404864] Fri Oct 27 06:34:44 2023: Process started. [pid: 165657, tid:23299101013888] Fri Oct 27 06:34:44 2023: Process started. [pid: 129879, tid:22908353324928] Fri Oct 27 06:34:44 2023: Process started. [pid: 173327, tid:22978284640128] Fri Oct 27 06:34:44 2023: Process started. [pid: 214895, tid:23060012480384] Fri Oct 27 06:34:44 2023: Process started. [pid: 278169, tid:22587477464960] Fri Oct 27 06:34:44 2023: Process started. [pid: 256348, tid:22722808895360] Fri Oct 27 06:34:44 2023: Process started. [pid: 196225, tid:22747109304192] Fri Oct 27 06:34:44 2023: Process started. [pid: 182384, tid:22461677094784] Fri Oct 27 06:34:44 2023: Process started. [pid: 240346, tid:22464469706624] Fri Oct 27 06:34:44 2023: Process started. [pid: 214682, tid:23109421664128] Fri Oct 27 06:34:44 2023: Process started. [pid: 225370, tid:23013012252544] Fri Oct 27 06:34:44 2023: Process started. [pid: 61468, tid:23269372839808] Fri Oct 27 06:34:44 2023: Process started. [pid: 44475, tid:23412698564480] Fri Oct 27 06:34:44 2023: Process started. [pid: 159598, tid:22784003651456] Fri Oct 27 06:34:44 2023: Process started. [pid: 27057, tid:23414499854208] Fri Oct 27 06:34:44 2023: Process started. [pid: 213214, tid:23237712586624] Fri Oct 27 06:34:44 2023: Process started. [pid: 38877, tid:23137977513856] Fri Oct 27 06:34:44 2023: Process started. [pid: 152624, tid:23423864178560] Fri Oct 27 06:34:44 2023: Process started. [pid: 243616, tid:23317776299904] Fri Oct 27 06:34:44 2023: Process started. [pid: 123441, tid:22899168888704] Fri Oct 27 06:34:44 2023: Process started. [pid: 102468, tid:22586392090496] Fri Oct 27 06:34:44 2023: Process started. [pid: 8523, tid:23034177148800] Fri Oct 27 06:34:44 2023: Process started. [pid: 223828, tid:22878245283712] Fri Oct 27 06:34:44 2023: Process started. [pid: 163451, tid:23181752145792] Fri Oct 27 06:34:44 2023: Process started. [pid: 84747, tid:22976808486784] Fri Oct 27 06:34:44 2023: Process started. [pid: 242926, tid:23386603448192] Fri Oct 27 06:34:44 2023: Process started. [pid: 201204, tid:22431930382208] Fri Oct 27 06:34:44 2023: Process started. [pid: 211074, tid:23335180507008] Fri Oct 27 06:34:44 2023: Process started. [pid: 5589, tid:23357821249408] Fri Oct 27 06:34:44 2023: Process started. [pid: 64259, tid:22904158734208] Fri Oct 27 06:34:44 2023: Process started. [pid: 1869, tid:23170214020992] Fri Oct 27 06:34:44 2023: Process started. [pid: 228445, tid:22851999057792] Fri Oct 27 06:34:44 2023: Process started. [pid: 69462, tid:22720220702592] Fri Oct 27 06:34:44 2023: Process started. [pid: 63680, tid:23024918398848] Fri Oct 27 06:34:44 2023: Process started. [pid: 149509, tid:22727205250944] Fri Oct 27 06:34:44 2023: Process started. [pid: 212719, tid:23223339050880] Fri Oct 27 06:34:44 2023: Process started. [pid: 227891, tid:22381149042560] Fri Oct 27 06:34:44 2023: Process started. [pid: 188026, tid:22765049177984] Tasks: 1. resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true) 2. mpi_filterDProofRepresentativeFile(24, true) [Rank 0 ; pid: 188026 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true). Loaded 6 custom axioms. [SHA-512/224 hash: d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f] (1) C0C1.0 - CpCqp - 0\imply(1\imply0) (2) CC0C1.2CC0.1C0.2 - CCpCqrCCpqCpr - (0\imply(1\imply2))\imply((0\imply1)\imply(0\imply2)) (3) CCN0N1C1.0 - CCNpNqCqp - (\not0\imply\not1)\imply(1\imply0) (4) CL0.0 - CLpp - \nece0\imply0 (5) CLC0.1CL0L1 - CLCpqCLpLq - \nece(0\imply1)\imply(\nece0\imply\nece1) (6) CNLN0LNLN0 - CNLNpLNLNp - \not\nece\not0\imply\nece\not\nece\not0 Supports necessitation steps. [Rank 1 ; pid: 221896 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 2 ; pid: 61468 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 3 ; pid: 165657 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 4 ; pid: 68765 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 5 ; pid: 11858 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 6 ; pid: 197576 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 7 ; pid: 127202 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 8 ; pid: 124323 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 9 ; pid: 20232 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 10 ; pid: 44470 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 11 ; pid: 232688 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 12 ; pid: 271884 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 13 ; pid: 43719 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 14 ; pid: 2433 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 15 ; pid: 202907 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 16 ; pid: 185115 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 17 ; pid: 98365 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 18 ; pid: 70919 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 19 ; pid: 36779 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 20 ; pid: 210940 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 21 ; pid: 64259 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 22 ; pid: 264831 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 23 ; pid: 214895 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 24 ; pid: 110102 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 25 ; pid: 129879 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 26 ; pid: 108798 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 27 ; pid: 214682 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 28 ; pid: 90596 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 29 ; pid: 256348 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 30 ; pid: 260097 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 31 ; pid: 240346 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 32 ; pid: 148156 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 33 ; pid: 80470 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 34 ; pid: 160001 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 35 ; pid: 278169 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 36 ; pid: 229215 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 37 ; pid: 70972 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 38 ; pid: 187523 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 39 ; pid: 225370 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 40 ; pid: 21026 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 41 ; pid: 136681 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 42 ; pid: 1869 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 43 ; pid: 263665 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 44 ; pid: 178986 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 45 ; pid: 173327 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 46 ; pid: 275597 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 47 ; pid: 159598 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 48 ; pid: 243616 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 49 ; pid: 38877 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 50 ; pid: 27057 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 51 ; pid: 213214 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 52 ; pid: 223828 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 53 ; pid: 44475 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 54 ; pid: 149509 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 55 ; pid: 63680 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 56 ; pid: 163451 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 57 ; pid: 227891 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 58 ; pid: 228445 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 59 ; pid: 102468 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 60 ; pid: 8523 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 61 ; pid: 212719 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 62 ; pid: 242926 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 63 ; pid: 196225 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 64 ; pid: 201204 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 65 ; pid: 211074 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 66 ; pid: 84747 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 67 ; pid: 182384 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 68 ; pid: 123441 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 69 ; pid: 152624 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 70 ; pid: 5589 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 71 ; pid: 69462 ; 72 processes] Calling resetRepresentativesFor("CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,CLpp,CLCpqCLpLq,CNLNpLNLNp", true, 4294967295, true), silently. [Rank 0 ; pid: 188026 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 1 ; pid: 221896 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 2 ; pid: 61468 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 3 ; pid: 165657 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 4 ; pid: 68765 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 5 ; pid: 11858 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 6 ; pid: 197576 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 7 ; pid: 127202 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 8 ; pid: 124323 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 9 ; pid: 20232 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 10 ; pid: 44470 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 11 ; pid: 232688 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 12 ; pid: 271884 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 13 ; pid: 43719 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 14 ; pid: 2433 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 15 ; pid: 202907 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 16 ; pid: 185115 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 17 ; pid: 98365 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 18 ; pid: 70919 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 19 ; pid: 36779 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 20 ; pid: 210940 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 21 ; pid: 64259 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 22 ; pid: 264831 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 23 ; pid: 214895 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 24 ; pid: 110102 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 25 ; pid: 129879 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 26 ; pid: 108798 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 27 ; pid: 214682 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 28 ; pid: 90596 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 29 ; pid: 256348 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 30 ; pid: 260097 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 31 ; pid: 240346 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 32 ; pid: 148156 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 33 ; pid: 80470 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 34 ; pid: 160001 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 35 ; pid: 278169 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 36 ; pid: 229215 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 37 ; pid: 70972 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 38 ; pid: 187523 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 39 ; pid: 225370 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 40 ; pid: 21026 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 41 ; pid: 136681 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 42 ; pid: 1869 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 43 ; pid: 263665 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 44 ; pid: 178986 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 45 ; pid: 173327 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 46 ; pid: 275597 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 47 ; pid: 159598 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 48 ; pid: 243616 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 49 ; pid: 38877 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 50 ; pid: 27057 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 51 ; pid: 213214 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 52 ; pid: 223828 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 53 ; pid: 44475 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 54 ; pid: 149509 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 55 ; pid: 63680 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 56 ; pid: 163451 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 57 ; pid: 227891 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 58 ; pid: 228445 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 59 ; pid: 102468 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 60 ; pid: 8523 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 61 ; pid: 212719 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 62 ; pid: 242926 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 63 ; pid: 196225 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 64 ; pid: 201204 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 65 ; pid: 211074 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 66 ; pid: 84747 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 67 ; pid: 182384 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 68 ; pid: 123441 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 69 ; pid: 152624 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 70 ; pid: 5589 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). [Rank 71 ; pid: 69462 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(24, true). Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 0 on "ncm0402.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 1 on "ncm0403.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 2 on "ncm0404.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 3 on "ncm0408.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 4 on "ncm0410.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 5 on "ncm0411.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 6 on "ncm0412.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 7 on "ncm0413.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 8 on "ncm0414.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 9 on "ncm0415.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 10 on "ncm0417.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 11 on "ncm0418.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 12 on "ncm0419.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 13 on "ncm0420.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 14 on "ncm0421.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 15 on "ncm0422.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 16 on "ncm0424.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 17 on "ncm0425.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 18 on "ncm0426.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 19 on "ncm0618.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 20 on "ncm0619.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 21 on "ncm0620.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 22 on "ncm0622.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 23 on "ncm0623.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 24 on "ncm0624.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 25 on "ncm0625.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 26 on "ncm0626.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 27 on "ncm0627.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 28 on "ncm0628.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 29 on "ncm0629.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 30 on "ncm0630.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 31 on "ncm0632.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 32 on "ncm0633.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 33 on "ncm0634.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 34 on "ncm0635.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 35 on "ncm0636.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 36 on "ncm0637.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 37 on "ncm0638.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 38 on "ncm0639.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 39 on "ncm0640.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 40 on "ncm0641.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 41 on "ncm0642.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 42 on "ncm0643.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 43 on "ncm0644.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 44 on "ncm0645.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 45 on "ncm0646.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 46 on "ncm0648.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 47 on "ncm0945.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 48 on "ncm0947.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 49 on "ncm0948.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 50 on "ncm0949.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 51 on "ncm0950.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 52 on "ncm0951.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 53 on "ncm0952.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 54 on "ncm0953.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 55 on "ncm0954.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 56 on "ncm0955.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 57 on "ncm0956.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 58 on "ncm0957.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 59 on "ncm0958.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 60 on "ncm0959.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 61 on "ncm0960.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 62 on "ncm0961.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 63 on "ncm0962.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 64 on "ncm0964.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 65 on "ncm0965.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 66 on "ncm0967.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 67 on "ncm0968.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 68 on "ncm0969.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 69 on "ncm0970.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 70 on "ncm0971.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 06:34:45 2023: MPI-based D-proof representative filter started. [rank 71 on "ncm0973.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] 0.01 ms taken to load initial representatives. 12.74 ms taken to read 6 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs2.txt. [tid:22764323854080] 15.36 ms taken to read 17 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs3.txt. [tid:22764321752832] 13.55 ms taken to read 28 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs4.txt. [tid:22764319651584] 9.54 ms taken to read 56 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs5.txt. [tid:22764317550336] 10.87 ms taken to read 89 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs6.txt. [tid:22764315449088] 4.28 ms taken to read 203 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs7.txt. [tid:22764313347840] 26.81 ms taken to read 325 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs8.txt. [tid:22764311246592] 9.14 ms taken to read 666 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs9.txt. [tid:22764309145344] 26.44 ms taken to read 1174 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs10.txt. [tid:22764307044096] 16.72 ms taken to read 2340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs11.txt. [tid:22764304942848] 32.60 ms taken to read 4106 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs12.txt. [tid:22764302841600] 33.84 ms taken to read 8396 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs13.txt. [tid:22764300740352] 52.73 ms taken to read 15153 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs14.txt. [tid:22764298639104] 331.95 ms taken to read 30340 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs15.txt. [tid:22764296537856] 209.97 ms taken to read 56725 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs16.txt. [tid:22764294436608] 354.06 ms taken to read 113539 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs17.txt. [tid:22764292335360] 894.98 ms taken to read 214468 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs18.txt. [tid:22764290234112] 1740.50 ms (1 s 740.50 ms) taken to read 431896 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs19.txt. [tid:22764288132864] 6730.68 ms (6 s 730.68 ms) taken to read 829754 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs20.txt. [tid:22764286031616] 1197.80 ms (1 s 197.80 ms) taken to read 1666562 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs21.txt. [tid:22764283930368] 1644.38 ms (1 s 644.38 ms) taken to read 3250922 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs22.txt. [tid:22764281829120] 2280.30 ms (2 s 280.30 ms) taken to read 6547739 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs23.txt. [tid:22764279727872] 6769.29 ms (6 s 769.29 ms) total read duration. Loaded 23 representative collections of sizes: 1 : 6 2 : 6 3 : 17 4 : 28 5 : 56 6 : 89 7 : 203 8 : 325 9 : 666 10 : 1174 11 : 2340 12 : 4106 13 : 8396 14 : 15153 15 : 30340 16 : 56725 17 : 113539 18 : 214468 19 : 431896 20 : 829754 21 : 1666562 22 : 3250922 23 : 6547739 13174510 representatives in total. 3798.45 ms (3 s 798.45 ms) taken to read 14191911 condensed detachment proofs and conclusions from data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs24-unfiltered24+.txt. [tid:22764279727872] 3800.17 ms (3 s 800.17 ms) additional read duration. Loaded 1 more representative collection of size: 24 : 14191911 27366421 representatives in total. Fri Oct 27 06:34:56 2023: Representative collections were initialized successfully on all ranks. Estimated removal count set to 1289155, based on entry 22:334530 and last known even pair (20:86809, 22:334530) with 334530/86809 ≈ 3.85363 and 334530 * (334530/86809)^1 ≈ 1289155.74. Fri Oct 27 06:34:56 2023: Inserted ≈ 5% of D-proof conclusions. [ 1368321 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 7 s 992.50 ms remaining ; 8 s 413.16 ms total) Fri Oct 27 06:34:57 2023: Inserted ≈10% of D-proof conclusions. [ 2736642 of 27366421] (ETC: Fri Oct 27 06:35:05 2023 ; 7 s 921.63 ms remaining ; 8 s 801.81 ms total) Fri Oct 27 06:34:57 2023: Inserted ≈15% of D-proof conclusions. [ 4104963 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 7 s 202.47 ms remaining ; 8 s 473.49 ms total) Fri Oct 27 06:34:58 2023: Inserted ≈20% of D-proof conclusions. [ 5473284 of 27366421] (ETC: Fri Oct 27 06:35:05 2023 ; 6 s 938.71 ms remaining ; 8 s 673.39 ms total) Fri Oct 27 06:34:58 2023: Inserted ≈25% of D-proof conclusions. [ 6841605 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 6 s 352.07 ms remaining ; 8 s 469.43 ms total) Fri Oct 27 06:34:58 2023: Inserted ≈30% of D-proof conclusions. [ 8209926 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 5 s 891.17 ms remaining ; 8 s 415.96 ms total) Fri Oct 27 06:34:59 2023: Inserted ≈35% of D-proof conclusions. [ 9578247 of 27366421] (ETC: Fri Oct 27 06:35:05 2023 ; 5 s 663.59 ms remaining ; 8 s 713.22 ms total) Fri Oct 27 06:34:59 2023: Inserted ≈40% of D-proof conclusions. [10946568 of 27366421] (ETC: Fri Oct 27 06:35:05 2023 ; 5 s 191.57 ms remaining ; 8 s 652.61 ms total) Fri Oct 27 06:35:00 2023: Inserted ≈45% of D-proof conclusions. [12314889 of 27366421] (ETC: Fri Oct 27 06:35:05 2023 ; 4 s 724.19 ms remaining ; 8 s 589.43 ms total) Fri Oct 27 06:35:00 2023: Inserted ≈50% of D-proof conclusions. [13683210 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 4 s 234.12 ms remaining ; 8 s 468.24 ms total) Fri Oct 27 06:35:01 2023: Inserted ≈55% of D-proof conclusions. [15051531 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 3 s 778.78 ms remaining ; 8 s 397.30 ms total) Fri Oct 27 06:35:01 2023: Inserted ≈60% of D-proof conclusions. [16419852 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 3 s 351.91 ms remaining ; 8 s 379.78 ms total) Fri Oct 27 06:35:01 2023: Inserted ≈65% of D-proof conclusions. [17788173 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 2 s 954.76 ms remaining ; 8 s 442.16 ms total) Fri Oct 27 06:35:02 2023: Inserted ≈70% of D-proof conclusions. [19156494 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 2 s 538.52 ms remaining ; 8 s 461.74 ms total) Fri Oct 27 06:35:02 2023: Inserted ≈75% of D-proof conclusions. [20524815 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 2 s 116.08 ms remaining ; 8 s 464.31 ms total) Fri Oct 27 06:35:03 2023: Inserted ≈80% of D-proof conclusions. [21893136 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 1 s 686.46 ms remaining ; 8 s 432.27 ms total) Fri Oct 27 06:35:03 2023: Inserted ≈85% of D-proof conclusions. [23261457 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 1 s 265.06 ms remaining ; 8 s 433.75 ms total) Fri Oct 27 06:35:04 2023: Inserted ≈90% of D-proof conclusions. [24629778 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 842.63 ms remaining ; 8 s 426.29 ms total) Fri Oct 27 06:35:04 2023: Inserted ≈95% of D-proof conclusions. [25998099 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 420.41 ms remaining ; 8 s 408.17 ms total) Fri Oct 27 06:35:04 2023: Inserted 100% of D-proof conclusions. [27366421 of 27366421] (ETC: Fri Oct 27 06:35:04 2023 ; 0.00 ms remaining ; 8 s 397.98 ms total) 8398.06 ms (8 s 398.06 ms) total insertion duration. Reservable workloads: { 0:[131406, 197108], 1:[328516, 394218], 2:[525626, 591328], 3:[722736, 788438], 4:[919846, 985548], 5:[1116956, 1182658], 6:[1314066, 1379768], 7:[1511176, 1576878], 8:[1708285, 1773987], 9:[1905395, 1971097], 10:[2102505, 2168207], 11:[2299615, 2365317], 12:[2496725, 2562427], 13:[2693835, 2759537], 14:[2890945, 2956647], 15:[3088055, 3153757], 16:[3285164, 3350866], 17:[3482274, 3547976], 18:[3679384, 3745086], 19:[3876494, 3942196], 20:[4073604, 4139306], 21:[4270714, 4336416], 22:[4467824, 4533526], 23:[4664934, 4730636], 24:[4862043, 4927745], 25:[5059153, 5124855], 26:[5256263, 5321965], 27:[5453373, 5519075], 28:[5650483, 5716185], 29:[5847593, 5913295], 30:[6044703, 6110405], 31:[6241813, 6307515], 32:[6438922, 6504624], 33:[6636032, 6701734], 34:[6833142, 6898844], 35:[7030252, 7095954], 36:[7227362, 7293064], 37:[7424472, 7490174], 38:[7621582, 7687284], 39:[7818692, 7884394], 40:[8015801, 8081503], 41:[8212911, 8278613], 42:[8410021, 8475723], 43:[8607131, 8672833], 44:[8804241, 8869943], 45:[9001351, 9067053], 46:[9198461, 9264163], 47:[9395571, 9461273], 48:[9592680, 9658382], 49:[9789790, 9855492], 50:[9986900, 10052602], 51:[10184010, 10249712], 52:[10381120, 10446822], 53:[10578230, 10643932], 54:[10775340, 10841042], 55:[10972450, 11038152], 56:[11169559, 11235261], 57:[11366669, 11432371], 58:[11563779, 11629481], 59:[11760889, 11826591], 60:[11957999, 12023701], 61:[12155109, 12220811], 62:[12352219, 12417921], 63:[12549329, 12615031], 64:[12746438, 12812140], 65:[12943548, 13009250], 66:[13140658, 13206360], 67:[13337768, 13403470], 68:[13534878, 13600580], 69:[13731988, 13797690], 70:[13929098, 13994800], 71:[14126208, 14191910] } Fri Oct 27 06:39:20 2023: Removed ≈ 2% of redundant conclusions. [ 25783 of approximately 1289155] (ETC: Fri Oct 27 10:06:21 2023 ; 3 h 27 min 378.25 ms remaining ; 3 h 31 min 13 s 854.36 ms total) Fri Oct 27 06:43:29 2023: Removed ≈ 4% of redundant conclusions. [ 51566 of approximately 1289155] (ETC: Fri Oct 27 10:04:25 2023 ; 3 h 20 min 55 s 776.56 ms remaining ; 3 h 29 min 18 s 98.56 ms total) Fri Oct 27 06:47:38 2023: Removed ≈ 6% of redundant conclusions. [ 77349 of approximately 1289155] (ETC: Fri Oct 27 10:03:44 2023 ; 3 h 16 min 6 s 183.60 ms remaining ; 3 h 28 min 37 s 213.50 ms total) Fri Oct 27 06:51:43 2023: Removed ≈ 8% of redundant conclusions. [ 103132 of approximately 1289155] (ETC: Fri Oct 27 10:02:44 2023 ; 3 h 11 min 1 s 32.53 ms remaining ; 3 h 27 min 37 s 639.85 ms total) Fri Oct 27 06:55:49 2023: Removed ≈ 10% of redundant conclusions. [ 128915 of approximately 1289155] (ETC: Fri Oct 27 10:02:07 2023 ; 3 h 6 min 18 s 303.58 ms remaining ; 3 h 27 min 331.96 ms total) Fri Oct 27 06:59:51 2023: Removed ≈ 12% of redundant conclusions. [ 154698 of approximately 1289155] (ETC: Fri Oct 27 10:01:18 2023 ; 3 h 1 min 26 s 759.43 ms remaining ; 3 h 26 min 11 s 310.99 ms total) Fri Oct 27 07:03:53 2023: Removed ≈ 14% of redundant conclusions. [ 180481 of approximately 1289155] (ETC: Fri Oct 27 10:00:35 2023 ; 2 h 56 min 42 s 647.42 ms remaining ; 3 h 25 min 28 s 652.01 ms total) Fri Oct 27 07:07:52 2023: Removed ≈ 16% of redundant conclusions. [ 206264 of approximately 1289155] (ETC: Fri Oct 27 09:59:49 2023 ; 2 h 51 min 56 s 610.32 ms remaining ; 3 h 24 min 41 s 669.88 ms total) Fri Oct 27 07:11:50 2023: Removed ≈ 18% of redundant conclusions. [ 232047 of approximately 1289155] (ETC: Fri Oct 27 09:59:05 2023 ; 2 h 47 min 15 s 200.68 ms remaining ; 3 h 23 min 58 s 39.19 ms total) Fri Oct 27 07:15:44 2023: Removed ≈ 20% of redundant conclusions. [ 257831 of approximately 1289155] (ETC: Fri Oct 27 09:58:10 2023 ; 2 h 42 min 26 s 754.32 ms remaining ; 3 h 23 min 3 s 442.91 ms total) Fri Oct 27 07:19:35 2023: Removed ≈ 22% of redundant conclusions. [ 283614 of approximately 1289155] (ETC: Fri Oct 27 09:57:15 2023 ; 2 h 37 min 39 s 763.87 ms remaining ; 3 h 22 min 7 s 901.19 ms total) Fri Oct 27 07:23:27 2023: Removed ≈ 24% of redundant conclusions. [ 309397 of approximately 1289155] (ETC: Fri Oct 27 09:56:30 2023 ; 2 h 33 min 3 s 115.53 ms remaining ; 3 h 21 min 23 s 44.29 ms total) Fri Oct 27 07:27:19 2023: Removed ≈ 26% of redundant conclusions. [ 335180 of approximately 1289155] (ETC: Fri Oct 27 09:55:54 2023 ; 2 h 28 min 35 s 37.96 ms remaining ; 3 h 20 min 47 s 344.81 ms total) Fri Oct 27 07:31:12 2023: Removed ≈ 28% of redundant conclusions. [ 360963 of approximately 1289155] (ETC: Fri Oct 27 09:55:24 2023 ; 2 h 24 min 12 s 526.72 ms remaining ; 3 h 20 min 17 s 393.04 ms total) Fri Oct 27 07:35:04 2023: Removed ≈ 30% of redundant conclusions. [ 386746 of approximately 1289155] (ETC: Fri Oct 27 09:54:58 2023 ; 2 h 19 min 54 s 137.58 ms remaining ; 3 h 19 min 51 s 618.47 ms total) Fri Oct 27 07:38:56 2023: Removed ≈ 32% of redundant conclusions. [ 412529 of approximately 1289155] (ETC: Fri Oct 27 09:54:33 2023 ; 2 h 15 min 37 s 105.44 ms remaining ; 3 h 19 min 26 s 323.33 ms total) Fri Oct 27 07:42:49 2023: Removed ≈ 34% of redundant conclusions. [ 438312 of approximately 1289155] (ETC: Fri Oct 27 09:54:15 2023 ; 2 h 11 min 25 s 788.42 ms remaining ; 3 h 19 min 8 s 154.45 ms total) Fri Oct 27 07:46:43 2023: Removed ≈ 36% of redundant conclusions. [ 464095 of approximately 1289155] (ETC: Fri Oct 27 09:54:00 2023 ; 2 h 7 min 17 s 63.87 ms remaining ; 3 h 18 min 52 s 900.73 ms total) Fri Oct 27 07:50:34 2023: Removed ≈ 38% of redundant conclusions. [ 489878 of approximately 1289155] (ETC: Fri Oct 27 09:53:42 2023 ; 2 h 3 min 7 s 145.64 ms remaining ; 3 h 18 min 34 s 737.62 ms total) Fri Oct 27 07:54:26 2023: Removed ≈ 40% of redundant conclusions. [ 515662 of approximately 1289155] (ETC: Fri Oct 27 09:53:26 2023 ; 1 h 58 min 59 s 493.73 ms remaining ; 3 h 18 min 19 s 156.22 ms total) Fri Oct 27 07:58:18 2023: Removed ≈ 42% of redundant conclusions. [ 541445 of approximately 1289155] (ETC: Fri Oct 27 09:53:10 2023 ; 1 h 54 min 52 s 401.70 ms remaining ; 3 h 18 min 3 s 449.62 ms total) Fri Oct 27 08:02:09 2023: Removed ≈ 44% of redundant conclusions. [ 567228 of approximately 1289155] (ETC: Fri Oct 27 09:52:55 2023 ; 1 h 50 min 46 s 375.62 ms remaining ; 3 h 17 min 48 s 524.61 ms total) Fri Oct 27 08:06:00 2023: Removed ≈ 46% of redundant conclusions. [ 593011 of approximately 1289155] (ETC: Fri Oct 27 09:52:41 2023 ; 1 h 46 min 41 s 8.39 ms remaining ; 3 h 17 min 33 s 714.13 ms total) Fri Oct 27 08:09:51 2023: Removed ≈ 48% of redundant conclusions. [ 618794 of approximately 1289155] (ETC: Fri Oct 27 09:52:29 2023 ; 1 h 42 min 37 s 707.02 ms remaining ; 3 h 17 min 21 s 737.20 ms total) Fri Oct 27 08:13:41 2023: Removed ≈ 50% of redundant conclusions. [ 644577 of approximately 1289155] (ETC: Fri Oct 27 09:52:16 2023 ; 1 h 38 min 34 s 376.57 ms remaining ; 3 h 17 min 8 s 743.96 ms total) Fri Oct 27 08:17:30 2023: Removed ≈ 52% of redundant conclusions. [ 670360 of approximately 1289155] (ETC: Fri Oct 27 09:52:00 2023 ; 1 h 34 min 30 s 504.16 ms remaining ; 3 h 16 min 53 s 538.87 ms total) Fri Oct 27 08:21:19 2023: Removed ≈ 54% of redundant conclusions. [ 696143 of approximately 1289155] (ETC: Fri Oct 27 09:51:46 2023 ; 1 h 30 min 27 s 833.35 ms remaining ; 3 h 16 min 39 s 623.78 ms total) Fri Oct 27 08:25:04 2023: Removed ≈ 56% of redundant conclusions. [ 721926 of approximately 1289155] (ETC: Fri Oct 27 09:51:27 2023 ; 1 h 26 min 23 s 300.05 ms remaining ; 3 h 16 min 20 s 210.76 ms total) Fri Oct 27 08:28:45 2023: Removed ≈ 58% of redundant conclusions. [ 747709 of approximately 1289155] (ETC: Fri Oct 27 09:51:02 2023 ; 1 h 22 min 17 s 16.96 ms remaining ; 3 h 15 min 54 s 782.74 ms total) Fri Oct 27 08:32:24 2023: Removed ≈ 60% of redundant conclusions. [ 773493 of approximately 1289155] (ETC: Fri Oct 27 09:50:36 2023 ; 1 h 18 min 11 s 675.17 ms remaining ; 3 h 15 min 29 s 187.91 ms total) Fri Oct 27 08:36:05 2023: Removed ≈ 62% of redundant conclusions. [ 799276 of approximately 1289155] (ETC: Fri Oct 27 09:50:13 2023 ; 1 h 14 min 8 s 290.23 ms remaining ; 3 h 15 min 6 s 24.52 ms total) Fri Oct 27 08:39:46 2023: Removed ≈ 64% of redundant conclusions. [ 825059 of approximately 1289155] (ETC: Fri Oct 27 09:49:52 2023 ; 1 h 10 min 6 s 831.15 ms remaining ; 3 h 14 min 45 s 637.04 ms total) Fri Oct 27 08:43:28 2023: Removed ≈ 66% of redundant conclusions. [ 850842 of approximately 1289155] (ETC: Fri Oct 27 09:49:35 2023 ; 1 h 6 min 7 s 63.14 ms remaining ; 3 h 14 min 27 s 824.79 ms total) Fri Oct 27 08:47:14 2023: Removed ≈ 68% of redundant conclusions. [ 876625 of approximately 1289155] (ETC: Fri Oct 27 09:49:24 2023 ; 1 h 2 min 10 s 279.74 ms remaining ; 3 h 14 min 17 s 112.89 ms total) Fri Oct 27 08:50:52 2023: Removed ≈ 70% of redundant conclusions. [ 902408 of approximately 1289155] (ETC: Fri Oct 27 09:49:03 2023 ; 58 min 10 s 768.84 ms remaining ; 3 h 13 min 55 s 881.10 ms total) Fri Oct 27 08:54:29 2023: Removed ≈ 72% of redundant conclusions. [ 928191 of approximately 1289155] (ETC: Fri Oct 27 09:48:40 2023 ; 54 min 11 s 790.96 ms remaining ; 3 h 13 min 33 s 519.85 ms total) Fri Oct 27 08:58:06 2023: Removed ≈ 74% of redundant conclusions. [ 953974 of approximately 1289155] (ETC: Fri Oct 27 09:48:20 2023 ; 50 min 14 s 231.24 ms remaining ; 3 h 13 min 13 s 172.87 ms total) Fri Oct 27 09:01:42 2023: Removed ≈ 76% of redundant conclusions. [ 979757 of approximately 1289155] (ETC: Fri Oct 27 09:47:59 2023 ; 46 min 17 s 434.79 ms remaining ; 3 h 12 min 52 s 615.04 ms total) Fri Oct 27 09:05:18 2023: Removed ≈ 78% of redundant conclusions. [1005540 of approximately 1289155] (ETC: Fri Oct 27 09:47:40 2023 ; 42 min 21 s 665.72 ms remaining ; 3 h 12 min 32 s 989.34 ms total) Fri Oct 27 09:08:56 2023: Removed ≈ 80% of redundant conclusions. [1031324 of approximately 1289155] (ETC: Fri Oct 27 09:47:23 2023 ; 38 min 27 s 288.15 ms remaining ; 3 h 12 min 16 s 440.76 ms total) Fri Oct 27 09:12:34 2023: Removed ≈ 82% of redundant conclusions. [1057107 of approximately 1289155] (ETC: Fri Oct 27 09:47:08 2023 ; 34 min 33 s 868.43 ms remaining ; 3 h 12 min 1 s 486.30 ms total) Fri Oct 27 09:16:14 2023: Removed ≈ 84% of redundant conclusions. [1082890 of approximately 1289155] (ETC: Fri Oct 27 09:46:55 2023 ; 30 min 41 s 275.23 ms remaining ; 3 h 11 min 47 s 959.05 ms total) Fri Oct 27 09:19:54 2023: Removed ≈ 86% of redundant conclusions. [1108673 of approximately 1289155] (ETC: Fri Oct 27 09:46:43 2023 ; 26 min 49 s 493.22 ms remaining ; 3 h 11 min 36 s 361.02 ms total) Fri Oct 27 09:23:33 2023: Removed ≈ 88% of redundant conclusions. [1134456 of approximately 1289155] (ETC: Fri Oct 27 09:46:31 2023 ; 22 min 58 s 59.18 ms remaining ; 3 h 11 min 23 s 796.80 ms total) Fri Oct 27 09:27:16 2023: Removed ≈ 90% of redundant conclusions. [1160239 of approximately 1289155] (ETC: Fri Oct 27 09:46:23 2023 ; 19 min 7 s 638.58 ms remaining ; 3 h 11 min 16 s 341.29 ms total) Fri Oct 27 09:30:52 2023: Removed ≈ 92% of redundant conclusions. [1186022 of approximately 1289155] (ETC: Fri Oct 27 09:46:08 2023 ; 15 min 16 s 937.41 ms remaining ; 3 h 11 min 1 s 650.94 ms total) Fri Oct 27 09:34:30 2023: Removed ≈ 94% of redundant conclusions. [1211805 of approximately 1289155] (ETC: Fri Oct 27 09:45:57 2023 ; 11 min 27 s 20.35 ms remaining ; 3 h 10 min 50 s 235.63 ms total) Fri Oct 27 09:38:11 2023: Removed ≈ 96% of redundant conclusions. [1237588 of approximately 1289155] (ETC: Fri Oct 27 09:45:49 2023 ; 7 min 37 s 675.59 ms remaining ; 3 h 10 min 41 s 712.16 ms total) [Rank 5] Workload transfer approved. Starting to work on 0:[175208, 189808]. [Rank 67] Workload transfer approved. Starting to work on 24:[4905845, 4920445]. [Rank 20] Workload transfer approved. Starting to work on 48:[9636482, 9651082]. [Rank 1] Workload transfer approved. Starting to work on 0:[189809, 194675]. [Rank 43] Workload transfer approved. Starting to work on 4:[978249, 983115]. [Rank 21] Workload transfer approved. Starting to work on 13:[2752238, 2757104]. Fri Oct 27 09:41:53 2023: Removed ≈ 98% of redundant conclusions. [1263371 of approximately 1289155] (ETC: Fri Oct 27 09:45:41 2023 ; 3 min 48 s 699.98 ms remaining ; 3 h 10 min 34 s 600.00 ms total) [Rank 4] Workload transfer approved. Starting to work on 14:[2949348, 2954214]. [Rank 13] Workload transfer approved. Starting to work on 17:[3540677, 3545543]. [Rank 6] Workload transfer approved. Starting to work on 38:[7679985, 7684851]. [Rank 29] Workload transfer approved. Starting to work on 47:[9453974, 9458840]. [Rank 1] Workload transfer approved. Starting to work on 48:[9651083, 9655949]. [Rank 43] Workload transfer approved. Starting to work on 61:[12213512, 12218378]. [Rank 70] Workload transfer approved. Starting to work on 64:[12804841, 12809707]. [Rank 35] Workload transfer approved. Starting to work on 65:[13001951, 13006817]. [Rank 21] Workload transfer approved. Starting to work on 17:[3545544, 3547165]. [Rank 34] Workload transfer approved. Starting to work on 25:[5122423, 5124044]. [Rank 19] Workload transfer approved. Starting to work on 27:[5516643, 5518264]. [Rank 15] Workload transfer approved. Starting to work on 28:[5713753, 5715374]. [Rank 71] Workload transfer approved. Starting to work on 30:[6107973, 6109594]. [Rank 0] Workload transfer approved. Starting to work on 31:[6305083, 6306704]. [Rank 7] Workload transfer approved. Starting to work on 37:[7487742, 7489363]. [Rank 8] Workload transfer approved. Starting to work on 38:[7684852, 7686473]. Fri Oct 27 09:45:34 2023: Removed ≈100% of redundant conclusions. [1289155 of approximately 1289155] (ETC: Fri Oct 27 09:45:34 2023 ; 0.00 ms remaining ; 3 h 10 min 27 s 247.94 ms total) [Rank 51] Workload transfer approved. Starting to work on 39:[7881962, 7883583]. [Rank 49] Workload transfer approved. Starting to work on 46:[9261731, 9263352]. [Rank 17] Workload transfer approved. Starting to work on 47:[9458841, 9460462]. [Rank 11] Workload transfer approved. Starting to work on 53:[10641500, 10643121]. [Rank 14] Workload transfer approved. Starting to work on 54:[10838610, 10840231]. [Rank 33] Workload transfer approved. Starting to work on 58:[11627049, 11628670]. [Rank 56] Workload transfer approved. Starting to work on 60:[12021269, 12022890]. [Rank 27] Workload transfer approved. Starting to work on 61:[12218379, 12220000]. [Rank 44] Workload transfer approved. Starting to work on 62:[12415489, 12417110]. [Rank 28] Workload transfer approved. Starting to work on 64:[12809708, 12811329]. [Rank 57] Workload transfer approved. Starting to work on 65:[13006818, 13008439]. [Rank 45] Workload transfer approved. Starting to work on 69:[13795258, 13796879]. [Rank 55] Workload transfer approved. Starting to work on 16:[3350056, 3350866]. [Rank 16] Workload transfer approved. Starting to work on 25:[5124045, 5124855]. [Rank 21] Workload transfer approved. Starting to work on 31:[6306705, 6307515]. [Rank 34] Workload transfer approved. Starting to work on 32:[6503814, 6504624]. [Rank 63] Workload transfer approved. Starting to work on 37:[7489364, 7490174]. [Rank 41] Workload transfer approved. Starting to work on 38:[7686474, 7687284]. [Rank 40] Workload transfer approved. Starting to work on 39:[7883584, 7884394]. [Rank 22] Workload transfer approved. Starting to work on 47:[9460463, 9461273]. [Rank 3] Workload transfer approved. Starting to work on 48:[9657572, 9658382]. [Rank 19] Workload transfer approved. Starting to work on 50:[10051792, 10052602]. [Rank 2] Workload transfer approved. Starting to work on 53:[10643122, 10643932]. [Rank 59] Workload transfer approved. Starting to work on 54:[10840232, 10841042]. [Rank 25] Workload transfer approved. Starting to work on 58:[11628671, 11629481]. [Rank 26] Workload transfer approved. Starting to work on 60:[12022891, 12023701]. [Rank 42] Workload transfer approved. Starting to work on 61:[12220001, 12220811]. [Rank 32] Workload transfer approved. Starting to work on 62:[12417111, 12417921]. [Rank 9] Workload transfer approved. Starting to work on 65:[13008440, 13009250]. [Rank 12] Workload transfer approved. Starting to work on 69:[13796880, 13797690]. 11928475.16 ms (3 h 18 min 48 s 475.16 ms) taken to detect 1304710 conclusions for which there are more general variants proven in lower or equal amounts of steps. Found 12887201 representative and 1304710 redundant condensed detachment proof strings. [Copy] Removal count: { 24, 1304710 } Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 1 on "ncm0403.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 2 on "ncm0404.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 3 on "ncm0408.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 4 on "ncm0410.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 5 on "ncm0411.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 6 on "ncm0412.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 7 on "ncm0413.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 8 on "ncm0414.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 9 on "ncm0415.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 10 on "ncm0417.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 11 on "ncm0418.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 12 on "ncm0419.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 13 on "ncm0420.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 14 on "ncm0421.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 15 on "ncm0422.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 16 on "ncm0424.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 17 on "ncm0425.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 18 on "ncm0426.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 19 on "ncm0618.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 20 on "ncm0619.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 21 on "ncm0620.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 22 on "ncm0622.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 23 on "ncm0623.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 24 on "ncm0624.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 25 on "ncm0625.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 26 on "ncm0626.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 27 on "ncm0627.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 28 on "ncm0628.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 29 on "ncm0629.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 30 on "ncm0630.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 31 on "ncm0632.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 32 on "ncm0633.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 33 on "ncm0634.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 34 on "ncm0635.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 35 on "ncm0636.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 36 on "ncm0637.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 37 on "ncm0638.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 38 on "ncm0639.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 39 on "ncm0640.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 40 on "ncm0641.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 41 on "ncm0642.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 42 on "ncm0643.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 43 on "ncm0644.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 44 on "ncm0645.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 45 on "ncm0646.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 46 on "ncm0648.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 47 on "ncm0945.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 48 on "ncm0947.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 49 on "ncm0948.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 50 on "ncm0949.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 51 on "ncm0950.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 52 on "ncm0951.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 53 on "ncm0952.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 54 on "ncm0953.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 55 on "ncm0954.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 56 on "ncm0955.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 57 on "ncm0956.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 58 on "ncm0957.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 59 on "ncm0958.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 60 on "ncm0959.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 61 on "ncm0960.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 62 on "ncm0961.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 63 on "ncm0962.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 64 on "ncm0964.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 65 on "ncm0965.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 66 on "ncm0967.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 67 on "ncm0968.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 68 on "ncm0969.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 69 on "ncm0970.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 70 on "ncm0971.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:53:54 2023: MPI-based D-proof representative filter complete. [rank 71 on "ncm0973.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] 2703.25 ms (2 s 703.25 ms) taken to filter and order new representative proofs. Fri Oct 27 09:53:57 2023: Starting to write 12887201 entries to data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs24.txt. 3299.90 ms (3 s 299.90 ms) taken to print and save 996813323 bytes of representative condensed detachment proof strings to data/d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f/dProofs-withConclusions/dProofs24.txt. Fri Oct 27 09:54:00 2023: MPI-based D-proof representative filter complete. [rank 0 on "ncm0402.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 185115, tid:22601236178816] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 90596, tid:23378356860800] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 214895, tid:23060012480384] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 263665, tid:22848938645376] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 124323, tid:22843799517056] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 165657, tid:23299101013888] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 102468, tid:22586392090496] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 1869, tid:23170214020992] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 38877, tid:23137977513856] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 136681, tid:23438505510784] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 36779, tid:23184168441728] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 271884, tid:23080020006784] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 11858, tid:23186030139264] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 278169, tid:22587477464960] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 256348, tid:22722808895360] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 61468, tid:23269372839808] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 21026, tid:22688141846400] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 98365, tid:22465365833600] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 160001, tid:22991548471168] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 221896, tid:23410194192256] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 214682, tid:23109421664128] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 80470, tid:22386371372928] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 5589, tid:23357821249408] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 227891, tid:22381149042560] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 188026, tid:22765049177984] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 202907, tid:23141182240640] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 108798, tid:23092767803264] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 210940, tid:23149081790336] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 69462, tid:22720220702592] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 129879, tid:22908353324928] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 64259, tid:22904158734208] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 43719, tid:22947466860416] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 63680, tid:23024918398848] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 148156, tid:22809531279232] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 197576, tid:22375951521664] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 264831, tid:22830988916608] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 20232, tid:22596695283584] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 173327, tid:22978284640128] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 68765, tid:22450204813184] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 127202, tid:22954551646080] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 196225, tid:22747109304192] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 178986, tid:22843087759232] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 213214, tid:23237712586624] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 182384, tid:22461677094784] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 2433, tid:23128085718912] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 163451, tid:23181752145792] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 232688, tid:22561912452992] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 223828, tid:22878245283712] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 229215, tid:22994335106944] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 110102, tid:22769206597504] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 123441, tid:22899168888704] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 212719, tid:23223339050880] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 242926, tid:23386603448192] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 201204, tid:22431930382208] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 84747, tid:22976808486784] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 149509, tid:22727205250944] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 27057, tid:23414499854208] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 187523, tid:23315005351808] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 8523, tid:23034177148800] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 44475, tid:23412698564480] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 275597, tid:22583170742144] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 70919, tid:23350307731328] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 70972, tid:22538402772864] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 211074, tid:23335180507008] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 159598, tid:22784003651456] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 240346, tid:22464469706624] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 152624, tid:23423864178560] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 228445, tid:22851999057792] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 225370, tid:23013012252544] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 260097, tid:23035240404864] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 243616, tid:23317776299904] Fri Oct 27 09:54:17 2023: Process terminated. [pid: 44470, tid:22632355481472]