let backtrack (context_unifier_space: context_unifier_space) : unit =

  (* try insertion sort *)
  let input_partners =
    context_unifier_space.Context_unifier.cus_input_partners
  in
  let ordering =
    context_unifier_space.Context_unifier.cus_input_partners_ordering
  in
    (* try to insert all input_partners with insertion sort *)
    for i = 1 to Array.length input_partners - 1 do

      let input_partner_to_move =
        input_partners.(ordering.(i))
      in
        match input_partner_to_move.Context_unifier.ip_resolved with
          | Some _ ->
              (* just ignore this resolved literal *)
              ()
                
          | None ->
              let rec insert_at j =
                if j = i then
                  (* biggest entry up to now, just keep in place *)
                  ()
                
                
                (* ignore other resolved literals *)
                else if
                  match input_partners.(ordering.(j)).Context_unifier.ip_resolved with
                    | Some _ -> true
                    | None -> false
                then
                  insert_at (j + 1)


                (* insert after queues with at least same length.
                   this way reordering / swapping of equal length queues is hopefully minimized. *)
                else if
                  (Stack.size input_partner_to_move.Context_unifier.ip_context_partners(*_length*))
                  >=
                  (Stack.size input_partners.(ordering.(j)).Context_unifier.ip_context_partners(*_length*))
                then
                  insert_at (j + 1)

                (* bigger than all other up to now, insert here and shift the others *)
                else begin
                  let swap = ordering.(i)
                  in
                    for k = i downto j + 1 do
                      ordering.(k) <- ordering.(k - 1);
                    done;
                    
                    ordering.(j) <- swap;
                end
              in
                insert_at 0
    done;

    (* check that the order is preserved *)
    if Const.debug then begin
      for i = 1 to Array.length input_partners - 1 do
        if 
          (
            (Stack.size input_partners.(ordering.(i)).Context_unifier.ip_context_partners(*_length*))
            >=
            (Stack.size input_partners.(ordering.(i - 1)).Context_unifier.ip_context_partners(*_length*))
          )
          ||
            (match input_partners.(ordering.(i)).Context_unifier.ip_resolved with
               | Some _ -> true
               | None -> false
            )
          ||
            (match input_partners.(ordering.(i - 1)).Context_unifier.ip_resolved with
               | Some _ -> true
               | None -> false
            )
            
        then
          ()
            
        else begin
          for i = 0 to Array.length input_partners - 1 do
            print_int
              (Stack.size input_partners.(ordering.(i)).Context_unifier.ip_context_partners(*_length*));
            print_newline ();
          done;
          failwith "Context_unifier_space.backtrack: order not preserved"
        end
      done
    end