I do wonder if throwing a similar amount of computational power behind old school rule based algorithms like the ones in Mathematica's FullSimplify would have yielded similar results.