Consider the following premises. s -> t_1. ~t_1. forall x_18: P_18(x_18). Can we infer ~s and P_18(a_18) from them?
 From forall x_18: P_18(x_18) we can infer P_18(a_18). From s -> t_1, ~t_1 we can infer ~s. Finally, from ~s, P_18(a_18) we can infer ~s and P_18(a_18). Therefore, the answer is yes.