let add_lemma (selection: selection) (lemma: clause) : unit =
  if filter_lemma selection lemma then begin
    if Config.print_lemmas selection.sel_config then begin
      print_endline ("REDUNDANT LEMMA: " ^ Term.clause_to_string lemma);
      (*    print_endline (" ^ String.concat " (List.map Term.literal_to_string lemma));*)
    end;
  end

  else begin
    match Config.lemma selection.sel_config with
      | Flags.LM_Propositional ->
          if Config.print_lemmas selection.sel_config then begin
            print_endline ("LEMMA: " ^ Term.clause_to_string lemma);
          end;
          let global_lemma =
            not selection.sel_bound#is_derivation_incomplete
          in
            Lemma_propositional.add_lemma selection.sel_lemmas_propositional lemma global_lemma
              
      | Flags.LM_None
      | Flags.LM_Grounded
      | Flags.LM_Lifted ->
          if Config.print_lemmas selection.sel_config then begin
            print_endline ("LEMMA: " ^ Term.clause_to_string lemma);
            (*    print_endline (" ^ string_of_int (List.length lemma));*)
            (*    print_endline (" ^ String.concat " (List.map Term.literal_to_string lemma));*)
          end;
          
          prune_lemmas selection;
          
          (* create clause *)
          let new_context_unifier_space =
            Context_unifier_space.create_space
              selection.sel_space_registry
              selection.sel_problem_literals
              lemma
              selection.sel_process_close
              selection.sel_process_assert
              selection.sel_process_split
              selection.sel_is_element_incomplete_assert
              selection.sel_is_element_incomplete_split
              true
          in      
            (* initially give the new lemma the worst existing utility value instead of 0,
               that might be too unfair. *)
            new_context_unifier_space.Context_unifier.cus_utility := (get_min_lemma_utility selection);
            
            let global_lemma =
              not selection.sel_bound#is_derivation_incomplete
            in
              selection.sel_lemma_spaces <- (new_context_unifier_space, global_lemma) :: selection.sel_lemma_spaces;
              
              (* is this a unit lemma? *)
              begin
                match lemma with
                  | unit_literal :: [] ->
                      (* check if contradictory - if so, close *)
                      begin
                        match Context.check_contradictory selection.sel_context unit_literal with
                          | Some element ->
                              (* close *)
                              let context_partner =
                                Context_unifier.create_context_partner
                                  element
                                  None
                                  true
                              in
                              let raw_context_unifier =
                                Context_unifier.create_context_unifier
                                  new_context_unifier_space [| context_partner |] false
                              in
                                selection.sel_best_closing := Some raw_context_unifier;
                                raise_close selection
                                  
                                  
                          | None ->
                              (* unit assert *)
                              let raw_context_unifier =
                                Context_unifier.create_context_unifier
                                  new_context_unifier_space [| Context_unifier.assert_partner |] false
                              in
                                Statistic.inc_computed_assert_candidates selection.sel_statistic;
                                selection.sel_unit_asserts <- (unit_literal, raw_context_unifier) :: selection.sel_unit_asserts
                      end
                      
                  | _ ->
                      ()
              end;
      
  end