404 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] |
404 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] |
405 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] |
405 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] |
406 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] |
406 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"] |
407 val remote_tofof_e = |
407 val remote_tofof_e = |
408 remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) |
408 remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) |
409 Axiom Conjecture [Tff] (K (200, ["simple_types"]) (* FUDGE *)) |
409 Axiom Conjecture [Tff] (K (200, ["simple"]) (* FUDGE *)) |
410 val remote_sine_e = |
410 val remote_sine_e = |
411 remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof] |
411 remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof] |
412 (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *)) |
412 (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *)) |
413 val remote_snark = |
413 val remote_snark = |
414 remote_atp snarkN "SNARK" ["20080805r024"] |
414 remote_atp snarkN "SNARK" ["20080805r024"] |
415 [("refutation.", "end_refutation.")] [] Hypothesis Conjecture |
415 [("refutation.", "end_refutation.")] [] Hypothesis Conjecture |
416 [Tff, Fof] (K (250, ["simple_types"]) (* FUDGE *)) |
416 [Tff, Fof] (K (250, ["simple"]) (* FUDGE *)) |
417 |
417 |
418 (* Setup *) |
418 (* Setup *) |
419 |
419 |
420 fun add_atp (name, config) thy = |
420 fun add_atp (name, config) thy = |
421 Data.map (Symtab.update_new (name, (config, stamp ()))) thy |
421 Data.map (Symtab.update_new (name, (config, stamp ()))) thy |