1 (* Title: HOL/Tools/ATP/atp_systems.ML
2 Author: Fabian Immler, TU Muenchen
3 Author: Jasmin Blanchette, TU Muenchen
5 Setup for supported ATPs.
8 signature ATP_SYSTEMS =
10 type atp_format = ATP_Problem.atp_format
11 type formula_kind = ATP_Problem.formula_kind
12 type failure = ATP_Proof.failure
14 type slice_spec = int * atp_format * string * string * bool
16 {exec : string * string,
17 required_execs : (string * string) list,
19 Proof.context -> bool -> string -> Time.time
20 -> (unit -> (string * real) list) -> string,
21 proof_delims : (string * string) list,
22 known_failures : (failure * string) list,
23 conj_sym_kind : formula_kind,
24 prem_kind : formula_kind,
26 Proof.context -> (real * (bool * (slice_spec * string))) list}
28 val force_sos : bool Config.T
31 val e_fun_weightN : string
32 val e_sym_offset_weightN : string
33 val e_weight_method : string Config.T
34 val e_default_fun_weight : real Config.T
35 val e_fun_weight_base : real Config.T
36 val e_fun_weight_span : real Config.T
37 val e_default_sym_offs_weight : real Config.T
38 val e_sym_offs_weight_base : real Config.T
39 val e_sym_offs_weight_span : real Config.T
40 val spass_incompleteN : string
45 val iprover_eqN : string
47 val dummy_tff1N : string
48 val dummy_thfN : string
49 val satallaxN : string
52 val spass_newN : string
54 val waldmeisterN : string
56 val remote_prefix : string
58 string -> string -> string list -> (string * string) list
59 -> (failure * string) list -> formula_kind -> formula_kind
60 -> (Proof.context -> slice_spec) -> string * atp_config
61 val add_atp : string * atp_config -> theory -> theory
62 val get_atp : theory -> string -> atp_config
63 val supported_atps : theory -> string list
64 val is_atp_installed : theory -> string -> bool
65 val refresh_systems_on_tptp : unit -> unit
66 val setup : theory -> theory
69 structure ATP_Systems : ATP_SYSTEMS =
74 open ATP_Problem_Generate
76 (* ATP configuration *)
78 type slice_spec = int * atp_format * string * string * bool
81 {exec : string * string,
82 required_execs : (string * string) list,
84 Proof.context -> bool -> string -> Time.time
85 -> (unit -> (string * real) list) -> string,
86 proof_delims : (string * string) list,
87 known_failures : (failure * string) list,
88 conj_sym_kind : formula_kind,
89 prem_kind : formula_kind,
90 best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
92 (* "best_slices" must be found empirically, taking a wholistic approach since
93 the ATPs are run in parallel. The "real" component gives the faction of the
94 time available given to the slice and should add up to 1.0. The first "bool"
95 component indicates whether the slice's strategy is complete; the "int", the
96 preferred number of facts to pass; the first "string", the preferred type
97 system (which should be sound or quasi-sound); the second "string", the
98 preferred lambda translation scheme; the second "bool", whether uncurried
99 aliased should be generated; the third "string", extra information to
100 the prover (e.g., SOS or no SOS).
102 The last slice should be the most "normal" one, because it will get all the
103 time available if the other slices fail early and also because it is used if
104 slicing is disabled (e.g., by the minimizer). *)
106 val known_perl_failures =
107 [(CantConnect, "HTTP error"),
108 (NoPerl, "env: perl"),
109 (NoLibwwwPerl, "Can't locate HTTP")]
111 fun known_szs_failures wrap =
112 [(Unprovable, wrap "CounterSatisfiable"),
113 (Unprovable, wrap "Satisfiable"),
114 (GaveUp, wrap "GaveUp"),
115 (GaveUp, wrap "Unknown"),
116 (GaveUp, wrap "Incomplete"),
117 (ProofMissing, wrap "Theorem"),
118 (ProofMissing, wrap "Unsatisfiable"),
119 (TimedOut, wrap "Timeout"),
120 (Inappropriate, wrap "Inappropriate"),
121 (OutOfResources, wrap "ResourceOut"),
122 (OutOfResources, wrap "MemoryOut"),
123 (Interrupted, wrap "Forced"),
124 (Interrupted, wrap "User")]
126 val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
127 val known_says_failures = known_szs_failures (prefix " says ")
132 val e_sineN = "e_sine"
133 val e_tofofN = "e_tofof"
134 val iproverN = "iprover"
135 val iprover_eqN = "iprover_eq"
137 val dummy_tff1N = "dummy_tff1" (* experimental *)
138 val dummy_thfN = "dummy_thf" (* experimental *)
139 val satallaxN = "satallax"
142 val spass_newN = "spass_new" (* experimental *)
143 val vampireN = "vampire"
144 val waldmeisterN = "waldmeister"
145 val z3_tptpN = "z3_tptp"
146 val remote_prefix = "remote_"
148 structure Data = Theory_Data
150 type T = (atp_config * stamp) Symtab.table
151 val empty = Symtab.empty
154 Symtab.merge (eq_snd (op =)) data
155 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
158 fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
161 val no_sosN = "no_sos"
163 val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
168 fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
170 val tstp_proof_delims =
171 [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
172 ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
174 val e_smartN = "smart"
176 val e_fun_weightN = "fun_weight"
177 val e_sym_offset_weightN = "sym_offset_weight"
179 val e_weight_method =
180 Attrib.setup_config_string @{binding atp_e_weight_method} (K e_smartN)
182 val e_default_fun_weight =
183 Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
184 val e_fun_weight_base =
185 Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
186 val e_fun_weight_span =
187 Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
188 val e_default_sym_offs_weight =
189 Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
190 val e_sym_offs_weight_base =
191 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
192 val e_sym_offs_weight_span =
193 Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
195 fun e_weight_method_case method fw sow =
196 if method = e_fun_weightN then fw
197 else if method = e_sym_offset_weightN then sow
198 else raise Fail ("unexpected " ^ quote method)
200 fun scaled_e_weight ctxt method w =
202 (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
204 (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
205 |> Real.ceil |> signed_string_of_int
207 fun e_weight_arguments ctxt method weights =
208 if method = e_autoN then
211 (* supplied by Stephan Schulz *)
212 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
213 \--destructive-er-aggressive --destructive-er --presat-simplify \
214 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
215 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
216 \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
218 (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
219 |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
222 |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
224 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
225 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
226 \FIFOWeight(PreferProcessed))'"
228 fun effective_e_weight_method ctxt =
229 if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
231 val e_config : atp_config =
232 {exec = ("E_HOME", "eproof"),
235 fn ctxt => fn _ => fn method => fn timeout => fn weights =>
236 "--tstp-in --tstp-out -l5 " ^ e_weight_arguments ctxt method weights ^
237 " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
238 proof_delims = tstp_proof_delims,
240 known_szs_status_failures @
241 [(TimedOut, "Failure: Resource limit exceeded (time)"),
242 (TimedOut, "time limit exceeded"),
243 (OutOfResources, "# Cannot determine problem status")],
244 conj_sym_kind = Hypothesis,
245 prem_kind = Conjecture,
246 best_slices = fn ctxt =>
247 let val method = effective_e_weight_method ctxt in
249 if method = e_smartN then
250 [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false),
252 (0.334, (true, ((50, FOF, "mono_guards??", combsN, false),
254 (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false),
255 e_sym_offset_weightN)))]
257 [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))]
260 val e = (eN, e_config)
265 val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice)
267 val leo2_config : atp_config =
268 {exec = ("LEO2_HOME", "leo"),
271 fn _ => fn _ => fn sos => fn timeout => fn _ =>
272 "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout)
273 |> sos = sosN ? prefix "--sos ",
274 proof_delims = tstp_proof_delims,
276 known_szs_status_failures @
277 [(TimedOut, "CPU time limit exceeded, terminating")],
278 conj_sym_kind = Axiom,
279 prem_kind = Hypothesis,
280 best_slices = fn ctxt =>
282 [(0.667, (false, ((150, leo2_thf0, "mono_native_higher", liftingN, false),
284 (0.333, (true, ((50, leo2_thf0, "mono_native_higher", liftingN, false),
286 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
289 val leo2 = (leo2N, leo2_config)
294 val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice)
296 val satallax_config : atp_config =
297 {exec = ("SATALLAX_HOME", "satallax"),
300 fn _ => fn _ => fn _ => fn timeout => fn _ =>
301 "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
303 [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
304 known_failures = known_szs_status_failures,
305 conj_sym_kind = Axiom,
306 prem_kind = Hypothesis,
309 K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN,
312 val satallax = (satallaxN, satallax_config)
317 val spass_incompleteN = "incomplete"
319 (* The "-VarWeight=3" option helps the higher-order problems, probably by
320 counteracting the presence of explicit application operators. *)
321 val spass_config : atp_config =
322 {exec = ("ISABELLE_ATP", "scripts/spass"),
323 required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
324 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
325 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
326 \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
327 |> sos = sosN ? prefix "-SOS=1 ",
328 proof_delims = [("Here is a proof", "Formulae used in the proof")],
330 known_perl_failures @
331 [(GaveUp, "SPASS beiseite: Completion found"),
332 (TimedOut, "SPASS beiseite: Ran out of time"),
333 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
334 (MalformedInput, "Undefined symbol"),
335 (MalformedInput, "Free Variable"),
336 (Unprovable, "No formulae and clauses found in input file"),
337 (InternalError, "Please report this error")],
338 conj_sym_kind = Hypothesis,
339 prem_kind = Conjecture,
340 best_slices = fn ctxt =>
342 [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
344 (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false),
346 (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
348 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
351 val spass = (spassN, spass_config)
353 val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_native", combsN, true)
354 val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_native", combsN, true)
355 val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_native", liftingN, true)
358 val spass_new_config : atp_config =
359 {exec = ("SPASS_NEW_HOME", "SPASS"),
361 arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ =>
362 (* TODO: add: -FPDFGProof -FPFCR *)
363 ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
364 (* TODO: not used yet *)
365 |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ",
366 proof_delims = #proof_delims spass_config,
367 known_failures = #known_failures spass_config,
368 conj_sym_kind = #conj_sym_kind spass_config,
369 prem_kind = #prem_kind spass_config,
370 best_slices = fn _ =>
372 [(0.300, (true, (spass_new_slice_1, ""))),
373 (0.333, (true, (spass_new_slice_2, ""))),
374 (0.333, (true, (spass_new_slice_3, "")))]}
376 val spass_new = (spass_newN, spass_new_config)
381 (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on
383 fun is_old_vampire_version () =
384 string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER
386 val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
388 val vampire_config : atp_config =
389 {exec = ("VAMPIRE_HOME", "vampire"),
391 arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
392 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
393 " --proof tptp --output_axiom_names on\
394 \ --forced_options propositional_to_bdd=off\
395 \ --thanks \"Andrei and Krystof\" --input_file"
396 |> sos = sosN ? prefix "--sos on ",
398 [("=========== Refutation ==========",
399 "======= End of refutation ======="),
400 ("% SZS output start Refutation", "% SZS output end Refutation"),
401 ("% SZS output start Proof", "% SZS output end Proof")],
403 known_szs_status_failures @
404 [(GaveUp, "UNPROVABLE"),
405 (GaveUp, "CANNOT PROVE"),
406 (Unprovable, "Satisfiability detected"),
407 (Unprovable, "Termination reason: Satisfiable"),
408 (Interrupted, "Aborted by signal SIGINT")],
409 conj_sym_kind = Conjecture,
410 prem_kind = Conjecture,
411 best_slices = fn ctxt =>
413 (if is_old_vampire_version () then
414 [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false),
416 (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false),
418 (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false),
421 [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
422 combs_or_liftingN, false), sosN))),
423 (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN,
425 (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN,
427 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
430 val vampire = (vampireN, vampire_config)
433 (* Z3 with TPTP syntax *)
435 val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit)
437 val z3_tptp_config : atp_config =
438 {exec = ("Z3_HOME", "z3"),
440 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
441 "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
443 known_failures = known_szs_status_failures,
444 conj_sym_kind = Hypothesis,
445 prem_kind = Hypothesis,
448 K [(0.5, (false, ((250, z3_tff0, "mono_native", combsN, false), ""))),
449 (0.25, (false, ((125, z3_tff0, "mono_native", combsN, false), ""))),
450 (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))),
451 (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))]}
453 val z3_tptp = (z3_tptpN, z3_tptp_config)
456 (* Not really a prover: Experimental Polymorphic TFF and THF output *)
458 fun dummy_config format type_enc : atp_config =
459 {exec = ("ISABELLE_ATP", "scripts/dummy_atp"),
461 arguments = K (K (K (K (K "")))),
463 known_failures = known_szs_status_failures,
464 conj_sym_kind = Hypothesis,
465 prem_kind = Hypothesis,
467 K [(1.0, (false, ((200, format, type_enc,
468 if is_format_higher_order format then keep_lamsN
469 else combsN, false), "")))]}
471 val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
472 val dummy_tff1_config = dummy_config dummy_tff1_format "poly_native"
473 val dummy_tff1 = (dummy_tff1N, dummy_tff1_config)
475 val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
476 val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
477 val dummy_thf = (dummy_thfN, dummy_thf_config)
480 (* Remote ATP invocation via SystemOnTPTP *)
482 val systems = Synchronized.var "atp_systems" ([] : string list)
485 case Isabelle_System.bash_output
486 "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
487 (output, 0) => split_lines output
489 error (case extract_known_failure known_perl_failures output of
490 SOME failure => string_for_failure failure
491 | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
493 fun find_system name [] systems =
494 find_first (String.isPrefix (name ^ "---")) systems
495 | find_system name (version :: versions) systems =
496 case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
497 NONE => find_system name versions systems
500 fun get_system name versions =
501 Synchronized.change_result systems
502 (fn systems => (if null systems then get_systems () else systems)
503 |> `(`(find_system name versions)))
505 fun the_system name versions =
506 case get_system name versions of
508 | (NONE, []) => error ("SystemOnTPTP is currently not available.")
510 error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
511 "(Available systems: " ^ commas_quote syss ^ ".)")
513 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
515 fun remote_config system_name system_versions proof_delims known_failures
516 conj_sym_kind prem_kind best_slice : atp_config =
517 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
519 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
520 "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
521 " -s " ^ the_system system_name system_versions,
522 proof_delims = union (op =) tstp_proof_delims proof_delims,
523 known_failures = known_failures @ known_perl_failures @ known_says_failures,
524 conj_sym_kind = conj_sym_kind,
525 prem_kind = prem_kind,
526 best_slices = fn ctxt => [(1.0, (false, (best_slice ctxt, "")))]}
528 fun remotify_config system_name system_versions best_slice
529 ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
530 : atp_config) : atp_config =
531 remote_config system_name system_versions proof_delims known_failures
532 conj_sym_kind prem_kind best_slice
534 fun remote_atp name system_name system_versions proof_delims known_failures
535 conj_sym_kind prem_kind best_slice =
536 (remote_prefix ^ name,
537 remote_config system_name system_versions proof_delims known_failures
538 conj_sym_kind prem_kind best_slice)
539 fun remotify_atp (name, config) system_name system_versions best_slice =
540 (remote_prefix ^ name,
541 remotify_config system_name system_versions best_slice config)
543 val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit)
546 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
547 (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *))
549 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
550 (K (100, leo2_thf0, "mono_native_higher", liftingN, false) (* FUDGE *))
551 val remote_satallax =
552 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
553 (K (100, satallax_thf0, "mono_native_higher", keep_lamsN, false)
556 remotify_atp vampire "Vampire" ["1.8"]
557 (K (250, FOF, "mono_guards??", combs_or_liftingN, false) (* FUDGE *))
559 remotify_atp z3_tptp "Z3" ["3.0"]
560 (K (250, z3_tff0, "mono_native", combsN, false) (* FUDGE *))
562 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
563 Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *))
565 remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
566 (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
567 val remote_iprover_eq =
568 remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
569 (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
571 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
572 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
573 (K (100, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *))
575 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
577 (K (150, explicit_tff0, "mono_native", liftingN, false) (* FUDGE *))
578 val remote_waldmeister =
579 remote_atp waldmeisterN "Waldmeister" ["710"]
580 [("#START OF PROOF", "Proved Goals:")]
581 [(OutOfResources, "Too many function symbols"),
582 (Crashed, "Unrecoverable Segmentation Fault")]
583 Hypothesis Hypothesis
584 (K (50, CNF_UEQ, "mono_tags??", combsN, false) (* FUDGE *))
588 fun add_atp (name, config) thy =
589 Data.map (Symtab.update_new (name, (config, stamp ()))) thy
590 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
592 fun get_atp thy name =
593 the (Symtab.lookup (Data.get thy) name) |> fst
594 handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
596 val supported_atps = Symtab.keys o Data.get
598 fun is_atp_installed thy name =
599 let val {exec, required_execs, ...} = get_atp thy name in
600 forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
603 fun refresh_systems_on_tptp () =
604 Synchronized.change systems (fn _ => get_systems ())
607 [e, leo2, dummy_tff1, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp,
608 remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
609 remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
611 val setup = fold add_atp atps