--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 01 16:07:34 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Aug 01 19:32:10 2014 +0200
@@ -397,17 +397,16 @@
(* LEO-II *)
-(* LEO-II supports definitions, but it performs significantly better on our
- benchmarks when they are not used. *)
val leo2_thf0 = THF (Monomorphic, THF_Without_Choice)
val leo2_config : atp_config =
{exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- "--foatp e --atp e=\"$E_HOME\"/eprover \
- \--atp epclextract=\"$E_HOME\"/epclextract \
- \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
- file_name,
+ arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
+ "--foatp e --atp e=\"$E_HOME\"/eprover \
+ \--atp epclextract=\"$E_HOME\"/epclextract \
+ \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
+ (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^
+ file_name,
proof_delims = tstp_proof_delims,
known_failures =
[(TimedOut, "CPU time limit exceeded, terminating"),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 16:07:34 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 19:32:10 2014 +0200
@@ -47,7 +47,7 @@
val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
val e_skolemize_rule = "skolemize"
-val leo2_extcnf_combined_rule = "extcnf_combined"
+val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
val satallax_skolemize_rule = "tab_ex"
val spass_pirate_datatype_rule = "DT"
val vampire_skolemisation_rule = "skolemisation"
@@ -61,10 +61,8 @@
val z3_th_lemma_rule = "th-lemma"
val zipperposition_cnf_rule = "cnf"
-(* Unfortunately, LEO-II's "extcnf_combined" rule captures clausification in general and not only
- skolemization. *)
val skolemize_rules =
- [e_skolemize_rule, leo2_extcnf_combined_rule, satallax_skolemize_rule, spass_skolemize_rule,
+ [e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule,
vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule,
zipperposition_cnf_rule]