1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 00:01:33 2011 +0200
     1.3 @@ -36,9 +36,11 @@
     1.4    val eN : string
     1.5    val spassN : string
     1.6    val vampireN : string
     1.7 -  val tofof_eN : string
     1.8 +  val leo2N : string
     1.9 +  val satallaxN : string
    1.10    val sine_eN : string
    1.11    val snarkN : string
    1.12 +  val tofof_eN : string
    1.13    val waldmeisterN : string
    1.14    val z3_atpN : string
    1.15    val remote_prefix : string
    1.16 @@ -98,9 +100,11 @@
    1.17  val spassN = "spass"
    1.18  val vampireN = "vampire"
    1.19  val z3_atpN = "z3_atp"
    1.20 -val tofof_eN = "tofof_e"
    1.21 +val leo2N = "leo2"
    1.22 +val satallaxN = "satallax"
    1.23  val sine_eN = "sine_e"
    1.24  val snarkN = "snark"
    1.25 +val tofof_eN = "tofof_e"
    1.26  val waldmeisterN = "waldmeister"
    1.27  val remote_prefix = "remote_"
    1.28  
    1.29 @@ -126,7 +130,8 @@
    1.30    if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000
    1.31  
    1.32  val tstp_proof_delims =
    1.33 -  ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
    1.34 +  [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
    1.35 +   ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
    1.36  
    1.37  val e_slicesN = "slices"
    1.38  val e_autoN = "auto"
    1.39 @@ -207,7 +212,7 @@
    1.40       e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
    1.41       " -tAutoDev --silent --cpu-limit=" ^
    1.42       string_of_int (to_secs (e_bonus ()) timeout),
    1.43 -   proof_delims = [tstp_proof_delims],
    1.44 +   proof_delims = tstp_proof_delims,
    1.45     known_failures =
    1.46       [(Unprovable, "SZS status: CounterSatisfiable"),
    1.47        (Unprovable, "SZS status CounterSatisfiable"),
    1.48 @@ -379,7 +384,7 @@
    1.49     arguments = fn _ => fn _ => fn timeout => fn _ =>
    1.50       " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
    1.51       ^ " -s " ^ the_system system_name system_versions,
    1.52 -   proof_delims = insert (op =) tstp_proof_delims proof_delims,
    1.53 +   proof_delims = union (op =) tstp_proof_delims proof_delims,
    1.54     known_failures =
    1.55       known_failures @ known_perl_failures @
    1.56       [(Unprovable, "says Satisfiable"),
    1.57 @@ -410,16 +415,23 @@
    1.58  val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
    1.59  val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
    1.60  val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
    1.61 -val remote_tofof_e =
    1.62 -  remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
    1.63 -             Axiom Conjecture [TFF] (K (200, ["simple"]) (* FUDGE *))
    1.64 +val remote_leo2 =
    1.65 +  remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
    1.66 +             (K (200, ["simple"]) (* FUDGE *))
    1.67 +val remote_satallax =
    1.68 +  remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
    1.69 +             (K (200, ["simple"]) (* FUDGE *))
    1.70  val remote_sine_e =
    1.71 -  remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [FOF]
    1.72 +  remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
    1.73 +             Axiom Conjecture [FOF]
    1.74               (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *))
    1.75  val remote_snark =
    1.76    remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
    1.77 -             [("refutation.", "end_refutation.")] [] Hypothesis Conjecture
    1.78 +             [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
    1.79               [TFF, FOF] (K (250, ["simple"]) (* FUDGE *))
    1.80 +val remote_tofof_e =
    1.81 +  remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
    1.82 +             Axiom Hypothesis [TFF] (K (200, ["simple"]) (* FUDGE *))
    1.83  val remote_waldmeister =
    1.84    remote_atp waldmeisterN "Waldmeister" ["710"]
    1.85               [("#START OF PROOF", "Proved Goals:")]
    1.86 @@ -448,8 +460,9 @@
    1.87  fun refresh_systems_on_tptp () =
    1.88    Synchronized.change systems (fn _ => get_systems ())
    1.89  
    1.90 -val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
    1.91 -            remote_tofof_e, remote_sine_e, remote_snark, remote_waldmeister]
    1.92 +val atps =
    1.93 +  [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
    1.94 +   remote_leo2, remote_sine_e, remote_snark, remote_tofof_e, remote_waldmeister]
    1.95  val setup = fold add_atp atps
    1.96  
    1.97  end;