Satisfiable. Model: s0 = 28 :: SWord16