tuned proofs (manually or with sledgehammer): avoid "smt" due to spurious failures under heavy load;