( 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 48 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: 2.9113888… h CPU utilization: 6707.84 core-h ) Sun Oct 1 11:56:29 2023: Process started. [pid: 162953, tid:22883746346880] Sun Oct 1 11:56:29 2023: Process started. [pid: 228572, tid:22686815242112] Sun Oct 1 11:56:29 2023: Process started. [pid: 103566, tid:23389857654656] Sun Oct 1 11:56:29 2023: Process started. [pid: 260994, tid:22660369487744] Sun Oct 1 11:56:29 2023: Process started. [pid: 6028, tid:22658019436416] Sun Oct 1 11:56:29 2023: Process started. [pid: 102522, tid:22668398028672] Sun Oct 1 11:56:29 2023: Process started. [pid: 256496, tid:22371252995968] Sun Oct 1 11:56:29 2023: Process started. [pid: 210847, tid:23437190748032] Sun Oct 1 11:56:29 2023: Process started. [pid: 16572, tid:22824990521216] Sun Oct 1 11:56:29 2023: Process started. [pid: 200307, tid:23243528345472] Sun Oct 1 11:56:29 2023: Process started. [pid: 223862, tid:23274358183808] Sun Oct 1 11:56:29 2023: Process started. [pid: 206927, tid:22740393527168] Sun Oct 1 11:56:29 2023: Process started. [pid: 257248, tid:23410566924160] Sun Oct 1 11:56:29 2023: Process started. [pid: 270316, tid:22476426356608] Sun Oct 1 11:56:29 2023: Process started. [pid: 267968, tid:22708276672384] Sun Oct 1 11:56:29 2023: Process started. [pid: 227619, tid:22953816307584] Sun Oct 1 11:56:29 2023: Process started. [pid: 63926, tid:22827390928768] Sun Oct 1 11:56:29 2023: Process started. [pid: 249424, tid:22711862007680] Sun Oct 1 11:56:29 2023: Process started. [pid: 223225, tid:22924446844800] Sun Oct 1 11:56:29 2023: Process started. [pid: 72713, tid:22934036006784] Sun Oct 1 11:56:30 2023: Process started. [pid: 224635, tid:23107796805504] Sun Oct 1 11:56:30 2023: Process started. [pid: 275006, tid:23253744117632] Sun Oct 1 11:56:30 2023: Process started. [pid: 250254, tid:22942087788416] Sun Oct 1 11:56:30 2023: Process started. [pid: 1438, tid:23001885915008] Sun Oct 1 11:56:30 2023: Process started. [pid: 219016, tid:23385297700736] Sun Oct 1 11:56:30 2023: Process started. [pid: 274763, tid:23206316066688] Sun Oct 1 11:56:30 2023: Process started. [pid: 276962, tid:22756119312256] Sun Oct 1 11:56:30 2023: Process started. [pid: 235377, tid:23380255713152] Sun Oct 1 11:56:30 2023: Process started. [pid: 255142, tid:22772861208448] Sun Oct 1 11:56:30 2023: Process started. [pid: 22859, tid:22540687116160] Sun Oct 1 11:56:30 2023: Process started. [pid: 195651, tid:23293449389952] Sun Oct 1 11:56:30 2023: Process started. [pid: 224584, tid:23427456882560] Sun Oct 1 11:56:30 2023: Process started. [pid: 230129, tid:22850536327040] Sun Oct 1 11:56:30 2023: Process started. [pid: 92970, tid:23432791201664] Sun Oct 1 11:56:30 2023: Process started. [pid: 41545, tid:23371999139712] Sun Oct 1 11:56:30 2023: Process started. [pid: 149358, tid:23335155562368] Sun Oct 1 11:56:30 2023: Process started. [pid: 158176, tid:22629302286208] Sun Oct 1 11:56:30 2023: Process started. [pid: 145846, tid:22898531383168] Sun Oct 1 11:56:30 2023: Process started. [pid: 242375, tid:22453605508992] Sun Oct 1 11:56:30 2023: Process started. [pid: 206445, tid:23262505375616] Sun Oct 1 11:56:30 2023: Process started. [pid: 174746, tid:22384182241152] Sun Oct 1 11:56:30 2023: Process started. [pid: 95570, tid:22513916409728] Sun Oct 1 11:56:30 2023: Process started. [pid: 139173, tid:23399086483328] Sun Oct 1 11:56:30 2023: Process started. [pid: 240930, tid:22703855765376] Sun Oct 1 11:56:30 2023: Process started. [pid: 157248, tid:22497801869184] Sun Oct 1 11:56:30 2023: Process started. [pid: 194382, tid:23420537935744] Sun Oct 1 11:56:30 2023: Process started. [pid: 163122, tid:22902969030528] Sun Oct 1 11:56:30 2023: Process started. [pid: 118291, tid:23254672766848] Tasks: 1. resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true) 2. mpi_filterDProofRepresentativeFile(137, true) [Rank 0 ; pid: 118291 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c] (1) CC0CCN0.1.2C3CCN4C2.4C0.4 - CCpCCNpqrCsCCNtCrtCpt - (0\imply((\not0\imply1)\imply2))\imply(3\imply((\not4\imply(2\imply4))\imply(0\imply4))) [Rank 1 ; pid: 240930 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 2 ; pid: 149358 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 3 ; pid: 92970 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 4 ; pid: 1438 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 5 ; pid: 139173 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 6 ; pid: 163122 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 7 ; pid: 22859 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 8 ; pid: 158176 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 9 ; pid: 223225 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 10 ; pid: 250254 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 11 ; pid: 276962 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 12 ; pid: 145846 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 13 ; pid: 227619 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 14 ; pid: 219016 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 15 ; pid: 224584 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 16 ; pid: 275006 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 17 ; pid: 102522 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 18 ; pid: 16572 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 19 ; pid: 174746 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 20 ; pid: 257248 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 21 ; pid: 95570 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 22 ; pid: 72713 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 23 ; pid: 195651 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 24 ; pid: 210847 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 25 ; pid: 200307 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 26 ; pid: 194382 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 27 ; pid: 256496 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 28 ; pid: 242375 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 29 ; pid: 228572 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 30 ; pid: 206927 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 31 ; pid: 235377 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 32 ; pid: 41545 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 33 ; pid: 255142 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 34 ; pid: 223862 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 35 ; pid: 224635 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 36 ; pid: 270316 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 37 ; pid: 260994 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 38 ; pid: 274763 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 39 ; pid: 230129 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 40 ; pid: 162953 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 41 ; pid: 249424 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 42 ; pid: 267968 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 43 ; pid: 6028 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 44 ; pid: 206445 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 45 ; pid: 157248 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 46 ; pid: 103566 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 47 ; pid: 63926 ; 48 processes] Calling resetRepresentativesFor("CC0CCN0.1.2C3CCN4C2.4C0.4", false, 0, true), silently. [Rank 0 ; pid: 118291 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 1 ; pid: 240930 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 2 ; pid: 149358 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 3 ; pid: 92970 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 4 ; pid: 1438 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 5 ; pid: 139173 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 6 ; pid: 163122 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 7 ; pid: 22859 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 8 ; pid: 158176 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 9 ; pid: 223225 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 10 ; pid: 250254 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 11 ; pid: 276962 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 12 ; pid: 145846 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 13 ; pid: 227619 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 14 ; pid: 219016 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 15 ; pid: 224584 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 16 ; pid: 275006 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 17 ; pid: 102522 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 18 ; pid: 16572 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 19 ; pid: 174746 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 20 ; pid: 257248 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 21 ; pid: 95570 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 22 ; pid: 72713 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 23 ; pid: 195651 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 24 ; pid: 210847 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 25 ; pid: 200307 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 26 ; pid: 194382 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 27 ; pid: 256496 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 28 ; pid: 242375 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 29 ; pid: 228572 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 30 ; pid: 206927 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 31 ; pid: 235377 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 32 ; pid: 41545 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 33 ; pid: 255142 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 34 ; pid: 223862 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 35 ; pid: 224635 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 36 ; pid: 270316 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 37 ; pid: 260994 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 38 ; pid: 274763 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 39 ; pid: 230129 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 40 ; pid: 162953 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 41 ; pid: 249424 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 42 ; pid: 267968 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 43 ; pid: 6028 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 44 ; pid: 206445 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 45 ; pid: 157248 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 46 ; pid: 103566 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). [Rank 47 ; pid: 63926 ; 48 processes] Calling mpi_filterDProofRepresentativeFile(137, true). Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 0 on "ncm0597.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 1 on "ncm0604.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 2 on "ncm0608.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 3 on "ncm0612.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 4 on "nrm081.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 5 on "nrm082.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 6 on "nrm084.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 7 on "nrm085.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 8 on "nrm088.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 9 on "nrm089.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 10 on "nrm091.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 11 on "nrm092.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 12 on "nrm095.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 13 on "nrm096.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 14 on "nrm097.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 15 on "nrm098.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 16 on "nrm099.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 17 on "nrm100.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 18 on "nrm101.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 19 on "nrm102.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 20 on "nrm103.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 21 on "nrm104.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 22 on "nrm105.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 23 on "nrm107.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 24 on "nrm109.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 25 on "nrm110.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 26 on "nrm111.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 27 on "nrm113.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 28 on "nrm115.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 29 on "nrm116.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 30 on "nrm117.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 31 on "nrm118.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 32 on "nrm120.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 33 on "nrm121.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 34 on "nrm123.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 35 on "nrm124.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 36 on "nrm125.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 37 on "nrm126.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 38 on "nrm128.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 39 on "nrm130.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 40 on "nrm132.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 41 on "nrm133.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 42 on "nrm135.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 43 on "nrm138.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 44 on "nrm139.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 45 on "nrm142.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 46 on "nrm143.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 11:56:31 2023: MPI-based D-proof representative filter started. [rank 47 on "nrm144.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] 0.01 ms taken to load initial representatives. 0.05 ms taken to read 0 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs11.txt. [tid:23254489204480] 3.32 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs3.txt. [tid:23254497609472] 4.39 ms taken to read 7 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs29.txt. [tid:23254470293248] 0.26 ms taken to read 20 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs33.txt. [tid:23254466090752] 1.45 ms taken to read 15 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs31.txt. [tid:23254468192000] 2.05 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs15.txt. [tid:23254485001984] 0.16 ms taken to read 6 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs27.txt. [tid:23254472394496] 1.07 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs25.txt. [tid:23254474495744] 0.70 ms taken to read 25 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs35.txt. [tid:23254463989504] 0.72 ms taken to read 4 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs19.txt. [tid:23254480799488] 0.30 ms taken to read 51 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs43.txt. [tid:23254455584512] 0.31 ms taken to read 30 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs37.txt. [tid:23254461888256] 0.53 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs5.txt. [tid:23254495508224] 0.53 ms taken to read 2 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs7.txt. [tid:23254493406976] 0.39 ms taken to read 3 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs17.txt. [tid:23254482900736] 0.20 ms taken to read 206 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs53.txt. [tid:23254445078272] 2.78 ms taken to read 63 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs45.txt. [tid:23254453483264] 2.84 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs13.txt. [tid:23254487103232] 0.03 ms taken to read 85 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs47.txt. [tid:23254451382016] 482.34 ms taken to read 53343 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs101.txt. [tid:23254497609472] 1781.04 ms (1 s 781.04 ms) taken to read 734352 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs123.txt. [tid:23254495508224] 2405.00 ms (2 s 405.00 ms) taken to read 935212 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs125.txt. [tid:23254493406976] 3.67 ms taken to read 1 condensed detachment proof and conclusion from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs9.txt. [tid:23254491305728] 446.43 ms taken to read 41840 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs99.txt. [tid:23254489204480] 4279.90 ms (4 s 279.90 ms) taken to read 2509883 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs133.txt. [tid:23254487103232] 3697.05 ms (3 s 697.05 ms) taken to read 134564 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs109.txt. [tid:23254485001984] 3004.60 ms (3 s 4.60 ms) taken to read 1197027 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs127.txt. [tid:23254482900736] 713.88 ms taken to read 361751 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs117.txt. [tid:23254480799488] 0.04 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs21.txt. [tid:23254478698240] 21.37 ms taken to read 5 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs23.txt. [tid:23254476596992] 7029.36 ms (7 s 29.36 ms) taken to read 221055 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs113.txt. [tid:23254474495744] 4344.45 ms (4 s 344.45 ms) taken to read 172053 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs111.txt. [tid:23254472394496] 1591.38 ms (1 s 591.38 ms) taken to read 67105 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs103.txt. [tid:23254470293248] 2279.08 ms (2 s 279.08 ms) taken to read 105925 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs107.txt. [tid:23254468192000] 1550.48 ms (1 s 550.48 ms) taken to read 84222 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs105.txt. [tid:23254466090752] 1639.28 ms (1 s 639.28 ms) taken to read 283569 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs115.txt. [tid:23254463989504] 1961.78 ms (1 s 961.78 ms) taken to read 579502 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs121.txt. [tid:23254461888256] 9.38 ms taken to read 37 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs39.txt. [tid:23254459787008] 21.99 ms taken to read 42 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs41.txt. [tid:23254457685760] 911.18 ms taken to read 458509 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs119.txt. [tid:23254455584512] 3692.93 ms (3 s 692.93 ms) taken to read 1965596 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs131.txt. [tid:23254453483264] 4341.32 ms (4 s 341.32 ms) taken to read 3196594 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs135.txt. [tid:23254451382016] 1.59 ms taken to read 122 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs49.txt. [tid:23254449280768] 12.52 ms taken to read 162 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs51.txt. [tid:23254447179520] 3188.89 ms (3 s 188.89 ms) taken to read 1534565 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs129.txt. [tid:23254445078272] 6.35 ms taken to read 251 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs55.txt. [tid:23254442977024] 2.89 ms taken to read 292 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs57.txt. [tid:23254440875776] 16.87 ms taken to read 339 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs59.txt. [tid:23254438774528] 173.42 ms taken to read 444 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs61.txt. [tid:23254436673280] 9.94 ms taken to read 598 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs63.txt. [tid:23254434572032] 6.27 ms taken to read 781 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs65.txt. [tid:23254432470784] 10.37 ms taken to read 1016 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs67.txt. [tid:23252348958464] 29.36 ms taken to read 1303 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs69.txt. [tid:23252214740736] 24.23 ms taken to read 1593 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs71.txt. [tid:23252346857216] 30.20 ms taken to read 1922 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs73.txt. [tid:23252344755968] 32.97 ms taken to read 2359 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs75.txt. [tid:23252342654720] 26.06 ms taken to read 2986 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs77.txt. [tid:23252340553472] 31.27 ms taken to read 3875 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs79.txt. [tid:23252338452224] 41.91 ms taken to read 5006 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs81.txt. [tid:23252336350976] 42.78 ms taken to read 6466 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs83.txt. [tid:23252334249728] 67.61 ms taken to read 8184 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs85.txt. [tid:23252332148480] 76.68 ms taken to read 10182 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs87.txt. [tid:23252330047232] 206.22 ms taken to read 12488 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs89.txt. [tid:23252327945984] 76.99 ms taken to read 15534 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs91.txt. [tid:23252325844736] 102.00 ms taken to read 19614 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs93.txt. [tid:23252323743488] 296.71 ms taken to read 25087 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs95.txt. [tid:23252321642240] 214.56 ms taken to read 32452 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs97.txt. [tid:23252319540992] 7087.01 ms (7 s 87.01 ms) total read duration. Loaded 68 representative collections of sizes: 1 : 1 3 : 1 5 : 2 7 : 2 9 : 1 11 : 0 13 : 1 15 : 2 17 : 3 19 : 4 21 : 5 23 : 5 25 : 5 27 : 6 29 : 7 31 : 15 33 : 20 35 : 25 37 : 30 39 : 37 41 : 42 43 : 51 45 : 63 47 : 85 49 : 122 51 : 162 53 : 206 55 : 251 57 : 292 59 : 339 61 : 444 63 : 598 65 : 781 67 : 1016 69 : 1303 71 : 1593 73 : 1922 75 : 2359 77 : 2986 79 : 3875 81 : 5006 83 : 6466 85 : 8184 87 : 10182 89 : 12488 91 : 15534 93 : 19614 95 : 25087 97 : 32452 99 : 41840 101 : 53343 103 : 67105 105 : 84222 107 : 105925 109 : 134564 111 : 172053 113 : 221055 115 : 283569 117 : 361751 119 : 458509 121 : 579502 123 : 734352 125 : 935212 127 : 1197027 129 : 1534565 131 : 1965596 133 : 2509883 135 : 3196594 14790342 representatives in total. 5733.95 ms (5 s 733.95 ms) taken to read 10430172 condensed detachment proofs and conclusions from data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137-unfiltered137+.txt. [tid:23252319540992] 5735.24 ms (5 s 735.24 ms) additional read duration. Loaded 1 more representative collection of size: 137 : 10430172 25220514 representatives in total. Sun Oct 1 11:56:46 2023: Representative collections were initialized successfully on all ranks. Estimated removal count set to 6392697, based on entry 135:5001838 and last known pair (133:3913588, 135:5001838) with 5001838/3913588 ≈ 1.27807 and 5001838 * (5001838/3913588)^1 ≈ 6392697.28. Sun Oct 1 11:56:47 2023: Inserted ≈ 5% of D-proof conclusions. [ 1261025 of 25220514] (ETC: Sun Oct 1 11:57:05 2023 ; 18 s 355.32 ms remaining ; 19 s 321.39 ms total) Sun Oct 1 11:56:48 2023: Inserted ≈10% of D-proof conclusions. [ 2522051 of 25220514] (ETC: Sun Oct 1 11:57:05 2023 ; 17 s 503.37 ms remaining ; 19 s 448.19 ms total) Sun Oct 1 11:56:48 2023: Inserted ≈15% of D-proof conclusions. [ 3783077 of 25220514] (ETC: Sun Oct 1 11:57:04 2023 ; 15 s 982.49 ms remaining ; 18 s 802.93 ms total) Sun Oct 1 11:56:49 2023: Inserted ≈20% of D-proof conclusions. [ 5044102 of 25220514] (ETC: Sun Oct 1 11:57:03 2023 ; 14 s 233.13 ms remaining ; 17 s 791.41 ms total) Sun Oct 1 11:56:50 2023: Inserted ≈25% of D-proof conclusions. [ 6305128 of 25220514] (ETC: Sun Oct 1 11:57:03 2023 ; 12 s 810.90 ms remaining ; 17 s 81.20 ms total) Sun Oct 1 11:56:51 2023: Inserted ≈30% of D-proof conclusions. [ 7566154 of 25220514] (ETC: Sun Oct 1 11:57:02 2023 ; 11 s 672.13 ms remaining ; 16 s 674.47 ms total) Sun Oct 1 11:56:51 2023: Inserted ≈35% of D-proof conclusions. [ 8827179 of 25220514] (ETC: Sun Oct 1 11:57:02 2023 ; 10 s 811.32 ms remaining ; 16 s 632.80 ms total) Sun Oct 1 11:56:52 2023: Inserted ≈40% of D-proof conclusions. [10088205 of 25220514] (ETC: Sun Oct 1 11:57:02 2023 ; 9 s 696.71 ms remaining ; 16 s 161.18 ms total) Sun Oct 1 11:56:53 2023: Inserted ≈45% of D-proof conclusions. [11349231 of 25220514] (ETC: Sun Oct 1 11:57:01 2023 ; 8 s 735.49 ms remaining ; 15 s 882.71 ms total) Sun Oct 1 11:56:53 2023: Inserted ≈50% of D-proof conclusions. [12610257 of 25220514] (ETC: Sun Oct 1 11:57:01 2023 ; 7 s 844.84 ms remaining ; 15 s 689.68 ms total) Sun Oct 1 11:56:54 2023: Inserted ≈55% of D-proof conclusions. [13871282 of 25220514] (ETC: Sun Oct 1 11:57:01 2023 ; 7 s 102.96 ms remaining ; 15 s 784.36 ms total) Sun Oct 1 11:56:55 2023: Inserted ≈60% of D-proof conclusions. [15132308 of 25220514] (ETC: Sun Oct 1 11:57:01 2023 ; 6 s 269.61 ms remaining ; 15 s 674.02 ms total) Sun Oct 1 11:56:56 2023: Inserted ≈65% of D-proof conclusions. [16393334 of 25220514] (ETC: Sun Oct 1 11:57:01 2023 ; 5 s 482.55 ms remaining ; 15 s 664.44 ms total) Sun Oct 1 11:56:57 2023: Inserted ≈70% of D-proof conclusions. [17654359 of 25220514] (ETC: Sun Oct 1 11:57:01 2023 ; 4 s 740.02 ms remaining ; 15 s 800.08 ms total) Sun Oct 1 11:56:58 2023: Inserted ≈75% of D-proof conclusions. [18915385 of 25220514] (ETC: Sun Oct 1 11:57:02 2023 ; 4 s 4.48 ms remaining ; 16 s 17.93 ms total) Sun Oct 1 11:56:59 2023: Inserted ≈80% of D-proof conclusions. [20176411 of 25220514] (ETC: Sun Oct 1 11:57:02 2023 ; 3 s 239.52 ms remaining ; 16 s 197.61 ms total) Sun Oct 1 11:57:00 2023: Inserted ≈85% of D-proof conclusions. [21437436 of 25220514] (ETC: Sun Oct 1 11:57:02 2023 ; 2 s 460.52 ms remaining ; 16 s 403.45 ms total) Sun Oct 1 11:57:00 2023: Inserted ≈90% of D-proof conclusions. [22698462 of 25220514] (ETC: Sun Oct 1 11:57:02 2023 ; 1 s 654.04 ms remaining ; 16 s 540.43 ms total) Sun Oct 1 11:57:01 2023: Inserted ≈95% of D-proof conclusions. [23959488 of 25220514] (ETC: Sun Oct 1 11:57:02 2023 ; 832.72 ms remaining ; 16 s 654.42 ms total) Sun Oct 1 11:57:02 2023: Inserted 100% of D-proof conclusions. [25220514 of 25220514] (ETC: Sun Oct 1 11:57:02 2023 ; 0.00 ms remaining ; 16 s 749.51 ms total) 16749.60 ms (16 s 749.60 ms) total insertion duration. Reservable workloads: { 0:[144864, 217294], 1:[362159, 434589], 2:[579454, 651884], 3:[796749, 869180], 4:[1014045, 1086475], 5:[1231340, 1303770], 6:[1448635, 1521065], 7:[1665930, 1738361], 8:[1883226, 1955656], 9:[2100521, 2172951], 10:[2317816, 2390246], 11:[2535111, 2607542], 12:[2752407, 2824837], 13:[2969702, 3042132], 14:[3186997, 3259427], 15:[3404292, 3476723], 16:[3621588, 3694018], 17:[3838883, 3911313], 18:[4056178, 4128608], 19:[4273473, 4345904], 20:[4490769, 4563199], 21:[4708064, 4780494], 22:[4925359, 4997789], 23:[5142654, 5215085], 24:[5359950, 5432380], 25:[5577245, 5649675], 26:[5794540, 5866970], 27:[6011835, 6084266], 28:[6229131, 6301561], 29:[6446426, 6518856], 30:[6663721, 6736151], 31:[6881016, 6953447], 32:[7098312, 7170742], 33:[7315607, 7388037], 34:[7532902, 7605332], 35:[7750197, 7822628], 36:[7967493, 8039923], 37:[8184788, 8257218], 38:[8402083, 8474513], 39:[8619378, 8691809], 40:[8836674, 8909104], 41:[9053969, 9126399], 42:[9271264, 9343694], 43:[9488559, 9560990], 44:[9705855, 9778285], 45:[9923150, 9995580], 46:[10140445, 10212875], 47:[10357740, 10430171] } Sun Oct 1 12:00:40 2023: Removed ≈ 2% of redundant conclusions. [ 127853 of approximately 6392697] (ETC: Sun Oct 1 14:57:47 2023 ; 2 h 57 min 6 s 839.72 ms remaining ; 3 h 43 s 712.37 ms total) Sun Oct 1 12:04:17 2023: Removed ≈ 4% of redundant conclusions. [ 255707 of approximately 6392697] (ETC: Sun Oct 1 14:57:39 2023 ; 2 h 53 min 22 s 637.49 ms remaining ; 3 h 36 s 79.17 ms total) Sun Oct 1 12:07:51 2023: Removed ≈ 6% of redundant conclusions. [ 383561 of approximately 6392697] (ETC: Sun Oct 1 14:57:02 2023 ; 2 h 49 min 11 s 33.27 ms remaining ; 2 h 59 min 58 s 970.09 ms total) Sun Oct 1 12:11:27 2023: Removed ≈ 8% of redundant conclusions. [ 511415 of approximately 6392697] (ETC: Sun Oct 1 14:56:57 2023 ; 2 h 45 min 29 s 928.03 ms remaining ; 2 h 59 min 53 s 398.64 ms total) Sun Oct 1 12:14:59 2023: Removed ≈ 10% of redundant conclusions. [ 639269 of approximately 6392697] (ETC: Sun Oct 1 14:56:22 2023 ; 2 h 41 min 22 s 871.00 ms remaining ; 2 h 59 min 18 s 744.25 ms total) Sun Oct 1 12:18:31 2023: Removed ≈ 12% of redundant conclusions. [ 767123 of approximately 6392697] (ETC: Sun Oct 1 14:55:55 2023 ; 2 h 37 min 24 s 54.69 ms remaining ; 2 h 58 min 51 s 879.10 ms total) Sun Oct 1 12:22:04 2023: Removed ≈ 14% of redundant conclusions. [ 894977 of approximately 6392697] (ETC: Sun Oct 1 14:55:42 2023 ; 2 h 33 min 38 s 413.96 ms remaining ; 2 h 58 min 39 s 84.87 ms total) Sun Oct 1 12:25:34 2023: Removed ≈ 16% of redundant conclusions. [1022831 of approximately 6392697] (ETC: Sun Oct 1 14:55:18 2023 ; 2 h 29 min 43 s 712.05 ms remaining ; 2 h 58 min 14 s 894.26 ms total) Sun Oct 1 12:29:07 2023: Removed ≈ 18% of redundant conclusions. [1150685 of approximately 6392697] (ETC: Sun Oct 1 14:55:13 2023 ; 2 h 26 min 6 s 5.32 ms remaining ; 2 h 58 min 10 s 249.45 ms total) Sun Oct 1 12:32:37 2023: Removed ≈ 20% of redundant conclusions. [1278539 of approximately 6392697] (ETC: Sun Oct 1 14:54:50 2023 ; 2 h 22 min 13 s 699.41 ms remaining ; 2 h 57 min 47 s 123.43 ms total) Sun Oct 1 12:36:05 2023: Removed ≈ 22% of redundant conclusions. [1406393 of approximately 6392697] (ETC: Sun Oct 1 14:54:26 2023 ; 2 h 18 min 21 s 641.87 ms remaining ; 2 h 57 min 23 s 129.88 ms total) Sun Oct 1 12:39:34 2023: Removed ≈ 24% of redundant conclusions. [1534247 of approximately 6392697] (ETC: Sun Oct 1 14:54:11 2023 ; 2 h 14 min 37 s 113.11 ms remaining ; 2 h 57 min 7 s 779.80 ms total) Sun Oct 1 12:43:02 2023: Removed ≈ 26% of redundant conclusions. [1662101 of approximately 6392697] (ETC: Sun Oct 1 14:53:54 2023 ; 2 h 10 min 52 s 72.81 ms remaining ; 2 h 56 min 50 s 908.71 ms total) Sun Oct 1 12:46:30 2023: Removed ≈ 28% of redundant conclusions. [1789955 of approximately 6392697] (ETC: Sun Oct 1 14:53:39 2023 ; 2 h 7 min 8 s 978.22 ms remaining ; 2 h 56 min 35 s 802.72 ms total) Sun Oct 1 12:49:57 2023: Removed ≈ 30% of redundant conclusions. [1917809 of approximately 6392697] (ETC: Sun Oct 1 14:53:24 2023 ; 2 h 3 min 26 s 421.32 ms remaining ; 2 h 56 min 20 s 601.65 ms total) Sun Oct 1 12:53:23 2023: Removed ≈ 32% of redundant conclusions. [2045663 of approximately 6392697] (ETC: Sun Oct 1 14:53:04 2023 ; 1 h 59 min 41 s 590.37 ms remaining ; 2 h 56 min 1 s 162.21 ms total) Sun Oct 1 12:56:47 2023: Removed ≈ 34% of redundant conclusions. [2173516 of approximately 6392697] (ETC: Sun Oct 1 14:52:43 2023 ; 1 h 55 min 56 s 23.31 ms remaining ; 2 h 55 min 39 s 426.80 ms total) Sun Oct 1 13:00:12 2023: Removed ≈ 36% of redundant conclusions. [2301370 of approximately 6392697] (ETC: Sun Oct 1 14:52:28 2023 ; 1 h 52 min 15 s 740.69 ms remaining ; 2 h 55 min 24 s 592.47 ms total) Sun Oct 1 13:03:37 2023: Removed ≈ 38% of redundant conclusions. [2429224 of approximately 6392697] (ETC: Sun Oct 1 14:52:12 2023 ; 1 h 48 min 35 s 664.49 ms remaining ; 2 h 55 min 9 s 134.00 ms total) Sun Oct 1 13:06:59 2023: Removed ≈ 40% of redundant conclusions. [2557078 of approximately 6392697] (ETC: Sun Oct 1 14:51:53 2023 ; 1 h 44 min 53 s 944.78 ms remaining ; 2 h 54 min 49 s 905.77 ms total) Sun Oct 1 13:10:21 2023: Removed ≈ 42% of redundant conclusions. [2684932 of approximately 6392697] (ETC: Sun Oct 1 14:51:34 2023 ; 1 h 41 min 13 s 176.86 ms remaining ; 2 h 54 min 30 s 992.50 ms total) Sun Oct 1 13:13:44 2023: Removed ≈ 44% of redundant conclusions. [2812786 of approximately 6392697] (ETC: Sun Oct 1 14:51:19 2023 ; 1 h 37 min 35 s 398.81 ms remaining ; 2 h 54 min 16 s 67.33 ms total) Sun Oct 1 13:17:06 2023: Removed ≈ 46% of redundant conclusions. [2940640 of approximately 6392697] (ETC: Sun Oct 1 14:51:04 2023 ; 1 h 33 min 57 s 864.79 ms remaining ; 2 h 54 min 488.47 ms total) Sun Oct 1 13:20:28 2023: Removed ≈ 48% of redundant conclusions. [3068494 of approximately 6392697] (ETC: Sun Oct 1 14:50:50 2023 ; 1 h 30 min 21 s 981.31 ms remaining ; 2 h 53 min 46 s 885.38 ms total) Sun Oct 1 13:23:51 2023: Removed ≈ 50% of redundant conclusions. [3196348 of approximately 6392697] (ETC: Sun Oct 1 14:50:38 2023 ; 1 h 26 min 47 s 572.10 ms remaining ; 2 h 53 min 35 s 142.58 ms total) Sun Oct 1 13:27:14 2023: Removed ≈ 52% of redundant conclusions. [3324202 of approximately 6392697] (ETC: Sun Oct 1 14:50:29 2023 ; 1 h 23 min 14 s 587.87 ms remaining ; 2 h 53 min 25 s 389.90 ms total) Sun Oct 1 13:30:38 2023: Removed ≈ 54% of redundant conclusions. [3452056 of approximately 6392697] (ETC: Sun Oct 1 14:50:21 2023 ; 1 h 19 min 42 s 942.90 ms remaining ; 2 h 53 min 17 s 700.61 ms total) Sun Oct 1 13:34:01 2023: Removed ≈ 56% of redundant conclusions. [3579910 of approximately 6392697] (ETC: Sun Oct 1 14:50:12 2023 ; 1 h 16 min 11 s 69.32 ms remaining ; 2 h 53 min 8 s 792.73 ms total) Sun Oct 1 13:37:24 2023: Removed ≈ 58% of redundant conclusions. [3707764 of approximately 6392697] (ETC: Sun Oct 1 14:50:03 2023 ; 1 h 12 min 39 s 574.01 ms remaining ; 2 h 52 min 59 s 937.11 ms total) Sun Oct 1 13:40:46 2023: Removed ≈ 60% of redundant conclusions. [3835618 of approximately 6392697] (ETC: Sun Oct 1 14:49:54 2023 ; 1 h 9 min 8 s 379.66 ms remaining ; 2 h 52 min 50 s 948.34 ms total) Sun Oct 1 13:44:10 2023: Removed ≈ 62% of redundant conclusions. [3963472 of approximately 6392697] (ETC: Sun Oct 1 14:49:49 2023 ; 1 h 5 min 39 s 106.45 ms remaining ; 2 h 52 min 46 s 69.01 ms total) Sun Oct 1 13:47:33 2023: Removed ≈ 64% of redundant conclusions. [4091326 of approximately 6392697] (ETC: Sun Oct 1 14:49:43 2023 ; 1 h 2 min 9 s 373.51 ms remaining ; 2 h 52 min 39 s 370.50 ms total) Sun Oct 1 13:51:01 2023: Removed ≈ 66% of redundant conclusions. [4219180 of approximately 6392697] (ETC: Sun Oct 1 14:49:43 2023 ; 58 min 42 s 315.61 ms remaining ; 2 h 52 min 39 s 751.70 ms total) Sun Oct 1 13:54:28 2023: Removed ≈ 68% of redundant conclusions. [4347033 of approximately 6392697] (ETC: Sun Oct 1 14:49:43 2023 ; 55 min 15 s 206.46 ms remaining ; 2 h 52 min 40 s 15.32 ms total) Sun Oct 1 13:57:49 2023: Removed ≈ 70% of redundant conclusions. [4474887 of approximately 6392697] (ETC: Sun Oct 1 14:49:34 2023 ; 51 min 45 s 157.53 ms remaining ; 2 h 52 min 30 s 520.25 ms total) Sun Oct 1 14:01:08 2023: Removed ≈ 72% of redundant conclusions. [4602741 of approximately 6392697] (ETC: Sun Oct 1 14:49:23 2023 ; 48 min 15 s 141.20 ms remaining ; 2 h 52 min 19 s 785.14 ms total) Sun Oct 1 14:04:26 2023: Removed ≈ 74% of redundant conclusions. [4730595 of approximately 6392697] (ETC: Sun Oct 1 14:49:12 2023 ; 44 min 45 s 359.39 ms remaining ; 2 h 52 min 8 s 300.51 ms total) Sun Oct 1 14:07:48 2023: Removed ≈ 76% of redundant conclusions. [4858449 of approximately 6392697] (ETC: Sun Oct 1 14:49:06 2023 ; 41 min 17 s 375.32 ms remaining ; 2 h 52 min 2 s 392.31 ms total) Sun Oct 1 14:11:08 2023: Removed ≈ 78% of redundant conclusions. [4986303 of approximately 6392697] (ETC: Sun Oct 1 14:48:58 2023 ; 37 min 49 s 155.28 ms remaining ; 2 h 51 min 54 s 337.33 ms total) Sun Oct 1 14:14:28 2023: Removed ≈ 80% of redundant conclusions. [5114157 of approximately 6392697] (ETC: Sun Oct 1 14:48:49 2023 ; 34 min 21 s 124.64 ms remaining ; 2 h 51 min 45 s 618.36 ms total) Sun Oct 1 14:17:48 2023: Removed ≈ 82% of redundant conclusions. [5242011 of approximately 6392697] (ETC: Sun Oct 1 14:48:42 2023 ; 30 min 53 s 786.12 ms remaining ; 2 h 51 min 38 s 806.96 ms total) Sun Oct 1 14:21:09 2023: Removed ≈ 84% of redundant conclusions. [5369865 of approximately 6392697] (ETC: Sun Oct 1 14:48:36 2023 ; 27 min 26 s 830.82 ms remaining ; 2 h 51 min 32 s 687.79 ms total) Sun Oct 1 14:24:31 2023: Removed ≈ 86% of redundant conclusions. [5497719 of approximately 6392697] (ETC: Sun Oct 1 14:48:32 2023 ; 24 min 365.86 ms remaining ; 2 h 51 min 28 s 322.71 ms total) Sun Oct 1 14:27:53 2023: Removed ≈ 88% of redundant conclusions. [5625573 of approximately 6392697] (ETC: Sun Oct 1 14:48:27 2023 ; 20 min 34 s 97.12 ms remaining ; 2 h 51 min 24 s 137.82 ms total) Sun Oct 1 14:31:17 2023: Removed ≈ 90% of redundant conclusions. [5753427 of approximately 6392697] (ETC: Sun Oct 1 14:48:25 2023 ; 17 min 8 s 223.32 ms remaining ; 2 h 51 min 22 s 228.41 ms total) Sun Oct 1 14:34:35 2023: Removed ≈ 92% of redundant conclusions. [5881281 of approximately 6392697] (ETC: Sun Oct 1 14:48:17 2023 ; 13 min 41 s 909.24 ms remaining ; 2 h 51 min 13 s 860.69 ms total) Sun Oct 1 14:37:57 2023: Removed ≈ 94% of redundant conclusions. [6009135 of approximately 6392697] (ETC: Sun Oct 1 14:48:13 2023 ; 10 min 16 s 201.63 ms remaining ; 2 h 51 min 10 s 22.30 ms total) Sun Oct 1 14:41:21 2023: Removed ≈ 96% of redundant conclusions. [6136989 of approximately 6392697] (ETC: Sun Oct 1 14:48:12 2023 ; 6 min 50 s 737.93 ms remaining ; 2 h 51 min 8 s 443.37 ms total) [Rank 8] Workload transfer approved. Starting to work on 43:[9552943, 9558308]. [Rank 1] Workload transfer approved. Starting to work on 47:[10422124, 10427489]. [Rank 13] Workload transfer approved. Starting to work on 0:[209248, 214612]. [Rank 42] Workload transfer approved. Starting to work on 2:[643838, 649202]. [Rank 18] Workload transfer approved. Starting to work on 5:[1295724, 1301088]. [Rank 41] Workload transfer approved. Starting to work on 36:[8031877, 8037241]. Sun Oct 1 14:44:50 2023: Removed ≈ 98% of redundant conclusions. [6264843 of approximately 6392697] (ETC: Sun Oct 1 14:48:16 2023 ; 3 min 25 s 446.99 ms remaining ; 2 h 51 min 12 s 344.65 ms total) [Rank 38] Workload transfer approved. Starting to work on 46:[10204829, 10210193]. [Rank 45] Workload transfer approved. Starting to work on 2:[649203, 650990]. [Rank 26] Workload transfer approved. Starting to work on 3:[866499, 868286]. [Rank 12] Workload transfer approved. Starting to work on 4:[1083794, 1085581]. [Rank 27] Workload transfer approved. Starting to work on 5:[1301089, 1302876]. [Rank 37] Workload transfer approved. Starting to work on 6:[1518384, 1520171]. [Rank 0] Workload transfer approved. Starting to work on 7:[1735680, 1737467]. [Rank 24] Workload transfer approved. Starting to work on 14:[3256746, 3258533]. [Rank 44] Workload transfer approved. Starting to work on 23:[5212404, 5214191]. [Rank 43] Workload transfer approved. Starting to work on 25:[5646994, 5648781]. [Rank 21] Workload transfer approved. Starting to work on 28:[6298880, 6300667]. [Rank 29] Workload transfer approved. Starting to work on 39:[8689128, 8690915]. [Rank 4] Workload transfer approved. Starting to work on 46:[10210194, 10211981]. [Rank 9] Workload transfer approved. Starting to work on 47:[10427490, 10429277]. [Rank 19] Workload transfer approved. Starting to work on 2:[650991, 651884]. [Rank 45] Workload transfer approved. Starting to work on 6:[1520172, 1521065]. [Rank 12] Workload transfer approved. Starting to work on 7:[1737468, 1738361]. [Rank 5] Workload transfer approved. Starting to work on 10:[2389353, 2390246]. [Rank 26] Workload transfer approved. Starting to work on 14:[3258534, 3259427]. [Rank 7] Workload transfer approved. Starting to work on 15:[3475830, 3476723]. [Rank 10] Workload transfer approved. Starting to work on 17:[3910420, 3911313]. [Rank 36] Workload transfer approved. Starting to work on 20:[4562306, 4563199]. [Rank 22] Workload transfer approved. Starting to work on 23:[5214192, 5215085]. [Rank 16] Workload transfer approved. Starting to work on 25:[5648782, 5649675]. [Rank 3] Workload transfer approved. Starting to work on 28:[6300668, 6301561]. [Rank 11] Workload transfer approved. Starting to work on 30:[6735258, 6736151]. [Rank 23] Workload transfer approved. Starting to work on 31:[6952554, 6953447]. [Rank 27] Workload transfer approved. Starting to work on 32:[7169849, 7170742]. [Rank 8] Workload transfer approved. Starting to work on 33:[7387144, 7388037]. [Rank 15] Workload transfer approved. Starting to work on 35:[7821735, 7822628]. [Rank 25] Workload transfer approved. Starting to work on 46:[10211982, 10212875]. [Rank 40] Workload transfer approved. Starting to work on 47:[10429278, 10430171]. 10414029.15 ms (2 h 53 min 34 s 29.15 ms) taken to detect 6364145 conclusions for which there are more general variants proven in lower or equal amounts of steps. Found 4066027 representative and 6364145 redundant condensed detachment proof strings. [Copy] Removal count: { 137, 6364145 } Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 1 on "ncm0604.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 2 on "ncm0608.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 3 on "ncm0612.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 4 on "nrm081.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 5 on "nrm082.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 6 on "nrm084.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 7 on "nrm085.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 8 on "nrm088.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 9 on "nrm089.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 10 on "nrm091.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 11 on "nrm092.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 12 on "nrm095.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 13 on "nrm096.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 14 on "nrm097.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 15 on "nrm098.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 16 on "nrm099.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 17 on "nrm100.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 18 on "nrm101.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 19 on "nrm102.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 20 on "nrm103.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 21 on "nrm104.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 22 on "nrm105.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 23 on "nrm107.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 24 on "nrm109.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 25 on "nrm110.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 26 on "nrm111.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 27 on "nrm113.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 28 on "nrm115.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 29 on "nrm116.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 30 on "nrm117.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 31 on "nrm118.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 32 on "nrm120.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 33 on "nrm121.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 34 on "nrm123.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 35 on "nrm124.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 36 on "nrm125.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 37 on "nrm126.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 38 on "nrm128.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 39 on "nrm130.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 40 on "nrm132.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 41 on "nrm133.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 42 on "nrm135.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 43 on "nrm138.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 44 on "nrm139.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 45 on "nrm142.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 46 on "nrm143.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:50:36 2023: MPI-based D-proof representative filter complete. [rank 47 on "nrm144.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] 1838.09 ms (1 s 838.09 ms) taken to filter and order new representative proofs. Sun Oct 1 14:50:38 2023: Starting to write 4066027 entries to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. 3005.54 ms (3 s 5.54 ms) taken to print and save 1235762264 bytes of representative condensed detachment proof strings to data/02974777ff5f71e12ef58ccebedeef133584aad66e06a2a13b2b4b2c/dProofs-withConclusions/dProofs137.txt. Sun Oct 1 14:50:41 2023: MPI-based D-proof representative filter complete. [rank 0 on "ncm0597.hpc.itc.rwth-aachen.de" ; 48 processes ; 48 local hardware thread contexts] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 206445, tid:23262505375616] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 223225, tid:22924446844800] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 260994, tid:22660369487744] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 219016, tid:23385297700736] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 149358, tid:23335155562368] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 210847, tid:23437190748032] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 145846, tid:22898531383168] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 41545, tid:23371999139712] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 174746, tid:22384182241152] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 139173, tid:23399086483328] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 72713, tid:22934036006784] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 228572, tid:22686815242112] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 227619, tid:22953816307584] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 274763, tid:23206316066688] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 275006, tid:23253744117632] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 63926, tid:22827390928768] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 256496, tid:22371252995968] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 200307, tid:23243528345472] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 1438, tid:23001885915008] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 276962, tid:22756119312256] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 235377, tid:23380255713152] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 223862, tid:23274358183808] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 163122, tid:22902969030528] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 157248, tid:22497801869184] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 224584, tid:23427456882560] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 242375, tid:22453605508992] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 224635, tid:23107796805504] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 257248, tid:23410566924160] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 270316, tid:22476426356608] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 162953, tid:22883746346880] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 118291, tid:23254672766848] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 6028, tid:22658019436416] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 16572, tid:22824990521216] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 255142, tid:22772861208448] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 102522, tid:22668398028672] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 95570, tid:22513916409728] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 249424, tid:22711862007680] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 230129, tid:22850536327040] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 206927, tid:22740393527168] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 195651, tid:23293449389952] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 267968, tid:22708276672384] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 250254, tid:22942087788416] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 158176, tid:22629302286208] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 194382, tid:23420537935744] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 22859, tid:22540687116160] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 92970, tid:23432791201664] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 240930, tid:22703855765376] Sun Oct 1 14:51:10 2023: Process terminated. [pid: 103566, tid:23389857654656]