It seems a practical system would do all of the above: - attempt a proof, could pass or fail, but if it times out, then fall back to... - property-based test

It seems a practical system would do all of the above: - attempt a proof, could pass or fail, but if it times out, then fall back to... - property-based test case generation, using logical statements and data generators, shrinking, etc.; many will pass, some will fail, but if some time out ... - generate simple tests, and edge cases, which may trivially pass, but could be edited by hand to become more useful If you add a timeout, then exponential runtimes, and even the Halting Problem, always give an answer, even if the answer is to try something simpler.