equal
deleted
inserted
replaced
459 else |
459 else |
460 I)) |
460 I)) |
461 * 0.001) |> seconds |
461 * 0.001) |> seconds |
462 val _ = |
462 val _ = |
463 if debug then |
463 if debug then |
464 quote name ^ " slice " ^ string_of_int (slice + 1) ^ |
464 quote name ^ " slice #" ^ string_of_int (slice + 1) ^ |
465 " of " ^ string_of_int num_actual_slices ^ " with " ^ |
465 " with " ^ string_of_int num_facts ^ " fact" ^ |
466 string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ |
466 plural_s num_facts ^ " for " ^ |
467 " for " ^ string_from_time slice_timeout ^ "..." |
467 string_from_time slice_timeout ^ "..." |
468 |> Output.urgent_message |
468 |> Output.urgent_message |
469 else |
469 else |
470 () |
470 () |
471 val (atp_problem, pool, conjecture_offset, facts_offset, |
471 val (atp_problem, pool, conjecture_offset, facts_offset, |
472 fact_names) = |
472 fact_names) = |