let backtrack (problem_literals: problem_literals) : unit =
  (* backtrack bindings database *)
  let unneeded_bindings =
    Bindings.fold
      (fun _ (binding, choice_point) acc ->
         if State.is_choice_point_invalid choice_point then
           binding :: acc

         else
           acc
      )
      problem_literals.bindings
      []
  in
    List.iter
      (Bindings.remove problem_literals.bindings)
      unneeded_bindings;
  

  (* the id of the most recently added context literal *)
  let context_id =
    try
      (Context.most_recent_element problem_literals.context).Context.el_id
    with
      | Not_found ->
          (* empty context, use -1 for validity comparisions below. *)
          -1
  in
    (* backtrack clause subsumption *)
    for i = 0 to Array.length problem_literals.subsumed_clauses - 1 do
      if 
        problem_literals.subsumed_clauses.(i) >= 0
        &&
        problem_literals.subsumed_clauses.(i) > context_id
      then
        problem_literals.subsumed_clauses.(i) <- -1;
    done;


    (* backtrack each problem literal *)
    problem_literals.index#iter
      (fun _ index ->
         index#iter
           (fun _ problem_literal ->
         
             (* backtrack problem literal subsumption *)
             if
               problem_literal.subsumed_at >= 0
               &&
               problem_literal.subsumed_at > context_id
             then begin
               problem_literal.subsumed_at <- -1;
             end;

         
             (* backtrack each input partner *)
             Elements.iter
               (fun _ element ->
                 (* update resolve state *)
                 begin
                   match element.input_partner.Context_unifier.ip_resolved with
                     | Some context_partner when
                           State.is_choice_point_invalid
                             context_partner.Context_unifier.cp_element.Context.el_choice_point ->
                         Context_unifier.set_resolved element.input_partner None
                           
                     | _ ->
                         ()
                 end;

                 let rec remove_invalid_context_partner () =
                   if Stack.size element.input_partner.Context_unifier.ip_context_partners = 0 then
                     ()

                   else begin
                     let context_partner =
                       Stack.top element.input_partner.Context_unifier.ip_context_partners
                     in
                       if State.is_choice_point_invalid
                         context_partner.Context_unifier.cp_element.Context.el_choice_point
                       then begin
                         Stack.remove_top element.input_partner.Context_unifier.ip_context_partners;
                               
                         begin
                           match context_partner.Context_unifier.cp_partial_context_unifier with
                             | Some subst when
                                   Subst.is_empty subst ->
                                 (* decrease counter for non-empty substs *)
                                 problem_literals.cached_partial_context_unifiers <-
                                   problem_literals.cached_partial_context_unifiers - 1;
                                     
                             | _ ->
                                 ()
                                   
                         end;
                           
                         remove_invalid_context_partner ()
                       end

                       else
                         ()
                     end
                 in
                   remove_invalid_context_partner ();
               )
               problem_literal.elements;
           )
      )