Consider the following premises. forall x_17: ~Q_17(x_17). forall x_17: P_17(x_17) or Q_11(x_17). Q_11(a_9) -> p. forall x_17: P_17(x_17) <-> Q_17(x_17). Can we infer ~p from them?
 From forall x_17: P_17(x_17) <-> Q_17(x_17), forall x_17: ~Q_17(x_17) we can infer forall x_17: ~P_17(x_17). From forall x_17: P_17(x_17) or Q_11(x_17), forall x_17: ~P_17(x_17) we can infer forall x_17: Q_11(x_17). From forall x_17: Q_11(x_17) we can infer Q_11(a_9). Finally, from Q_11(a_9) -> p, Q_11(a_9) we can infer p, which contradicts ~p. Therefore, the answer is no.