I think this example fits the question nicely (but it concerns a paper I coauthored, so if there is some feeling that this is shameless self-promotion please say it frankly in the comments and I'll delete the answer).
We were trying to classify all bilinear estimates in $\mathbb{R}^3$ for spaces of wave-Sobolev type. The precise definition of the spaces is pointless here, let's say they are some sort of Sobolev spaces with weights measuring the amount of mass close to the light cone in Fourier variables; they are characterized by two indices $H^{s,b}$ and are an essential tool in the theory of nonlinear waves. A bilinear estimate is a product estimate of the form $$H^{s_1,b_1}\cdot H^{s_2,b_2}\subset H^{s_3,b_3}$$ and one is interested in finding all the 6-tuples $(s_1,s_2,s_3,b_1,b_2,b_3)$ for which the estimate is true. There is a long list of counterexamples (21 plus symmetries; some of the trickiest ones were found by Terry Tao when he was young :) which bound a polyhedron with a large number of faces in the space of 6-tuples $\mathbb{R}^6$. Now the problem is: if a 6-tuple is inside the polyhedron, is the corresponding bilinear estimate true? in other words, is the list of counterexamples exhaustive?
In order to solve the problem we had to compute the vertices of the conjectured polyhedron (and then prove the estimates at the vertices, or near the vertices). Usually, one manages to do this kind of computation by hand with some neat tricks. But in this case, just writing the complete set of inequalities by hand takes a good 20 minutes. We had to admit, reluctantly, that this was physically impossible to do with pencil and paper. Of course this is a trivial problem for a computer and a simple algorithm gave us the answer.
