Completeness conjecture for the simplicial model axiom system of $KB4_n$

Let $A$ be the set of agents, and let $\KBfour+\mathbf{NE}+(\mathbf{SA_a})_{a \in A}$ be the axiom system consisting of the $KB4_n$ axioms together with the non-emptiness axiom $\mathbf{NE}$ and the single-agent axiom schemes $\mathbf{SA_a}$. The system is interpreted over the class of simplicial models. Completeness conjecture.

$$\KBfour+\mathbf{NE}+(\mathbf{SA_a})_{a \in A}$$

is complete with respect to the class of simplicial models. The paper gives a soundness proof and says that the completeness proof is more involved and is left for future work.