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: It is not sunny. It is windy. It is sunny if and only if Susan is a server. If David were a taxi driver, then it is not windy. If it is overcast, then David is a taxi driver.
David is not a taxi driver can be inferred via the modus tollens rule. It is not sunny and it is windy can be inferred via the conjunction rule. It is windy and it is not sunny can be inferred via the conjunction rule. If it is sunny, then Susan is a server can be inferred via the biconditional elimination rule. If Susan were a server, then it is sunny can be inferred via the biconditional elimination rule. Susan is not a server can be inferred via the biconditional elimination rule.