let compute_for_element (problem_literals: problem_literals) (context_element: Context.element)
    (candidate_type: Context_unifier.candidate_type) : unit =
  (* find all potentially unifying problem literals *)
  let unifying_candidates =
    let index =
      problem_literals.index#find (Term.request_negated_literal ~insert_db:false context_element.Context.el_literal)
    in
      index#find_all_unifiable ~p_preserving:false context_element.Context.el_literal.Term.atom
  in

  (* for each problem literal, i.e. input clause literal ... *)
    List.iter
      (fun problem_literal ->
       (* ignore the clause literal if it is subsumed wrt. to this context literal *)
       if is_problem_literal_subsumed_at ~directly:false
         problem_literals problem_literal context_element then
           ()
       else
         (* ... and for each input literal, i.e. problem literal variant *)
         Elements.iter
           (fun _ element ->
              (* ignore the clause literal if it is resolved wrt. to this context literal *)
              if is_input_partner_resolved_at element.input_partner context_element then
                ()

              else begin
                try
                  (* is there a pair between the context element and this problem literal? *)
                  let context_partner =
                    Stack.find
                      element.input_partner.Context_unifier.ip_context_partners
                      (fun x ->
                         compare
                           context_element.Context.el_id
                           x.Context_unifier.cp_element.Context.el_id
                      )
                  in
                    (* yes, so start context unifier recomputation *)
                    List.iter
                      (fun space ->
                         (* ignore if clause is subsumed wrt. to this context literal *)
                         if is_space_subsumed_at problem_literals space context_partner.Context_unifier.cp_element then
                           ()
                                                  
                         else begin
                           (* result can be ignored, as a closing context unifier can not be found here. *)
                           ignore (
                             add_to_clause problem_literals.config problem_literals.bound problem_literals.context space
                               element.input_partner context_partner candidate_type false
                               : bool);
                         end
                      )
                      element.spaces;
                with
                  | Not_found ->
                      (* no, so ignore this clause literal *)
                      ()
              end
           )
           problem_literal.elements
      )
      unifying_candidates