Consider the following premises. s -> s_3. s_3 -> s. p_4 <-> s_3. Can we infer ~(s -> p_4) from them?
 From s_3 -> s, s -> s_3 we can infer s_3 <-> s. From s_3 <-> s we can infer s -> s_3. From p_4 <-> s_3 we can infer s_3 -> p_4. Finally, from s -> s_3, s_3 -> p_4 we can infer s -> p_4, which contradicts ~(s -> p_4). Therefore, the answer is no.