What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? p. ~q_13. r -> s_4. s_4 <-> q_13.
p and ~q_13. ~q_13 and p. s_4 -> q_13. q_13 -> s_4. ~s_4.