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