Consider the following premises. s -> s_3. ~u. s_3 <-> u. s_3 -> s. q. Can we infer ~q from them? If possible, name the inference rules being used at each step.
That contradicts the premises. Therefore the answer is no.