Consider the following premises. forall y: R(y) or P(y). forall y: ~R(y) or S_4(y). P(b_1) -> q_3. S_4(b_1) <-> q_3. Can we infer ~q_3 from them?
 From forall y: R(y) or P(y), forall y: ~R(y) or S_4(y) we can infer forall y: P(y) or S_4(y). From forall y: P(y) or S_4(y) we can infer P(b_1) or S_4(b_1). From S_4(b_1) <-> q_3 we can infer S_4(b_1) -> q_3. Finally, from P(b_1) -> q_3, S_4(b_1) -> q_3, P(b_1) or S_4(b_1) we can infer q_3, which contradicts ~q_3. Therefore, the answer is no.