What can be inferred from the following premises in a single inference step (ignoring inferences that add new predicates or constants)? Name the inference rule being used: Charles is running if and only if Michael is making tea. For all x_13, x_13 will go running or x_13 will read a book. If Michael makes tea, then it is late. It is not late.
Michael is not making tea can be inferred via the modus tollens rule. If Charles goes running, then Michael is making tea can be inferred via the biconditional elimination rule. If Michael makes tea, then Charles is running can be inferred via the biconditional elimination rule.