( 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 24 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: 5.7669444… h CPU utilization: 6643.52 core-h ) Wed Oct 25 06:32:49 2023: Process started. [pid: 219274, tid:22775743391616] Wed Oct 25 06:32:49 2023: Process started. [pid: 152778, tid:22436410099584] Wed Oct 25 06:32:49 2023: Process started. [pid: 76535, tid:23449706489728] Wed Oct 25 06:32:49 2023: Process started. [pid: 207941, tid:22977923180416] Wed Oct 25 06:32:49 2023: Process started. [pid: 16103, tid:23426246346624] Wed Oct 25 06:32:49 2023: Process started. [pid: 126416, tid:23227615475584] Wed Oct 25 06:32:49 2023: Process started. [pid: 220307, tid:22914250774400] Wed Oct 25 06:32:49 2023: Process started. [pid: 160231, tid:22467159914368] Wed Oct 25 06:32:49 2023: Process started. [pid: 100216, tid:22360707860352] Wed Oct 25 06:32:49 2023: Process started. [pid: 76757, tid:22495734925184] Wed Oct 25 06:32:49 2023: Process started. [pid: 144552, tid:22889496663936] Wed Oct 25 06:32:49 2023: Process started. [pid: 202139, tid:23313681463168] Wed Oct 25 06:32:49 2023: Process started. [pid: 82020, tid:23453930772352] Wed Oct 25 06:32:49 2023: Process started. [pid: 187089, tid:22596628207488] Wed Oct 25 06:32:49 2023: Process started. [pid: 151749, tid:23073912756096] Wed Oct 25 06:32:49 2023: Process started. [pid: 178711, tid:22729006552960] Wed Oct 25 06:32:49 2023: Process started. [pid: 107050, tid:23051326764928] Wed Oct 25 06:32:49 2023: Process started. [pid: 89745, tid:23103458248576] Wed Oct 25 06:32:49 2023: Process started. [pid: 176193, tid:23090230581120] Wed Oct 25 06:32:49 2023: Process started. [pid: 202610, tid:23044036302720] Wed Oct 25 06:32:49 2023: Process started. [pid: 167632, tid:22556067878784] Wed Oct 25 06:32:49 2023: Process started. [pid: 36039, tid:23246155868032] Wed Oct 25 06:32:49 2023: Process started. [pid: 269685, tid:23030561900416] Wed Oct 25 06:32:49 2023: Process started. [pid: 96078, tid:22810527561600] Tasks: 1. resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true) 2. mpi_filterDProofRepresentativeFile(79, true) [Rank 0 ; pid: 96078 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true). Loaded 1 custom axioms. [SHA-512/224 hash: 7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69] (1) CCC0.1CCCN2N3.2.4CC4.0C3.0 - CCCpqCCCNrNsrtCCtpCsp - ((0\imply1)\imply(((\not2\imply\not3)\imply2)\imply4))\imply((4\imply0)\imply(3\imply0)) [Rank 1 ; pid: 219274 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 2 ; pid: 100216 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 3 ; pid: 107050 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 4 ; pid: 176193 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 5 ; pid: 178711 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 6 ; pid: 151749 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 7 ; pid: 167632 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 8 ; pid: 76757 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 9 ; pid: 202610 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 10 ; pid: 207941 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 11 ; pid: 202139 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 12 ; pid: 36039 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 13 ; pid: 126416 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 14 ; pid: 187089 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 15 ; pid: 220307 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 16 ; pid: 269685 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 17 ; pid: 160231 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 18 ; pid: 76535 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 19 ; pid: 144552 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 20 ; pid: 82020 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 21 ; pid: 152778 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 22 ; pid: 89745 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 23 ; pid: 16103 ; 24 processes] Calling resetRepresentativesFor("CCCpqCCCNrNsrtCCtpCsp", true, 0, true), silently. [Rank 0 ; pid: 96078 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 1 ; pid: 219274 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 2 ; pid: 100216 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 3 ; pid: 107050 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 4 ; pid: 176193 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 5 ; pid: 178711 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 6 ; pid: 151749 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 7 ; pid: 167632 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 8 ; pid: 76757 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 9 ; pid: 202610 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 10 ; pid: 207941 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 11 ; pid: 202139 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 12 ; pid: 36039 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 13 ; pid: 126416 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 14 ; pid: 187089 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 15 ; pid: 220307 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 16 ; pid: 269685 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 17 ; pid: 160231 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 18 ; pid: 76535 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 19 ; pid: 144552 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 20 ; pid: 82020 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 21 ; pid: 152778 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 22 ; pid: 89745 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). [Rank 23 ; pid: 16103 ; 24 processes] Calling mpi_filterDProofRepresentativeFile(79, true). Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 0 on "nrm082.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 1 on "nrm084.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 2 on "nrm085.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 3 on "nrm086.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 4 on "nrm087.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 5 on "nrm089.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 6 on "nrm090.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 7 on "nrm091.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 8 on "nrm094.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 9 on "nrm095.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 10 on "nrm096.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 11 on "nrm097.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 12 on "nrm098.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 13 on "nrm099.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 14 on "nrm100.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 15 on "nrm101.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 16 on "nrm102.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 17 on "nrm103.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 18 on "nrm104.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 19 on "nrm105.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 20 on "nrm106.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 21 on "nrm107.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 22 on "nrm108.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 06:32:50 2023: MPI-based D-proof representative filter started. [rank 23 on "nrm109.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] 0.01 ms taken to load initial representatives. 9.42 ms taken to read 1 condensed detachment proof and conclusion from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs3.txt. [tid:22810352404224] 17.90 ms taken to read 2 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs5.txt. [tid:22810350302976] 19.40 ms taken to read 3 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs7.txt. [tid:22810348201728] 11.67 ms taken to read 6 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs9.txt. [tid:22810346100480] 19.78 ms taken to read 7 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs11.txt. [tid:22810343999232] 11.71 ms taken to read 12 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs13.txt. [tid:22810341897984] 14.16 ms taken to read 15 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs15.txt. [tid:22810339796736] 13.19 ms taken to read 23 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs17.txt. [tid:22810337695488] 18.35 ms taken to read 36 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs19.txt. [tid:22810335594240] 17.19 ms taken to read 61 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs21.txt. [tid:22810333492992] 27.80 ms taken to read 99 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs23.txt. [tid:22810331391744] 37.65 ms taken to read 152 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs25.txt. [tid:22810329290496] 14.14 ms taken to read 214 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs27.txt. [tid:22810327189248] 34.04 ms taken to read 299 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs29.txt. [tid:22810325088000] 22.68 ms taken to read 400 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs31.txt. [tid:22810322986752] 30.49 ms taken to read 560 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs33.txt. [tid:22810320885504] 26.02 ms taken to read 797 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs35.txt. [tid:22810318784256] 27.06 ms taken to read 1162 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs37.txt. [tid:22810316683008] 38.84 ms taken to read 1706 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs39.txt. [tid:22810314581760] 39.15 ms taken to read 2502 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs41.txt. [tid:22810312480512] 53.96 ms taken to read 3673 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs43.txt. [tid:22810310379264] 61.75 ms taken to read 5333 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs45.txt. [tid:22810308278016] 60.11 ms taken to read 7756 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs47.txt. [tid:22810306176768] 88.98 ms taken to read 11285 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs49.txt. [tid:22808893585152] 142.63 ms taken to read 16457 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs51.txt. [tid:22808891483904] 336.97 ms taken to read 24156 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs53.txt. [tid:22808889382656] 310.07 ms taken to read 35569 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs55.txt. [tid:22808887281408] 501.69 ms taken to read 52769 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs57.txt. [tid:22808885180160] 1078.70 ms (1 s 78.70 ms) taken to read 78319 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs59.txt. [tid:22808883078912] 1759.54 ms (1 s 759.54 ms) taken to read 116867 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs61.txt. [tid:22808880977664] 3542.32 ms (3 s 542.32 ms) taken to read 174207 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs63.txt. [tid:22808878876416] 8597.53 ms (8 s 597.53 ms) taken to read 260535 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs65.txt. [tid:22808876775168] 606.22 ms taken to read 389264 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs67.txt. [tid:22808874673920] 993.06 ms taken to read 582969 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs69.txt. [tid:22808872572672] 1324.12 ms (1 s 324.12 ms) taken to read 872258 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs71.txt. [tid:22808870471424] 1914.37 ms (1 s 914.37 ms) taken to read 1307863 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs73.txt. [tid:22808868370176] 2257.98 ms (2 s 257.98 ms) taken to read 1959086 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs75.txt. [tid:22808866268928] 2757.80 ms (2 s 757.80 ms) taken to read 2940441 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs77.txt. [tid:22808864167680] 8619.99 ms (8 s 619.99 ms) total read duration. Loaded 39 representative collections of sizes: 1 : 1 3 : 1 5 : 2 7 : 3 9 : 6 11 : 7 13 : 12 15 : 15 17 : 23 19 : 36 21 : 61 23 : 99 25 : 152 27 : 214 29 : 299 31 : 400 33 : 560 35 : 797 37 : 1162 39 : 1706 41 : 2502 43 : 3673 45 : 5333 47 : 7756 49 : 11285 51 : 16457 53 : 24156 55 : 35569 57 : 52769 59 : 78319 61 : 116867 63 : 174207 65 : 260535 67 : 389264 69 : 582969 71 : 872258 73 : 1307863 75 : 1959086 77 : 2940441 8846865 representatives in total. 6172.80 ms (6 s 172.80 ms) taken to read 10090963 condensed detachment proofs and conclusions from data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79-unfiltered79+.txt. [tid:22808864167680] 6174.64 ms (6 s 174.64 ms) additional read duration. Loaded 1 more representative collection of size: 79 : 10090963 18937828 representatives in total. Wed Oct 25 06:33:06 2023: Representative collections were initialized successfully on all ranks. Estimated removal count set to 5696629, based on entry 77:3795683 and last known pair (75:2529076, 77:3795683) with 3795683/2529076 ≈ 1.50082 and 3795683 * (3795683/2529076)^1 ≈ 5696629.69. Wed Oct 25 06:33:06 2023: Inserted ≈ 5% of D-proof conclusions. [ 946891 of 18937828] (ETC: Wed Oct 25 06:33:20 2023 ; 13 s 825.74 ms remaining ; 14 s 553.41 ms total) Wed Oct 25 06:33:07 2023: Inserted ≈10% of D-proof conclusions. [ 1893782 of 18937828] (ETC: Wed Oct 25 06:33:21 2023 ; 13 s 754.05 ms remaining ; 15 s 282.28 ms total) Wed Oct 25 06:33:08 2023: Inserted ≈15% of D-proof conclusions. [ 2840674 of 18937828] (ETC: Wed Oct 25 06:33:21 2023 ; 13 s 428.75 ms remaining ; 15 s 798.53 ms total) Wed Oct 25 06:33:09 2023: Inserted ≈20% of D-proof conclusions. [ 3787565 of 18937828] (ETC: Wed Oct 25 06:33:22 2023 ; 12 s 937.23 ms remaining ; 16 s 171.54 ms total) Wed Oct 25 06:33:10 2023: Inserted ≈25% of D-proof conclusions. [ 4734457 of 18937828] (ETC: Wed Oct 25 06:33:22 2023 ; 12 s 179.74 ms remaining ; 16 s 239.65 ms total) Wed Oct 25 06:33:10 2023: Inserted ≈30% of D-proof conclusions. [ 5681348 of 18937828] (ETC: Wed Oct 25 06:33:22 2023 ; 11 s 520.30 ms remaining ; 16 s 457.57 ms total) Wed Oct 25 06:33:11 2023: Inserted ≈35% of D-proof conclusions. [ 6628239 of 18937828] (ETC: Wed Oct 25 06:33:22 2023 ; 10 s 384.57 ms remaining ; 15 s 976.27 ms total) Wed Oct 25 06:33:12 2023: Inserted ≈40% of D-proof conclusions. [ 7575131 of 18937828] (ETC: Wed Oct 25 06:33:21 2023 ; 9 s 484.63 ms remaining ; 15 s 807.72 ms total) Wed Oct 25 06:33:13 2023: Inserted ≈45% of D-proof conclusions. [ 8522022 of 18937828] (ETC: Wed Oct 25 06:33:21 2023 ; 8 s 688.50 ms remaining ; 15 s 797.26 ms total) Wed Oct 25 06:33:13 2023: Inserted ≈50% of D-proof conclusions. [ 9468914 of 18937828] (ETC: Wed Oct 25 06:33:21 2023 ; 7 s 692.70 ms remaining ; 15 s 385.40 ms total) Wed Oct 25 06:33:14 2023: Inserted ≈55% of D-proof conclusions. [10415805 of 18937828] (ETC: Wed Oct 25 06:33:21 2023 ; 6 s 782.27 ms remaining ; 15 s 71.71 ms total) Wed Oct 25 06:33:14 2023: Inserted ≈60% of D-proof conclusions. [11362696 of 18937828] (ETC: Wed Oct 25 06:33:20 2023 ; 5 s 808.16 ms remaining ; 14 s 520.41 ms total) Wed Oct 25 06:33:15 2023: Inserted ≈65% of D-proof conclusions. [12309588 of 18937828] (ETC: Wed Oct 25 06:33:20 2023 ; 4 s 888.79 ms remaining ; 13 s 967.96 ms total) Wed Oct 25 06:33:15 2023: Inserted ≈70% of D-proof conclusions. [13256479 of 18937828] (ETC: Wed Oct 25 06:33:19 2023 ; 4 s 54.08 ms remaining ; 13 s 513.59 ms total) Wed Oct 25 06:33:15 2023: Inserted ≈75% of D-proof conclusions. [14203371 of 18937828] (ETC: Wed Oct 25 06:33:19 2023 ; 3 s 291.10 ms remaining ; 13 s 164.40 ms total) Wed Oct 25 06:33:16 2023: Inserted ≈80% of D-proof conclusions. [15150262 of 18937828] (ETC: Wed Oct 25 06:33:18 2023 ; 2 s 570.16 ms remaining ; 12 s 850.78 ms total) Wed Oct 25 06:33:16 2023: Inserted ≈85% of D-proof conclusions. [16097153 of 18937828] (ETC: Wed Oct 25 06:33:18 2023 ; 1 s 889.12 ms remaining ; 12 s 594.15 ms total) Wed Oct 25 06:33:17 2023: Inserted ≈90% of D-proof conclusions. [17044045 of 18937828] (ETC: Wed Oct 25 06:33:18 2023 ; 1 s 256.29 ms remaining ; 12 s 562.94 ms total) Wed Oct 25 06:33:17 2023: Inserted ≈95% of D-proof conclusions. [17990936 of 18937828] (ETC: Wed Oct 25 06:33:18 2023 ; 621.20 ms remaining ; 12 s 423.91 ms total) Wed Oct 25 06:33:18 2023: Inserted 100% of D-proof conclusions. [18937828 of 18937828] (ETC: Wed Oct 25 06:33:18 2023 ; 0.00 ms remaining ; 12 s 357.01 ms total) 12357.09 ms (12 s 357.09 ms) total insertion duration. Reservable workloads: { 0:[280304, 420455], 1:[700761, 840912], 2:[1121218, 1261369], 3:[1541675, 1681826], 4:[1962131, 2102282], 5:[2382588, 2522739], 6:[2803045, 2943196], 7:[3223502, 3363653], 8:[3643959, 3784110], 9:[4064415, 4204566], 10:[4484872, 4625023], 11:[4905329, 5045480], 12:[5325786, 5465937], 13:[5746243, 5886394], 14:[6166699, 6306850], 15:[6587156, 6727307], 16:[7007613, 7147764], 17:[7428070, 7568221], 18:[7848527, 7988678], 19:[8268983, 8409134], 20:[8689440, 8829591], 21:[9109897, 9250048], 22:[9530354, 9670505], 23:[9950811, 10090962] } Wed Oct 25 06:40:43 2023: Removed ≈ 2% of redundant conclusions. [ 113932 of approximately 5696629] (ETC: Wed Oct 25 12:42:15 2023 ; 6 h 1 min 32 s 771.22 ms remaining ; 6 h 8 min 55 s 478.54 ms total) Wed Oct 25 06:47:56 2023: Removed ≈ 4% of redundant conclusions. [ 227865 of approximately 5696629] (ETC: Wed Oct 25 12:38:16 2023 ; 5 h 50 min 20 s 544.13 ms remaining ; 6 h 4 min 56 s 399.50 ms total) Wed Oct 25 06:55:06 2023: Removed ≈ 6% of redundant conclusions. [ 341797 of approximately 5696629] (ETC: Wed Oct 25 12:36:03 2023 ; 5 h 40 min 56 s 962.59 ms remaining ; 6 h 2 min 42 s 723.15 ms total) Wed Oct 25 07:02:16 2023: Removed ≈ 8% of redundant conclusions. [ 455730 of approximately 5696629] (ETC: Wed Oct 25 12:34:56 2023 ; 5 h 32 min 40 s 780.11 ms remaining ; 6 h 1 min 36 s 498.80 ms total) Wed Oct 25 07:09:21 2023: Removed ≈ 10% of redundant conclusions. [ 569662 of approximately 5696629] (ETC: Wed Oct 25 12:33:32 2023 ; 5 h 24 min 11 s 194.64 ms remaining ; 6 h 12 s 434.69 ms total) Wed Oct 25 07:16:25 2023: Removed ≈ 12% of redundant conclusions. [ 683595 of approximately 5696629] (ETC: Wed Oct 25 12:32:20 2023 ; 5 h 15 min 54 s 991.64 ms remaining ; 5 h 58 min 59 s 761.17 ms total) Wed Oct 25 07:23:25 2023: Removed ≈ 14% of redundant conclusions. [ 797528 of approximately 5696629] (ETC: Wed Oct 25 12:31:03 2023 ; 5 h 7 min 38 s 504.31 ms remaining ; 5 h 57 min 43 s 376.84 ms total) Wed Oct 25 07:30:24 2023: Removed ≈ 16% of redundant conclusions. [ 911460 of approximately 5696629] (ETC: Wed Oct 25 12:29:59 2023 ; 4 h 59 min 34 s 831.18 ms remaining ; 5 h 56 min 38 s 605.69 ms total) Wed Oct 25 07:37:18 2023: Removed ≈ 18% of redundant conclusions. [1025393 of approximately 5696629] (ETC: Wed Oct 25 12:28:44 2023 ; 4 h 51 min 25 s 289.05 ms remaining ; 5 h 55 min 23 s 522.23 ms total) Wed Oct 25 07:44:14 2023: Removed ≈ 20% of redundant conclusions. [1139325 of approximately 5696629] (ETC: Wed Oct 25 12:27:52 2023 ; 4 h 43 min 37 s 375.10 ms remaining ; 5 h 54 min 31 s 715.15 ms total) Wed Oct 25 07:51:04 2023: Removed ≈ 22% of redundant conclusions. [1253258 of approximately 5696629] (ETC: Wed Oct 25 12:26:41 2023 ; 4 h 35 min 36 s 691.25 ms remaining ; 5 h 53 min 20 s 884.40 ms total) Wed Oct 25 07:58:00 2023: Removed ≈ 24% of redundant conclusions. [1367190 of approximately 5696629] (ETC: Wed Oct 25 12:26:05 2023 ; 4 h 28 min 5 s 273.41 ms remaining ; 5 h 52 min 44 s 828.74 ms total) Wed Oct 25 08:04:55 2023: Removed ≈ 26% of redundant conclusions. [1481123 of approximately 5696629] (ETC: Wed Oct 25 12:25:33 2023 ; 4 h 20 min 38 s 648.23 ms remaining ; 5 h 52 min 13 s 305.71 ms total) Wed Oct 25 08:11:54 2023: Removed ≈ 28% of redundant conclusions. [1595056 of approximately 5696629] (ETC: Wed Oct 25 12:25:20 2023 ; 4 h 13 min 26 s 433.68 ms remaining ; 5 h 52 min 46.16 ms total) Wed Oct 25 08:18:51 2023: Removed ≈ 30% of redundant conclusions. [1708988 of approximately 5696629] (ETC: Wed Oct 25 12:25:04 2023 ; 4 h 6 min 12 s 620.96 ms remaining ; 5 h 51 min 43 s 740.53 ms total) Wed Oct 25 08:25:46 2023: Removed ≈ 32% of redundant conclusions. [1822921 of approximately 5696629] (ETC: Wed Oct 25 12:24:41 2023 ; 3 h 58 min 54 s 902.08 ms remaining ; 5 h 51 min 20 s 736.82 ms total) Wed Oct 25 08:32:43 2023: Removed ≈ 34% of redundant conclusions. [1936853 of approximately 5696629] (ETC: Wed Oct 25 12:24:27 2023 ; 3 h 51 min 44 s 335.25 ms remaining ; 5 h 51 min 7 s 169.81 ms total) Wed Oct 25 08:39:38 2023: Removed ≈ 36% of redundant conclusions. [2050786 of approximately 5696629] (ETC: Wed Oct 25 12:24:09 2023 ; 3 h 44 min 31 s 219.07 ms remaining ; 5 h 50 min 48 s 777.25 ms total) Wed Oct 25 08:46:32 2023: Removed ≈ 38% of redundant conclusions. [2164719 of approximately 5696629] (ETC: Wed Oct 25 12:23:53 2023 ; 3 h 37 min 20 s 281.66 ms remaining ; 5 h 50 min 32 s 712.24 ms total) Wed Oct 25 08:53:29 2023: Removed ≈ 40% of redundant conclusions. [2278651 of approximately 5696629] (ETC: Wed Oct 25 12:23:43 2023 ; 3 h 30 min 13 s 638.61 ms remaining ; 5 h 50 min 22 s 727.32 ms total) Wed Oct 25 09:00:22 2023: Removed ≈ 42% of redundant conclusions. [2392584 of approximately 5696629] (ETC: Wed Oct 25 12:23:26 2023 ; 3 h 23 min 3 s 305.66 ms remaining ; 5 h 50 min 5 s 698.27 ms total) Wed Oct 25 09:07:14 2023: Removed ≈ 44% of redundant conclusions. [2506516 of approximately 5696629] (ETC: Wed Oct 25 12:23:07 2023 ; 3 h 15 min 52 s 568.04 ms remaining ; 5 h 49 min 46 s 723.65 ms total) Wed Oct 25 09:14:05 2023: Removed ≈ 46% of redundant conclusions. [2620449 of approximately 5696629] (ETC: Wed Oct 25 12:22:47 2023 ; 3 h 8 min 42 s 178.32 ms remaining ; 5 h 49 min 26 s 994.58 ms total) Wed Oct 25 09:20:52 2023: Removed ≈ 48% of redundant conclusions. [2734381 of approximately 5696629] (ETC: Wed Oct 25 12:22:22 2023 ; 3 h 1 min 30 s 26.93 ms remaining ; 5 h 49 min 2 s 352.98 ms total) Wed Oct 25 09:27:40 2023: Removed ≈ 50% of redundant conclusions. [2848314 of approximately 5696629] (ETC: Wed Oct 25 12:21:59 2023 ; 2 h 54 min 19 s 587.90 ms remaining ; 5 h 48 min 39 s 172.13 ms total) Wed Oct 25 09:34:28 2023: Removed ≈ 52% of redundant conclusions. [2962247 of approximately 5696629] (ETC: Wed Oct 25 12:21:41 2023 ; 2 h 47 min 12 s 370.32 ms remaining ; 5 h 48 min 20 s 770.90 ms total) Wed Oct 25 09:41:14 2023: Removed ≈ 54% of redundant conclusions. [3076179 of approximately 5696629] (ETC: Wed Oct 25 12:21:18 2023 ; 2 h 40 min 3 s 907.02 ms remaining ; 5 h 47 min 58 s 53.48 ms total) Wed Oct 25 09:48:00 2023: Removed ≈ 56% of redundant conclusions. [3190112 of approximately 5696629] (ETC: Wed Oct 25 12:20:58 2023 ; 2 h 32 min 57 s 522.01 ms remaining ; 5 h 47 min 38 s 2.58 ms total) Wed Oct 25 09:54:47 2023: Removed ≈ 58% of redundant conclusions. [3304044 of approximately 5696629] (ETC: Wed Oct 25 12:20:39 2023 ; 2 h 25 min 52 s 385.39 ms remaining ; 5 h 47 min 19 s 5.69 ms total) Wed Oct 25 10:01:31 2023: Removed ≈ 60% of redundant conclusions. [3417977 of approximately 5696629] (ETC: Wed Oct 25 12:20:19 2023 ; 2 h 18 min 47 s 654.16 ms remaining ; 5 h 46 min 59 s 131.75 ms total) Wed Oct 25 10:08:20 2023: Removed ≈ 62% of redundant conclusions. [3531909 of approximately 5696629] (ETC: Wed Oct 25 12:20:07 2023 ; 2 h 11 min 46 s 501.14 ms remaining ; 5 h 46 min 46 s 572.52 ms total) Wed Oct 25 10:15:05 2023: Removed ≈ 64% of redundant conclusions. [3645842 of approximately 5696629] (ETC: Wed Oct 25 12:19:49 2023 ; 2 h 4 min 43 s 983.79 ms remaining ; 5 h 46 min 28 s 838.19 ms total) Wed Oct 25 10:21:59 2023: Removed ≈ 66% of redundant conclusions. [3759775 of approximately 5696629] (ETC: Wed Oct 25 12:19:46 2023 ; 1 h 57 min 47 s 179.06 ms remaining ; 5 h 46 min 25 s 819.26 ms total) Wed Oct 25 10:28:50 2023: Removed ≈ 68% of redundant conclusions. [3873707 of approximately 5696629] (ETC: Wed Oct 25 12:19:39 2023 ; 1 h 50 min 49 s 295.46 ms remaining ; 5 h 46 min 19 s 40.11 ms total) Wed Oct 25 10:35:30 2023: Removed ≈ 70% of redundant conclusions. [3987640 of approximately 5696629] (ETC: Wed Oct 25 12:19:17 2023 ; 1 h 43 min 47 s 246.87 ms remaining ; 5 h 45 min 57 s 485.91 ms total) Wed Oct 25 10:42:12 2023: Removed ≈ 72% of redundant conclusions. [4101572 of approximately 5696629] (ETC: Wed Oct 25 12:18:59 2023 ; 1 h 36 min 46 s 856.28 ms remaining ; 5 h 45 min 38 s 760.99 ms total) Wed Oct 25 10:48:51 2023: Removed ≈ 74% of redundant conclusions. [4215505 of approximately 5696629] (ETC: Wed Oct 25 12:18:38 2023 ; 1 h 29 min 46 s 636.23 ms remaining ; 5 h 45 min 17 s 825.22 ms total) Wed Oct 25 10:55:32 2023: Removed ≈ 76% of redundant conclusions. [4329438 of approximately 5696629] (ETC: Wed Oct 25 12:18:21 2023 ; 1 h 22 min 48 s 157.45 ms remaining ; 5 h 45 min 655.43 ms total) Wed Oct 25 11:02:14 2023: Removed ≈ 78% of redundant conclusions. [4443370 of approximately 5696629] (ETC: Wed Oct 25 12:18:05 2023 ; 1 h 15 min 50 s 746.86 ms remaining ; 5 h 44 min 45 s 202.78 ms total) Wed Oct 25 11:08:58 2023: Removed ≈ 80% of redundant conclusions. [4557303 of approximately 5696629] (ETC: Wed Oct 25 12:17:52 2023 ; 1 h 8 min 54 s 414.93 ms remaining ; 5 h 44 min 32 s 71.00 ms total) Wed Oct 25 11:15:41 2023: Removed ≈ 82% of redundant conclusions. [4671235 of approximately 5696629] (ETC: Wed Oct 25 12:17:40 2023 ; 1 h 1 min 58 s 777.45 ms remaining ; 5 h 44 min 19 s 859.01 ms total) Wed Oct 25 11:22:25 2023: Removed ≈ 84% of redundant conclusions. [4785168 of approximately 5696629] (ETC: Wed Oct 25 12:17:29 2023 ; 55 min 3 s 875.89 ms remaining ; 5 h 44 min 9 s 216.18 ms total) Wed Oct 25 11:29:10 2023: Removed ≈ 86% of redundant conclusions. [4899100 of approximately 5696629] (ETC: Wed Oct 25 12:17:20 2023 ; 48 min 9 s 567.30 ms remaining ; 5 h 43 min 59 s 742.09 ms total) Wed Oct 25 11:36:00 2023: Removed ≈ 88% of redundant conclusions. [5013033 of approximately 5696629] (ETC: Wed Oct 25 12:17:16 2023 ; 41 min 16 s 354.32 ms remaining ; 5 h 43 min 56 s 270.29 ms total) Wed Oct 25 11:42:48 2023: Removed ≈ 90% of redundant conclusions. [5126966 of approximately 5696629] (ETC: Wed Oct 25 12:17:11 2023 ; 34 min 23 s 72.95 ms remaining ; 5 h 43 min 50 s 725.89 ms total) Wed Oct 25 11:49:30 2023: Removed ≈ 92% of redundant conclusions. [5240898 of approximately 5696629] (ETC: Wed Oct 25 12:17:00 2023 ; 27 min 29 s 573.09 ms remaining ; 5 h 43 min 39 s 632.83 ms total) Wed Oct 25 11:56:14 2023: Removed ≈ 94% of redundant conclusions. [5354831 of approximately 5696629] (ETC: Wed Oct 25 12:16:51 2023 ; 20 min 36 s 666.77 ms remaining ; 5 h 43 min 31 s 97.25 ms total) Wed Oct 25 12:03:00 2023: Removed ≈ 96% of redundant conclusions. [5468763 of approximately 5696629] (ETC: Wed Oct 25 12:16:44 2023 ; 13 min 44 s 176.38 ms remaining ; 5 h 43 min 24 s 333.64 ms total) [Rank 10] Workload transfer approved. Starting to work on 0:[404884, 415265]. [Rank 4] Workload transfer approved. Starting to work on 1:[825341, 835722]. Wed Oct 25 12:09:49 2023: Removed ≈ 98% of redundant conclusions. [5582696 of approximately 5696629] (ETC: Wed Oct 25 12:16:41 2023 ; 6 min 52 s 31.38 ms remaining ; 5 h 43 min 21 s 492.96 ms total) [Rank 16] Workload transfer approved. Starting to work on 11:[5029909, 5040290]. [Rank 13] Workload transfer approved. Starting to work on 0:[415266, 418725]. [Rank 15] Workload transfer approved. Starting to work on 1:[835723, 839182]. [Rank 20] Workload transfer approved. Starting to work on 2:[1256180, 1259639]. [Rank 14] Workload transfer approved. Starting to work on 3:[1676637, 1680096]. [Rank 13] Workload transfer approved. Starting to work on 11:[5040291, 5043750]. [Rank 6] Workload transfer approved. Starting to work on 19:[8403945, 8407404]. [Rank 9] Workload transfer approved. Starting to work on 21:[9244859, 9248318]. [Rank 15] Workload transfer approved. Starting to work on 0:[418726, 419879]. [Rank 14] Workload transfer approved. Starting to work on 2:[1259640, 1260793]. [Rank 20] Workload transfer approved. Starting to work on 5:[2521010, 2522163]. [Rank 3] Workload transfer approved. Starting to work on 7:[3361924, 3363077]. [Rank 0] Workload transfer approved. Starting to work on 12:[5464208, 5465361]. [Rank 15] Workload transfer approved. Starting to work on 18:[7986949, 7988102]. [Rank 14] Workload transfer approved. Starting to work on 2:[1260794, 1261369]. [Rank 20] Workload transfer approved. Starting to work on 7:[3363078, 3363653]. [Rank 11] Workload transfer approved. Starting to work on 17:[7567646, 7568221]. [Rank 22] Workload transfer approved. Starting to work on 18:[7988103, 7988678]. [Rank 1] Workload transfer approved. Starting to work on 21:[9249473, 9250048]. 20713005.97 ms (5 h 45 min 13 s 5.97 ms) taken to detect 5681764 conclusions for which there are more general variants proven in lower or equal amounts of steps. Found 4409199 representative and 5681764 redundant condensed detachment proof strings. [Copy] Removal count: { 79, 5681764 } Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 1 on "nrm084.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 2 on "nrm085.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 3 on "nrm086.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 4 on "nrm087.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 5 on "nrm089.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 6 on "nrm090.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 7 on "nrm091.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 8 on "nrm094.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 9 on "nrm095.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 10 on "nrm096.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 11 on "nrm097.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 12 on "nrm098.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 13 on "nrm099.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 14 on "nrm100.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 15 on "nrm101.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 16 on "nrm102.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 17 on "nrm103.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 18 on "nrm104.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 19 on "nrm105.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 20 on "nrm106.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 21 on "nrm107.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 22 on "nrm108.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:32 2023: MPI-based D-proof representative filter complete. [rank 23 on "nrm109.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] 1197.36 ms (1 s 197.36 ms) taken to filter and order new representative proofs. Wed Oct 25 12:18:33 2023: Starting to write 4409199 entries to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. 3045.40 ms (3 s 45.40 ms) taken to print and save 1224028908 bytes of representative condensed detachment proof strings to data/7f473b6ba952b3deadf36cd7f1c4b5286ef32fef64808d14fff70a69/dProofs-withConclusions/dProofs79.txt. Wed Oct 25 12:18:36 2023: MPI-based D-proof representative filter complete. [rank 0 on "nrm082.hpc.itc.rwth-aachen.de" ; 24 processes ; 48 local hardware thread contexts] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 167632, tid:22556067878784] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 152778, tid:22436410099584] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 160231, tid:22467159914368] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 220307, tid:22914250774400] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 144552, tid:22889496663936] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 207941, tid:22977923180416] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 82020, tid:23453930772352] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 76757, tid:22495734925184] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 126416, tid:23227615475584] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 89745, tid:23103458248576] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 96078, tid:22810527561600] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 219274, tid:22775743391616] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 269685, tid:23030561900416] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 76535, tid:23449706489728] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 16103, tid:23426246346624] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 187089, tid:22596628207488] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 202139, tid:23313681463168] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 176193, tid:23090230581120] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 151749, tid:23073912756096] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 107050, tid:23051326764928] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 202610, tid:23044036302720] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 100216, tid:22360707860352] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 36039, tid:23246155868032] Wed Oct 25 12:18:50 2023: Process terminated. [pid: 178711, tid:22729006552960]