sig
  type literal = Term.literal
  type flags = Flags.flags
  type problem = Problem.problem
  type config
  val create :
    flags:Config.flags ->
    problem:Config.problem ->
    is_horn:bool ->
    start_time:float -> fof:bool -> theorem:bool -> Config.config
  val start_time : Config.config -> float
  val is_horn : Config.config -> bool
  val is_fof : Config.config -> bool
  val is_theorem : Config.config -> bool
  val problem : Config.config -> Config.problem
  val resolve : Config.config -> bool
  val subsume : Config.config -> bool
  val compact : Config.config -> bool
  val productivity : Config.config -> bool
  val mixed_literals : Config.config -> bool
  val finite_domain : Config.config -> bool
  val finite_domain_functionality : Config.config -> bool
  val lemma : Config.config -> Flags.opt_lemma
  val lemma_min : Config.config -> int
  val lemma_max : Config.config -> int
  val lemma_uip : Config.config -> bool
  val lemma_parametric_assert : Config.config -> int
  val equality : Config.config -> Flags.opt_equality
  val plus_v : Config.config -> bool
  val default_v : Config.config -> Config.literal
  val backtracking : Config.config -> Flags.opt_backtracking
  val iterative_deepening : Config.config -> Flags.opt_iterative_deepening
  val deepening_bound : Config.config -> int
  val lookahead_exceeding : Config.config -> bool
  val restart : Config.config -> Flags.opt_restart
  val jumping : Config.config -> bool
  val neg_assert_candidates :
    Config.config -> Flags.opt_neg_assert_candidates
  val term_indexing : Config.config -> bool
  val problem_file_name : Config.config -> string
  val time_out_CPU : Config.config -> float
  val time_out_WC : Config.config -> float
  val print_level : Config.config -> int
  val print_configuration : Config.config -> bool
  val print_equality_axioms : Config.config -> bool
  val print_lemmas : Config.config -> bool
  val print_finite_domain_axioms : Config.config -> bool
  val print_finite_domain_problem :
    Config.config -> Flags.opt_print_fd_problem
  val print_statistics : Config.config -> bool
  val print_model_context : Config.config -> bool
  val print_model_context_file : Config.config -> string
  val print_model_DIG : Config.config -> bool
  val print_model_DIG_file : Config.config -> string
  val print_model_finite : Config.config -> bool
  val print_model_tptp : Config.config -> bool
  val print_model_tptp_file : Config.config -> string
  val print_derivation_online : Config.config -> bool
  val print_derivation_context_unifier : Config.config -> bool
  val print_assert_candidates : Config.config -> bool
  val print_split_candidates : Config.config -> bool
  val print : Config.config -> unit
end