+ val simplify :
+ Index.Index(B).DT.t ->
+ int ->
+ B.t Terms.bag ->
+ B.t Terms.unit_clause ->
+ B.t Terms.bag * (B.t Terms.unit_clause option)
+
+ (* may raise success *)
+ val simplify_goal :
+ no_demod:bool ->
+ int ->
+ Index.Index(B).DT.t ->
+ B.t Terms.bag ->
+ B.t Terms.unit_clause list ->
+ B.t Terms.unit_clause ->
+ (B.t Terms.bag * B.t Terms.unit_clause) option
+
+ val one_pass_simplification:
+ B.t Terms.unit_clause ->
+ Index.Index(B).active_set ->
+ B.t Terms.bag ->
+ int ->
+ B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
+ val keep_simplified:
+ B.t Terms.unit_clause ->
+ Index.Index(B).active_set ->
+ B.t Terms.bag ->
+ int ->
+ B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
+
+ val orphan_murder:
+ B.t Terms.bag ->
+ B.t Terms.unit_clause list ->
+ B.t Terms.unit_clause ->
+ bool
+
+ val are_alpha_eq :
+ B.t Terms.unit_clause ->
+ B.t Terms.unit_clause ->
+ bool
+ end