let get_lemma ~(uip: bool) (state: state) (context: context) context_unifier (clause: clause) (conflict_literals: literal array) regress_stop : clause option =

try
  (* fake data to get the regression with the closing clause started *)
  let closing_info =
    State.create_literal_info Lemma.close_literal State.Propagation
      (State.active_choice_point state) context_unifier
      clause [] conflict_literals (-1) (fun () -> ()) (Some [regress_stop])
  in
  let regression_start = {
    tr_clause_literal = Lemma.close_literal;
    tr_context_literal = Lemma.close_literal;
    (* pseudo-context literal: most recent context element *)
    tr_context_literal_id = Pervasives.max_int;
    tr_regress_info = closing_info;
  }
  in

  let uip =
    if uip then begin
      let uip =
        find_uip state context
          regress_stop
          (To_regress.add regression_start To_regress.empty)
      in
        Some uip
    end

    else
      None
  in


  (* do the regression *)
  let memoized =
    regress
      state context
      uip regress_stop
      (To_regress.add regression_start To_regress.empty)
  in

    let regressed_literals, constraints, ground =
      memoized.mm_regressed, memoized.mm_constraints, memoized.mm_ground
    in

  (* create the conflict set by applying the constraints to the regressed literals *)
  let regressed =
    LiteralTable.fold
      (fun _ literals acc ->
         !literals :: acc
      )
      regressed_literals.regressed_literals
      []
  in
  let unifier =
    Unification.unify_constraints' ~recompute:false constraints
  in
  let regressed =
    Subst.apply_to_literal_groups' unifier regressed
  in


  let simplified =
(*    Term.remove_duplicates (ground @ (Lemma.simplify regressed))*)
    Term.remove_duplicates (Term.remove_variants (ground @ (Lemma.simplify regressed)))
  in

  let normalized =
    Term.sort_clause simplified
  in
    (* needed to avoid learning right splits as real lemmas *)
    match clause, normalized with
      | unit_clause :: [], unit_lemma :: [] when
          Unification.is_literal_instance unit_lemma unit_clause ->
          None
            
      | _ ->
          (* normalize variables. *)
          Some (Subst.apply_to_clause Subst.empty normalized 0)
with
  | LIMIT ->
      None