equal
deleted
inserted
replaced
657 val core = |
657 val core = |
658 File.shell_path command ^ " " ^ |
658 File.shell_path command ^ " " ^ |
659 arguments ctxt full_proof extra slice_timeout weights ^ " " ^ |
659 arguments ctxt full_proof extra slice_timeout weights ^ " " ^ |
660 File.shell_path prob_file |
660 File.shell_path prob_file |
661 val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1" |
661 val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1" |
662 val _ = |
662 val _ = atp_problem |> lines_for_atp_problem format |
663 atp_problem |
663 |> cons ("% " ^ command ^ "\n") |
664 |> tptp_lines_for_atp_problem format |
664 |> File.write_list prob_file |
665 |> cons ("% " ^ command ^ "\n") |
|
666 |> File.write_list prob_file |
|
667 val conjecture_shape = |
665 val conjecture_shape = |
668 conjecture_offset + 1 |
666 conjecture_offset + 1 |
669 upto conjecture_offset + length hyp_ts + 1 |
667 upto conjecture_offset + length hyp_ts + 1 |
670 |> map single |
668 |> map single |
671 val ((output, msecs), (atp_proof, outcome)) = |
669 val ((output, msecs), (atp_proof, outcome)) = |