Consider the following premises. W_3(j_3) or q. R(j_3) -> q_3. forall z: R(z) <-> W_3(z). q -> q_3. Can we infer ~q_3 from them? If possible, name the inference rules being used at each step.
 From forall z: R(z) <-> W_3(z) we can infer forall z: W_3(z) -> R(z) via universal biconditional elimination. From forall z: W_3(z) -> R(z) we can infer W_3(j_3) -> R(j_3) via universal instantiation. From W_3(j_3) -> R(j_3), R(j_3) -> q_3 we can infer W_3(j_3) -> q_3 via transitivity. Finally, from W_3(j_3) -> q_3, q -> q_3, W_3(j_3) or q we can infer q_3 via disjunction elimination, which contradicts ~q_3. Therefore, the answer is no.