let add (problem_literals: problem_literals)
    (context_element: Context.element) (candidate_type: Context_unifier.candidate_type) : unit =

  match candidate_type with
    | Context_unifier.Assert
    | Context_unifier.Split ->
        failwith "Problem_literals.add"

    | Context_unifier.Close
    | Context_unifier.CloseAssert
    | Context_unifier.All ->
        (* subsume all clauses with the new context literal *)
        subsume problem_literals context_element;
        
        (* unify, i.e. find candidates for partial context unifiers *)
        let unifying_candidates =
          let index =
            problem_literals.index#find (Term.request_negated_literal ~insert_db:false context_element.Context.el_literal)
          in
            index#find_all_unifiable_subst ~p_preserving:false context_element.Context.el_literal.Term.atom
        in
          (* try each problem_literal.
             close_found shows that a closing context unifier has been found. *)
          ignore (
            List.fold_left
              (fun close_found (problem_literal, subst) ->
                 add_to_problem_literal
                   problem_literals
                   problem_literal
                   context_element
                   candidate_type
                   close_found
                   subst
              )
              false
              unifying_candidates
              : bool)