sig
  val simplify :
    ?start:(Wpo.t -> unit) ->
    ?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
    Wpo.t -> bool Task.task
  val prove :
    Wpo.t ->
    ?config:VCS.config ->
    ?mode:VCS.mode ->
    ?start:(Wpo.t -> unit) ->
    ?progress:(Wpo.t -> string -> unit) ->
    ?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
    VCS.prover -> bool Task.task
  val spawn :
    Wpo.t ->
    delayed:bool ->
    ?config:VCS.config ->
    ?start:(Wpo.t -> unit) ->
    ?progress:(Wpo.t -> string -> unit) ->
    ?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
    ?success:(Wpo.t -> VCS.prover option -> unit) ->
    ?pool:Task.pool -> (VCS.mode * VCS.prover) list -> unit
end