+ B.t Terms.bag ->
+ B.t Terms.unit_clause ->
+ (B.t Terms.bag * B.t Terms.unit_clause) option
+
+ (* may raise success *)
+ val backward_simplify :
+ int ->
+ Index.Index(B).DT.t ->
+ B.t Terms.bag ->
+ B.t Terms.unit_clause ->
+ B.t Terms.bag * B.t Terms.unit_clause
+