let check_split
  (config: config)
  (bound: bound)
  (subst: subst)
  (context_unifier_space: context_unifier_space)
  (context_partners: context_partners)
  (is_element_incomplete: bool)
  : raw_context_unifier option =

  let rec min_complexity_at (i: int) (acc: Bound.complexity option) : Bound.complexity option =
    (* all remainder literals exceed the bound? *)
    if i >= Array.length context_partners then begin
      acc
    end

    else
      let input_index =
        context_unifier_space.Context_unifier.cus_input_partners.(i).Context_unifier.ip_index
      in
      let context_partner =
        context_partners.(input_index)
      in
      let remainder =
        not context_partner.Context_unifier.cp_empty_remainder
        ||
        Context_unifier.is_remainder 
          subst
          context_partner.Context_unifier.cp_element
          input_index
      in
        if remainder then begin
          (* a remainder literal, so check its bound complexity *)
          let clause_literal =
            context_unifier_space.Context_unifier.cus_input_partners.(i).Context_unifier.ip_literal
          in
          let complexity =
            bound#get_complexity_subst
              clause_literal
              subst
              Subst.input_literal_offset
          in
            if bound#exceeds complexity then begin
              let new_acc =
                match acc with
                  | Some min_complexity when
                      bound#compare_complexity min_complexity complexity <= 0 ->
                      
                      acc
                    
                  | _ ->
                      Some complexity
              in
                min_complexity_at (i + 1) new_acc
            end

            else begin
              raise Exit
            end
        end

        else
          min_complexity_at (i + 1) acc
  in
    
    (* keep only split candidates within the deepening bound *)
    begin
      try
        match min_complexity_at 0 None with
          | None ->
              (* no remainder literal?!?! *)
              print_endline (Subst.subst_to_string subst);
              print_endline (Context_unifier.context_unifier_to_string
                               context_unifier_space context_partners);
              failwith "Context_unifier_check.check_split.min_complexity_at I"

          | Some complexity ->
              begin
                match Config.restart config with
                  | Flags.RS_Eager
                  | Flags.RS_Lazy ->
                      (* register the minimum complexity for the potential next restart *)
                      if
                        bound#register
                          complexity
                          (Context_unifier.get_creation_choice_point context_partners) 
                      then begin
                        None
                      end
                          
                      else
                        (* min complexity is within the bound?!? *)
                        failwith "Context_unifier_check.check_split.min_complexity_at II"

                  | Flags.RS_Delayed ->
                      (* exceeding bound and delayed restarting *)
                      (* this context element is already incomplete,
                         so all its context unifiers will be recomputed anyway. *)
                      if is_element_incomplete then
                        None

                      (* keep all split candidates *)
                      else
                        let raw_context_unifier =
                          Context_unifier.create_context_unifier
                            context_unifier_space
                            (Array.copy context_partners)
                            true
                        in
                          Some raw_context_unifier
              end
                
      with
        | Exit ->
            (* valid complexity found *)
            let raw_context_unifier =
              Context_unifier.create_context_unifier
                context_unifier_space
                (Array.copy context_partners)
                false
            in
              Some raw_context_unifier
    end