let backtrack (state: state) (context: context) (config: config) (closing_context_unifier: raw_context_unifier) (*(domain_constants: Term.term list)*) :
    choice_point * literal list(*explanation*) * clause option
    =
  let clause =
    closing_context_unifier.Context_unifier.rcu_space.Context_unifier.cus_clause
  in
  let context_literals =
    Context_unifier.get_context_literals
      closing_context_unifier.Context_unifier.rcu_context_partners
  in

  let regression_explanation =
    State.get_explanation state context_literals
  in

  let literal_explanation =
    List.map
      State.left_split_literal
      regression_explanation
  in

    if Const.debug then begin
      let explanation =
        regression_explanation
      in
      let explanation' =
        State.get_explanation state (Array.of_list literal_explanation)
      in
        
        if not (Tools.lists_equal State.choice_point_equal explanation explanation') then begin
          print_endline (State.explanation_to_string explanation);
          print_endline (State.explanation_to_string explanation');
          failwith ("Not closing explanation 1!")
        end;
        
    end;

    let closing_explanation  =
      match Config.backtracking config with
        | Flags.BT_Naive ->
            State.get_branch state
              
        | Flags.BT_Backjumping ->
            regression_explanation
    in



    (* scoring must be done before the used dependency information is backtracked *)
    score state closing_context_unifier;

  let retract, _retract_next, _right_explanation =
    match closing_explanation with
      | [] ->
          raise UNSATISFIABLE
          
      | root :: [] ->
          if
            State.choice_point_equal (State. root_choice_point state) root
            ||
            State.choice_point_equal State.valid_choice_point root
          then
            raise UNSATISFIABLE
          else
            root, (State.root_choice_point state), []

      | retract :: retract_next :: tail ->
          retract, retract_next, (retract_next :: tail)
  in

    if false && Const.debug && not (List.memq (State.left_split_literal retract) literal_explanation) then begin
      print_endline (Term.literal_to_string (State.left_split_literal retract));
      print_endline (Term.clause_to_string literal_explanation);
      failwith ("Not closing explanation 2!")
    end;

  let backjump =
    (* how much do we actually want to backtrack?
       we could go right to the backjump target, like SAT solvers do.
       but in our case that mostly leads to the recomputation
       of most of the jumped over derivation, and thus a performance loss.
       therefore, just retract the most recent responsible left split. *)
    retract;
    (*
    let rec find_backjump branch =
      match branch with
       | [] ->
           failwith "
             
       | _ :: [] ->
           failwith "
             
       | x :: y :: tail ->
           if State.choice_point_equal y retract_next then
             x
           else
             find_backjump (y :: tail)
    in
      find_backjump (State.get_branch state)
    *)
  in


  (* lemma must be computed before the used dependency information is backtracked *)
  let lemma =
    match Config.lemma config with
      | Flags.LM_None ->
          None

      | Flags.LM_Grounded ->
          Lemma_grounded.get_lemma ~uip:(Config.lemma_uip config) state context
            (Context_unifier.recompute_full_unifier ~recompute:false closing_context_unifier)
            clause context_literals retract

      | Flags.LM_Lifted ->
          Lemma_lifted.get_lemma ~uip:(Config.lemma_uip config) state context
          (Context_unifier.recompute_full_unifier ~recompute:false closing_context_unifier)
          clause context_literals retract

      | Flags.LM_Propositional ->
            Some (
              List.map
                (fun literal ->
                   Term.request_negated_literal literal
                )
              literal_explanation
            )
  in


    invalidate state backjump;

    (* remove invalidated context literals. *)
    State.backtrack_literal_info state;

    (*retract, right_explanation, lemma*)
    retract, literal_explanation, lemma