106 val spassN = "spass" |
106 val spassN = "spass" |
107 val vampireN = "vampire" |
107 val vampireN = "vampire" |
108 val z3_atpN = "z3_atp" |
108 val z3_atpN = "z3_atp" |
109 val leo2N = "leo2" |
109 val leo2N = "leo2" |
110 val satallaxN = "satallax" |
110 val satallaxN = "satallax" |
111 val sine_eN = "sine_e" |
111 val e_sineN = "e_sine" |
112 val snarkN = "snark" |
112 val snarkN = "snark" |
113 val tofof_eN = "tofof_e" |
113 val e_tofofN = "e_tofof" |
114 val waldmeisterN = "waldmeister" |
114 val waldmeisterN = "waldmeister" |
115 val remote_prefix = "remote_" |
115 val remote_prefix = "remote_" |
116 |
116 |
117 structure Data = Theory_Data |
117 structure Data = Theory_Data |
118 ( |
118 ( |
420 remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF] |
420 remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF] |
421 (K (100, "simple_higher") (* FUDGE *)) |
421 (K (100, "simple_higher") (* FUDGE *)) |
422 val remote_satallax = |
422 val remote_satallax = |
423 remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF] |
423 remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF] |
424 (K (64, "simple_higher") (* FUDGE *)) |
424 (K (64, "simple_higher") (* FUDGE *)) |
425 val remote_sine_e = |
425 val remote_e_sine = |
426 remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom |
426 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom |
427 Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *)) |
427 Conjecture [FOF] (K (500, "mangled_guards?") (* 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 (100, "simple") (* FUDGE *)) |
431 [TFF, FOF] (K (100, "simple") (* FUDGE *)) |
432 val remote_tofof_e = |
432 val remote_e_tofof = |
433 remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config) |
433 remote_atp e_tofofN "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"] |
437 [("#START OF PROOF", "Proved Goals:")] |
437 [("#START OF PROOF", "Proved Goals:")] |
438 [(OutOfResources, "Too many function symbols"), |
438 [(OutOfResources, "Too many function symbols"), |
460 fun refresh_systems_on_tptp () = |
460 fun refresh_systems_on_tptp () = |
461 Synchronized.change systems (fn _ => get_systems ()) |
461 Synchronized.change systems (fn _ => get_systems ()) |
462 |
462 |
463 val atps = |
463 val atps = |
464 [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp, |
464 [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp, |
465 remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e, |
465 remote_leo2, remote_satallax, remote_e_sine, remote_snark, remote_e_tofof, |
466 remote_waldmeister] |
466 remote_waldmeister] |
467 val setup = fold add_atp atps |
467 val setup = fold add_atp atps |
468 |
468 |
469 end; |
469 end; |