381 known_failures = |
381 known_failures = |
382 known_failures @ known_perl_failures @ |
382 known_failures @ known_perl_failures @ |
383 [(Unprovable, "says Satisfiable"), |
383 [(Unprovable, "says Satisfiable"), |
384 (IncompleteUnprovable, "says Unknown"), |
384 (IncompleteUnprovable, "says Unknown"), |
385 (IncompleteUnprovable, "says GaveUp"), |
385 (IncompleteUnprovable, "says GaveUp"), |
386 (TimedOut, "says Timeout")], |
386 (TimedOut, "says Timeout"), |
|
387 (Inappropriate, "says Inappropriate")], |
387 conj_sym_kind = conj_sym_kind, |
388 conj_sym_kind = conj_sym_kind, |
388 prem_kind = prem_kind, |
389 prem_kind = prem_kind, |
389 formats = formats, |
390 formats = formats, |
390 best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]} |
391 best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]} |
391 |
392 |
418 [("refutation.", "end_refutation.")] [] Hypothesis Conjecture |
419 [("refutation.", "end_refutation.")] [] Hypothesis Conjecture |
419 [TFF, FOF] (K (250, ["simple"]) (* FUDGE *)) |
420 [TFF, FOF] (K (250, ["simple"]) (* FUDGE *)) |
420 val remote_waldmeister = |
421 val remote_waldmeister = |
421 remote_atp waldmeisterN "Waldmeister" ["710"] |
422 remote_atp waldmeisterN "Waldmeister" ["710"] |
422 [("#START OF PROOF", "Proved Goals:")] |
423 [("#START OF PROOF", "Proved Goals:")] |
423 [(OutOfResources, "Too many function symbols")] Hypothesis |
424 [(OutOfResources, "Too many function symbols"), |
424 Hypothesis [CNF_UEQ] (K (100, ["poly_args"]) (* FUDGE *)) |
425 (Crashed, "Unrecoverable Segmentation Fault")] |
|
426 Hypothesis Hypothesis [CNF_UEQ] |
|
427 (K (100, ["poly_args"]) (* FUDGE *)) |
425 |
428 |
426 (* Setup *) |
429 (* Setup *) |
427 |
430 |
428 fun add_atp (name, config) thy = |
431 fun add_atp (name, config) thy = |
429 Data.map (Symtab.update_new (name, (config, stamp ()))) thy |
432 Data.map (Symtab.update_new (name, (config, stamp ()))) thy |