let register_input_partner
(problem_literals: problem_literals) (input_partner: input_partner) (space: context_unifier_space) : unit =
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