Hemaspaandra~et~al.~[JCSS 2010] conjectured that satisfiability for multi-modal logic restricted to the connectives XOR and 1, over frame classes T, S4, and S5, is solvable in polynomial time. We refute this for S5 frames, by proving NP-hardness.

翻译：Hemaspaandra等人[JCSS 2010]曾猜想，在框架类T、S4和S5上，将多模态逻辑的联结词限制为XOR和1时，其可满足性问题可在多项式时间内求解。我们通过证明其在S5框架上的NP难性，推翻了这一猜想。