--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Apr 07 12:37:42 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Apr 08 17:17:21 2022 +0200
@@ -171,8 +171,9 @@
val e_config : atp_config =
{exec = (["E_HOME"], ["eprover-ho", "eprover"]),
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem =>
- ["--tstp-in --tstp-out --silent " ^ extra_options ^ " --cpu-limit=" ^
- string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path problem],
+ ["--tstp-in --tstp-out --silent " ^ extra_options ^
+ " --demod-under-lambda=true --cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
+ " --proof-object=1 " ^ File.bash_path problem],
proof_delims =
[("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
tstp_proof_delims,