F5 termination at the F5 rejection degree

Let $d$ denote the current degree in the F5 algorithm, and let $d_{\textrm{FR}}$ be the degree at which all Gröbner-basis-critical (GB-critical) pairs have been rejected by the F5 criteria. F5 termination conjecture. The F5 algorithm can terminate once all GB-critical pairs are rejected by the F5 criteria. That is, it can terminate once $d=d_{\textrm{FR}}$. The conjecture would provide a more precise degree bound for termination than the general bound computed by the F5+ variant. The paper presents it as an open question arising from experimental timings; the broader question of whether F5 terminates correctly on all systems, or even on all regular systems, is also stated to remain open.