 The algorithm SQEMA outputs the following first-order condition for \(\osim (A \wedge B) \vdash (\osim A \vee \osim B)\) in terms of \(C\) alone: \(\forall x \forall y \forall z ((xCy \amp xCz) \Rightarrow ((y =z)\amp xCy))\), which is equivalent to:  \[ \forall x \forall y \forall z ((xCy \amp xCz) \Rightarrow (y =z)),\]  implying that \(C\) is a function if \(C\) is serial. For functional frames, negation as impossibility and negation as unnecessity coincide.