Consider the following premises. ~q_17. forall x_16: Q(x_16) <-> S_16(x_16). Q(d) -> p. p -> q_17. Can we infer S_16(d) from them?
 From p -> q_17, ~q_17 we can infer ~p. From forall x_16: Q(x_16) <-> S_16(x_16) we can infer Q(d) <-> S_16(d). From Q(d) -> p, ~p we can infer ~Q(d). Finally, from Q(d) <-> S_16(d), ~Q(d) we can infer ~S_16(d), which contradicts S_16(d). Therefore, the answer is no.