+ (* bag, maxvar, meeting point *)
+ 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 :
+ B.t Terms.bag ->
+ int -> (* maxvar *)
+ B.t Terms.unit_clause -> (* selected passive *)
+ Index.Index(B).active_set ->
+ B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
+
+ val infer_left :