Consider the following premises. ~r. forall z: R(z). p_17 <-> r. Can we infer ~p_17 and R(f_3) from them?
 From p_17 <-> r, ~r we can infer ~p_17. From forall z: R(z) we can infer R(f_3). Finally, from ~p_17, R(f_3) we can infer ~p_17 and R(f_3). Therefore, the answer is yes.