src/HOL/Tools/res_atp.ML
changeset 16675 96bdc59afc05
parent 16520 7a9cda53bfa2
child 16741 7a6c17b826c0
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jul 04 15:15:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Jul 04 15:51:56 2005 +0200
     1.3 @@ -48,7 +48,6 @@
     1.4  (*val spass = ref true;*)
     1.5  
     1.6  val custom_spass = ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub","-DocProof","-TimeLimit=60"];
     1.7 -
     1.8  val vampire = ref false;
     1.9  
    1.10  val trace_res = ref false;
    1.11 @@ -209,7 +208,7 @@
    1.12       else
    1.13         let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    1.14         in  
    1.15 -	   ([("vampire", thmstr, goalstring, vampire, "-t 300%-m 100000", 
    1.16 +	   ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000", 
    1.17  	      clasimpfile, axfile, hypsfile, probfile)] @ 
    1.18  	    (make_atp_list xs sign (n+1)))
    1.19         end