diff -r 1d25deb1f185 -r 7df66b448c4a src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Sun Apr 29 11:44:33 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Sun Apr 29 11:44:33 2012 +0200
@@ -10,7 +10,8 @@
   val nitpick_tptp_file : theory -> int -> string -> unit
   val refute_tptp_file : theory -> int -> string -> unit
   val sledgehammer_tptp_file : theory -> int -> string -> unit
-  val isabelle_tptp_file : theory -> int -> string -> unit
+  val isabelle_demo_tptp_file : theory -> int -> string -> unit
+  val isabelle_comp_tptp_file : theory -> int -> string -> unit
   val translate_tptp_file : string -> string -> string -> unit
 end;
 
@@ -175,33 +176,44 @@
       {add = [(Facts.named (Thm.derivation_name ext), [])],
        del = [], only = true}
 
-fun sledgehammer_tac ctxt timeout i =
+fun sledgehammer_tac demo ctxt timeout i =
   let
-    fun slice overload_params fraq prover =
-      SOLVE_TIMEOUT (timeout div fraq) prover
-                    (atp_tac ctxt overload_params (timeout div fraq) prover i)
+    val frac = if demo then 6 else 4
+    fun slice prover =
+      SOLVE_TIMEOUT (timeout div frac) prover
+                    (atp_tac ctxt [] (timeout div frac) prover i)
   in
-    slice [] 5 ATP_Systems.satallaxN
-    ORELSE slice [] 5 ATP_Systems.leo2N
-    ORELSE slice [] 5 ATP_Systems.spassN
-    ORELSE slice [] 5 ATP_Systems.vampireN
-    ORELSE slice [] 5 ATP_Systems.eN
+    (if demo then
+       slice ATP_Systems.satallaxN
+       ORELSE slice ATP_Systems.leo2N
+     else
+       no_tac)
+    ORELSE slice ATP_Systems.spassN
+    ORELSE slice ATP_Systems.vampireN
+    ORELSE slice ATP_Systems.eN
+    ORELSE slice ATP_Systems.z3_tptpN
   end
 
+fun smt_solver_tac solver ctxt =
+  let
+    val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
+  in SMT_Solver.smt_tac ctxt [] end
+
 fun auto_etc_tac ctxt timeout i =
   SOLVE_TIMEOUT (timeout div 20) "nitpick"
       (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "simp"
       (asm_full_simp_tac (simpset_of ctxt) i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
       (auto_tac ctxt
        THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
-  ORELSE SOLVE_TIMEOUT (timeout div 5) "smt" (SMT_Solver.smt_tac ctxt [] i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "z3" (smt_solver_tac "z3" ctxt i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "cvc3" (smt_solver_tac "cvc3" ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
 
 fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
@@ -233,22 +245,27 @@
       read_tptp_file thy (freeze_problem_consts thy) file_name
     val conj = make_conj assms conjs
   in
-    can_tac ctxt (sledgehammer_tac ctxt timeout 1) conj
+    can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
     |> print_szs_from_success conjs
   end
 
-fun isabelle_tptp_file thy timeout file_name =
+fun isabelle_tptp_file demo thy timeout file_name =
   let
     val (conjs, assms, ctxt) =
       read_tptp_file thy (freeze_problem_consts thy) file_name
     val conj = make_conj assms conjs
+    val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.spassN
   in
     (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
-     can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
-     can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj)
+     can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
+     can_tac ctxt (atp_tac ctxt [] timeout last_hope 1) conj)
     |> print_szs_from_success conjs
   end
 
+val isabelle_demo_tptp_file = isabelle_tptp_file true
+val isabelle_comp_tptp_file = isabelle_tptp_file false
+
+
 (** Translator between TPTP(-like) file formats **)
 
 fun translate_tptp_file format in_file_name out_file_name = ()