# HG changeset patch # User desharna # Date 1614928954 -3600 # Node ID 39826af584bf516296ad4fb765fc8d9e0a46d6d5 # Parent 96ef620c8b1eda5a1f9a366c4e5366df14ce5295# Parent 3bb9df8900fdc56439616fb134b4e3e2817f2f48 merged diff -r 3bb9df8900fd -r 39826af584bf src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Thu Mar 04 22:46:44 2021 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Fri Mar 05 08:22:34 2021 +0100 @@ -56,7 +56,6 @@ val _ = problem |> lines_of_atp_problem format ord (K []) |> File.write_list prob_file - val exec = exec false val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = File.bash_path (Path.explode path) ^ " " ^ diff -r 3bb9df8900fd -r 39826af584bf src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Mar 04 22:46:44 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Mar 05 08:22:34 2021 +0100 @@ -14,7 +14,7 @@ type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = - {exec : bool -> string list * string list, + {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, @@ -73,7 +73,7 @@ type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = - {exec : bool -> string list * string list, + {exec : string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, @@ -165,7 +165,7 @@ (* agsyHOL *) val agsyhol_config : atp_config = - {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]), + {exec = (["AGSYHOL_HOME"], ["agsyHOL"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = tstp_proof_delims, @@ -183,7 +183,7 @@ (* Alt-Ergo *) val alt_ergo_config : atp_config = - {exec = K (["WHY3_HOME"], ["why3"]), + {exec = (["WHY3_HOME"], ["why3"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, @@ -272,7 +272,7 @@ end val e_config : atp_config = - {exec = fn _ => (["E_HOME"], ["eprover"]), + {exec = (["E_HOME"], ["eprover"]), arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => "--auto-schedule --tstp-in --tstp-out --silent " ^ @@ -320,7 +320,7 @@ (* iProver *) val iprover_config : atp_config = - {exec = K (["IPROVER_HOME"], ["iproveropt", "iprover"]), + {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--clausifier \"$E_HOME\"/eprover " ^ "--clausifier_options \"--tstp-format --silent --cnf\" " ^ @@ -342,7 +342,7 @@ (* LEO-II *) val leo2_config : atp_config = - {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]), + {exec = (["LEO2_HOME"], ["leo.opt", "leo"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => "--foatp e --atp e=\"$E_HOME\"/eprover \ \--atp epclextract=\"$E_HOME\"/epclextract \ @@ -368,7 +368,7 @@ (* Include choice? Disabled now since it's disabled for Satallax as well. *) val leo3_config : atp_config = - {exec = K (["LEO3_HOME"], ["leo3"]), + {exec = (["LEO3_HOME"], ["leo3"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \ \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ @@ -389,7 +389,7 @@ (* Choice is disabled until there is proper reconstruction for it. *) val satallax_config : atp_config = - {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), + {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => (case getenv "E_HOME" of "" => "" @@ -418,34 +418,38 @@ val spass_H2SOS = "-Heuristic=2 -SOS" val spass_config : atp_config = - {exec = K (["SPASS_HOME"], ["SPASS"]), - arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ => - "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ - "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name - |> extra_options <> "" ? prefix (extra_options ^ " "), - proof_delims = [("Here is a proof", "Formulae used in the proof")], - known_failures = - [(GaveUp, "SPASS beiseite: Completion found"), - (TimedOut, "SPASS beiseite: Ran out of time"), - (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), - (MalformedInput, "Undefined symbol"), - (MalformedInput, "Free Variable"), - (Unprovable, "No formulae and clauses found in input file"), - (InternalError, "Please report this error")] @ - known_perl_failures, - prem_role = Conjecture, - best_slices = fn _ => - (* FUDGE *) - [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")), - (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)), - (0.1666, (((50, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)), - (0.1000, (((250, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)), - (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)), - (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), - (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)), - (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))], - best_max_mono_iters = default_max_mono_iters, - best_max_new_mono_instances = default_max_new_mono_instances} + let + val format = DFG Monomorphic + in + {exec = (["SPASS_HOME"], ["SPASS"]), + arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ => + "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ + "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name + |> extra_options <> "" ? prefix (extra_options ^ " "), + proof_delims = [("Here is a proof", "Formulae used in the proof")], + known_failures = + [(GaveUp, "SPASS beiseite: Completion found"), + (TimedOut, "SPASS beiseite: Ran out of time"), + (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), + (MalformedInput, "Undefined symbol"), + (MalformedInput, "Free Variable"), + (Unprovable, "No formulae and clauses found in input file"), + (InternalError, "Please report this error")] @ + known_perl_failures, + prem_role = Conjecture, + best_slices = fn _ => + (* FUDGE *) + [(0.1667, (((150, meshN), format, "mono_native", combsN, true), "")), + (0.1667, (((500, meshN), format, "mono_native", liftingN, true), spass_H2SOS)), + (0.1666, (((50, meshN), format, "mono_native", liftingN, true), spass_H2LR0LT0)), + (0.1000, (((250, meshN), format, "mono_native", combsN, true), spass_H2NuVS0)), + (0.1000, (((1000, mepoN), format, "mono_native", liftingN, true), spass_H1SOS)), + (0.1000, (((150, meshN), format, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), + (0.1000, (((300, meshN), format, "mono_native", combsN, true), spass_H2SOS)), + (0.1000, (((100, meshN), format, "mono_native", combs_and_liftingN, true), spass_H2))], + best_max_mono_iters = default_max_mono_iters, + best_max_new_mono_instances = default_max_new_mono_instances} + end val spass = (spassN, fn () => spass_config) @@ -486,32 +490,36 @@ "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s" val vampire_config : atp_config = - {exec = K (["VAMPIRE_HOME"], ["vampire"]), - arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ => - (check_vampire_noncommercial (); - vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^ - " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ file_name - |> sos = sosN ? prefix "--sos on "), - proof_delims = - [("=========== Refutation ==========", - "======= End of refutation =======")] @ - tstp_proof_delims, - known_failures = - [(GaveUp, "UNPROVABLE"), - (GaveUp, "CANNOT PROVE"), - (Unprovable, "Satisfiability detected"), - (Unprovable, "Termination reason: Satisfiable"), - (Interrupted, "Aborted by signal SIGINT")] @ - known_szs_status_failures, - prem_role = Hypothesis, - best_slices = fn ctxt => - (* FUDGE *) - [(0.333, (((500, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), sosN)), - (0.333, (((150, meshN), TFF (Without_FOOL, Monomorphic), "poly_tags??", combs_or_liftingN, false), sosN)), - (0.334, (((50, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), no_sosN))] - |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single), - best_max_mono_iters = default_max_mono_iters, - best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} + let + val format = TFF (Without_FOOL, Monomorphic) + in + {exec = (["VAMPIRE_HOME"], ["vampire"]), + arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ => + (check_vampire_noncommercial (); + vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^ + " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ file_name + |> sos = sosN ? prefix "--sos on "), + proof_delims = + [("=========== Refutation ==========", + "======= End of refutation =======")] @ + tstp_proof_delims, + known_failures = + [(GaveUp, "UNPROVABLE"), + (GaveUp, "CANNOT PROVE"), + (Unprovable, "Satisfiability detected"), + (Unprovable, "Termination reason: Satisfiable"), + (Interrupted, "Aborted by signal SIGINT")] @ + known_szs_status_failures, + prem_role = Hypothesis, + best_slices = fn ctxt => + (* FUDGE *) + [(0.333, (((500, meshN), format, "mono_native", combs_or_liftingN, false), sosN)), + (0.333, (((150, meshN), format, "poly_tags??", combs_or_liftingN, false), sosN)), + (0.334, (((50, meshN), format, "mono_native", combs_or_liftingN, false), no_sosN))] + |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single), + best_max_mono_iters = default_max_mono_iters, + best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} + end val vampire = (vampireN, fn () => vampire_config) @@ -519,20 +527,24 @@ (* Z3 with TPTP syntax (half experimental, half legacy) *) val z3_tptp_config : atp_config = - {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]), - arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => - "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name, - proof_delims = [("SZS status Theorem", "")], - known_failures = known_szs_status_failures, - prem_role = Hypothesis, - best_slices = - (* FUDGE *) - K [(0.5, (((250, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")), - (0.25, (((125, mepoN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")), - (0.125, (((62, mashN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")), - (0.125, (((31, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), ""))], - best_max_mono_iters = default_max_mono_iters, - best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} + let + val format = TFF (Without_FOOL, Monomorphic) + in + {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]), + arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => + "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name, + proof_delims = [("SZS status Theorem", "")], + known_failures = known_szs_status_failures, + prem_role = Hypothesis, + best_slices = + (* FUDGE *) + K [(0.5, (((250, meshN), format, "mono_native", combsN, false), "")), + (0.25, (((125, mepoN), format, "mono_native", combsN, false), "")), + (0.125, (((62, mashN), format, "mono_native", combsN, false), "")), + (0.125, (((31, meshN), format, "mono_native", combsN, false), ""))], + best_max_mono_iters = default_max_mono_iters, + best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} + end val z3_tptp = (z3_tptpN, fn () => z3_tptp_config) @@ -544,20 +556,24 @@ val zipperposition_cdots = "--mode ho-competitive --boolean-reasoning cases-simpl --ext-rules ext-family --ext-rules-max-depth 1 --ho-prim-enum pragmatic --ho-prim-max 1 --bool-subterm-selection A --avatar off --recognize-injectivity true --ho-elim-leibniz 1 --ho-unif-level full-framework --no-max-vars -q '6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)' -q '6|const|conjecture-relative-var(1.02,l,f)' -q '1|prefer-processed|fifo' -q '1|prefer-non-goals|conjecture-relative-var(1,l,f)' -q '4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)' --select e-selection7 --ho-choice-inst true --sine 50 --sine-tolerance 2 --sine-depth-max 4 --sine-depth-min 1 --scan-clause-ac true --lambdasup 0 --kbo-weight-fun invfreqrank" val zipperposition_config : atp_config = - {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]), - arguments = fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ => - "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name - |> extra_options <> "" ? prefix (extra_options ^ " "), - proof_delims = tstp_proof_delims, - known_failures = known_szs_status_failures, - prem_role = Hypothesis, - best_slices = fn _ => - (* FUDGE *) - [(0.333, (((128, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)), - (0.333, (((32, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)), - (0.334, (((512, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))], - best_max_mono_iters = default_max_mono_iters, - best_max_new_mono_instances = default_max_new_mono_instances} + let + val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice) + in + {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]), + arguments = fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ => + "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name + |> extra_options <> "" ? prefix (extra_options ^ " "), + proof_delims = tstp_proof_delims, + known_failures = known_szs_status_failures, + prem_role = Hypothesis, + best_slices = fn _ => + (* FUDGE *) + [(0.333, (((128, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)), + (0.333, (((32, "meshN"), format, "poly_native_higher", keep_lamsN, false), zipperposition_s6)), + (0.334, (((512, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_cdots))], + best_max_mono_iters = default_max_mono_iters, + best_max_new_mono_instances = default_max_new_mono_instances} + end val zipperposition = (zipperpositionN, fn () => zipperposition_config) @@ -604,7 +620,7 @@ val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice = - {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]), + {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]), arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ => (if command <> "" then "-c " ^ quote command ^ " " else "") ^ "-s " ^ the_remote_system system_name system_versions ^ " " ^ @@ -666,7 +682,7 @@ (* Dummy prover *) fun dummy_config prem_role format type_enc uncurried_aliases : atp_config = - {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]), + {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]), arguments = K (K (K (K (K (K ""))))), proof_delims = [], known_failures = known_szs_status_failures, @@ -698,7 +714,7 @@ fun is_atp_installed thy name = let val {exec, ...} = get_atp thy name () in - exists (fn var => getenv var <> "") (fst (exec false)) + exists (fn var => getenv var <> "") (fst exec) end fun refresh_systems_on_tptp () = diff -r 3bb9df8900fd -r 39826af584bf src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Mar 04 22:46:44 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Mar 05 08:22:34 2021 +0100 @@ -158,7 +158,6 @@ Path.explode dest_dir + problem_file_name else error ("No such directory: " ^ quote dest_dir) - val exec = exec full_proofs val command0 = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => diff -r 3bb9df8900fd -r 39826af584bf src/HOL/Tools/monomorph.ML --- a/src/HOL/Tools/monomorph.ML Thu Mar 04 22:46:44 2021 +0100 +++ b/src/HOL/Tools/monomorph.ML Fri Mar 05 08:22:34 2021 +0100 @@ -37,6 +37,7 @@ val max_new_instances: int Config.T val max_thm_instances: int Config.T val max_new_const_instances_per_round: int Config.T + val max_duplicated_instances: int Config.T (* monomorphization *) val monomorph: (term -> typ list Symtab.table) -> Proof.context -> @@ -74,6 +75,9 @@ val max_new_const_instances_per_round = Attrib.setup_config_int \<^binding>\monomorph_max_new_const_instances_per_round\ (K 5) +val max_duplicated_instances = + Attrib.setup_config_int \<^binding>\monomorph_max_duplicated_instances\ (K 16000) + fun limit_rounds ctxt f = let val max = Config.get ctxt max_rounds @@ -173,28 +177,32 @@ | add _ = I in Term.fold_aterms add (Thm.prop_of thm) end -fun add_insts max_instances max_thm_insts ctxt round used_grounds +fun add_insts max_instances max_duplicated_instances max_thm_insts ctxt round used_grounds new_grounds id thm tvars schematics cx = let exception ENOUGH of - typ list Symtab.table * (int * ((int * (sort * typ) Vartab.table) * thm) list Inttab.table) + typ list Symtab.table * (int * int * ((int * (sort * typ) Vartab.table) * thm) list Inttab.table) val thy = Proof_Context.theory_of ctxt - fun add subst (cx as (next_grounds, (n, insts))) = - if n >= max_instances then + fun add subst (cx as (next_grounds, (hits, misses, insts))) = + if hits >= max_instances orelse misses >= max_duplicated_instances then raise ENOUGH cx else let val thm' = instantiate ctxt subst thm val rthm = ((round, subst), thm') - val rthms = Inttab.lookup_list insts id; + val rthms = Inttab.lookup_list insts id val n_insts' = if member (eq_snd Thm.eq_thm) rthms rthm then - (n, insts) + (hits, misses + 1, insts) else - (if length rthms >= max_thm_insts then n else n + 1, - Inttab.cons_list (id, rthm) insts) + let + val (hits', misses') = + if length rthms >= max_thm_insts then (hits, misses + 1) else (hits + 1, misses) + in + (hits', misses', Inttab.cons_list (id, rthm) insts) + end val next_grounds' = add_new_grounds used_grounds new_grounds thm' next_grounds in (next_grounds', n_insts') end @@ -241,17 +249,20 @@ fun is_new round initial_round = (round = initial_round) fun is_active round initial_round = (round > initial_round) -fun find_instances max_instances max_thm_insts max_new_grounds thm_infos ctxt round - (known_grounds, new_grounds0, insts) = +fun find_instances max_instances max_duplicated_instances max_thm_insts max_new_grounds thm_infos + ctxt round (known_grounds, new_grounds0, insts) = let val new_grounds = Symtab.map (fn _ => fn grounds => if length grounds <= max_new_grounds then grounds else take max_new_grounds (sort Term_Ord.typ_ord grounds)) new_grounds0 - val add_new = add_insts max_instances max_thm_insts ctxt round - fun consider_all pred f (cx as (_, (n, _))) = - if n >= max_instances then cx else fold_schematics pred f thm_infos cx + val add_new = add_insts max_instances max_duplicated_instances max_thm_insts ctxt round + fun consider_all pred f (cx as (_, (hits, misses, _))) = + if hits >= max_instances orelse misses >= max_duplicated_instances then + cx + else + fold_schematics pred f thm_infos cx val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds) val empty_grounds = clear_grounds known_grounds' @@ -274,11 +285,12 @@ val empty_grounds = clear_grounds known_grounds val max_instances = Config.get ctxt max_new_instances |> fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos + val max_duplicated_instances = Config.get ctxt max_duplicated_instances + val (_, _, (_, _, insts)) = + limit_rounds ctxt (find_instances max_instances max_duplicated_instances max_thm_insts + max_new_grounds thm_infos) (empty_grounds, known_grounds, (0, 0, Inttab.empty)) in - (empty_grounds, known_grounds, (0, Inttab.empty)) - |> limit_rounds ctxt (find_instances max_instances max_thm_insts - max_new_grounds thm_infos) - |> (fn (_, _, (_, insts)) => insts) + insts end