716 fun remotify_atp (name, config) system_name system_versions best_slice = |
716 fun remotify_atp (name, config) system_name system_versions best_slice = |
717 (remote_prefix ^ name, |
717 (remote_prefix ^ name, |
718 remotify_config system_name system_versions best_slice o config) |
718 remotify_config system_name system_versions best_slice o config) |
719 |
719 |
720 fun gen_remote_waldmeister name = |
720 fun gen_remote_waldmeister name = |
721 remote_atp name "Waldmeister" ["710"] |
721 remote_atp name "Waldmeister" ["710"] tstp_proof_delims |
722 [("#START OF PROOF", "Proved Goals:")] |
722 ([(OutOfResources, "Too many function symbols"), |
723 [(OutOfResources, "Too many function symbols"), |
723 (Inappropriate, "**** Unexpected end of file."), |
724 (Inappropriate, "**** Unexpected end of file."), |
724 (Crashed, "Unrecoverable Segmentation Fault")] |
725 (Crashed, "Unrecoverable Segmentation Fault")] |
725 @ known_szs_status_failures) |
726 Hypothesis |
726 Hypothesis |
727 (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *)) |
727 (K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *)) |
728 |
728 |
729 val explicit_tff0 = TFF Monomorphic |
729 val explicit_tff0 = TFF Monomorphic |
730 |
730 |