Module type Sigs.PROVER

module type PROVER = sig .. end

type rule_t 

module Seq: Sigs.SEQUENT 

module Proof: Sigs.PROOF 

val last_search_depth : int Pervasives.ref

val idfs : int ->
       int -> rule_t -> rule_t -> Seq.t -> Proof.t option

val print_proof_stats : Proof.t -> unit

val melt_proof : Pervasives.out_channel -> Proof.t -> unit