let unregister_space (problem_literals: problem_literals) (space: context_unifier_space) : unit  =
  Array.iter
    (fun input_partner ->
       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 "unregister_clause_literal: problem_literal"
       in
         
       let element =
         try
           Elements.find index problem_literal.elements
         with
           | Not_found ->
               failwith "unregister_clause_literal: element"
       in
         (* remove space from input partner *)
         element.spaces <- List.find_all (fun space' -> space != space') element.spaces;
         
         (* remove input partner if no space left *)
         begin
           match element.spaces with
             | [] ->
                 problem_literal.elements <- Elements.remove index problem_literal.elements;
                 
         (* too cautious in unregistering bindings.
            less performant, less memory wasted. *)
         begin
           Stack.iter
             (fun context_partner ->
                match context_partner.Context_unifier.cp_partial_context_unifier with
                  | None ->
                      ()

                  | Some subst ->
                      Subst.iter (Bindings.remove problem_literals.bindings) subst
             )
             input_partner.Context_unifier.ip_context_partners;
           match input_partner.Context_unifier.ip_resolved with
             | None ->
                 ()

             | Some context_partner ->
                 begin
                   match context_partner.Context_unifier.cp_partial_context_unifier with
                     | None ->
                         ()
                           
                     | Some subst ->
                         Subst.iter (Bindings.remove problem_literals.bindings) subst
                 end
         end

             | _ ->
                 ()
         end;
         
         (* remove problem literal if no input partner left *)
         if Elements.is_empty problem_literal.elements then begin
           LiteralTable.remove problem_literals.problem_literals literal;
           let index =
             problem_literals.index#find problem_literal.literal
           in
             if not (index#remove problem_literal.literal.Term.atom (Some problem_literal)) then
               failwith "unregister_clause_literal: problem literal 2"               
         end;
    )
    space.Context_unifier.cus_input_partners