+ type t = B.t
+ type input = B.input
+ type state =
+ B.t Terms.bag
+ * int
+ * Index.Index(B).active_set
+ * (WeightPassiveSet.t * AgePassiveSet.t)
+ * B.t Terms.unit_clause list
+ * (WeightPassiveSet.t * AgePassiveSet.t)
+ type szsontology =
+ | Unsatisfiable of (B.t Terms.bag * int * int list) list
+ | GaveUp
+ | Error of string
+ | Timeout of int * B.t Terms.bag
+ exception Stop of szsontology
+ type bag = B.t Terms.bag * int
+
+ let empty_state =
+ Terms.empty_bag,
+ 0,
+ ([],IDX.DT.empty),
+ (WeightPassiveSet.empty,AgePassiveSet.empty),
+ [],
+ (WeightPassiveSet.empty,AgePassiveSet.empty)
+;;
+