Consider the following premises. s or ~w. w <-> u_1. ~u_1. w or ~s. Can we infer s from them?
 From w <-> u_1, ~u_1 we can infer ~w. From s or ~w we can infer w -> s. From w or ~s we can infer s -> w. From s -> w, w -> s we can infer s <-> w. Finally, from s <-> w, ~w we can infer ~s, which contradicts s. Therefore, the answer is no.