Decidability conjecture for the two-variable, one-unary-predicate fragment of QS5

Let $\mathbf{QS5}$ be the quantified modal logic QS5, and consider its fragment using two individual variables and a single unary predicate letter. Decidability conjecture. The fragment of $\mathbf{QS5}$ in the language with two individual variables and a single unary predicate letter is algorithmically decidable. This is presented as a remaining question in the algorithmic complexity of quantified modal fragments, following the known undecidability results for related fragments with either more individual variables or more unary predicate letters.