module Dummy : sig ... endmodule St : sig ... endmodule Proof : sig ... endtype atom = St.formulatype res = | Sat of (St.term, St.formula) Solver_intf.sat_state| Unsat of (St.clause, Proof.proof) Solver_intf.unsat_stateval assume : ?tag:int -> atom list list -> unitval unsat_core : Proof.proof -> St.clause listval true_at_level0 : atom -> boolval get_tag : St.clause -> int optionmodule Dot : sig ... endmodule Dedukti : sig ... endval print_clause : Format.formatter -> St.clause -> unitval print_dot : Format.formatter -> Proof.proof -> unitval print_dedukti : Format.formatter -> Proof.proof -> unit