sig
  type var = Var.var
  type symbol = Symbol.symbol
  type func = private {
    symbol : Term.symbol;
    subterms : Term.term array;
    ground : bool;
    hash : int;
    in_db : bool;
  }
  and term =
      private Var of Term.var
    | Const of Term.symbol
    | Func of Term.func
  type literal = private {
    sign : bool;
    atom : Term.term;
    literal_in_db : bool;
  }
  type clause = Term.literal list
  module TermTable :
    sig
      type key = term
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
    end
  module LiteralTable :
    sig
      type key = literal
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
    end
  module ClauseTable :
    sig
      type key = clause
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
    end
  module ClauseApproxTable :
    sig
      type key = clause
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
    end
  module LiteralTypeTable :
    sig
      type key = literal
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
    end
  val true_literal : Term.literal
  val false_literal : Term.literal
  val null_term : Term.term
  val null_literal : Term.literal
  val assert_literal : Term.literal
  val init_literal : Term.literal
  val plus_v : Term.literal
  val minus_v : Term.literal
  val v_par : Term.var
  val v_term : Term.term
  val request_var : Term.var -> Term.term
  val request_const : Term.symbol -> Term.term
  val request_func :
    ?insert_db:bool -> Term.symbol * Term.term array -> Term.term
  val request_literal : ?insert_db:bool -> bool -> Term.term -> Term.literal
  val insert_term : Term.term -> Term.term
  val insert_literal : Term.literal -> Term.literal
  val request_negated_literal :
    ?insert_db:bool -> Term.literal -> Term.literal
  val request_skolemized_literal : Term.literal -> Term.literal
  val request_skolemized_clause : Term.clause -> Term.clause
  val request_universal_term : Term.term -> Term.term
  val request_universal_literal : Term.literal -> Term.literal
  val request_universal_clause : Term.clause -> Term.clause
  val replace_term_in_term : Term.term -> Term.term -> Term.term -> Term.term
  val replace_term_in_literal :
    Term.literal -> Term.term -> Term.term -> Term.literal
  val replace_terms_in_term :
    Term.term -> (Term.term * Term.term) list -> Term.term
  val replace_terms_in_literal :
    Term.literal -> (Term.term * Term.term) list -> Term.literal
  val replace_vars_in_term :
    Term.term -> (Term.var -> Term.term -> Term.term) -> Term.term
  val replace_vars_in_literal :
    Term.literal -> (Term.var -> Term.term -> Term.term) -> Term.literal
  val remove_duplicates : clause -> clause
  val get_term_sort : Term.term -> Symbol.sort
  val get_literal_sort : Term.literal -> Symbol.sort
  val is_connection_literal : Term.literal -> bool
  val is_fd_relation : Term.literal -> bool
  val is_fd_size_marker : Term.literal -> bool
  val is_fd_element : Term.term -> bool
  val is_input_term : Term.term -> bool
  val is_input_literal : Term.literal -> bool
  val is_fd_term : Term.term -> bool
  val is_fd_literal : Term.literal -> bool
  val is_skolem_free_term : Term.term -> bool
  val is_skolem_free_literal : Term.literal -> bool
  val hash_of_term : Term.term -> int
  val hash_of_literal : Term.literal -> int
  val hash_of_clause : Term.clause -> int
  val top_symbol_term : Term.term -> Term.symbol
  val top_symbol_literal : Term.literal -> Term.symbol
  val is_term_var : Term.term -> bool
  val is_literal_var : Term.literal -> bool
  val vars_of_term : Term.term -> Term.var list
  val vars_of_literal : Term.literal -> Term.var list
  val vars_of_clause : Term.clause -> Term.var list
  val term_contains_var : Term.term -> Term.var -> bool
  val literal_contains_var : Term.literal -> Term.var -> bool
  val term_contains_term : Term.term -> Term.term -> bool
  val literal_contains_term : Term.literal -> Term.term -> bool
  val is_term_ground : Term.term -> bool
  val is_literal_ground : Term.literal -> bool
  val is_schema_term : Term.term -> bool
  val create_schema_term : Term.symbol -> Term.term
  val create_schema_term_from_term : Term.term -> Term.term
  val is_definit : Term.clause -> bool
  val is_Horn : Term.clause -> bool
  val are_Horn : Term.clause list -> bool
  val is_BS : Term.clause -> bool
  val are_BS : Term.clause list -> bool
  val contains_empty_clause : Term.clause list -> bool
  val contains_equality : Term.clause list -> bool
  val is_tautology : Term.clause -> bool
  val term_equal : Term.term -> Term.term -> bool
  val literal_equal : Term.literal -> Term.literal -> bool
  val clause_equal : Term.clause -> Term.clause -> bool
  val clause_approx_equal : Term.clause -> Term.clause -> bool
  val compare_terms : Term.term -> Term.term -> int
  val compare_literals : Term.literal -> Term.literal -> int
  val sort_clause : Term.clause -> Term.clause
  val are_terms_variants : Term.term -> Term.term -> bool
  val are_literals_variants : Term.literal -> Term.literal -> bool
  val are_literals_skolem_variants : Term.literal -> Term.literal -> bool
  val remove_variants : Term.literal list -> Term.literal list
  val remove_duplicates : Term.literal list -> Term.literal list
  val tptp_get_domain_element : int -> Term.term
  val tptp_replace_var : Term.var -> Term.term
  val to_tptp_term : Term.term -> Term.term
  val term_to_string : ?pretty:bool -> Term.term -> string
  val literal_to_string : ?pretty:bool -> Term.literal -> string
  val clause_to_string : ?pretty:bool -> Term.clause -> string
  val tptp_clause_to_tptp_string : string -> Term.clause -> string
end