G. Ebner, S. Hetzl, A. Leitsch, G. Reis, D. Weller: "On the Generation of Quantified Lemmas"; Journal of Automated Reasoning, 63 (2019), 1; 95 - 126.
https://publik.tuwien.ac.at/files/publik_287144.pdf