functor (Symbol : SymbolType) ->
  sig
    type symbol = Symbol.t
    type term = private Var of int | Const of symbol
    val mk_var : int -> term
    val mk_const : symbol -> term
    type literal
    type clause
    type soft_lit = symbol * term list
    type soft_clause = soft_lit * soft_lit list
    val mk_literal : symbol -> term list -> literal
    val of_soft_lit : soft_lit -> literal
    val open_literal : literal -> soft_lit
    val mk_clause : literal -> literal list -> clause
    val of_soft_clause : soft_clause -> clause
    val open_clause : clause -> soft_clause
    val is_ground : literal -> bool
    val arity : literal -> int
    val eq_term : term -> term -> bool
    val eq_literal : literal -> literal -> bool
    val hash_literal : literal -> int
    val check_safe : clause -> bool
    val is_fact : clause -> bool
    val eq_clause : clause -> clause -> bool
    val hash_clause : clause -> int
    val pp_term : Format.formatter -> term -> unit
    val pp_literal : Format.formatter -> literal -> unit
    val pp_clause : Format.formatter -> clause -> unit
    val quantify1 : (term -> 'a) -> 'a
    val quantify2 : (term -> term -> 'a) -> 'a
    val quantify3 : (term -> term -> term -> 'a) -> 'a
    val quantify4 : (term -> term -> term -> term -> 'a) -> 'a
    val quantifyn : int -> (term list -> 'a) -> 'a
    exception UnsafeClause
    type db
    type explanation =
        Axiom
      | Resolution of clause * literal
      | ExtExplanation of string * Univ.t
    val db_create : unit -> db
    val db_copy : db -> db
    val db_mem : db -> clause -> bool
    val db_add : ?expl:explanation -> db -> clause -> unit
    val db_add_fact : ?expl:explanation -> db -> literal -> unit
    val db_goal : db -> literal -> unit
    val db_match : db -> literal -> (literal -> unit) -> unit
    val db_query : db -> literal -> int list -> (symbol list -> unit) -> unit
    val db_size : db -> int
    val db_fold : ('a -> clause -> 'a) -> 'a -> db -> 'a
    type fact_handler = literal -> unit
    type goal_handler = literal -> unit
    val db_subscribe_fact : db -> symbol -> fact_handler -> unit
    val db_subscribe_all_facts : db -> fact_handler -> unit
    val db_subscribe_goal : db -> goal_handler -> unit
    type user_fun = soft_lit -> soft_lit
    val db_add_fun : db -> symbol -> user_fun -> unit
    val db_goals : db -> (literal -> unit) -> unit
    val db_explain : db -> literal -> literal list
    val db_premises : db -> literal -> clause * literal list
    val db_explanations : db -> clause -> explanation list
    module Query :
      sig
        type set
        val ask : db -> ?neg:literal list -> int array -> literal list -> set
        val iter : set -> (term array -> unit) -> unit
        val to_list : set -> term array list
        val cardinal : set -> int
        val pp_plan : Format.formatter -> set -> unit
      end
  end