sig
  type 'a or_error = [ `Error of string | `Ok of 'a ]
  type untyped = Libzipperposition.STerm.t
  module A = Ast_tptp
  module Prover :
    sig
      type t = {
        name : string;
        command : string;
        unsat : string list;
        sat : string list;
      }
      val lookup : string -> CallProver.Prover.t
      val list_provers : unit -> string list
      val register : string -> CallProver.Prover.t -> unit
      val p_E : CallProver.Prover.t
      val p_Eproof : CallProver.Prover.t
      val p_SPASS : CallProver.Prover.t
      val p_Zenon : CallProver.Prover.t
      val default : CallProver.Prover.t list
    end
  val name : CallProver.Prover.t -> string
  type result = Unsat | Sat | Unknown | Error of string
  val call :
    ?timeout:int ->
    ?args:string list ->
    prover:CallProver.Prover.t ->
    CallProver.untyped A.t list -> CallProver.result CallProver.or_error
  val call_proof :
    ?timeout:int ->
    ?args:string list ->
    prover:CallProver.Prover.t ->
    CallProver.untyped A.t list ->
    (CallProver.result * Trace_tstp.t) CallProver.or_error
  val call_with_out :
    ?timeout:int ->
    ?args:string list ->
    prover:CallProver.Prover.t ->
    CallProver.untyped A.t list ->
    (CallProver.result * string) CallProver.or_error
  module Eprover :
    sig
      type result = {
        answer : CallProver.Eprover.szs_answer;
        output : string;
        decls : CallProver.untyped A.t Sequence.t option;
        proof : Trace_tstp.t option;
      }
      and szs_answer = Theorem | CounterSatisfiable | Unknown
      val string_of_answer : CallProver.Eprover.szs_answer -> string
      val run_eproof :
        steps:int ->
        input:string -> CallProver.Eprover.result CallProver.or_error
      val run_eprover :
        ?opts:string list ->
        ?level:int ->
        steps:int ->
        input:string -> unit -> CallProver.Eprover.result CallProver.or_error
      val discover :
        ?opts:string list ->
        steps:int ->
        CallProver.untyped A.t Sequence.t ->
        CallProver.untyped A.t Sequence.t CallProver.or_error
      val cnf :
        ?opts:string list ->
        CallProver.untyped A.t Sequence.t ->
        CallProver.untyped A.t Sequence.t CallProver.or_error
    end
end