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