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. If Charles goes running, then Elisabeth is a sailor. If Elisabeth were a sailor, then Charles is running. Elisabeth is not a sailor. If it is cold, then it is sunny.
Charles is not running can be inferred via the modus tollens rule. It is not cold can be inferred via the modus tollens rule. It is not sunny and Elisabeth is not a sailor can be inferred via the conjunction rule. Elisabeth is not a sailor and it is not sunny can be inferred via the conjunction rule. Charles is running if and only if Elisabeth is a sailor can be inferred via the biconditional introduction rule. Elisabeth is a sailor if and only if Charles is running can be inferred via the biconditional introduction rule.