diff --git a/names.sml b/names.sml
index 7f59984..a447a27 100755
--- a/names.sml
+++ b/names.sml
@@ -1133,7 +1133,7 @@ val spass_windows_binary = (case Paths.findFileWithPossibleSuffix("SPASS",".exe"
 
 val spass_binary = if (Paths.is_unix) then Paths.findIterated(["spass","SPASS"],"./SPASS") else spass_windows_binary
 
-val vampire_linux_binary = Paths.findIterated(["vampire","vampire_linux64","vampire_lin64"],"./vampire")
+val vampire_linux_binary = Paths.findIterated(["vampire_z3_rel_static_sledge_5980"],"./vampire_z3_rel_static_sledge_5980")
 			     
 val vampire_binary = (case Paths.findFileWithPossibleSuffix("vampire",".exe") of
                                    SOME(str) => str
diff --git a/topenv_part2.sml b/topenv_part2.sml
index b4df006..66559ea 100644
--- a/topenv_part2.sml
+++ b/topenv_part2.sml
@@ -1881,7 +1881,7 @@ fun findLine(in_stream,l) = let fun loop() =
 			             in
                                        if line = "" then false
 				       else
-				         if line = l then true else loop()
+				         if (String.isSubstring l line) then true else loop()
  				     end
 			           in 
 				      loop()
@@ -2915,7 +2915,7 @@ fun unLimVampireProvePrimMethod([v,listVal(hyp_vals)],env,ab) =
 
 fun polyVProve(goal, premises,env,ab,max_seconds,mono:bool,subsorting:bool) = 
   let val vi = getVampIndex()
-      val (vamp_in_fname,vamp_out_fname) = (Paths.vampireInName(vi),Paths.vampireOutName(vi))
+      val (vamp_in_fname,vamp_out_fname,vamp_error_fname) = (Paths.vampireInName(vi),Paths.vampireOutName(vi),Paths.vampireErrorName(vi))
       val ax_index = ref(0)
       val premise_array = Array.fromList(premises)
       fun getAxNum() = (Basic.inc(ax_index);"ax"^(Int.toString(!ax_index)))
@@ -2946,7 +2946,7 @@ fun polyVProve(goal, premises,env,ab,max_seconds,mono:bool,subsorting:bool) =
       fun write(str) = TextIO.output(vamp_problem_stream,str)
       val _ = (List.app write hyps;write conc)
       val _ = TextIO.closeOut(vamp_problem_stream)
-      val cmd = Names.vampire_binary ^ " --proof tptp --show_skolemisations on --time_limit "^max_seconds^" --input_file "^vamp_in_fname^" > "^vamp_out_fname
+      val cmd = Names.vampire_binary ^ " --proof tptp --mode casc --show_skolemisations on --time_limit "^max_seconds^" --input_file "^vamp_in_fname^" > "^vamp_out_fname ^ " 2> " ^ vamp_error_fname 
       val _ = OS.Process.system(cmd)
       val vamp_answer_stream = TextIO.openIn(vamp_out_fname)
       val answer_bit = findLine(vamp_answer_stream,vamp_proof_line)