let compare_context_unifiers ~(different: bool) (first: raw_context_unifier) (second: raw_context_unifier) : int =

  (* as first and second are context unifiers of the same clause
     they must have the same number of context partners *)
  let rec cmp_context_partners (index: int) =
    if index >= Array.length first.rcu_context_partners then begin
      (* there can only be one valid candidate with at a position in the ordering *)
      if
        different
        &&
        not (is_raw_context_unifier_invalid first)
        &&
        not (is_raw_context_unifier_invalid second)
      then begin
        print_endline (raw_context_unifier_to_string first);
        print_endline (raw_context_unifier_to_string second);
        failwith "Context_unifier.compare_context_unifiers";
      end

      else begin
        (* at least one of the candidates is invalid *)
        0
      end

    end
    else
      let cmp =
        compare
          first.rcu_context_partners.(index).cp_element.Context.el_id
          second.rcu_context_partners.(index).cp_element.Context.el_id
      in
        if cmp <> 0 then
          cmp
        else
          cmp_context_partners (index + 1)
  in

    if first == second then
      0
    else
      let cmp_creation_point =
        Tools.compare_int
          (creating_context_element first).Context.el_id
          (creating_context_element second).Context.el_id
      in
        if cmp_creation_point <> 0 then
          cmp_creation_point
        else
          let cmp_clause =
            compare first.rcu_space.cus_id second.rcu_space.cus_id
          in
            if cmp_clause <> 0 then
              cmp_clause
            else if
              Const.debug
              &&
                (Array.length first.rcu_context_partners != Array.length second.rcu_context_partners)
            then
              failwith "Context_unifier.cmp_context_partners 1"
            else
              cmp_context_partners 0