- (* let _ = Unix.alarm !seconds in *)
- match P.paramod ~timeout:(Unix.gettimeofday () +. float_of_int !seconds) ~max_steps:max_int bag ~g_passives:[g_passives] ~passives with
- | [] -> fail_msg ()
- | (bag,_,l)::_ ->
- print_endline ("% SZS status Unsatisfiable for " ^
- Filename.basename !problem_file);
- print_endline ("% SZS output start CNFRefutation for " ^
- Filename.basename !problem_file);
- flush stdout;
- List.iter (fun x ->
- print_endline (Pp.pp_unit_clause ~margin:max_int
- (fst(Terms.M.find x bag)))) l;
- print_endline ("% SZS output end CNFRefutation for " ^
- Filename.basename !problem_file);
+ let _ = Unix.alarm !seconds in
+ match
+ P.paramod
+ ~timeout:(Unix.gettimeofday () +. float_of_int (!seconds / 2) )
+ ~max_steps:max_int bag ~g_passives:[g_passives] ~passives
+ with
+ | [] ->
+ leaf_compare := (fun (_,a) (_,b) -> Pervasives.compare a b);
+ (match
+ P.paramod
+ ~timeout:(Unix.gettimeofday () +. float_of_int (!seconds / 2) )
+ ~max_steps:max_int bag ~g_passives:[g_passives] ~passives
+ with
+ | [] -> fail_msg ()
+ | (bag,_,l)::_ -> success_msg bag l Pp.pp_unit_clause)
+ | (bag,_,l)::_ -> success_msg bag l Pp.pp_unit_clause