+(* if is_orphan then prerr_endline
+ ("WRONG discarded: " ^ (Pp.pp_unit_clause current));
+ List.iter (fun x ->
+ prerr_endline (Pp.pp_unit_clause x))
+ (fst actives);*)
+
+(* List.iter (fun (id,_,_,_) -> let (cl,d) =
+ Terms.M.find id bag in
+ if d then prerr_endline
+ ("WRONG discarded: " ^ (Pp.pp_unit_clause cl)))
+ (current::fst actives);*)