Consider the following premises. ~s_1. s_1 -> q_10. q_10 -> s_1. Can we infer ~q_10 or q from them? If possible, name the inference rules being used at each step.
 From s_1 -> q_10, q_10 -> s_1 we can infer s_1 <-> q_10 via biconditional introduction. From s_1 <-> q_10, ~s_1 we can infer ~q_10 via biconditional elimination. Finally, from ~q_10 we can infer ~q_10 or q via addition. Therefore, the answer is yes.