309 fn ctxt => fn _ => fn heuristic => fn timeout => |
309 fn ctxt => fn _ => fn heuristic => fn timeout => |
310 fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => |
310 fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => |
311 "--tstp-in --tstp-out --output-level=5 --silent " ^ |
311 "--tstp-in --tstp-out --output-level=5 --silent " ^ |
312 e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^ |
312 e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^ |
313 e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^ |
313 e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^ |
314 "--term-ordering=" ^ (if is_lpo then "LPO4" else "Auto") ^ " " ^ |
314 "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ |
315 "--cpu-limit=" ^ string_of_int (to_secs 2 timeout), |
315 "--cpu-limit=" ^ string_of_int (to_secs 2 timeout), |
316 proof_delims = tstp_proof_delims, |
316 proof_delims = tstp_proof_delims, |
317 known_failures = |
317 known_failures = |
318 known_szs_status_failures @ |
318 known_szs_status_failures @ |
319 [(TimedOut, "Failure: Resource limit exceeded (time)"), |
319 [(TimedOut, "Failure: Resource limit exceeded (time)"), |