# HG changeset patch # User blanchet # Date 1292583709 -3600 # Node ID 78e4508d2e5438fba52da341809f1f13a61a1328 # Parent 8b6f3917bc7661a5cac8391301a382f888554a8e fewer facts to SInE-E diff -r 8b6f3917bc76 -r 78e4508d2e54 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Dec 17 11:12:37 2010 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Dec 17 12:01:49 2010 +0100 @@ -243,7 +243,7 @@ val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] val remote_sine_e = remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")] - 800 (* FUDGE *) true + 600 (* FUDGE *) true val remote_snark = remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] [] 250 (* FUDGE *) true