Exploiting Algebraic Laws to Improve Mechanized Axiomatizations.