src/HOL/Tools/ATP/atp_systems.ML
changeset 66361 5deeb0dbccb4
parent 63768 a09cfea0c2c9
child 66363 8aca34dbe195
equal deleted inserted replaced
66360:af5c71cffec5 66361:5deeb0dbccb4
   722     (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
   722     (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
   723 val remote_satallax =
   723 val remote_satallax =
   724   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
   724   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
   725     (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   725     (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
   726 val remote_vampire =
   726 val remote_vampire =
   727   remotify_atp vampire "Vampire" ["4.0", "3.0", "2.6"]
   727   remotify_atp vampire "Vampire" ["4.2", "4.0"]
   728     (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
   728     (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
   729 val remote_e_sine =
   729 val remote_e_sine =
   730   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
   730   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
   731     (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
   731     (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
   732 val remote_snark =
   732 val remote_snark =