proposition: Lemma augment_with_clause_not_OutOfFuel : forall (a : (list literal)) (st : state), ~ is_fail (augment_with_clause a st).
proof: Proof. unfold augment_with_clause. intros. destruct_in_goal FR. apply insert_normalised_clause_not_OutOfFuel. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause