Consider the following premises. P_6(j_3) or s_3. forall x_6: ~Q_6(x_6). forall x_6: P_6(x_6) -> Q_6(x_6). Can we infer ~s_3 from them? If possible, name the inference rules being used at each step.
 From forall x_6: P_6(x_6) -> Q_6(x_6), forall x_6: ~Q_6(x_6) we can infer forall x_6: ~P_6(x_6) via universal modus tollens. From forall x_6: ~P_6(x_6) we can infer ~P_6(j_3) via universal instantiation. Finally, from P_6(j_3) or s_3, ~P_6(j_3) we can infer s_3 via disjunctive syllogism, which contradicts ~s_3. Therefore, the answer is no.