--- a/src/HOL/Tools/res_atp.ML Mon Jul 04 15:15:55 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Jul 04 15:51:56 2005 +0200
@@ -48,7 +48,6 @@
(*val spass = ref true;*)
val custom_spass = ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub","-DocProof","-TimeLimit=60"];
-
val vampire = ref false;
val trace_res = ref false;
@@ -209,7 +208,7 @@
else
let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
in
- ([("vampire", thmstr, goalstring, vampire, "-t 300%-m 100000",
+ ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
clasimpfile, axfile, hypsfile, probfile)] @
(make_atp_list xs sign (n+1)))
end