710 (K (((50, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *)) |
710 (K (((50, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *)) |
711 |
711 |
712 val remote_agsyhol = |
712 val remote_agsyhol = |
713 remotify_atp agsyhol "agsyHOL" ["1.0", "1"] |
713 remotify_atp agsyhol "agsyHOL" ["1.0", "1"] |
714 (K (((60, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) |
714 (K (((60, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) |
|
715 val remote_alt_ergo = |
|
716 remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] |
|
717 (K (((250, ""), TFF Polymorphic, "poly_native", keep_lamsN, false), "") (* FUDGE *)) |
715 val remote_e = |
718 val remote_e = |
716 remotify_atp e "E" ["2.0", "1.9.1", "1.8"] |
719 remotify_atp e "E" ["2.0", "1.9.1", "1.8"] |
717 (K (((750, ""), TFF Monomorphic, "mono_native", combsN, false), "") (* FUDGE *)) |
720 (K (((750, ""), TFF Monomorphic, "mono_native", combsN, false), "") (* FUDGE *)) |
718 val remote_iprover = |
721 val remote_iprover = |
719 remotify_atp iprover "iProver" ["0.99"] |
722 remotify_atp iprover "iProver" ["0.99"] |
722 remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] |
725 remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] |
723 (K (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) |
726 (K (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) |
724 val remote_leo3 = |
727 val remote_leo3 = |
725 remotify_atp leo3 "Leo-III" ["1.1"] |
728 remotify_atp leo3 "Leo-III" ["1.1"] |
726 (K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) |
729 (K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) |
727 val remote_vampire = |
|
728 remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"] |
|
729 (K (((400, ""), TFF Monomorphic, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *)) |
|
730 val remote_snark = |
730 val remote_snark = |
731 remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"] |
731 remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"] |
732 [("refutation.", "end_refutation.")] [] Hypothesis |
732 [("refutation.", "end_refutation.")] [] Hypothesis |
733 (K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *)) |
733 (K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *)) |
|
734 val remote_vampire = |
|
735 remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"] |
|
736 (K (((400, ""), TFF Monomorphic, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *)) |
734 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" |
737 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" |
735 |
738 |
736 |
739 |
737 (* Setup *) |
740 (* Setup *) |
738 |
741 |
766 end |
769 end |
767 end |
770 end |
768 |
771 |
769 val atps = |
772 val atps = |
770 [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, leo2, leo3, satallax, spass, vampire, |
773 [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, leo2, leo3, satallax, spass, vampire, |
771 z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_iprover, remote_leo2, remote_leo3, |
774 z3_tptp, zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, |
772 remote_vampire, remote_snark, remote_pirate, remote_waldmeister] |
775 remote_leo2, remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister] |
773 |
776 |
774 val _ = Theory.setup (fold add_atp atps) |
777 val _ = Theory.setup (fold add_atp atps) |
775 |
778 |
776 end; |
779 end; |