let register_input_partner
    (problem_literals: problem_literals) (input_partner: input_partner) (space: context_unifier_space) : unit  =

  (* ensure that this clause fits into the subsumed marker array *)
  extend_subsumed_clauses problem_literals space;

  let literal =
    input_partner.Context_unifier.ip_literal
  in
  let index =
    input_partner.Context_unifier.ip_index
  in
  let problem_literal =
    try
      LiteralTable.find problem_literals.problem_literals literal
    with
      | Not_found ->
          failwith "register_clause_literal: problem_literal"
  in

  let element =
    try
      Elements.find index problem_literal.elements
    with
      | Not_found ->
          failwith "register_clause_literal: element"
  in
    element.spaces <- space :: element.spaces