equal
deleted
inserted
replaced
151 |
151 |
152 val vampire_config : atp_config = |
152 val vampire_config : atp_config = |
153 {exec = ("VAMPIRE_HOME", "vampire"), |
153 {exec = ("VAMPIRE_HOME", "vampire"), |
154 required_execs = [], |
154 required_execs = [], |
155 arguments = fn complete => fn timeout => |
155 arguments = fn complete => fn timeout => |
156 ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^ |
156 (* This would work too but it's less tested: "--proof tptp " ^ *) |
157 " --thanks Andrei --input_file") |
157 "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^ |
|
158 " --thanks \"Andrei and Krystof\" --input_file" |
158 |> not complete ? prefix "--sos on ", |
159 |> not complete ? prefix "--sos on ", |
159 has_incomplete_mode = true, |
160 has_incomplete_mode = true, |
160 proof_delims = |
161 proof_delims = |
161 [("=========== Refutation ==========", |
162 [("=========== Refutation ==========", |
162 "======= End of refutation ======="), |
163 "======= End of refutation ======="), |