src/HOL/Tools/ATP/atp_systems.ML
changeset 42971 b01cbbf0bcc5
parent 42969 10baeee358a5
child 42974 347d5197896e
equal deleted inserted replaced
42970:05d1dc9fefdb 42971:b01cbbf0bcc5
   415 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   415 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   416 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   416 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   417 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
   417 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
   418 val remote_leo2 =
   418 val remote_leo2 =
   419   remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
   419   remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
   420              (K (150, ["simple"]) (* FUDGE *))
   420              (K (100, ["simple"]) (* FUDGE *))
   421 val remote_satallax =
   421 val remote_satallax =
   422   remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
   422   remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
   423              (K (150, ["simple"]) (* FUDGE *))
   423              (K (64, ["simple"]) (* FUDGE *))
   424 val remote_sine_e =
   424 val remote_sine_e =
   425   remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
   425   remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
   426              Axiom Conjecture [FOF]
   426              Axiom Conjecture [FOF]
   427              (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *))
   427              (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *))
   428 val remote_snark =
   428 val remote_snark =
   429   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   429   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   430              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   430              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   431              [TFF, FOF] (K (250, ["simple"]) (* FUDGE *))
   431              [TFF, FOF] (K (100, ["simple"]) (* FUDGE *))
   432 val remote_tofof_e =
   432 val remote_tofof_e =
   433   remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
   433   remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
   434              Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *))
   434              Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *))
   435 val remote_waldmeister =
   435 val remote_waldmeister =
   436   remote_atp waldmeisterN "Waldmeister" ["710"]
   436   remote_atp waldmeisterN "Waldmeister" ["710"]