src/HOL/TPTP/atp_problem_import.ML
changeset 48086 5b87cfc300f9
parent 48083 a4148c95134d
child 48143 0186df5074c8
equal deleted inserted replaced
48085:ff5e900d7b1a 48086:5b87cfc300f9
   210     fun slice mult aggressivity prover =
   210     fun slice mult aggressivity prover =
   211       SOLVE_TIMEOUT (mult * timeout div frac)
   211       SOLVE_TIMEOUT (mult * timeout div frac)
   212           (prover ^
   212           (prover ^
   213            (if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")"
   213            (if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")"
   214             else ""))
   214             else ""))
   215           (atp_tac ctxt aggressivity [] (timeout div frac) prover i)
   215           (atp_tac ctxt aggressivity [] (mult * timeout div frac) prover i)
   216   in
   216   in
   217     slice 2 0 ATP_Systems.spassN
   217     slice 2 0 ATP_Systems.spassN
   218     ORELSE slice 2 0 ATP_Systems.vampireN
   218     ORELSE slice 2 0 ATP_Systems.vampireN
   219     ORELSE slice 2 0 ATP_Systems.eN
   219     ORELSE slice 2 0 ATP_Systems.eN
   220     ORELSE slice 2 0 ATP_Systems.z3_tptpN
   220     ORELSE slice 2 0 ATP_Systems.z3_tptpN