B.t Terms.bag * (B.t Terms.unit_clause option)
(* may raise success *)
- val simplify_goal :
+ val simplify_goal :
+ no_demod:bool ->
int ->
Index.Index(B).DT.t ->
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
+
end