sig
(* bag, maxvar, meeting point *)
- exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+ exception Success of
+ B.t Terms.bag
+ * int
+ * B.t Terms.unit_clause
+ * B.t Terms.substitution
(* The returned active set is the input one + the selected clause *)
val infer_right :