46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maeder{- |

46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederModule : $Header$

46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederDescription : Interface to the theorem prover e-krhyper in CASC-mode.

46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2010

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederMaintainer : luecke@informatik.uni-bremen.de

46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederStability : provisional

46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederPortability : needs POSIX

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maeder

46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederCheck out

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederfor details. For the ease of maintenance we are using e-krhyper in

a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian Maederits CASC-mode, aka tptp-input. It works for single input files and

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederfof-style.

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maeder-}

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maedermodule SoftFOL.ProveHyperHyper (hyperProver)

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder where

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maederimport Logic.Prover

3f9fabb8ac5cfd9234431ecf19b51ff3e985595aChristian Maeder

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maederimport Common.ProofTree

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport qualified Common.Result as Result

df0e8744a2befcba003ea6d93214601c743bde74Christian Maederimport Common.AS_Annotation as AS_Anno

df0e8744a2befcba003ea6d93214601c743bde74Christian Maeder

0607966fab6924a9fda8b55a9dccb28236a856deSimon Ulbrichtimport SoftFOL.Sign

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maederimport SoftFOL.Translate

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport SoftFOL.ProverState

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport GUI.GenericATP

df0e8744a2befcba003ea6d93214601c743bde74Christian Maederimport Proofs.BatchProcessing

9aec0bc9d57df2669c8095fb1b4bd954d80b5537Christian Maederimport Interfaces.GenericATPState

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maederimport System.IO

b8cd2804f426fd97148615fe31c1f47afac7a683Christian Maederimport System.Process

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport System.Posix.Time

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport System.Directory

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maeder

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport Control.Monad (when)

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport qualified Control.Concurrent as Concurrent

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport Common.Utils(trim)

d864f0a0e04e61b5f87963496765eafcf646ed7bChristian Maederimport Data.List

d864f0a0e04e61b5f87963496765eafcf646ed7bChristian Maeder

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport Data.Time (timeToTimeOfDay)

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport Data.Time.LocalTime(TimeOfDay(..))

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport Data.Time.Clock (UTCTime(..), secondsToDiffTime, getCurrentTime)

d864f0a0e04e61b5f87963496765eafcf646ed7bChristian Maeder

d864f0a0e04e61b5f87963496765eafcf646ed7bChristian Maeder{- | The Prover implementation. -}

a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian MaederhyperProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree

6204e46b2e31a71e6e98c6ecc5efc11e61a76a01Christian MaederhyperProver = mkAutomaticProver "ekrhyper" () hyperGUI hyperCMDLautomaticBatch

df0e8744a2befcba003ea6d93214601c743bde74Christian Maeder

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder{- |

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder Record for prover specific functions. This is used by both GUI and command

a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder line interface.

59bbf8aeab565e86d79c8482a4c7bd7a1841ca7bChristian Maeder-}

d83bd347856e87ba96c0c8e0c5b473db4eb975d0Christian MaederatpFun :: String -- ^ theory name

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState

59bbf8aeab565e86d79c8482a4c7bd7a1841ca7bChristian MaederatpFun thName = ATPFunctions

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder { initialProverState = spassProverState

59bbf8aeab565e86d79c8482a4c7bd7a1841ca7bChristian Maeder , atpTransSenName = transSenName

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder , atpInsertSentence = insertSentenceGen

59bbf8aeab565e86d79c8482a4c7bd7a1841ca7bChristian Maeder , goalOutput = showTPTPProblem thName

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder , proverHelpText = "for more information visit " ++

59bbf8aeab565e86d79c8482a4c7bd7a1841ca7bChristian Maeder "http://www.uni-koblenz.de/~bpelzer/ekrhyper/"

b8cd2804f426fd97148615fe31c1f47afac7a683Christian Maeder , batchTimeEnv = "HETS_HYPER_BATCH_TIME_LIMIT"

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder , fileExtensions = FileExtensions

59bbf8aeab565e86d79c8482a4c7bd7a1841ca7bChristian Maeder { problemOutput = ".tptp"

59bbf8aeab565e86d79c8482a4c7bd7a1841ca7bChristian Maeder , proverOutput = ".hyper"

b8cd2804f426fd97148615fe31c1f47afac7a683Christian Maeder , theoryConfiguration = ".hypcf" }

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder , runProver = runHyper

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder , createProverOptions = extraOpts }

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder{- |

59bbf8aeab565e86d79c8482a4c7bd7a1841ca7bChristian Maeder Invokes the generic prover GUI.

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maeder-}

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian MaederhyperGUI :: String -- ^ theory name

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder -> Theory Sign Sentence ProofTree

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder -- ^ theory consisting of a SoftFOL.Sign.Sign

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder -- and a list of Named SoftFOL.Sign.Sentence

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder -> IO([ProofStatus ProofTree]) -- ^ proof status for each goal

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian MaederhyperGUI thName th freedefs =

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder genericATPgui (atpFun thName) True (proverName hyperProver) thName th

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder freedefs emptyProofTree

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder{- |

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder automatic command line interface to the prover.

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder-}

f0d823af5e37881b77328bbcff8c96b58b92c89fChristian MaederhyperCMDLautomaticBatch ::

081deee1bac477ab8db717646baba47f0fe95479Christian Maeder Bool -- ^ True means include proved theorems

081deee1bac477ab8db717646baba47f0fe95479Christian Maeder -> Bool -- ^ True means save problem file

081deee1bac477ab8db717646baba47f0fe95479Christian Maeder -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])

081deee1bac477ab8db717646baba47f0fe95479Christian Maeder -- ^ used to store the result of the batch run

081deee1bac477ab8db717646baba47f0fe95479Christian Maeder -> String -- ^ theory name

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder -> TacticScript -- ^ default tactic script

5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder -> Theory Sign Sentence ProofTree -- ^ theory consisting of a

5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder -- 'SoftFOL.Sign.Sign' and a list of Named 'SoftFOL.Sign.Sentence'

5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints

5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder -> IO (Concurrent.ThreadId,Concurrent.MVar ())

5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder -- ^ fst: identifier of the batch thread for killing it

595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht -- snd: MVar to wait for the end of the thread

595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon UlbrichthyperCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar

595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht thName defTS th freedefs =

595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch

595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht resultMVar (proverName hyperProver) thName

595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

4e1239f8b5fa139bd9be8d0431d711c7b88a58c2Christian Maeder

5b68f1141555736e0b7ddbe14218bcabcc44636fChristian MaederprelTxt :: Int -> String

863c98ae89e37c21c0c04b9b130b5136688976eeChristian MaederprelTxt t =

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder "% only print essential output\n" ++

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder "#(set_verbosity(1)).\n\n" ++

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder "% assume all input to be in tptp-syntax\n" ++

e4147f07c61def118b6052ccdf57207b0c113921Simon Ulbricht "#(set_parameter(input_type, 2)).\n\n" ++

595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht "% To prevent blowing up my memory\n" ++

e3d7fd1b63d824960b1c17b6c7009d52d7528c1eChristian Maeder "#(set_memory_limit(500)).\n\n" ++

e3d7fd1b63d824960b1c17b6c7009d52d7528c1eChristian Maeder "% produce SZS results\n" ++

e3d7fd1b63d824960b1c17b6c7009d52d7528c1eChristian Maeder "#(set_flag(szs_output_flag, true)).\n\n" ++

e3d7fd1b63d824960b1c17b6c7009d52d7528c1eChristian Maeder "% do not use special evaluable symbols\n" ++

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht "#(clear_builtins).\n\n" ++

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht "% initial term weight bound, 3 recommended for TPTP-problems\n" ++

e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht "#(set_parameter(max_weight_initial, 3)).\n\n" ++

2de7f67ad6bfc38baabe7176c1bad5d8f176bd48Christian Maeder "% Terminate if out of memory\n" ++

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder "#(set_parameter(limit_termination_method,0)).\n\n" ++

3f9fabb8ac5cfd9234431ecf19b51ff3e985595aChristian Maeder "% Terminate if out of time\n" ++

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder "#(set_parameter(timeout_termination_method,0)).\n\n" ++

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder "% Start timer\n" ++

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder "#(start_wallclock_timer("++ show t ++".0)).\n"

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder

3f9fabb8ac5cfd9234431ecf19b51ff3e985595aChristian MaederrunTxt :: String

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian MaederrunTxt =

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder "% start derivation with the input received so far\n" ++

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder "#(run).\n\n" ++

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder "% print normal E-KRHyper proof\n" ++

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder "%#(print_proof).\n\n" ++

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder "% print result and proof using SZS terminology;\n" ++

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder "% requires postprocessing with post_szs script for proper legibility\n" ++

a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian Maeder "%#(print_szs_proof).\n"

3f9fabb8ac5cfd9234431ecf19b51ff3e985595aChristian Maeder

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian MaederrunHyper :: SoftFOLProverState

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder -- ^ logical part containing the input Sign and axioms and possibly

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder -- goals that have been proved earlier as additional axioms

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder -> GenericConfig ProofTree -- ^ configuration to use

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder -> Bool -- ^ True means save TPTP file

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder -> String -- ^ name of the theory in the DevGraph

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder -> AS_Anno.Named SPTerm -- ^ goal to prove

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder -> IO (ATPRetval, GenericConfig ProofTree)

2f2d2bc388803936d992afbb3596ff1c6ebcb197Christian Maeder -- ^ (retval, configuration with proof status and complete output)

863c98ae89e37c21c0c04b9b130b5136688976eeChristian MaederrunHyper sps cfg saveTPTP thName nGoal =

2fe147b05116aea0862eab9c0342b3c4be8ec1fdChristian Maeder let

0607966fab6924a9fda8b55a9dccb28236a856deSimon Ulbricht saveFile = thName++'_':AS_Anno.senAttr nGoal

0607966fab6924a9fda8b55a9dccb28236a856deSimon Ulbricht tmpFile = (reverse $ fst $ span (/='/') $ reverse thName) ++

069541f0927770d9f3eded5e163a815f3e59767fChristian Maeder '_':AS_Anno.senAttr nGoal

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder prelFile = "prelude_" ++ (reverse $ fst $ span (/='/') $ reverse

863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder thName)

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder ++ '_':AS_Anno.senAttr nGoal

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder runFile = "run_" ++ (reverse $ fst $ span (/='/') $ reverse

a58949e654464bf3ae767a41d10d6ffd67d697ecChristian Maeder thName)

c62c1b82e3316ff978475d6e61a5ed172fe60b0bChristian Maeder ++ '_':AS_Anno.senAttr nGoal

eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht simpleOptions = extraOpts cfg

eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht tl = configTimeLimit cfg

eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht in

eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht do

eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht prob <- showTPTPProblem thName sps nGoal $

eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht simpleOptions ++ ["Requested prover: ekrhyper"]

eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht when saveTPTP

34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder (writeFile (saveFile ++".tptp") prob)

d83bd347856e87ba96c0c8e0c5b473db4eb975d0Christian Maeder t <- getCurrentTime

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder let stpTmpFile = "/tmp/" ++ tmpFile ++ (show $ utctDay t) ++

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder "-" ++ (show $ utctDayTime t) ++ ".tptp"

4e1239f8b5fa139bd9be8d0431d711c7b88a58c2Christian Maeder stpPrelFile = "/tmp/" ++ prelFile ++ (show $ utctDay t) ++

eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht "-" ++ (show $ utctDayTime t) ++ ".tme"

eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht stpRunFile = "/tmp/" ++ runFile ++ (show $ utctDay t) ++

c62c1b82e3316ff978475d6e61a5ed172fe60b0bChristian Maeder "-" ++ (show $ utctDayTime t) ++ ".tme"

c62c1b82e3316ff978475d6e61a5ed172fe60b0bChristian Maeder writeFile stpPrelFile $ prelTxt tl

c62c1b82e3316ff978475d6e61a5ed172fe60b0bChristian Maeder writeFile stpRunFile $ runTxt

c62c1b82e3316ff978475d6e61a5ed172fe60b0bChristian Maeder writeFile stpTmpFile $ prob

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder let command = "ekrh " ++ stpPrelFile ++ " " ++ stpTmpFile ++

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder " " ++ stpRunFile

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder t_start <- epochTime

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder (_, stdouth, stderrh, proch) <- runInteractiveCommand command

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder waitForProcess proch

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder t_end <- epochTime

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder removeFile stpPrelFile

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder removeFile stpRunFile

61116f0ae514354dddda28edc7af459e8b23e8b4Christian Maeder removeFile stpTmpFile

54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder let t_t = (round (realToFrac (t_end - t_start + 1) :: Double) :: Integer)

61116f0ae514354dddda28edc7af459e8b23e8b4Christian Maeder let t_u = timeToTimeOfDay $ secondsToDiffTime $

61116f0ae514354dddda28edc7af459e8b23e8b4Christian Maeder if t_t == 0

then

1

else

t_t

stdoutC <- hGetContents stdouth

stderrC <- hGetContents stderrh

(pStat, ret) <- examineProof sps cfg stdoutC stderrC simpleOptions nGoal t_u

return (pStat, cfg

{

proofStatus = ret

, resultOutput = lines (stdoutC ++ stderrC)

, timeUsed = usedTime ret

})

{- | Mapping type from SZS to Hets -}

data HyperResult = HProved | HDisproved | HTimeout | HError | HMemout

{- | examine SZS output -}

examineProof :: SoftFOLProverState

-> GenericConfig ProofTree

-> String

-> String

-> [String]

-> AS_Anno.Named SPTerm

-> TimeOfDay

-> IO (ATPRetval, ProofStatus ProofTree)

examineProof sps cfg stdoutC stderrC simpleOptions nGoal tUsed =

let

tScript opts = TacticScript $ show ATPTacticScript

{ tsTimeLimit = configTimeLimit cfg

, tsExtraOpts = opts }

defaultStatus =

ProofStatus { goalName = senAttr nGoal

, goalStatus = openGoalStatus

, usedAxioms = []

, usedProver = proverName hyperProver

, proofTree = emptyProofTree

, usedTime = tUsed

, tacticScript = tScript simpleOptions}

out = filter ("% SZS status " `isPrefixOf`) $

lines (stdoutC ++ stderrC)

getAxioms =

let

fl = formulaLists $ initialLogicalPart sps

fs = concatMap formulae $ filter (\x ->

case originType x of

SPOriginAxioms -> True

_ -> False

) fl

in map AS_Anno.senAttr fs

in

do

if (length out /= 1)

then

return (ATPError ("Internal Error in ekrhyper.\nOutput was:\n\n" ++

stdoutC ++ stderrC), defaultStatus)

else

do

let outp = map (trim . drop (length "% SZS status ")) out

let res = case outp of

["Theorem"] -> HProved

["Satisfiable"] -> HProved

["Timeout"] -> HTimeout

["CounterSatisfiable"] -> HDisproved

["Unsatisfiable"] -> HDisproved

["MemoryOut"] -> HMemout

_ -> HError

case res of

HProved -> return (ATPSuccess, defaultStatus

{

goalStatus = Proved True

, usedAxioms = getAxioms

, proofTree = ProofTree $ unlines out

})

HTimeout -> return (ATPTLimitExceeded, defaultStatus)

HDisproved -> return (ATPSuccess, defaultStatus

{

goalStatus = Disproved

, usedAxioms = getAxioms

, proofTree = ProofTree $ unlines out

})

HMemout -> return (ATPError ("Out of Memory."

++ "\nOutput was:\n\n" ++

stdoutC ++ stderrC)

, defaultStatus)

HError -> return (ATPError ("Internal Error in ekrhyper."

++ "\nOutput was:\n\n" ++

stdoutC ++ stderrC)

, defaultStatus)