| Timeout of int * t Terms.bag
type bag = t Terms.bag * int
val empty_state : state
+ val size_of_state : state -> int * int
val bag_of_state :state -> bag
val replace_bag : state -> bag -> state
+ (* we suppose input has been already saturated *)
val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
val forward_infer_step :