src/HOL/TPTP/atp_problem_import.ML

     fun slice mult aggressivity prover =
       SOLVE_TIMEOUT (mult * timeout div frac)
           (prover ^
            (if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")"
             else ""))
-          (atp_tac ctxt aggressivity [] (timeout div frac) prover i)
+          (atp_tac ctxt aggressivity [] (mult * timeout div frac) prover i)
   in
     slice 2 0 ATP_Systems.spassN
     ORELSE slice 2 0 ATP_Systems.vampireN
     ORELSE slice 2 0 ATP_Systems.eN
     ORELSE slice 2 0 ATP_Systems.z3_tptpN