sig
  type abdrule_t
  type proof_t
  type defs_t
  module Seq : SEQUENT
  module Proof : PROOF
  val bfs :
    int ->
    Sigs.ABDUCER.abdrule_t ->
    Seq.t ->
    Sigs.ABDUCER.defs_t ->
    (Sigs.ABDUCER.defs_t -> bool) ->
    (Sigs.ABDUCER.proof_t * Sigs.ABDUCER.defs_t) option
  val print_proof_stats : Proof.t -> unit
  val melt_proof : Pervasives.out_channel -> Proof.t -> unit
end