On the other hand, symbolic reasoning easily gets superhuman results in narrow domains. The Robbins Conjecture was proved on hardware like that after 60 years. You could check out this theorem prover benchmark suite that has been maintained for over 30 years https://www.tptp.org/