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