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 not working. For all x_12, if x_12 drives a car, then x_12 is working. David is running. For all x_12, if x_12 works, then x_12 is driving a car.
Charles is not working and David is running can be inferred via the conjunction rule. David is running and Charles is not working can be inferred via the conjunction rule. For all x_12, x_12 will drive a car if and only if x_12 will work can be inferred via the universal biconditional introduction rule. For all x_12, x_12 will work if and only if x_12 will drive a car can be inferred via the universal biconditional introduction rule.