functor (Seq : Sigs.SEQUENT) ->
  sig
    type rule_t = Proofrule.Make(Seq).t
    module Seq :
      sig
        type t = Seq.t
        val equal : t -> t -> bool
        val equal_upto_tags : t -> t -> bool
        val tags : t -> Tags.t
        val to_string : t -> string
        val to_melt : t -> Latex.t
        val pp : Format.formatter -> t -> unit
      end
    module Proof :
      sig
        type t = Proof.Make(Seq).t
        type seq_t = Seq.t
        type node_t = Proofnode.Make(Seq).t
        val mk : seq_t -> t
        val add_axiom : int -> string -> t -> t
        val add_backlink : int -> string -> int -> Tagpairs.t -> t -> t
        val add_inf :
          int ->
          string ->
          (seq_t * Tagpairs.t * Tagpairs.t) list -> t -> int list * t
        val add_subprf : t -> int -> t -> t
        val extract_subproof : int -> t -> t
        val find : int -> t -> node_t
        val get_seq : int -> t -> seq_t
        val size : t -> int
        val num_backlinks : t -> int
        val fresh_idx : t -> int
        val fresh_idxs : 'a list -> t -> int list
        val get_ancestry : int -> t -> (int * node_t) list
        val is_closed_at : t -> int -> bool
        val check : t -> bool
        val is_closed : t -> bool
        val to_list : t -> (int * node_t) list
        val pp : Format.formatter -> t -> unit
        val to_string : t -> string
        val to_melt : t -> Latex.t
      end
    val last_search_depth : int ref
    val idfs : int -> int -> rule_t -> rule_t -> Seq.t -> Proof.t option
    val print_proof_stats : Proof.t -> unit
    val melt_proof : out_channel -> Proof.t -> unit
  end