Consider the following premises. R(f) -> u_1. forall x: R_1(x) -> R(x). R(f). u_1 -> R_1(f). Can we infer ~u_1 from them? If possible, name the inference rules being used at each step.
 From forall x: R_1(x) -> R(x) we can infer R_1(f) -> R(f) via universal instantiation. From u_1 -> R_1(f), R_1(f) -> R(f) we can infer u_1 -> R(f) via transitivity. From R(f) -> u_1, u_1 -> R(f) we can infer R(f) <-> u_1 via biconditional introduction. From R(f) <-> u_1 we can infer R(f) -> u_1 via biconditional elimination. Finally, from R(f) -> u_1, R(f) we can infer u_1 via modus ponens, which contradicts ~u_1. Therefore, the answer is no.