Automation of aggregate theories: The cornerstones of equational expressibility.