dProofs37_72node_3456cpu.log

( This log file was generated by 'pmGenerator 1.2' (master branch), compiled by 'Intel(R) oneAPI DPC++/C++ Compiler 2022.1.0 (2022.1.0.20220316)'.
  The run was executed on 72 CLAIX-2018 MPI nodes
  — 2-socket Intel Xeon Platinum 8160 (Skylake) each, 24 cores each (48 cores total per node), 2.1 GHz, 3.7 GHz turbo mode, 192 GiB main memory each —
  running Linux, Rocky 8.8. Initialization and completion messages with rank numbers have been grouped and sorted for better readability.
  Wall-clock time:     3.367222… h
  CPU utilization: 11637.12 core-h )
Sun Oct  8 03:47:17 2023: Process started. [pid: 144148, tid:23116026656640]
Sun Oct  8 03:47:17 2023: Process started. [pid: 242351, tid:22503515588480]
Sun Oct  8 03:47:17 2023: Process started. [pid: 241793, tid:22584760813440]
Sun Oct  8 03:47:17 2023: Process started. [pid: 64376, tid:22917157205888]
Sun Oct  8 03:47:17 2023: Process started. [pid: 19964, tid:22961693058944]
Sun Oct  8 03:47:17 2023: Process started. [pid: 213934, tid:23295930787712]
Sun Oct  8 03:47:17 2023: Process started. [pid: 4377, tid:23391805265792]
Sun Oct  8 03:47:17 2023: Process started. [pid: 266890, tid:23000403081088]
Sun Oct  8 03:47:17 2023: Process started. [pid: 191182, tid:22456621848448]
Sun Oct  8 03:47:17 2023: Process started. [pid: 53779, tid:22395707942784]
Sun Oct  8 03:47:17 2023: Process started. [pid: 7340, tid:23416728905600]
Sun Oct  8 03:47:17 2023: Process started. [pid: 174265, tid:22919258355584]
Sun Oct  8 03:47:17 2023: Process started. [pid: 16017, tid:22517335689088]
Sun Oct  8 03:47:17 2023: Process started. [pid: 141014, tid:22516286936960]
Sun Oct  8 03:47:17 2023: Process started. [pid: 274913, tid:23445347125120]
Sun Oct  8 03:47:17 2023: Process started. [pid: 264404, tid:23372568577920]
Sun Oct  8 03:47:17 2023: Process started. [pid: 247121, tid:23232258328448]
Sun Oct  8 03:47:17 2023: Process started. [pid: 119702, tid:22706731603840]
Sun Oct  8 03:47:17 2023: Process started. [pid: 72040, tid:23418285553536]
Sun Oct  8 03:47:17 2023: Process started. [pid: 214790, tid:23412578580352]
Sun Oct  8 03:47:17 2023: Process started. [pid: 41379, tid:22667835283328]
Sun Oct  8 03:47:17 2023: Process started. [pid: 112118, tid:22586012252032]
Sun Oct  8 03:47:17 2023: Process started. [pid: 272776, tid:23144273532800]
Sun Oct  8 03:47:17 2023: Process started. [pid: 192292, tid:22993984075648]
Sun Oct  8 03:47:17 2023: Process started. [pid: 153345, tid:22874864760704]
Sun Oct  8 03:47:17 2023: Process started. [pid: 69648, tid:23316489893760]
Sun Oct  8 03:47:17 2023: Process started. [pid: 266136, tid:22906699331456]
Sun Oct  8 03:47:17 2023: Process started. [pid: 46992, tid:22416714008448]
Sun Oct  8 03:47:17 2023: Process started. [pid: 224126, tid:22981444573056]
Sun Oct  8 03:47:17 2023: Process started. [pid: 73621, tid:22920977119104]
Sun Oct  8 03:47:17 2023: Process started. [pid: 36137, tid:22865524660096]
Sun Oct  8 03:47:17 2023: Process started. [pid: 76826, tid:23167811704704]
Sun Oct  8 03:47:17 2023: Process started. [pid: 192416, tid:23377128978304]
Sun Oct  8 03:47:17 2023: Process started. [pid: 223989, tid:22607758268288]
Sun Oct  8 03:47:17 2023: Process started. [pid: 277895, tid:22411962369920]
Sun Oct  8 03:47:17 2023: Process started. [pid: 12594, tid:23028655658880]
Sun Oct  8 03:47:17 2023: Process started. [pid: 206512, tid:22620788389760]
Sun Oct  8 03:47:17 2023: Process started. [pid: 151476, tid:22649087707008]
Sun Oct  8 03:47:17 2023: Process started. [pid: 185497, tid:22390539585408]
Sun Oct  8 03:47:17 2023: Process started. [pid: 140584, tid:22641637353344]
Sun Oct  8 03:47:17 2023: Process started. [pid: 187245, tid:23252716263296]
Sun Oct  8 03:47:17 2023: Process started. [pid: 255292, tid:23083132225408]
Sun Oct  8 03:47:17 2023: Process started. [pid: 267930, tid:23178940303232]
Sun Oct  8 03:47:17 2023: Process started. [pid: 159768, tid:22726571190144]
Sun Oct  8 03:47:17 2023: Process started. [pid: 14579, tid:23207509055360]
Sun Oct  8 03:47:17 2023: Process started. [pid: 37660, tid:22493060892544]
Sun Oct  8 03:47:17 2023: Process started. [pid: 194199, tid:23043894237056]
Sun Oct  8 03:47:17 2023: Process started. [pid: 64272, tid:23183020058496]
Sun Oct  8 03:47:17 2023: Process started. [pid: 200731, tid:23174724573056]
Sun Oct  8 03:47:17 2023: Process started. [pid: 152898, tid:23206841644928]
Sun Oct  8 03:47:17 2023: Process started. [pid: 271886, tid:23276829611904]
Sun Oct  8 03:47:17 2023: Process started. [pid: 16690, tid:22587741017984]
Sun Oct  8 03:47:17 2023: Process started. [pid: 29129, tid:23167240877952]
Sun Oct  8 03:47:17 2023: Process started. [pid: 145560, tid:22738870323072]
Sun Oct  8 03:47:17 2023: Process started. [pid: 34892, tid:22974424766336]
Sun Oct  8 03:47:17 2023: Process started. [pid: 192369, tid:22952097716096]
Sun Oct  8 03:47:17 2023: Process started. [pid: 80698, tid:22439611471744]
Sun Oct  8 03:47:17 2023: Process started. [pid: 217224, tid:22886804883328]
Sun Oct  8 03:47:17 2023: Process started. [pid: 274947, tid:22679768917888]
Sun Oct  8 03:47:17 2023: Process started. [pid: 266373, tid:22587237492608]
Sun Oct  8 03:47:17 2023: Process started. [pid: 56141, tid:22518876723072]
Sun Oct  8 03:47:17 2023: Process started. [pid: 268527, tid:23445407307648]
Sun Oct  8 03:47:17 2023: Process started. [pid: 191466, tid:22752370349952]
Sun Oct  8 03:47:17 2023: Process started. [pid: 50365, tid:23152355161984]
Sun Oct  8 03:47:17 2023: Process started. [pid: 40169, tid:22707366307712]
Sun Oct  8 03:47:17 2023: Process started. [pid: 48653, tid:22383189854080]
Sun Oct  8 03:47:17 2023: Process started. [pid: 110363, tid:22746529421184]
Sun Oct  8 03:47:17 2023: Process started. [pid: 22786, tid:22647756724096]
Sun Oct  8 03:47:17 2023: Process started. [pid: 95078, tid:23023488616320]
Sun Oct  8 03:47:17 2023: Process started. [pid: 270289, tid:23139634558848]
Sun Oct  8 03:47:17 2023: Process started. [pid: 216393, tid:23306580535168]
Sun Oct  8 03:47:17 2023: Process started. [pid: 141087, tid:23278695380864]
Tasks:
1. resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true)
2. mpi_filterDProofRepresentativeFile(37, true)

[Rank 0 ; pid: 141087 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true).
Loaded 1 custom axioms. [SHA-512/224 hash: db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff]
(1) C0CC1C0.2CCN2CCN3.4.1C3.2    -    CpCCqCprCCNrCCNstqCsr    -    0\imply((1\imply(0\imply2))\imply((\not2\imply((\not3\imply4)\imply1))\imply(3\imply2)))
[Rank 1 ; pid: 223989 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 2 ; pid: 268527 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 3 ; pid: 48653 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 4 ; pid: 194199 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 5 ; pid: 36137 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 6 ; pid: 242351 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 7 ; pid: 14579 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 8 ; pid: 266890 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 9 ; pid: 267930 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 10 ; pid: 76826 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 11 ; pid: 200731 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 12 ; pid: 110363 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 13 ; pid: 34892 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 14 ; pid: 187245 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 15 ; pid: 274947 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 16 ; pid: 73621 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 17 ; pid: 50365 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 18 ; pid: 241793 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 19 ; pid: 264404 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 20 ; pid: 206512 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 21 ; pid: 53779 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 22 ; pid: 224126 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 23 ; pid: 266373 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 24 ; pid: 37660 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 25 ; pid: 185497 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 26 ; pid: 69648 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 27 ; pid: 12594 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 28 ; pid: 64376 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 29 ; pid: 216393 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 30 ; pid: 145560 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 31 ; pid: 217224 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 32 ; pid: 191182 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 33 ; pid: 46992 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 34 ; pid: 151476 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 35 ; pid: 277895 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 36 ; pid: 40169 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 37 ; pid: 41379 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 38 ; pid: 274913 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 39 ; pid: 152898 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 40 ; pid: 192416 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 41 ; pid: 192369 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 42 ; pid: 255292 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 43 ; pid: 22786 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 44 ; pid: 140584 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 45 ; pid: 266136 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 46 ; pid: 72040 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 47 ; pid: 159768 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 48 ; pid: 16017 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 49 ; pid: 247121 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 50 ; pid: 112118 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 51 ; pid: 4377 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 52 ; pid: 19964 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 53 ; pid: 272776 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 54 ; pid: 119702 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 55 ; pid: 7340 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 56 ; pid: 141014 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 57 ; pid: 56141 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 58 ; pid: 174265 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 59 ; pid: 29129 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 60 ; pid: 213934 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 61 ; pid: 214790 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 62 ; pid: 271886 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 63 ; pid: 80698 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 64 ; pid: 16690 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 65 ; pid: 191466 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 66 ; pid: 64272 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 67 ; pid: 192292 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 68 ; pid: 153345 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 69 ; pid: 95078 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 70 ; pid: 270289 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 71 ; pid: 144148 ; 72 processes] Calling resetRepresentativesFor("CpCCqCprCCNrCCNstqCsr", true, 0, true), silently.
[Rank 0 ; pid: 141087 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 1 ; pid: 223989 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 2 ; pid: 268527 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 3 ; pid: 48653 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 4 ; pid: 194199 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 5 ; pid: 36137 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 6 ; pid: 242351 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 7 ; pid: 14579 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 8 ; pid: 266890 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 9 ; pid: 267930 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 10 ; pid: 76826 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 11 ; pid: 200731 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 12 ; pid: 110363 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 13 ; pid: 34892 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 14 ; pid: 187245 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 15 ; pid: 274947 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 16 ; pid: 73621 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 17 ; pid: 50365 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 18 ; pid: 241793 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 19 ; pid: 264404 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 20 ; pid: 206512 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 21 ; pid: 53779 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 22 ; pid: 224126 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 23 ; pid: 266373 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 24 ; pid: 37660 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 25 ; pid: 185497 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 26 ; pid: 69648 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 27 ; pid: 12594 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 28 ; pid: 64376 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 29 ; pid: 216393 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 30 ; pid: 145560 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 31 ; pid: 217224 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 32 ; pid: 191182 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 33 ; pid: 46992 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 34 ; pid: 151476 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 35 ; pid: 277895 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 36 ; pid: 40169 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 37 ; pid: 41379 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 38 ; pid: 274913 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 39 ; pid: 152898 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 40 ; pid: 192416 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 41 ; pid: 192369 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 42 ; pid: 255292 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 43 ; pid: 22786 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 44 ; pid: 140584 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 45 ; pid: 266136 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 46 ; pid: 72040 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 47 ; pid: 159768 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 48 ; pid: 16017 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 49 ; pid: 247121 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 50 ; pid: 112118 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 51 ; pid: 4377 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 52 ; pid: 19964 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 53 ; pid: 272776 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 54 ; pid: 119702 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 55 ; pid: 7340 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 56 ; pid: 141014 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 57 ; pid: 56141 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 58 ; pid: 174265 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 59 ; pid: 29129 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 60 ; pid: 213934 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 61 ; pid: 214790 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 62 ; pid: 271886 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 63 ; pid: 80698 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 64 ; pid: 16690 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 65 ; pid: 191466 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 66 ; pid: 64272 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 67 ; pid: 192292 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 68 ; pid: 153345 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 69 ; pid: 95078 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 70 ; pid: 270289 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
[Rank 71 ; pid: 144148 ; 72 processes] Calling mpi_filterDProofRepresentativeFile(37, true).
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 0 on "ncm0257.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 1 on "ncm0258.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 2 on "ncm0259.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 3 on "ncm0260.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 4 on "ncm0261.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 5 on "ncm0262.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 6 on "ncm0263.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 7 on "ncm0265.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 8 on "ncm0267.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 9 on "ncm0268.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 10 on "ncm0270.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 11 on "ncm0271.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 12 on "ncm0272.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 13 on "ncm0273.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 14 on "ncm0274.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 15 on "ncm0275.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 16 on "ncm0276.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 17 on "ncm0277.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 18 on "ncm0278.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 19 on "ncm0279.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 20 on "ncm0280.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 21 on "ncm0281.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 22 on "ncm0284.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 23 on "ncm0285.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 24 on "ncm0286.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 25 on "ncm0585.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 26 on "ncm0586.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 27 on "ncm0587.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 28 on "ncm0588.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 29 on "ncm0591.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 30 on "ncm0592.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 31 on "ncm0593.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 32 on "ncm0594.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 33 on "ncm0595.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 34 on "ncm0598.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 35 on "ncm0599.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 36 on "ncm0600.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 37 on "ncm0601.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 38 on "ncm0602.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 39 on "ncm0605.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 40 on "ncm0606.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 41 on "ncm0607.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 42 on "ncm0608.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 43 on "ncm0609.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 44 on "ncm0610.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 45 on "ncm0611.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 46 on "ncm0612.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 47 on "ncm0613.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 48 on "ncm0614.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 49 on "ncm0615.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 50 on "ncm0616.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 51 on "ncm0803.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 52 on "ncm0806.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 53 on "ncm0807.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 54 on "ncm0808.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 55 on "ncm0811.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 56 on "ncm0812.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 57 on "ncm0813.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 58 on "ncm0816.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 59 on "ncm0817.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 60 on "ncm0818.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 61 on "ncm0819.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 62 on "ncm0820.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 63 on "ncm0822.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 64 on "ncm0823.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 65 on "ncm0825.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 66 on "ncm0826.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 67 on "ncm0827.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 68 on "ncm0829.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 69 on "ncm0830.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 70 on "ncm0831.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 03:47:18 2023: MPI-based D-proof representative filter started. [rank 71 on "ncm0832.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
0.01 ms taken to load initial representatives.
0.73 ms taken to read 1 condensed detachment proof and conclusion from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs3.txt. [tid:23278520223488]
0.13 ms taken to read 2 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs5.txt. [tid:23278518122240]
3.04 ms taken to read 5 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs7.txt. [tid:23278516020992]
0.06 ms taken to read 10 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs9.txt. [tid:23278513919744]
0.03 ms taken to read 24 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs11.txt. [tid:23278511818496]
1.49 ms taken to read 57 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs13.txt. [tid:23278509717248]
0.52 ms taken to read 137 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs15.txt. [tid:23278507616000]
1.54 ms taken to read 339 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs17.txt. [tid:23278505514752]
7.36 ms taken to read 854 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs19.txt. [tid:23278503413504]
15.19 ms taken to read 2171 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs21.txt. [tid:23278501312256]
127.58 ms taken to read 5583 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs23.txt. [tid:23278499211008]
501.93 ms taken to read 14478 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs25.txt. [tid:23278497109760]
2480.69 ms (2 s 480.69 ms) taken to read 37874 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs27.txt. [tid:23278495008512]
1038.80 ms (1 s 38.80 ms) taken to read 99756 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs29.txt. [tid:23278492907264]
1314.05 ms (1 s 314.06 ms) taken to read 264466 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs31.txt. [tid:23278490806016]
3041.12 ms (3 s 41.12 ms) taken to read 705026 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs33.txt. [tid:23278488704768]
6192.87 ms (6 s 192.87 ms) taken to read 1888450 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs35.txt. [tid:23278486603520]
6221.07 ms (6 s 221.07 ms) total read duration.
Loaded 18 representative collections of sizes:
1 : 1
3 : 1
5 : 2
7 : 5
9 : 10
11 : 24
13 : 57
15 : 137
17 : 339
19 : 854
21 : 2171
23 : 5583
25 : 14478
27 : 37874
29 : 99756
31 : 264466
33 : 705026
35 : 1888450
3019234 representatives in total.
14056.88 ms (14 s 56.88 ms) taken to read 5132280 condensed detachment proofs and conclusions from data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs37-unfiltered37+.txt. [tid:23278486603520]
14058.90 ms (14 s 58.90 ms) additional read duration.
Loaded 1 more representative collection of size:
37 : 5132280
8151514 representatives in total.
Sun Oct  8 03:47:39 2023: Representative collections were initialized successfully on all ranks.
Estimated removal count set to 51633, based on entry 35:19094 and last known pair (33:7061, 35:19094) with 19094/7061 ≈ 2.70415 and 19094 * (19094/7061)^1 ≈ 51633.03.
Sun Oct  8 03:47:41 2023: Inserted ≈ 5% of D-proof conclusions. [ 407575 of 8151514] (ETC: Sun Oct  8 03:48:07 2023 ; 26 s 421.52 ms remaining ; 27 s 812.13 ms total)
Sun Oct  8 03:47:42 2023: Inserted ≈10% of D-proof conclusions. [ 815151 of 8151514] (ETC: Sun Oct  8 03:48:09 2023 ; 26 s 888.37 ms remaining ; 29 s 875.96 ms total)
Sun Oct  8 03:47:44 2023: Inserted ≈15% of D-proof conclusions. [1222727 of 8151514] (ETC: Sun Oct  8 03:48:11 2023 ; 26 s 654.20 ms remaining ; 31 s 357.88 ms total)
Sun Oct  8 03:47:46 2023: Inserted ≈20% of D-proof conclusions. [1630302 of 8151514] (ETC: Sun Oct  8 03:48:11 2023 ; 25 s  74.63 ms remaining ; 31 s 343.28 ms total)
Sun Oct  8 03:47:47 2023: Inserted ≈25% of D-proof conclusions. [2037878 of 8151514] (ETC: Sun Oct  8 03:48:11 2023 ; 23 s 389.54 ms remaining ; 31 s 186.05 ms total)
Sun Oct  8 03:47:49 2023: Inserted ≈30% of D-proof conclusions. [2445454 of 8151514] (ETC: Sun Oct  8 03:48:11 2023 ; 22 s  13.41 ms remaining ; 31 s 447.72 ms total)
Sun Oct  8 03:47:51 2023: Inserted ≈35% of D-proof conclusions. [2853029 of 8151514] (ETC: Sun Oct  8 03:48:11 2023 ; 20 s 717.24 ms remaining ; 31 s 872.66 ms total)
Sun Oct  8 03:47:52 2023: Inserted ≈40% of D-proof conclusions. [3260605 of 8151514] (ETC: Sun Oct  8 03:48:10 2023 ; 18 s 419.07 ms remaining ; 30 s 698.46 ms total)
Sun Oct  8 03:47:53 2023: Inserted ≈45% of D-proof conclusions. [3668181 of 8151514] (ETC: Sun Oct  8 03:48:09 2023 ; 15 s 960.69 ms remaining ; 29 s  19.43 ms total)
Sun Oct  8 03:47:53 2023: Inserted ≈50% of D-proof conclusions. [4075757 of 8151514] (ETC: Sun Oct  8 03:48:07 2023 ; 13 s 715.78 ms remaining ; 27 s 431.55 ms total)
Sun Oct  8 03:47:54 2023: Inserted ≈55% of D-proof conclusions. [4483332 of 8151514] (ETC: Sun Oct  8 03:48:06 2023 ; 11 s 874.80 ms remaining ; 26 s 388.44 ms total)
Sun Oct  8 03:47:55 2023: Inserted ≈60% of D-proof conclusions. [4890908 of 8151514] (ETC: Sun Oct  8 03:48:05 2023 ; 10 s 187.34 ms remaining ; 25 s 468.35 ms total)
Sun Oct  8 03:47:56 2023: Inserted ≈65% of D-proof conclusions. [5298484 of 8151514] (ETC: Sun Oct  8 03:48:04 2023 ; 8 s 639.35 ms remaining ; 24 s 683.86 ms total)
Sun Oct  8 03:47:56 2023: Inserted ≈70% of D-proof conclusions. [5706059 of 8151514] (ETC: Sun Oct  8 03:48:04 2023 ; 7 s 217.67 ms remaining ; 24 s  58.89 ms total)
Sun Oct  8 03:47:57 2023: Inserted ≈75% of D-proof conclusions. [6113635 of 8151514] (ETC: Sun Oct  8 03:48:03 2023 ; 5 s 863.99 ms remaining ; 23 s 455.95 ms total)
Sun Oct  8 03:47:58 2023: Inserted ≈80% of D-proof conclusions. [6521211 of 8151514] (ETC: Sun Oct  8 03:48:02 2023 ; 4 s 594.89 ms remaining ; 22 s 974.44 ms total)
Sun Oct  8 03:47:59 2023: Inserted ≈85% of D-proof conclusions. [6928786 of 8151514] (ETC: Sun Oct  8 03:48:02 2023 ; 3 s 380.77 ms remaining ; 22 s 538.47 ms total)
Sun Oct  8 03:47:59 2023: Inserted ≈90% of D-proof conclusions. [7336362 of 8151514] (ETC: Sun Oct  8 03:48:02 2023 ; 2 s 218.14 ms remaining ; 22 s 181.40 ms total)
Sun Oct  8 03:48:00 2023: Inserted ≈95% of D-proof conclusions. [7743938 of 8151514] (ETC: Sun Oct  8 03:48:01 2023 ; 1 s  98.47 ms remaining ; 21 s 969.36 ms total)
Sun Oct  8 03:48:01 2023: Inserted 100% of D-proof conclusions. [8151514 of 8151514] (ETC: Sun Oct  8 03:48:01 2023 ; 0.00 ms remaining ; 21 s 715.06 ms total)
21715.22 ms (21 s 715.22 ms) total insertion duration.
Reservable workloads: { 0:[47521, 71280], 1:[118803, 142562], 2:[190085, 213844], 3:[261366, 285125], 4:[332648, 356407], 5:[403930, 427689], 6:[475211, 498970], 7:[546493, 570252], 8:[617775, 641534], 9:[689056, 712815], 10:[760338, 784097], 11:[831620, 855379], 12:[902901, 926660], 13:[974183, 997942], 14:[1045465, 1069224], 15:[1116746, 1140505], 16:[1188028, 1211787], 17:[1259310, 1283069], 18:[1330591, 1354350], 19:[1401873, 1425632], 20:[1473155, 1496914], 21:[1544436, 1568195], 22:[1615718, 1639477], 23:[1687000, 1710759], 24:[1758281, 1782040], 25:[1829563, 1853322], 26:[1900845, 1924604], 27:[1972126, 1995885], 28:[2043408, 2067167], 29:[2114690, 2138449], 30:[2185971, 2209730], 31:[2257253, 2281012], 32:[2328535, 2352294], 33:[2399816, 2423575], 34:[2471098, 2494857], 35:[2542380, 2566139], 36:[2613661, 2637420], 37:[2684943, 2708702], 38:[2756225, 2779984], 39:[2827506, 2851265], 40:[2898788, 2922547], 41:[2970070, 2993829], 42:[3041351, 3065110], 43:[3112633, 3136392], 44:[3183915, 3207674], 45:[3255196, 3278955], 46:[3326478, 3350237], 47:[3397760, 3421519], 48:[3469041, 3492800], 49:[3540323, 3564082], 50:[3611605, 3635364], 51:[3682886, 3706645], 52:[3754168, 3777927], 53:[3825450, 3849209], 54:[3896731, 3920490], 55:[3968013, 3991772], 56:[4039295, 4063054], 57:[4110576, 4134335], 58:[4181858, 4205617], 59:[4253140, 4276899], 60:[4324421, 4348180], 61:[4395703, 4419462], 62:[4466985, 4490744], 63:[4538266, 4562025], 64:[4609548, 4633307], 65:[4680830, 4704589], 66:[4752111, 4775870], 67:[4823393, 4847152], 68:[4894675, 4918434], 69:[4965956, 4989715], 70:[5037238, 5060997], 71:[5108520, 5132279] }
Sun Oct  8 03:51:25 2023: Removed ≈  2% of redundant conclusions. [ 1032 of approximately 51633] (ETC: Sun Oct  8 06:37:01 2023 ; 2 h 45 min 35 s 462.71 ms remaining ; 2 h 48 min 58 s  95.02 ms total)
Sun Oct  8 03:54:55 2023: Removed ≈  4% of redundant conclusions. [ 2065 of approximately 51633] (ETC: Sun Oct  8 06:39:52 2023 ; 2 h 44 min 57 s 501.66 ms remaining ; 2 h 51 min 49 s 831.00 ms total)
Sun Oct  8 03:58:31 2023: Removed ≈  6% of redundant conclusions. [ 3097 of approximately 51633] (ETC: Sun Oct  8 06:42:35 2023 ; 2 h 44 min  4 s 653.67 ms remaining ; 2 h 54 min 32 s 824.36 ms total)
Sun Oct  8 04:02:02 2023: Removed ≈  8% of redundant conclusions. [ 4130 of approximately 51633] (ETC: Sun Oct  8 06:42:56 2023 ; 2 h 40 min 54 s 377.32 ms remaining ; 2 h 54 min 53 s 747.01 ms total)
Sun Oct  8 04:05:37 2023: Removed ≈ 10% of redundant conclusions. [ 5163 of approximately 51633] (ETC: Sun Oct  8 06:43:47 2023 ; 2 h 38 min 10 s 536.69 ms remaining ; 2 h 55 min 44 s 972.69 ms total)
Sun Oct  8 04:09:10 2023: Removed ≈ 12% of redundant conclusions. [ 6195 of approximately 51633] (ETC: Sun Oct  8 06:44:05 2023 ; 2 h 34 min 55 s 621.46 ms remaining ; 2 h 56 min  2 s 983.03 ms total)
Sun Oct  8 04:12:47 2023: Removed ≈ 14% of redundant conclusions. [ 7228 of approximately 51633] (ETC: Sun Oct  8 06:44:45 2023 ; 2 h 31 min 58 s 106.80 ms remaining ; 2 h 56 min 42 s 301.73 ms total)
Sun Oct  8 04:16:08 2023: Removed ≈ 16% of redundant conclusions. [ 8261 of approximately 51633] (ETC: Sun Oct  8 06:43:40 2023 ; 2 h 27 min 31 s 849.36 ms remaining ; 2 h 55 min 37 s 847.88 ms total)
Sun Oct  8 04:19:33 2023: Removed ≈ 18% of redundant conclusions. [ 9293 of approximately 51633] (ETC: Sun Oct  8 06:43:06 2023 ; 2 h 23 min 33 s 266.98 ms remaining ; 2 h 55 min  3 s 750.92 ms total)
Sun Oct  8 04:23:07 2023: Removed ≈ 20% of redundant conclusions. [10326 of approximately 51633] (ETC: Sun Oct  8 06:43:25 2023 ; 2 h 20 min 18 s  84.25 ms remaining ; 2 h 55 min 22 s 452.46 ms total)
Sun Oct  8 04:26:37 2023: Removed ≈ 22% of redundant conclusions. [11359 of approximately 51633] (ETC: Sun Oct  8 06:43:22 2023 ; 2 h 16 min 45 s 148.08 ms remaining ; 2 h 55 min 19 s 352.70 ms total)
Sun Oct  8 04:30:08 2023: Removed ≈ 24% of redundant conclusions. [12391 of approximately 51633] (ETC: Sun Oct  8 06:43:25 2023 ; 2 h 13 min 17 s 294.54 ms remaining ; 2 h 55 min 22 s 509.28 ms total)
Sun Oct  8 04:33:35 2023: Removed ≈ 26% of redundant conclusions. [13424 of approximately 51633] (ETC: Sun Oct  8 06:43:13 2023 ; 2 h  9 min 37 s 585.15 ms remaining ; 2 h 55 min 10 s  90.66 ms total)
Sun Oct  8 04:37:13 2023: Removed ≈ 28% of redundant conclusions. [14457 of approximately 51633] (ETC: Sun Oct  8 06:43:40 2023 ; 2 h  6 min 26 s 789.92 ms remaining ; 2 h 55 min 37 s 140.19 ms total)
Sun Oct  8 04:40:37 2023: Removed ≈ 30% of redundant conclusions. [15489 of approximately 51633] (ETC: Sun Oct  8 06:43:19 2023 ; 2 h  2 min 42 s  17.48 ms remaining ; 2 h 55 min 16 s 905.95 ms total)
Sun Oct  8 04:44:06 2023: Removed ≈ 32% of redundant conclusions. [16522 of approximately 51633] (ETC: Sun Oct  8 06:43:13 2023 ; 1 h 59 min  7 s  86.36 ms remaining ; 2 h 55 min 10 s 253.49 ms total)
Sun Oct  8 04:47:44 2023: Removed ≈ 34% of redundant conclusions. [17555 of approximately 51633] (ETC: Sun Oct  8 06:43:36 2023 ; 1 h 55 min 52 s 203.41 ms remaining ; 2 h 55 min 33 s 573.53 ms total)
Sun Oct  8 04:51:10 2023: Removed ≈ 36% of redundant conclusions. [18587 of approximately 51633] (ETC: Sun Oct  8 06:43:25 2023 ; 1 h 52 min 14 s 650.52 ms remaining ; 2 h 55 min 22 s 611.23 ms total)
Sun Oct  8 04:54:48 2023: Removed ≈ 38% of redundant conclusions. [19620 of approximately 51633] (ETC: Sun Oct  8 06:43:44 2023 ; 1 h 48 min 55 s 984.25 ms remaining ; 2 h 55 min 41 s 732.26 ms total)
Sun Oct  8 04:58:11 2023: Removed ≈ 40% of redundant conclusions. [20653 of approximately 51633] (ETC: Sun Oct  8 06:43:23 2023 ; 1 h 45 min 12 s 114.81 ms remaining ; 2 h 55 min 20 s 123.43 ms total)
Sun Oct  8 05:01:34 2023: Removed ≈ 42% of redundant conclusions. [21685 of approximately 51633] (ETC: Sun Oct  8 06:43:06 2023 ; 1 h 41 min 32 s 487.18 ms remaining ; 2 h 55 min  3 s 986.60 ms total)
Sun Oct  8 05:05:13 2023: Removed ≈ 44% of redundant conclusions. [22718 of approximately 51633] (ETC: Sun Oct  8 06:43:26 2023 ; 1 h 38 min 13 s 518.18 ms remaining ; 2 h 55 min 23 s 950.35 ms total)
Sun Oct  8 05:08:45 2023: Removed ≈ 46% of redundant conclusions. [23751 of approximately 51633] (ETC: Sun Oct  8 06:43:30 2023 ; 1 h 34 min 44 s 893.69 ms remaining ; 2 h 55 min 27 s 512.94 ms total)
Sun Oct  8 05:12:27 2023: Removed ≈ 48% of redundant conclusions. [24783 of approximately 51633] (ETC: Sun Oct  8 06:43:54 2023 ; 1 h 31 min 27 s 189.27 ms remaining ; 2 h 55 min 51 s 956.93 ms total)
Sun Oct  8 05:15:59 2023: Removed ≈ 50% of redundant conclusions. [25816 of approximately 51633] (ETC: Sun Oct  8 06:43:56 2023 ; 1 h 27 min 56 s 957.41 ms remaining ; 2 h 55 min 53 s 710.42 ms total)
Sun Oct  8 05:19:36 2023: Removed ≈ 52% of redundant conclusions. [26849 of approximately 51633] (ETC: Sun Oct  8 06:44:07 2023 ; 1 h 24 min 30 s 959.23 ms remaining ; 2 h 56 min  4 s 430.20 ms total)
Sun Oct  8 05:23:06 2023: Removed ≈ 54% of redundant conclusions. [27881 of approximately 51633] (ETC: Sun Oct  8 06:44:05 2023 ; 1 h 20 min 59 s  92.65 ms remaining ; 2 h 56 min  2 s 880.22 ms total)
Sun Oct  8 05:26:47 2023: Removed ≈ 56% of redundant conclusions. [28914 of approximately 51633] (ETC: Sun Oct  8 06:44:22 2023 ; 1 h 17 min 34 s 904.77 ms remaining ; 2 h 56 min 19 s 105.50 ms total)
Sun Oct  8 05:30:11 2023: Removed ≈ 58% of redundant conclusions. [29947 of approximately 51633] (ETC: Sun Oct  8 06:44:09 2023 ; 1 h 13 min 58 s   8.90 ms remaining ; 2 h 56 min  6 s 619.65 ms total)
Sun Oct  8 05:33:41 2023: Removed ≈ 60% of redundant conclusions. [30979 of approximately 51633] (ETC: Sun Oct  8 06:44:07 2023 ; 1 h 10 min 26 s  97.30 ms remaining ; 2 h 56 min  4 s 834.03 ms total)
Sun Oct  8 05:37:14 2023: Removed ≈ 62% of redundant conclusions. [32012 of approximately 51633] (ETC: Sun Oct  8 06:44:10 2023 ; 1 h  6 min 55 s 686.28 ms remaining ; 2 h 56 min  7 s 347.73 ms total)
Sun Oct  8 05:40:50 2023: Removed ≈ 64% of redundant conclusions. [33045 of approximately 51633] (ETC: Sun Oct  8 06:44:16 2023 ; 1 h  3 min 26 s 523.96 ms remaining ; 2 h 56 min 13 s 609.39 ms total)
Sun Oct  8 05:45:19 2023: Removed ≈ 66% of redundant conclusions. [34077 of approximately 51633] (ETC: Sun Oct  8 06:45:43 2023 ; 1 h        24 s 898.24 ms remaining ; 2 h 57 min 40 s 991.73 ms total)
Sun Oct  8 05:50:07 2023: Removed ≈ 68% of redundant conclusions. [35110 of approximately 51633] (ETC: Sun Oct  8 06:47:34 2023 ; 57 min 26 s 875.09 ms remaining ; 2 h 59 min 31 s 197.83 ms total)
Sun Oct  8 05:53:53 2023: Removed ≈ 70% of redundant conclusions. [36143 of approximately 51633] (ETC: Sun Oct  8 06:47:49 2023 ; 53 min 56 s  16.00 ms remaining ; 2 h 59 min 46 s 650.37 ms total)
Sun Oct  8 05:57:29 2023: Removed ≈ 72% of redundant conclusions. [37175 of approximately 51633] (ETC: Sun Oct  8 06:47:50 2023 ; 50 min 20 s 601.04 ms remaining ; 2 h 59 min 47 s 293.80 ms total)
Sun Oct  8 06:01:03 2023: Removed ≈ 74% of redundant conclusions. [38208 of approximately 51633] (ETC: Sun Oct  8 06:47:47 2023 ; 46 min 43 s 944.75 ms remaining ; 2 h 59 min 44 s  65.49 ms total)
Sun Oct  8 06:04:42 2023: Removed ≈ 76% of redundant conclusions. [39241 of approximately 51633] (ETC: Sun Oct  8 06:47:51 2023 ; 43 min  9 s 369.42 ms remaining ; 2 h 59 min 48 s 969.59 ms total)
Sun Oct  8 06:08:15 2023: Removed ≈ 78% of redundant conclusions. [40273 of approximately 51633] (ETC: Sun Oct  8 06:47:47 2023 ; 39 min 32 s 821.50 ms remaining ; 2 h 59 min 44 s 849.71 ms total)
Sun Oct  8 06:11:44 2023: Removed ≈ 80% of redundant conclusions. [41306 of approximately 51633] (ETC: Sun Oct  8 06:47:40 2023 ; 35 min 55 s 603.16 ms remaining ; 2 h 59 min 37 s 598.34 ms total)
Sun Oct  8 06:15:08 2023: Removed ≈ 82% of redundant conclusions. [42339 of approximately 51633] (ETC: Sun Oct  8 06:47:25 2023 ; 32 min 17 s 261.00 ms remaining ; 2 h 59 min 22 s 491.65 ms total)
Sun Oct  8 06:18:43 2023: Removed ≈ 84% of redundant conclusions. [43371 of approximately 51633] (ETC: Sun Oct  8 06:47:25 2023 ; 28 min 42 s 210.24 ms remaining ; 2 h 59 min 22 s 875.97 ms total)
Sun Oct  8 06:22:31 2023: Removed ≈ 86% of redundant conclusions. [44404 of approximately 51633] (ETC: Sun Oct  8 06:47:40 2023 ; 25 min  8 s 990.50 ms remaining ; 2 h 59 min 37 s 936.98 ms total)
Sun Oct  8 06:27:27 2023: Removed ≈ 88% of redundant conclusions. [45437 of approximately 51633] (ETC: Sun Oct  8 06:49:11 2023 ; 21 min 44 s 221.28 ms remaining ; 3 h  1 min  8 s 440.49 ms total)
Sun Oct  8 06:31:56 2023: Removed ≈ 90% of redundant conclusions. [46469 of approximately 51633] (ETC: Sun Oct  8 06:50:09 2023 ; 18 min 12 s 769.60 ms remaining ; 3 h  2 min  6 s 214.75 ms total)
Sun Oct  8 06:36:09 2023: Removed ≈ 92% of redundant conclusions. [47502 of approximately 51633] (ETC: Sun Oct  8 06:50:46 2023 ; 14 min 37 s 183.00 ms remaining ; 3 h  2 min 43 s 831.90 ms total)
Sun Oct  8 06:40:55 2023: Removed ≈ 94% of redundant conclusions. [48535 of approximately 51633] (ETC: Sun Oct  8 06:51:57 2023 ; 11 min  2 s  77.35 ms remaining ; 3 h  3 min 54 s 551.23 ms total)
[Rank 18] Workload transfer approved. Starting to work on 0:[63361, 68640].
[Rank 1] Workload transfer approved. Starting to work on 14:[1061305, 1066584].
[Rank 30] Workload transfer approved. Starting to work on 49:[3556163, 3561442].
Sun Oct  8 06:46:29 2023: Removed ≈ 96% of redundant conclusions. [49567 of approximately 51633] (ETC: Sun Oct  8 06:53:56 2023 ; 7 min 26 s 269.73 ms remaining ; 3 h  5 min 53 s  71.24 ms total)
[Rank 26] Workload transfer approved. Starting to work on 0:[68641, 70400].
[Rank 4] Workload transfer approved. Starting to work on 5:[425050, 426809].
[Rank 12] Workload transfer approved. Starting to work on 9:[710176, 711935].
[Rank 65] Workload transfer approved. Starting to work on 13:[995303, 997062].
[Rank 63] Workload transfer approved. Starting to work on 14:[1066585, 1068344].
[Rank 42] Workload transfer approved. Starting to work on 22:[1636838, 1638597].
[Rank 68] Workload transfer approved. Starting to work on 25:[1850683, 1852442].
[Rank 40] Workload transfer approved. Starting to work on 32:[2349655, 2351414].
[Rank 60] Workload transfer approved. Starting to work on 34:[2492218, 2493977].
[Rank 47] Workload transfer approved. Starting to work on 43:[3133753, 3135512].
[Rank 64] Workload transfer approved. Starting to work on 49:[3561443, 3563202].
[Rank 28] Workload transfer approved. Starting to work on 57:[4131696, 4133455].
[Rank 29] Workload transfer approved. Starting to work on 58:[4202978, 4204737].
[Rank 59] Workload transfer approved. Starting to work on 62:[4488105, 4489864].
[Rank 31] Workload transfer approved. Starting to work on 66:[4773231, 4774990].
[Rank 38] Workload transfer approved. Starting to work on 2:[212965, 213844].
[Rank 46] Workload transfer approved. Starting to work on 5:[426810, 427689].
[Rank 2] Workload transfer approved. Starting to work on 7:[569373, 570252].
[Rank 16] Workload transfer approved. Starting to work on 8:[640655, 641534].
Sun Oct  8 06:52:31 2023: Removed ≈ 98% of redundant conclusions. [50600 of approximately 51633] (ETC: Sun Oct  8 06:56:17 2023 ; 3 min 45 s 965.16 ms remaining ; 3 h  8 min 14 s 539.35 ms total)
[Rank 71] Workload transfer approved. Starting to work on 9:[711936, 712815].
[Rank 17] Workload transfer approved. Starting to work on 10:[783218, 784097].
[Rank 26] Workload transfer approved. Starting to work on 15:[1139626, 1140505].
[Rank 48] Workload transfer approved. Starting to work on 19:[1424753, 1425632].
[Rank 41] Workload transfer approved. Starting to work on 22:[1638598, 1639477].
[Rank 69] Workload transfer approved. Starting to work on 23:[1709880, 1710759].
[Rank 37] Workload transfer approved. Starting to work on 24:[1781161, 1782040].
[Rank 7] Workload transfer approved. Starting to work on 25:[1852443, 1853322].
[Rank 4] Workload transfer approved. Starting to work on 32:[2351415, 2352294].
[Rank 11] Workload transfer approved. Starting to work on 34:[2493978, 2494857].
[Rank 13] Workload transfer approved. Starting to work on 44:[3206795, 3207674].
[Rank 35] Workload transfer approved. Starting to work on 50:[3634485, 3635364].
[Rank 6] Workload transfer approved. Starting to work on 51:[3705766, 3706645].
[Rank 24] Workload transfer approved. Starting to work on 54:[3919611, 3920490].
[Rank 25] Workload transfer approved. Starting to work on 55:[3990893, 3991772].
[Rank 15] Workload transfer approved. Starting to work on 62:[4489865, 4490744].
[Rank 20] Workload transfer approved. Starting to work on 66:[4774991, 4775870].
[Rank 19] Workload transfer approved. Starting to work on 67:[4846273, 4847152].
12019808.70 ms (3 h 20 min 19 s 808.70 ms) taken to detect 51100 conclusions for which there are more general variants proven in lower or equal amounts of steps.
Found 5081180 representative and 51100 redundant condensed detachment proof strings.
[Copy] Removal count: { 37, 51100 }
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 1 on "ncm0258.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 2 on "ncm0259.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 3 on "ncm0260.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 4 on "ncm0261.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 5 on "ncm0262.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 6 on "ncm0263.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 7 on "ncm0265.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 8 on "ncm0267.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 9 on "ncm0268.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 10 on "ncm0270.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 11 on "ncm0271.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 12 on "ncm0272.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 13 on "ncm0273.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 14 on "ncm0274.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 15 on "ncm0275.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 16 on "ncm0276.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 17 on "ncm0277.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 18 on "ncm0278.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 19 on "ncm0279.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 20 on "ncm0280.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 21 on "ncm0281.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 22 on "ncm0284.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 23 on "ncm0285.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 24 on "ncm0286.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 25 on "ncm0585.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 26 on "ncm0586.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 27 on "ncm0587.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 28 on "ncm0588.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 29 on "ncm0591.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 30 on "ncm0592.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 31 on "ncm0593.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 32 on "ncm0594.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 33 on "ncm0595.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 34 on "ncm0598.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 35 on "ncm0599.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 36 on "ncm0600.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 37 on "ncm0601.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 38 on "ncm0602.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 39 on "ncm0605.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 40 on "ncm0606.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 41 on "ncm0607.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 42 on "ncm0608.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 43 on "ncm0609.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 44 on "ncm0610.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 45 on "ncm0611.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 46 on "ncm0612.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 47 on "ncm0613.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 48 on "ncm0614.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 49 on "ncm0615.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 50 on "ncm0616.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 51 on "ncm0803.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 52 on "ncm0806.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 53 on "ncm0807.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 54 on "ncm0808.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 55 on "ncm0811.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 56 on "ncm0812.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 57 on "ncm0813.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 58 on "ncm0816.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 59 on "ncm0817.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 60 on "ncm0818.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 61 on "ncm0819.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 62 on "ncm0820.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 63 on "ncm0822.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 64 on "ncm0823.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 65 on "ncm0825.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 66 on "ncm0826.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 67 on "ncm0827.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 68 on "ncm0829.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 69 on "ncm0830.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 70 on "ncm0831.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:08:21 2023: MPI-based D-proof representative filter complete. [rank 71 on "ncm0832.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
18847.04 ms (18 s 847.04 ms) taken to filter and order new representative proofs.
Sun Oct  8 07:08:40 2023: Starting to write 5081180 entries to data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs37.txt.
27063.87 ms (27 s 63.87 ms) taken to print and save 9046645168 bytes of representative condensed detachment proof strings to data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/dProofs-withConclusions/dProofs37.txt.
Sun Oct  8 07:09:07 2023: MPI-based D-proof representative filter complete. [rank 0 on "ncm0257.hpc.itc.rwth-aachen.de" ; 72 processes ; 48 local hardware thread contexts]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 73621, tid:22920977119104]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 200731, tid:23174724573056]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 141087, tid:23278695380864]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 110363, tid:22746529421184]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 50365, tid:23152355161984]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 144148, tid:23116026656640]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 191466, tid:22752370349952]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 16017, tid:22517335689088]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 153345, tid:22874864760704]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 14579, tid:23207509055360]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 41379, tid:22667835283328]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 4377, tid:23391805265792]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 241793, tid:22584760813440]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 145560, tid:22738870323072]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 242351, tid:22503515588480]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 159768, tid:22726571190144]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 217224, tid:22886804883328]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 213934, tid:23295930787712]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 69648, tid:23316489893760]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 40169, tid:22707366307712]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 112118, tid:22586012252032]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 274947, tid:22679768917888]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 206512, tid:22620788389760]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 80698, tid:22439611471744]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 192292, tid:22993984075648]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 141014, tid:22516286936960]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 140584, tid:22641637353344]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 266373, tid:22587237492608]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 272776, tid:23144273532800]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 95078, tid:23023488616320]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 274913, tid:23445347125120]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 37660, tid:22493060892544]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 29129, tid:23167240877952]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 271886, tid:23276829611904]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 19964, tid:22961693058944]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 191182, tid:22456621848448]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 56141, tid:22518876723072]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 255292, tid:23083132225408]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 7340, tid:23416728905600]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 36137, tid:22865524660096]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 46992, tid:22416714008448]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 48653, tid:22383189854080]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 72040, tid:23418285553536]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 247121, tid:23232258328448]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 12594, tid:23028655658880]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 192416, tid:23377128978304]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 266136, tid:22906699331456]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 264404, tid:23372568577920]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 223989, tid:22607758268288]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 192369, tid:22952097716096]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 194199, tid:23043894237056]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 119702, tid:22706731603840]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 22786, tid:22647756724096]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 64376, tid:22917157205888]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 270289, tid:23139634558848]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 151476, tid:22649087707008]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 216393, tid:23306580535168]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 185497, tid:22390539585408]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 174265, tid:22919258355584]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 76826, tid:23167811704704]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 277895, tid:22411962369920]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 267930, tid:23178940303232]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 53779, tid:22395707942784]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 187245, tid:23252716263296]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 268527, tid:23445407307648]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 266890, tid:23000403081088]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 16690, tid:22587741017984]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 152898, tid:23206841644928]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 224126, tid:22981444573056]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 34892, tid:22974424766336]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 214790, tid:23412578580352]
Sun Oct  8 07:09:19 2023: Process terminated. [pid: 64272, tid:23183020058496]