--- a/src/HOL/TPTP/atp_problem_import.ML Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Wed Jun 06 10:35:05 2012 +0200
@@ -290,11 +290,13 @@
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.vampireN
+ val (last_hope_atp, last_hope_aggressive) =
+ if demo then (ATP_Systems.satallaxN, 0) else (ATP_Systems.vampireN, 2)
in
(can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
- can_tac ctxt (atp_tac ctxt 2 [] timeout last_hope 1) conj)
+ can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
+ (atp_tac ctxt last_hope_aggressive [] timeout last_hope_atp 1)) conj)
|> print_szs_from_success conjs
end