Consider the following premises. p_11 or Q(j_4). ~p_11 or r_11. forall z: ~Q(z). p -> ~r_11. Can we infer ~p from them?
 From forall z: ~Q(z) we can infer ~Q(j_4). From p_11 or Q(j_4), ~p_11 or r_11 we can infer Q(j_4) or r_11. From Q(j_4) or r_11, ~Q(j_4) we can infer r_11. Finally, from p -> ~r_11, r_11 we can infer ~p. Therefore, the answer is yes.