sig
  type rule_t
  module Seq : SEQUENT
  module Proof : PROOF
  val last_search_depth : int Pervasives.ref
  val idfs :
    int ->
    int ->
    Sigs.PROVER.rule_t -> Sigs.PROVER.rule_t -> Seq.t -> Proof.t option
  val print_proof_stats : Proof.t -> unit
  val melt_proof : Pervasives.out_channel -> Proof.t -> unit
end