The presentation conjecture for the prop $\mathrm{LagRel}_k^{\circ}$

Let $\mathrm{LagRel}_k^{\circ}$ be the prop generated by the eight morphisms

$$\Delta^{\dagger} \oplus +,\quad !^{\dagger} \oplus 0,\quad \Delta \oplus +^{\dagger},\quad ! \oplus 0^{\dagger},\quad + \oplus \Delta^{\dagger},\quad 0 \oplus !^{\dagger},\quad +^{\dagger} \oplus \Delta,\quad 0^{\dagger} \oplus !.$$

The theorem preceding the conjecture gives two extraspecial commutative Frobenius monoids and two bimonoids formed from these generators. Presentation conjecture. The prop $\mathrm{LagRel}_k^{\circ}$ is presented by generators and equations corresponding to the theorem giving these Frobenius-monoid and bimonoid structures. The conjecture asks whether those relations are complete for $\mathrm{LagRel}_k^{\circ}$; the supplied text gives no resolution.