What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? W(a_17) <-> s. s or ~W(a_17). forall x_1: ~W(x_1).
W(a_17) -> s. W(a_17) -> s. s -> W(a_17).