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

Let $\mathbf{QS5}$ be the quantified modal logic QS5, and consider its fragment using two individual variables and two unary predicate letters. Undecidability conjecture. The fragment of $\mathbf{QS5}$ in the language with two individual variables and two unary predicate letters is algorithmically undecidable. This would settle one of the remaining decidability questions for small-variable, small-signature fragments of quantified modal logics; the paper notes that the corresponding fragment with three individual variables and one unary predicate letter, and with two individual variables and three unary predicate letters, is already undecidable.