sig
  val first :
    ProofEngine.tree ->
    ?anchor:ProofEngine.node -> Strategy.t array -> ProofEngine.fork option
  val index :
    ProofEngine.tree ->
    anchor:ProofEngine.node -> index:int -> ProofEngine.fork option
  val search :
    ProofEngine.tree ->
    ?anchor:ProofEngine.node ->
    ?sequent:Conditions.sequent ->
    Strategy.heuristic list -> ProofEngine.fork option
  val backtrack :
    ProofEngine.tree ->
    ?anchor:ProofEngine.node ->
    ?loop:bool -> ?width:int -> unit -> ProofEngine.fork option
end