364 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] |
364 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] |
365 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] |
365 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] |
366 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] |
366 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] |
367 val remote_tofof_e = |
367 val remote_tofof_e = |
368 remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) |
368 remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) |
369 Conjecture [Tff] (K 200 (* FUDGE *)) [] |
369 Conjecture [Tff] (K 200 (* FUDGE *)) ["many_typed"] |
370 val remote_sine_e = |
370 val remote_sine_e = |
371 remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *)) |
371 remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *)) |
372 (#best_type_systems e_config) |
372 (#best_type_systems e_config) |
373 val remote_snark = |
373 val remote_snark = |
374 remote_atp snarkN "SNARK" ["20080805r024"] |
374 remote_atp snarkN "SNARK" ["20080805r024"] |
375 [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof] |
375 [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof] |
376 (K 250 (* FUDGE *)) [] |
376 (K 250 (* FUDGE *)) ["many_typed"] |
377 |
377 |
378 (* Setup *) |
378 (* Setup *) |
379 |
379 |
380 fun add_atp (name, config) thy = |
380 fun add_atp (name, config) thy = |
381 Data.map (Symtab.update_new (name, (config, stamp ()))) thy |
381 Data.map (Symtab.update_new (name, (config, stamp ()))) thy |