let make_admissible
  (config: Config.config)
  (raw_context_unifier: raw_context_unifier)
  (subst: subst)
  (remainder_states: bool array)
  : subst =

  (* get the variables for each input literal producing a remainder literal. *)
  let (remainder_input_vars: Subst.var list list) =
    vars_of_remainder_input_literals raw_context_unifier remainder_states
  in

  (* get the variables of the remainder literals.
     as the remainder literals are not build yet,
     get the variables in the terms bound to the input literals instead. *)
  let (remainder_literal_vars: Subst.var list list) =
    List.map
      (fun vars ->
         Subst.get_bound_vars subst vars
      )
      remainder_input_vars
  in

  (* get the universal variables occurring in more than one remainder literal. *)
  let (shared_remainder_literal_vars: Subst.var list) =
    Tools.lists_shared Subst.var_equal remainder_literal_vars
  in
    
  (* map the shared variables to fresh parameters. *)
  let (subst, fresh_pars) =
    make_v_free
      subst
      shared_remainder_literal_vars
      []
  in

  (* fixed_vars are the variables which may not be reversed
     in an attempt to make the remainder literals more universal. *)
  let fixed_pars =
    add_pars_of_non_remainder_context_literals 
      raw_context_unifier
      remainder_states
      (
        fresh_pars
        @
        raw_context_unifier.Context_unifier.rcu_space.Context_unifier.cus_shared_vars
        @
        shared_remainder_literal_vars
      )
  in

  (* reverse as many par -> var mappings as possible. *)
  let reversed_subst =
    reverse_subst
      subst
      remainder_input_vars
      fixed_pars
      raw_context_unifier.Context_unifier.rcu_space.Context_unifier.cus_shared_vars
  in
    if Config.mixed_literals config then
      reversed_subst
    else
      (* make all mixed literals universal variable free. *)
      parameterize_mixed_literals
        reversed_subst
        remainder_literal_vars
        fresh_pars