What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? ~p_2. p_2 <-> s_1. T_3(b) <-> s_1. forall y: P(y) <-> T_3(y).
p_2 -> s_1. T_3(b) -> s_1. s_1 -> p_2. s_1 -> T_3(b). ~s_1. forall y: P(y) -> T_3(y). forall y: T_3(y) -> P(y).