Consider the following premises. q_11 or ~t. ~u or s_1. u or t. s_1 <-> q_11. Can we infer ~q_11 from them? If possible, name the inference rules being used at each step.
 From s_1 <-> q_11 we can infer s_1 -> q_11 via biconditional elimination. From q_11 or ~t we can infer t -> q_11 via rewriting. From u or t, ~u or s_1 we can infer t or s_1 via resolution. Finally, from t -> q_11, s_1 -> q_11, t or s_1 we can infer q_11 via disjunction elimination, which contradicts ~q_11. Therefore, the answer is no.