What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? q -> T(f_1). r_1 -> q. forall x: T_1(x) <-> T(x).
r_1 -> T(f_1). forall x: T_1(x) -> T(x). forall x: T(x) -> T_1(x).