d589d7c9f60e62a48f0cc2178c5b972500a192deishmal{- |

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalModule : $Header$

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalDescription : The SZS ontology for TPTP prover results

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalCopyright : (c) Christian Maeder DFKI GmbH 2010

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalLicense : GPLv2 or higher, see LICENSE.txt

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

f52d2fdccd375423dd9b3397990828f27c1b6e72ishmalMaintainer : Christian.Maeder@dfki.de

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalStability : provisional

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalPortability : portable

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalsee <http://www.cs.miami.edu/~tptp/> under Documents and SZSOntology

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal-}

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalmodule Common.SZSOntology where

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalimport Data.Char

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalsuccesses :: [(String, String)]

d589d7c9f60e62a48f0cc2178c5b972500a192deishmalsuccesses =

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal [ ("Success", "SUC")

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal -- The logical data has been processed successfully.

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal , ("UnsatisfiabilityPreserving", "UNP")

cac9aa6475006090bd6d3a75e4964d1af6805266ishmal {- If there does not exist a model of Ax then there does not exist a model of

cac9aa6475006090bd6d3a75e4964d1af6805266ishmal C, i.e., if Ax is unsatisfiable then C is unsatisfiable. -}

cac9aa6475006090bd6d3a75e4964d1af6805266ishmal

f3d3720abcbae388db665983633890de94371df8ishmal , ("SatisfiabilityPreserving", "SAP")

cac9aa6475006090bd6d3a75e4964d1af6805266ishmal {- If there exists a model of Ax then there exists a model of C, i.e., if Ax

cac9aa6475006090bd6d3a75e4964d1af6805266ishmal is satisfiable then C is satisfiable.

f3d3720abcbae388db665983633890de94371df8ishmal - F is satisfiable. -}

cac9aa6475006090bd6d3a75e4964d1af6805266ishmal

f3d3720abcbae388db665983633890de94371df8ishmal , ("EquiSatisfiable", "ESA")

3c208ff1f520c7b749a005157391bea0d7e60b0fishmal {- There exists a model of Ax iff there exists a model of C, i.e., Ax is

3c208ff1f520c7b749a005157391bea0d7e60b0fishmal (un)satisfiable iff C is (un)satisfiable. -}

3c208ff1f520c7b749a005157391bea0d7e60b0fishmal

3c208ff1f520c7b749a005157391bea0d7e60b0fishmal , ("Satisfiable", "SAT")

3c208ff1f520c7b749a005157391bea0d7e60b0fishmal {- Some interpretations are models of Ax, and

cac9aa6475006090bd6d3a75e4964d1af6805266ishmal some models of Ax are models of C.

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal - F is satisfiable, and ~F is not valid.

781f943ec1c021ce4eebe4a549079a48cb8526deishmal - Possible dataforms are Models of Ax | C. -}

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal , ("FinitelySatisfiable", "FSA")

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal {- Some finite interpretations are finite models of Ax, and

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal some finite models of Ax are finite models of C.

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal - F is satisfiable, and ~F is not valid.

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal - Possible dataforms are FiniteModels of Ax | C. -}

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

7092ea0fb59c2fd1af2285468a955620e3889e81ishmal , ("Theorem", "THM")

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal {- All models of Ax are models of C.

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal - F is valid, and C is a theorem of Ax.

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal - Possible dataforms are Proofs of C from Ax. -}

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal , ("Equivalent", "EQV")

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal {- Some interpretations are models of Ax,

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal all models of Ax are models of C, and

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal all models of C are models of Ax.

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal - F is valid, C is a theorem of Ax, and Ax is a theorem of C.

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal - Possible dataforms are Proofs of C from Ax and of Ax from C. -}

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal

d589d7c9f60e62a48f0cc2178c5b972500a192deishmal , ("TautologousConclusion", "TAC")

f3d3720abcbae388db665983633890de94371df8ishmal {- Some interpretations are models of Ax, and

f3d3720abcbae388db665983633890de94371df8ishmal all interpretations are models of C.

f3d3720abcbae388db665983633890de94371df8ishmal - F is valid, and C is a tautology.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - Possible dataforms are Proofs of C. -}

55b7747a6490959dc0c16c7941109097ea125a36ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("WeakerConclusion", "WEC")

3c208ff1f520c7b749a005157391bea0d7e60b0fishmal {- Some interpretations are models of Ax,

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal all models of Ax are models of C, and

3c208ff1f520c7b749a005157391bea0d7e60b0fishmal some models of C are not models of Ax.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - See Theorem and Satisfiable. -}

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("EquivalentTheorem", "ETH")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal {- Some, but not all, interpretations are models of Ax,

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal all models of Ax are models of C, and

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal all models of C are models of Ax.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - See Equivalent. -}

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("Tautology", "TAU")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal {- All interpretations are models of Ax, and

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal all interpretations are models of C.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - F is valid, ~F is unsatisfiable, and C is a tautology.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - Possible dataforms are Proofs of Ax and of C. -}

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("WeakerTautologousConclusion", "WTC")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal {- Some, but not all, interpretations are models of Ax, and

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal all interpretations are models of C.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - F is valid, and C is a tautology.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - See TautologousConclusion and WeakerConclusion. -}

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("WeakerTheorem", "WTH")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal {- Some interpretations are models of Ax,

3c208ff1f520c7b749a005157391bea0d7e60b0fishmal all models of Ax are models of C,

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal some models of C are not models of Ax, and

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal some interpretations are not models of C.

55b7747a6490959dc0c16c7941109097ea125a36ishmal - See Theorem and Satisfiable. -}

55b7747a6490959dc0c16c7941109097ea125a36ishmal

55b7747a6490959dc0c16c7941109097ea125a36ishmal , ("ContradictoryAxioms", "CAX")

55b7747a6490959dc0c16c7941109097ea125a36ishmal {- No interpretations are models of Ax.

55b7747a6490959dc0c16c7941109097ea125a36ishmal - F is valid, and anything is a theorem of Ax.

55b7747a6490959dc0c16c7941109097ea125a36ishmal - Possible dataforms are Refutations of Ax. -}

55b7747a6490959dc0c16c7941109097ea125a36ishmal

55b7747a6490959dc0c16c7941109097ea125a36ishmal , ("SatisfiableConclusionContradictoryAxioms", "SCA")

55b7747a6490959dc0c16c7941109097ea125a36ishmal {- No interpretations are models of Ax, and

55b7747a6490959dc0c16c7941109097ea125a36ishmal some interpretations are models of C.

55b7747a6490959dc0c16c7941109097ea125a36ishmal - See ContradictoryAxioms. -}

55b7747a6490959dc0c16c7941109097ea125a36ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("TautologousConclusionContradictoryAxioms", "TCA")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- No interpretations are models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all interpretations are models of C.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - See TautologousConclusion and SatisfiableConclusionContradictoryAxioms. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("WeakerConclusionContradictoryAxioms", "WCA")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- No interpretations are models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal some, but not all, interpretations are models of C.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - See SatisfiableConclusionContradictoryAxioms and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal SatisfiableCounterConclusionContradictoryAxioms. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("CounterUnsatisfiabilityPreserving", "CUP")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- If there does not exist a model of Ax then there does not exist a model of

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal ~C, i.e., if Ax is unsatisfiable then ~C is unsatisfiable. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("CounterSatisfiabilityPreserving", "CSP")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- If there exists a model of Ax then there exists a model of ~C, i.e., if Ax

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal is satisfiable then ~C is satisfiable. -}

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("EquiCounterSatisfiable", "ECS")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal {- There exists a model of Ax iff there exists a model of ~C, i.e., Ax is

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal (un)satisfiable iff ~C is (un)satisfiable. -}

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("CounterSatisfiable", "CSA")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal {- Some interpretations are models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal some models of Ax are models of ~C.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - F is not valid, ~F is satisfiable, and C is not a theorem of Ax.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - Possible dataforms are Models of Ax | ~C. -}

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("CounterTheorem", "CTH")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal {- All models of Ax are models of ~C.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - F is not valid, and ~C is a theorem of Ax.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - Possible dataforms are Proofs of ~C from Ax. -}

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("CounterEquivalent", "CEQ")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- Some interpretations are models of Ax,

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal all models of Ax are models of ~C, and

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal all models of ~C are models of Ax

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal (i.e., all interpretations are models of Ax xor of C).

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - F is not valid, and ~C is a theorem of Ax.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - Possible dataforms are Proofs of ~C from Ax and of Ax from ~C. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("UnsatisfiableConclusion", "UNC")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- Some interpretations are models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all interpretations are models of ~C

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal (i.e., no interpretations are models of C).

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - F is not valid, and ~C is a tautology.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - Possible dataforms are Proofs of ~C. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("WeakerCounterConclusion", "WCC")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- Some interpretations are models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all models of Ax are models of ~C, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal some models of ~C are not models of Ax.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - See CounterTheorem and CounterSatisfiable. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("EquivalentCounterTheorem", "ECT")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- Some, but not all, interpretations are models of Ax,

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all models of Ax are models of ~C, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all models of ~C are models of Ax.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - See CounterEquivalent. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("FinitelyUnsatisfiable", "FUN")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- All finite interpretations are finite models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all finite interpretations are finite models of ~C

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal (i.e., no finite interpretations are finite models of C). -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("Unsatisfiable", "UNS")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- All interpretations are models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all interpretations are models of ~C.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal (i.e., no interpretations are models of C).

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal - F is unsatisfiable, ~F is valid, and ~C is a tautology.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - Possible dataforms are Proofs of Ax and of C, and Refutations of F. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("WeakerUnsatisfiableConclusion", "WUC")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- Some, but not all, interpretations are models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all interpretations are models of ~C.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - See Unsatisfiable and WeakerCounterConclusion. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("WeakerCounterTheorem", "WCT")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- Some interpretations are models of Ax,

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all models of Ax are models of ~C,

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal some models of ~C are not models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal some interpretations are not models of ~C.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - See CounterSatisfiable. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("SatisfiableCounterConclusionContradictoryAxioms", "SCC")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- No interpretations are models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal some interpretations are models of ~C.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - See ContradictoryAxioms. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("UnsatisfiableConclusionContradictoryAxioms", "UCA")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- No interpretations are models of Ax, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal all interpretations are models of ~C

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal (i.e., no interpretations are models of C).

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - See UnsatisfiableConclusion and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - SatisfiableCounterConclusionContradictoryAxioms. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("NoConsequence", "NOC") ]

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal {- Some interpretations are models of Ax,

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal some models of Ax are models of C, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal some models of Ax are models of ~C.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - F is not valid, F is satisfiable, ~F is not valid, ~F is satisfiable, and

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal C is not a theorem of Ax.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal - Possible dataforms are pairs of models, one Model of Ax | C and one Model

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal of Ax | ~C. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmalnosuccess :: [(String, String)]

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmalnosuccess =

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal [ ("NoSuccess", "NOS")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- The logical data has not been processed successfully (yet).

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("Open", "OPN")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- A success value has never been established.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("Unknown", "UNK")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Success value unknown, and no assumption has been made.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("Assumed", "ASS(U,S)")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal {- The success ontology value S has been assumed because the actual value is

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal unknown for the no-success ontology reason U. U is taken from the

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal subontology starting at Unknown in the no-success ontology. -}

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("Stopped", "STP")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal {- Software attempted to process the data, and stopped without a success

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal status. -}

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("Error", "ERR")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Software stopped due to an error.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("OSError", "OSE")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Software stopped due to an operating system error.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("InputError", "INE")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Software stopped due to an input error.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("SyntaxError", "SYE")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- Software stopped due to an input syntax error.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("SemanticError", "SEE")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- Software stopped due to an input semantic error.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("TypeError", "TYE")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- Software stopped due to an input type error (for typed logical data).

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("Forced", "FOR")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- Software was forced to stop by an external force.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("User", "USR")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- Software was forced to stop by the user.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("ResourceOut", "RSO")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Software stopped because some resource ran out.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("Timeout", "TMO")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- Software stopped because the CPU time limit ran out.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("MemoryOut", "MMO")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Software stopped because the memory limit ran out.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("GaveUp", "GUP")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Software gave up of its own accord.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("Incomplete", "INC")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Software gave up because it's incomplete.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("Inappropriate", "IAP")

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Software gave up because it cannot process this type of data.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal , ("InProgress", "INP")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- Software is still running.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("NotTried", "NTT")

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal -- Software has not tried to process the data.

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal , ("NotTriedYet", "NTY") ]

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal -- Software has not tried to process the data yet, but might in the future.

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsCheck :: [(String, String)] -> [String] -> String -> Bool

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsCheck pl l = maybe False (`elem` l)

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal . (`lookup` map (\ (t, r) -> (map toLower t, r)) pl) . map toLower

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsProved :: String -> Bool

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsProved = szsCheck successes ["SAT", "THM"]

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsDisproved :: String -> Bool

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsDisproved = szsCheck successes ["CSA", "UNS"]

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsTimeout :: String -> Bool

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsTimeout = szsCheck nosuccess ["TMO", "RSO"]

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmalszsMemoryOut :: String -> Bool

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmalszsMemoryOut = szsCheck nosuccess ["MMO"]

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsStopped :: String -> Bool

dc939c1ce8e07f33f7d5a461fce1529206d37ba5ishmalszsStopped = szsCheck nosuccess ["STP"]

1df3a36f6d4cb38963d36fc74aa47990fd055859ishmal