diff options
Diffstat (limited to 'source')
| -rw-r--r-- | source/Meaning.hs | 2 | ||||
| -rw-r--r-- | source/Provers.hs | 12 |
2 files changed, 7 insertions, 7 deletions
diff --git a/source/Meaning.hs b/source/Meaning.hs index 00a944f..9b4bc45 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -406,7 +406,7 @@ glossStmt = \case f' <- glossStmt f quantify <- glossQuantifier quantifier pure (quantify vars [constraints] f') - Raw.StmtExists np -> do + Raw.StmtExists np -> do (vars, constraints) <- glossNPList np pure (Sem.makeExists vars constraints) Raw.SymbolicQuantified quant vs bound suchThat have -> do diff --git a/source/Provers.hs b/source/Provers.hs index 37e02ca..273751c 100644 --- a/source/Provers.hs +++ b/source/Provers.hs @@ -82,10 +82,10 @@ vampire path _verbosity timeLimit memoryLimit = Prover , "--time_limit", toSeconds timeLimit , "--memory_limit", toMegabytes memoryLimit ] - , proverSaysYes = ["% SZS output end Proof for"] - , proverSaysNo = ["% SZS status CounterSatisfiable for"] - , proverDoesNotKnow = ["% SZS status Timeout for"] - , proverWarnsContradiction = ["% SZS status ContradictoryAxioms for"] + , proverSaysYes = ["% SZS status Theorem"] + , proverSaysNo = ["% SZS status CounterSatisfiable"] + , proverDoesNotKnow = ["% SZS status Timeout"] + , proverWarnsContradiction = ["% SZS status ContradictoryAxioms"] } -- WIP: setting up a clausifier @@ -96,8 +96,8 @@ iprover _verbosity timeLimit _memoryLimit = Prover , proverArgs = [ "--time_out_real " <> toSeconds timeLimit ] - , proverSaysYes = ["% SZS status Theorem for"] - , proverSaysNo = ["% SZS status CounterSatisfiable for"] + , proverSaysYes = ["% SZS status Theorem"] + , proverSaysNo = ["% SZS status CounterSatisfiable"] , proverDoesNotKnow = ["% SZS status Unknown"] , proverWarnsContradiction = [] } |