A set of vertices S in a graph G is independent if no neighbor of a vertex of S belongs to S. The independence number &alpha is the maximum cardinality of an independent set of G. A series of best possible lower and upper bounds on &alpha and some other common invariants of G are obtained by the system AGX 2, and proved either automatically or by hand. In the present paper, we report on such lower and upper bounds considering, as second invariant, minimum, average and maximum degree, diameter, radius, average distance, spread of eccentricities, chromatic number and matching number.