Introduction of history and prophecy variables can allow a proof to be expressed in a weaker logic or a more localized form. This fact has been used, for example, to allow purely propositional, quantifier-free, invariant generators to produce proofs for parameterized systems requiring universal quantification in the inductive invariant. However, automatic synthesis of history and prophecy remains an open problem. We introduce counterexample-guided heuristics for this purpose based on property-driven refutation of counterexamples and Craig interpolation. The approach is evaluated on a set of benchmarks based on array manipulating programs with multiple loops.