let context_unifier_to_string
  (context_unifier_space: context_unifier_space) (context_partners: context_partners)
  : string =
  let context_literals =
    Array.to_list (
      Array.map
        (fun context_partner ->
(*           string_of_int context_partner.cp_element.Context.el_id
           ^ "
           ^*) Term.literal_to_string context_partner.cp_element.Context.el_literal
        )
        context_partners
    )
  in
  (
    if context_unifier_space.cus_lemma then
      "Lemma : "
    else
      "Clause : "
  )
  (*^ string_of_int context_unifier_space.cus_id ^ "*)
    ^ Term.clause_to_string (get_input_clause context_unifier_space)
    ^ "\n"
    ^ "Context: "
    ^ "["
    ^ String.concat ", " context_literals ^ "]"
(*  ^ Term.clause_to_string
    (
      Array.to_list (get_context_literals context_partners)) *)
    
  ^ "\n"