A set of vertices S in a graph G is independent if no neighbor of a vertex of S belongs to S. A set of vertices U in a graph G is irredundant if each vertex v of U has a private neighbor, which may be v itself, i.e., a neighbor of v which is not a neighbor of any other vertex of U. The independence number α (resp. upper irredundance number IR) is the maximum number of vertices of an independent (resp. irredundant) set of G. In previous work, a series of best possible lower and upper bounds on α and some other usual invariants of G were obtained by the system AGX 2, and proved either automatically or by hand. These results are strengthened in the present paper by systematically replacing α by IR. The resulting conjectures were tested by AGX which could find no counter-example to an upper bound nor any case where a lower bound could not be shown to remain tight. Some proofs for the bounds on α carry over. In all other cases, new proofs are provided.