let rec select_right_split (candidates: candidates) : selected option =
  
  match candidates.cd_right_splits with
    | [] ->
        None
            
    | ((candidate, split_literal, index, context_literals) as right_split) :: tail ->
        (* remove the right split *)
        candidates.cd_right_splits <- tail;
        
        (* drop invalidated right splits *)
        if
          Tools.array_exists
            (fun literal -> Context.element_for_literal candidates.cd_context literal = None)
            context_literals
        then begin
          select_right_split candidates
        end

        (* apply this right split *)
        else begin
          (* ignore if not necessary, i.e. effect already achieved by lemma propagation. *)
          match Context.check_contradictory candidates.cd_context split_literal with
            | Some _ ->
                select_right_split candidates
              
            | None ->

          (* keep the right split for later? *)
          begin
            if Array.length context_literals = 0 then
              (* incomplete branch - arbitrary backtracking,
                 no actual right split learned.
                 apply this right split once for completeness and then forget about it. *)
              ()
                    
            else
              (* move the right split to the applied right splits *)
              candidates.cd_applied_right_splits <-
                (right_split, State.active_choice_point candidates.cd_state) :: candidates.cd_applied_right_splits;
          end;

          (* we always do the right split.
             conceptually, its effect could have already been carried out
             some other assert on a lemma.
             but we enforce doing right splits before lemma propagation.
             the reason is that it is possible to ignore negative assert candidates.
             but then, if lemma propagation is done first,
             the right split could be inconsistent with the context
             when it is finally selected.
             for simplifying the resulting conflict analysis (or avoiding a new special case)
             enforcing eager right splits is the easiest way. *)
          let right_split =
            Term.request_negated_literal (Term.request_skolemized_literal split_literal)
          in
            (*check_right_split_consistent candidates right_split;*)

                  match Context.check_contradictory candidates.cd_context right_split with
              | Some element ->
                  let input_partner =
                    Context_unifier.create_input_partner
                      0
                      right_split
                      [] (* don't care about variables *)
                  in
                  let universal =
                    Term.request_universal_literal right_split
                  in
                  let vars =
                    List.map
                      (fun var ->
                         Subst.make_var var Subst.input_literal_offset
                      )
                      (Term.vars_of_literal universal)
                  in
                  let space =
                    Context_unifier.create_space
                      (Context_unifier_space.get_id candidates.cd_space_registry)
                      (* need to be universal, otherwise learning generalized lemmas
                         will compute parameterized lemmas as well. *)
                      [universal]
                      vars
                      vars
                      vars
                      [| input_partner |]
                      [| |] (* don't care about ordering *)
                      (fun _ -> ()) (* no close candidates computed *)
                      (fun _ -> false) (* no assert candidates computed *)
                      (fun _ -> ()) (* no split candidates computed *)
                      (fun _ -> false) (* not used in recomputation of candidates *)
                      (fun _ -> false) (* not used in recomputation of candidates *)
                      true          (* this is said to be a lemma *)
                  in
                  let context_partner =
                    Context_unifier.create_context_partner
                      element
                      None
                      true
                  in
                  let context_unifier =
                    Context_unifier.create_context_unifier
                      space
                      [| context_partner |]
                      false
                  in
                    raise (Context_unifier.CLOSE context_unifier)
                   
                  

              | None ->            
          let context_unifier =
            Context_unifier.recompute_full_unifier ~recompute:false candidate.ca_raw_context_unifier
          in
            State.apply_split_right
              candidates.cd_state
              right_split
              context_unifier
              candidate.ca_raw_context_unifier.Context_unifier.rcu_space.Context_unifier.cus_clause
              candidate.ca_raw_context_unifier.Context_unifier.rcu_space.Context_unifier.cus_vars
              index
              (Context_unifier.create_space_utility_inc candidate.ca_raw_context_unifier.Context_unifier.rcu_space)
              context_literals;
                      
            Some
              {
                Selection_types.candidate_type = (*Selection_types*)State.SplitRight;
                Selection_types.literal = right_split;
                Selection_types.raw_context_unifier = candidate.ca_raw_context_unifier;
              }
        end