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