  We present a new proof of Stembridge's theorem about the enumeration of
totally symmetric plane partitions using the methodology suggested in the
recent Koutschan-Kauers-Zeilberger semi-rigorous proof of the Andrews-Robbins
q-TSPP conjecture. Our proof makes heavy use of computer algebra and is
completely automatic. We describe new methods that make the computations
feasible in the first place. The tantalizing aspect of this work is that the
same methods can be applied to prove the q-TSPP conjecture (that is a
q-analogue of Stembridge's theorem and open for more than 25 years); the only
hurdle here is still the computational complexity.
