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"] |