Consider the following premises. s_3 and q_17. forall x_30: P_30(x_30). ~s_3. Can we infer q_10 and P_30(a_30) from them? If possible, name the inference rules being used at each step.
 From forall x_30: P_30(x_30) we can infer P_30(a_30) via universal instantiation. From s_3 and q_17 we can infer s_3 via simplification. From s_3 we can infer s_3 or q_10 via addition. From s_3 or q_10, ~s_3 we can infer q_10 via disjunctive syllogism. Finally, from q_10, P_30(a_30) we can infer q_10 and P_30(a_30) via conjunction. Therefore, the answer is yes. Notice, however, that the premises were contradictory, so we can infer anything from them.