Consider the following premises. ~U_1(e_1). forall x_7: U_1(x_7) <-> S_7(x_7). S_7(e_1) or q. Can we infer q from them? If possible, name the inference rules being used at each step.
 From forall x_7: U_1(x_7) <-> S_7(x_7) we can infer U_1(e_1) <-> S_7(e_1) via universal instantiation. From U_1(e_1) <-> S_7(e_1), ~U_1(e_1) we can infer ~S_7(e_1) via biconditional elimination. Finally, from S_7(e_1) or q, ~S_7(e_1) we can infer q via disjunctive syllogism. Therefore, the answer is yes.