Lemma generation for horn clause satisfiability: A preliminary study