The classification conjecture for multiplicatively idempotent congruence-simple semirings

Let $S$ be a multiplicatively idempotent congruence-simple semiring. The semiring $S$ is finite and isomorphic to one of the semirings $\mathbb{S}_1$, $\dots$, $\mathbb{S}_8$.

Classification conjecture. Every multiplicatively idempotent congruence-simple semiring is finite and isomorphic to one of the semirings $\mathbb{S}_1$, $\dots$, $\mathbb{S}_8$.

Theorem 3.3 establishes this classification for finite semirings; the conjecture asks whether finiteness holds without assuming it.