1 2signature minisatProve = sig 3 exception SAT_cex of Thm.thm 4 val GEN_SAT : satConfig.sat_config -> Thm.thm 5 val SAT_PROVE : Term.term -> Thm.thm 6 val SAT_ORACLE : Term.term -> Thm.thm 7 val ZSAT_PROVE : Term.term -> Thm.thm 8 val ZSAT_ORACLE : Term.term -> Thm.thm 9end 10