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: forall x_1: R(x_1). R(h_4) -> u. R(h_4) or ~u.
u -> R(h_4) can be inferred via the rewriting rule.