361 known_failures = #known_failures spass_config, |
361 known_failures = #known_failures spass_config, |
362 conj_sym_kind = #conj_sym_kind spass_config, |
362 conj_sym_kind = #conj_sym_kind spass_config, |
363 prem_kind = #prem_kind spass_config, |
363 prem_kind = #prem_kind spass_config, |
364 best_slices = fn _ => |
364 best_slices = fn _ => |
365 (* FUDGE *) |
365 (* FUDGE *) |
366 [(0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN, |
366 [(0.334, (true, (300, DFG DFG_Sorted, "mono_simple", combsN, |
367 spass_incompleteN))), |
367 "" (* spass_incompleteN *)))), |
368 (0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN, |
368 (0.333, (true, (50, DFG DFG_Sorted, "mono_simple", combsN, ""))), |
369 ""))), |
369 (0.333, (true, (150, DFG DFG_Sorted, "mono_simple", liftingN, "")))]} |
370 (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN, "")))]} |
|
371 |
370 |
372 val spass_new = (spass_newN, spass_new_config) |
371 val spass_new = (spass_newN, spass_new_config) |
373 |
372 |
374 |
373 |
375 (* Vampire *) |
374 (* Vampire *) |