Consider the following premises. p or ~S_22(a_22). forall x_22: R_22(x_22) -> S_22(x_22). w -> S_22(a_22). w or R_22(a_22). q_1 -> p. Can we infer ~p from them?
 From forall x_22: R_22(x_22) -> S_22(x_22) we can infer R_22(a_22) -> S_22(a_22). From w -> S_22(a_22), R_22(a_22) -> S_22(a_22), w or R_22(a_22) we can infer S_22(a_22). From p or ~S_22(a_22) we can infer S_22(a_22) -> p. From S_22(a_22) we can infer S_22(a_22) or q_1. Finally, from S_22(a_22) -> p, q_1 -> p, S_22(a_22) or q_1 we can infer p, which contradicts ~p. Therefore, the answer is no.