Indeed, existing automated theorem provers do spend a lot of time discarding true statements as "insufficiently interesting". In general, the longer a statement

Indeed, existing automated theorem provers do spend a lot of time discarding true statements as "insufficiently interesting". In general, the longer a statement the less interesting it is. The easier it is to prove with simpler statements, the less interesting it is. And if it's superceded by a more general rule it is less interesting. For example, an automated theorem prover can easily prove many statements of the form "A or not-A or (any long statement)". Those are all uninteresting tautologies that should be discarded. It's interesting to theorize about improving these heuristics with AI methods, there is some work along these lines like ENIGMA-NG.