Consider the following premises. q_1 -> p_8. p_8 -> q_1. ~S_4(a_17). p_8 -> P_4(a_17). forall x: P_4(x) -> S_4(x). Can we infer q_1 from them?
 From forall x: P_4(x) -> S_4(x) we can infer P_4(a_17) -> S_4(a_17). From p_8 -> P_4(a_17), P_4(a_17) -> S_4(a_17) we can infer p_8 -> S_4(a_17). From p_8 -> S_4(a_17), ~S_4(a_17) we can infer ~p_8. From p_8 -> q_1, q_1 -> p_8 we can infer p_8 <-> q_1. Finally, from p_8 <-> q_1, ~p_8 we can infer ~q_1, which contradicts q_1. Therefore, the answer is no.