diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,15 @@ # Revision history for tptp +## 0.1.1.0 -- 2019-12-07 + +* Parse SZS ontology information in the TSTP input. + +* Parse single line comments starting with #. + +* Increase the upper bound of the prettyprinter dependency. + +* Support compilation with GHC 8.8.1. + ## 0.1.0.3 -- 2019-06-11 * Support compilation with GHC 7.8. diff --git a/src/Data/TPTP.hs b/src/Data/TPTP.hs --- a/src/Data/TPTP.hs +++ b/src/Data/TPTP.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE CPP #-} @@ -79,11 +80,17 @@ UnitName, Unit(..), TPTP(..), + TSTP(..), -- * Annotations Intro(..), Source(..), - Status(..), + Status, + SZS(..), + SZSOntology(..), + Success(..), + NoSuccess(..), + Dataform(..), Parent(..), Expression(..), Info(..), @@ -112,12 +119,19 @@ -- * Languages -- | The language of logical formulas available in TPTP. +-- +-- The languages of TPTP form a hierarchy displayed on the following diagram, +-- where arrows indicate inclusion. E.g. each formula in FOF is syntactically a +-- formula in TFF0, but not the other way around. +-- +-- > CNF --> FOF --> TFF0 --> TFF1 +-- data Language = CNF_ -- ^ __CNF__ - the language of clausal normal forms of -- unsorted first-order logic. | FOF_ -- ^ __FOF__ - the language of full unsorted first-order logic. | TFF_ -- ^ __TFF__ - the language of full sorted first-order logic, - -- both monomorphic (TFF0) and polymorphic (TFF1). + -- both monomorphic (__TFF0__) and polymorphic (__TFF1__). deriving (Eq, Show, Ord, Enum, Bounded) instance Named Language where @@ -131,7 +145,7 @@ -- | The atomic word in the TPTP language - a non-empty string of space or -- visible characters from the ASCII range 0x20 to 0x7E. If the string satisfies --- the regular expression @[a-z][a-zA-Z0-9_]*@ it is displayed in the TPTP +-- the regular expression @[a-z][a-zA-Z0-9_]*@, then it is displayed in the TPTP -- language as is, otherwise it is displayed in single quotes with the -- characters @'@ and @\\@ escaped using @\\@. -- @@ -247,7 +261,7 @@ = Standard s -- ^ The identifier contained in the TPTP specification. | Extended Text -- ^ The identifier not contained in the standard TPTP but -- implemented by some theorem prover. For example, Vampire - -- implements uses the sort constructor @$array@. + -- implements the sort constructor @$array@. deriving (Eq, Show, Ord) -- | A smart 'Extended' constructor - only uses 'Extended' if the given string @@ -492,9 +506,9 @@ -- | The literal in first-order logic. -- The logical tautology is represented as --- 'Predicate (Reserved (Standard Tautology)) []' +-- @Predicate (Reserved (Standard Tautology)) []@ -- and the logical falsum is represented as --- 'Predicate (Reserved (Standard Falsum)) []'. +-- @Predicate (Reserved (Standard Falsum)) []@. data Literal = Predicate (Name Predicate) [Term] -- ^ Application of a predicate symbol. @@ -714,7 +728,12 @@ units :: [Unit] } deriving (Eq, Show, Ord) +-- | The TSTP output - zero or more TSTP units, possibly annotated with the +-- status of the proof search and the resulting dataform. +data TSTP = TSTP SZS [Unit] + deriving (Eq, Show, Ord) + -- * Annotations -- | The marking of the way a formula is introduced in a TSTP proof. @@ -746,16 +765,61 @@ | UnknownSource deriving (Eq, Show, Ord) --- | The status of an inference. --- See +-- | The status values of the SZS ontologies of a TPTP text. +data SZS = SZS (Maybe Status) (Maybe Dataform) + deriving (Eq, Show, Ord) + +-- | The auxiliary wrapper used to provide 'Named' instances with full names of +-- SZS ontologies to 'Success', 'NoSuccess' and 'Dataform'. +newtype SZSOntology a = SZSOntology { unwrapSZSOntology :: a } + deriving (Eq, Show, Ord, Enum, Bounded) + +-- | The status of the proof search. +type Status = Either NoSuccess Success + +-- | The SZS Success ontology. Values of this ontology are used to mark +-- the result of the proof search and also the status of an inference in +-- a TSTP proof. See +-- -- for details. -data Status - = SUC | UNP | SAP | ESA | SAT | FSA | THM | EQV | TAC | WEC | ETH | TAU | WTC - | WTH | CAX | SCA | TCA | WCA | CUP | CSP | ECS | CSA | CTH | CEQ | UNC | WCC - | ECT | FUN | UNS | WUC | WCT | SCC | UCA | NOC +data Success + = SUC -- ^ Success. + | UNP -- ^ UnsatisfiabilityPreserving. + | SAP -- ^ SatisfiabilityPreserving. + | ESA -- ^ EquiSatisfiable. + | SAT -- ^ Satisfiable. + | FSA -- ^ FinitelySatisfiable. + | THM -- ^ Theorem. + | EQV -- ^ Equivalent. + | TAC -- ^ TautologousConclusion. + | WEC -- ^ WeakerConclusion. + | ETH -- ^ EquivalentTheorem. + | TAU -- ^ Tautology. + | WTC -- ^ WeakerTautologousConclusion. + | WTH -- ^ WeakerTheorem. + | CAX -- ^ ContradictoryAxioms. + | SCA -- ^ SatisfiableConclusionContradictoryAxioms. + | TCA -- ^ TautologousConclusionContradictoryAxioms. + | WCA -- ^ WeakerConclusionContradictoryAxioms. + | CUP -- ^ CounterUnsatisfiabilityPreserving. + | CSP -- ^ CounterSatisfiabilityPreserving. + | ECS -- ^ EquiCounterSatisfiable. + | CSA -- ^ CounterSatisfiable. + | CTH -- ^ CounterTheorem. + | CEQ -- ^ CounterEquivalent. + | UNC -- ^ UnsatisfiableConclusion. + | WCC -- ^ WeakerCounterConclusion. + | ECT -- ^ EquivalentCounterTheorem. + | FUN -- ^ FinitelyUnsatisfiable. + | UNS -- ^ Unsatisfiable. + | WUC -- ^ WeakerUnsatisfiableConclusion. + | WCT -- ^ WeakerCounterTheorem. + | SCC -- ^ SatisfiableCounterConclusionContradictoryAxioms. + | UCA -- ^ UnsatisfiableConclusionContradictoryAxioms. + | NOC -- ^ NoConsequence. deriving (Eq, Show, Ord, Enum, Bounded) -instance Named Status where +instance Named Success where name = \case SUC -> "suc" UNP -> "unp" @@ -792,6 +856,193 @@ UCA -> "uca" NOC -> "noc" +instance Named (SZSOntology Success) where + name (SZSOntology s) = case s of + SUC -> "Success" + UNP -> "UnsatisfiabilityPreserving" + SAP -> "SatisfiabilityPreserving" + ESA -> "EquiSatisfiable" + SAT -> "Satisfiable" + FSA -> "FinitelySatisfiable" + THM -> "Theorem" + EQV -> "Equivalent" + TAC -> "TautologousConclusion" + WEC -> "WeakerConclusion" + ETH -> "EquivalentTheorem" + TAU -> "Tautology" + WTC -> "WeakerTautologousConclusion" + WTH -> "WeakerTheorem" + CAX -> "ContradictoryAxioms" + SCA -> "SatisfiableConclusionContradictoryAxioms" + TCA -> "TautologousConclusionContradictoryAxioms" + WCA -> "WeakerConclusionContradictoryAxioms" + CUP -> "CounterUnsatisfiabilityPreserving" + CSP -> "CounterSatisfiabilityPreserving" + ECS -> "EquiCounterSatisfiable" + CSA -> "CounterSatisfiable" + CTH -> "CounterTheorem" + CEQ -> "CounterEquivalent" + UNC -> "UnsatisfiableConclusion" + WCC -> "WeakerCounterConclusion" + ECT -> "EquivalentCounterTheorem" + FUN -> "FinitelyUnsatisfiable" + UNS -> "Unsatisfiable" + WUC -> "WeakerUnsatisfiableConclusion" + WCT -> "WeakerCounterTheorem" + SCC -> "SatisfiableCounterConclusionContradictoryAxioms" + UCA -> "UnsatisfiableConclusionContradictoryAxioms" + NOC -> "NoConsequence" + +-- | The SZS NoSuccess ontology. Values of this ontology are used to mark +-- the result of the proof search. See +-- +-- for details. +data NoSuccess + = NOS -- ^ NoSuccess. + | OPN -- ^ Open. + | UNK -- ^ Unknown. + | ASS -- ^ Assumed. + | STP -- ^ Stopped. + | ERR -- ^ Error. + | OSE -- ^ OSError. + | INE -- ^ InputError. + | USE -- ^ UsageError. + | SYE -- ^ SyntaxError. + | SEE -- ^ SemanticError. + | TYE -- ^ TypeError. + | FOR -- ^ Forced. + | USR -- ^ User. + | RSO -- ^ ResourceOut. + | TMO -- ^ Timeout. + | MMO -- ^ MemoryOut. + | GUP -- ^ GaveUp. + | INC -- ^ Incomplete. + | IAP -- ^ Inappropriate. + | INP -- ^ InProgress. + | NTT -- ^ NotTried. + | NTY -- ^ NotTriedYet. + deriving (Eq, Show, Ord, Enum, Bounded) + +instance Named (SZSOntology NoSuccess) where + name (SZSOntology ns) = case ns of + NOS -> "NoSuccess" + OPN -> "Open" + UNK -> "Unknown" + ASS -> "Assumed" + STP -> "Stopped" + ERR -> "Error" + OSE -> "OSError" + INE -> "InputError" + USE -> "UsageError" + SYE -> "SyntaxError" + SEE -> "SemanticError" + TYE -> "TypeError" + FOR -> "Forced" + USR -> "User" + RSO -> "ResourceOut" + TMO -> "Timeout" + MMO -> "MemoryOut" + GUP -> "GaveUp" + INC -> "Incomplete" + IAP -> "Inappropriate" + INP -> "InProgress" + NTT -> "NotTried" + NTY -> "NotTriedYet" + +-- | The SZS Dataform ontology. Values of this ontology are used to mark +-- the form of logical data produced during proof search. See +-- +-- for details. +data Dataform + = LDa -- ^ LogicalData. + | Sln -- ^ Solution. + | Prf -- ^ Proof. + | Der -- ^ Derivation. + | Ref -- ^ Refutation. + | CRf -- ^ CNFRefutation. + | Int_ -- ^ Interpretation. + | Mod -- ^ Model. + | Pin -- ^ PartialInterpretation. + | PMo -- ^ PartialModel. + | SIn -- ^ StrictlyPartialInterpretation. + | SMo -- ^ StrictlyPartialModel. + | DIn -- ^ DomainInterpretation. + | DMo -- ^ DomainModel. + | DPI -- ^ DomainPartialInterpretation. + | DPM -- ^ DomainPartialModel. + | DSI -- ^ DomainStrictlyPartialInterpretation. + | DSM -- ^ DomainStrictlyPartialModel. + | FIn -- ^ FiniteInterpretation. + | FMo -- ^ FiniteModel. + | FPI -- ^ FinitePartialInterpretation. + | FPM -- ^ FinitePartialModel. + | FSI -- ^ FiniteStrictlyPartialInterpretation. + | FSM -- ^ FiniteStrictlyPartialModel. + | HIn -- ^ HerbrandInterpretation. + | HMo -- ^ HerbrandModel. + | TIn -- ^ FormulaInterpretation. + | TMo -- ^ FormulaModel. + | TPI -- ^ FormulaPartialInterpretation. + | TSI -- ^ FormulaStrictlyPartialInterpretation. + | TSM -- ^ FormulaStrictlyPartialModel. + | Sat -- ^ Saturation. + | Lof -- ^ ListOfFormulae. + | Lth -- ^ ListOfTHF. + | Ltf -- ^ ListOfTFF. + | Lfo -- ^ ListOfFOF. + | Lcn -- ^ ListOfCNF. + | NSo -- ^ NotASolution. + | Ass -- ^ Assurance. + | IPr -- ^ IncompleteProof. + | IIn -- ^ IncompleteInterpretation. + | Non -- ^ None. + deriving (Eq, Show, Ord, Enum, Bounded) + +instance Named (SZSOntology Dataform) where + name (SZSOntology d) = case d of + LDa -> "LogicalData" + Sln -> "Solution" + Prf -> "Proof" + Der -> "Derivation" + Ref -> "Refutation" + CRf -> "CNFRefutation" + Int_ -> "Interpretation" + Mod -> "Model" + Pin -> "PartialInterpretation" + PMo -> "PartialModel" + SIn -> "StrictlyPartialInterpretation" + SMo -> "StrictlyPartialModel" + DIn -> "DomainInterpretation" + DMo -> "DomainModel" + DPI -> "DomainPartialInterpretation" + DPM -> "DomainPartialModel" + DSI -> "DomainStrictlyPartialInterpretation" + DSM -> "DomainStrictlyPartialModel" + FIn -> "FiniteInterpretation" + FMo -> "FiniteModel" + FPI -> "FinitePartialInterpretation" + FPM -> "FinitePartialModel" + FSI -> "FiniteStrictlyPartialInterpretation" + FSM -> "FiniteStrictlyPartialModel" + HIn -> "HerbrandInterpretation" + HMo -> "HerbrandModel" + TIn -> "FormulaInterpretation" + TMo -> "FormulaModel" + TPI -> "FormulaPartialInterpretation" + TSI -> "FormulaStrictlyPartialInterpretation" + TSM -> "FormulaStrictlyPartialModel" + Sat -> "Saturation" + Lof -> "ListOfFormulae" + Lth -> "ListOfTHF" + Ltf -> "ListOfTFF" + Lfo -> "ListOfFOF" + Lcn -> "ListOfCNF" + NSo -> "NotASolution" + Ass -> "Assurance" + IPr -> "IncompleteProof" + IIn -> "IncompleteInterpretation" + Non -> "None" + -- | The parent of a formula in an inference. data Parent = Parent Source [Info] deriving (Eq, Show, Ord) @@ -807,7 +1058,7 @@ data Info = Description Atom | Iquote Atom - | Status (Reserved Status) + | Status (Reserved Success) | Assumptions (NonEmpty UnitName) | NewSymbols Atom [Either Var Atom] | Refutation Atom diff --git a/src/Data/TPTP/Parse/Combinators.hs b/src/Data/TPTP/Parse/Combinators.hs --- a/src/Data/TPTP/Parse/Combinators.hs +++ b/src/Data/TPTP/Parse/Combinators.hs @@ -1,3 +1,4 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE CPP #-} @@ -13,7 +14,8 @@ module Data.TPTP.Parse.Combinators ( -- * Whitespace - whitespace, + skipWhitespace, + input, -- * Names atom, @@ -40,8 +42,10 @@ -- * Units unit, tptp, + tstp, -- * Annotations + szs, intro, parent, source, @@ -52,13 +56,20 @@ import Prelude hiding (pure, (<$>), (<*>), (*>), (<*)) #endif -import Control.Applicative (pure, (<*>), (*>), (<*), (<|>), optional) +import Control.Applicative (pure, (<*>), (*>), (<*), (<|>), optional, empty, many) import Data.Char (isAscii, isAsciiLower, isAsciiUpper, isDigit, isPrint) import Data.Function (on) import Data.Functor ((<$>), ($>)) +import Data.Maybe (fromMaybe) +#if !MIN_VERSION_base(4, 8, 0) +import Data.Monoid (Monoid(..)) +#endif import Data.List (sortBy, genericLength) import Data.List.NonEmpty (NonEmpty) import qualified Data.List.NonEmpty as NEL (fromList, toList) +#if !MIN_VERSION_base(4, 11, 0) +import Data.Semigroup (Semigroup(..)) +#endif import qualified Data.Scientific as Sci (base10Exponent, coefficient) @@ -68,8 +79,8 @@ import Data.Attoparsec.Text as Atto ( Parser, (), char, string, decimal, scientific, signed, isEndOfLine, endOfLine, - satisfy, option, eitherP, choice, manyTill, takeWhile, skipSpace, skipMany, - skipWhile, endOfInput, sepBy, sepBy1 + satisfy, option, eitherP, choice, manyTill, takeWhile, skip, skipSpace, + skipMany, skipWhile, endOfInput, sepBy, sepBy1 ) import Data.TPTP hiding (name, clause) @@ -78,29 +89,52 @@ -- * Helper functions --- | Consume a single line comment - characters between @%@ and newline. -comment :: Parser () -comment = char '%' *> skipWhile (not . isEndOfLine) - *> (endOfLine <|> endOfInput) - "comment" +-- | Consume all character until the end of line. +skipLine :: Parser () +skipLine = skipWhile (not . isEndOfLine) +{-# INLINE skipLine #-} --- | Consume a block comments - characters between /* and */. -blockComment :: Parser () -blockComment = string "/*" *> bc "block comment" +-- | Consume the first character of a single line comment - @%@ or @#@. +-- The grammar of the TPTP language only defines @%@, +-- but some theorem provers in addition use @#@. +skipBeginComment :: Parser () +skipBeginComment = skip (\c -> c == '%' || c == '#') +{-# INLINE skipBeginComment #-} + +-- | Parse the contents of a single line comment. +commented :: Parser p -> Parser p +commented p = skipBeginComment *> p <* skipLine <* (endOfLine <|> endOfInput) + "commented" + +-- | Consume a single line comment - characters between @%@ or @#@ and newline. +skipComment :: Parser () +skipComment = commented (pure ()) "comment" +{-# INLINE skipComment #-} + +-- | Consume a block comment - characters between /* and */. +skipBlockComment :: Parser () +skipBlockComment = string "/*" *> bc "block comment" where bc = skipWhile (/= '*') *> (string "*/" $> () <|> bc) -- | Consume white space and trailing comments. -whitespace :: Parser () -whitespace = skipSpace *> skipMany ((comment <|> blockComment) *> skipSpace) - "whitespace" +skipWhitespace :: Parser () +skipWhitespace = skipSpace + *> skipMany ((skipComment <|> skipBlockComment) *> skipSpace) + "whitespace" -- | @lexeme@ makes a given parser consume trailing whitespace. This function is -- needed because off-the-shelf attoparsec parsers do not do it. lexeme :: Parser a -> Parser a -lexeme p = p <* whitespace +lexeme p = p <* skipWhitespace {-# INLINE lexeme #-} +-- | @input@ runs a given parser skipping leading whitespace. The function +-- succeeds if the parser consumes the entire input. +input :: Parser a -> Parser a +input p = skipWhitespace *> p <* endOfInput "input" +{-# INLINE input #-} + -- | Parse an unsigned integer. integer :: Parser Integer integer = lexeme decimal "integer" @@ -151,11 +185,15 @@ maybeP = optional . comma {-# INLINE maybeP #-} +named :: (Named a, Enum a, Bounded a) => Parser a +named = choice + $ fmap (\(n, c) -> string n $> c "named " ++ Text.unpack n) + $ sortBy (flip compare `on` fst) + $ fmap (\c -> (TPTP.name c, c)) [minBound..] + enum :: (Named a, Enum a, Bounded a) => Parser a -enum = choice - $ fmap (\(n, c) -> token n $> c "reserved " ++ Text.unpack n) - $ sortBy (flip compare `on` fst) - $ fmap (\c -> (TPTP.name c, c)) [minBound..] +enum = lexeme named +{-# INLINE enum #-} -- * Parser combinators @@ -206,7 +244,7 @@ <|> Defined <$> atom "name" --- | Parser a function name. +-- | Parse a function name. function :: Parser (Name Function) function = name "function" {-# INLINE function #-} @@ -413,10 +451,51 @@ -- | Parse a TPTP input. tptp :: Parser TPTP -tptp = TPTP <$> manyTill unit endOfInput "derivation" +tptp = TPTP <$> manyTill unit endOfInput "tptp" +-- | Parse a TSTP input. +tstp :: Parser TSTP +tstp = TSTP <$> szs <*> manyTill unit endOfInput <* endOfInput "tstp" + -- ** Annotations + +instance Semigroup SZS where + SZS s d <> SZS s' d' = SZS (s <|> s') (d <|> d') + +instance Monoid SZS where + mempty = SZS empty empty + mappend = (<>) + +-- | Parse the SZS ontology information of a TSTP output inside a comment. +szs :: Parser SZS +szs = fromMaybe mempty . mconcat <$> many szsComment + +szsComment :: Parser (Maybe SZS) +szsComment = commented (skipSpace *> optional szsAnnotation) <* skipSpace + "szs comment" + +szsAnnotation :: Parser SZS +szsAnnotation = string "SZS" *> skipSpace *> (szsStatus <|> szsDataform) + "szs annotation" + +szsStatus :: Parser SZS +szsStatus = string "status" *> skipSpace + *> (fromStatus <$> status) + "status" + where + fromStatus s = SZS (Just s) Nothing + status = eitherP (unwrapSZSOntology <$> named) + (unwrapSZSOntology <$> named) + +szsDataform :: Parser SZS +szsDataform = string "output" *> skipSpace + *> string "start" *> skipSpace + *> (fromDataform <$> dataform) + "dataform" + where + fromDataform d = SZS Nothing (Just d) + dataform = unwrapSZSOntology <$> named -- | Parse an introduction marking. intro :: Parser Intro diff --git a/src/Data/TPTP/Parse/Text.hs b/src/Data/TPTP/Parse/Text.hs --- a/src/Data/TPTP/Parse/Text.hs +++ b/src/Data/TPTP/Parse/Text.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE CPP #-} - -- | -- Module : Data.TPTP.Parse.Text -- Description : An attoparsec-based parser for the TPTP language. @@ -18,43 +16,59 @@ -- * Runners of parsers for TPTP inputs parseTPTP, parseTPTPOnly, - parseTPTPWith -) where + parseTPTPWith, -#if !MIN_VERSION_base(4, 8, 0) -import Control.Applicative ((*>), (<*)) -#endif + -- * Runners of parsers for TSTP inputs + parseTSTP, + parseTSTPOnly, + parseTSTPWith, +) where -import Data.Attoparsec.Text (Result, parse, parseOnly, parseWith, endOfInput) +import Data.Attoparsec.Text (Result, parse, parseOnly, parseWith) import Data.Text (Text) -import Data.TPTP (Unit, TPTP) -import Data.TPTP.Parse.Combinators (whitespace, unit, tptp) +import Data.TPTP (Unit, TPTP, TSTP) +import Data.TPTP.Parse.Combinators (input, unit, tptp, tstp) + -- | Run a parser for a single TPTP unit on 'Text'. parseUnit :: Text -> Result Unit -parseUnit = parse (whitespace *> unit <* endOfInput) +parseUnit = parse (input unit) -- | Run a parser for a single TPTP unit that cannot be resupplied -- via a 'Data.Attoparsec.Text.Partial' result. parseUnitOnly :: Text -> Either String Unit -parseUnitOnly = parseOnly (whitespace *> unit <* endOfInput) +parseUnitOnly = parseOnly (input unit) -- | Run a parser for a single TPTP unit with an initial input string, -- and a monadic action that can supply more input if needed. parseUnitWith :: Monad m => m Text -> Text -> m (Result Unit) -parseUnitWith m = parseWith m (whitespace *> unit <* endOfInput) +parseUnitWith m = parseWith m (input unit) -- | Run a parser for a TPTP input on 'Text'. parseTPTP :: Text -> Result TPTP -parseTPTP = parse (whitespace *> tptp <* endOfInput) +parseTPTP = parse (input tptp) -- | Run a parser for a TPTP input that cannot be resupplied -- via a 'Data.Attoparsec.Text.Partial' result. parseTPTPOnly :: Text -> Either String TPTP -parseTPTPOnly = parseOnly (whitespace *> tptp <* endOfInput) +parseTPTPOnly = parseOnly (input tptp) -- | Run a parser for a TPTP input with an initial input string, -- and a monadic action that can supply more input if needed. parseTPTPWith :: Monad m => m Text -> Text -> m (Result TPTP) -parseTPTPWith m = parseWith m (whitespace *> tptp <* endOfInput) +parseTPTPWith m = parseWith m (input tptp) + +-- | Run a parser for a TSTP input on 'Text'. +parseTSTP :: Text -> Result TSTP +parseTSTP = parse tstp + +-- | Run a parser for a TSTP input that cannot be resupplied +-- via a 'Data.Attoparsec.Text.Partial' result. +parseTSTPOnly :: Text -> Either String TSTP +parseTSTPOnly = parseOnly tstp + +-- | Run a parser for a TSTP input with an initial input string, +-- and a monadic action that can supply more input if needed. +parseTSTPWith :: Monad m => m Text -> Text -> m (Result TSTP) +parseTSTPWith m = parseWith m tstp diff --git a/src/Data/TPTP/Parse/Text/Lazy.hs b/src/Data/TPTP/Parse/Text/Lazy.hs --- a/src/Data/TPTP/Parse/Text/Lazy.hs +++ b/src/Data/TPTP/Parse/Text/Lazy.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE CPP #-} - -- | -- Module : Data.TPTP.Parse.Text.Lazy -- Description : An attoparsec-based parser for the TPTP language. @@ -14,23 +12,27 @@ parseUnit, -- * Runners of parsers for TPTP inputs - parseTPTP -) where + parseTPTP, -#if !MIN_VERSION_base(4, 8, 0) -import Control.Applicative ((*>), (<*)) -#endif + -- * Runners of parsers for TSTP inputs + parseTSTP +) where -import Data.Attoparsec.Text.Lazy (Result, parse, endOfInput) +import Data.Attoparsec.Text.Lazy (Result, parse) import Data.Text.Lazy (Text) -import Data.TPTP (Unit, TPTP) -import Data.TPTP.Parse.Combinators (whitespace, unit, tptp) +import Data.TPTP (Unit, TPTP, TSTP) +import Data.TPTP.Parse.Combinators (input, unit, tptp, tstp) + -- | Parse a single TPTP unit from 'Data.Text.Lazy.Text'. parseUnit :: Text -> Result Unit -parseUnit = parse (whitespace *> unit <* endOfInput) +parseUnit = parse (input unit) -- | Parse a TPTP input from 'Data.Text.Lazy.Text'. parseTPTP :: Text -> Result TPTP -parseTPTP = parse (whitespace *> tptp <* endOfInput) +parseTPTP = parse (input tptp) + +-- | Parse a TSTP input from 'Data.Text.Lazy.Text'. +parseTSTP :: Text -> Result TSTP +parseTSTP = parse tstp diff --git a/src/Data/TPTP/Pretty.hs b/src/Data/TPTP/Pretty.hs --- a/src/Data/TPTP/Pretty.hs +++ b/src/Data/TPTP/Pretty.hs @@ -37,7 +37,7 @@ ) import Data.Text.Prettyprint.Doc ( Doc, Pretty(..), - hsep, sep, (<+>), brackets, parens, punctuate, comma, space + hsep, sep, (<+>), brackets, parens, punctuate, comma, space, line ) import Data.TPTP @@ -45,6 +45,9 @@ -- * Helper functions +comment :: Doc ann -> Doc ann +comment c = "%" <+> c <> line + sepBy :: [Doc ann] -> Doc ann -> Doc ann sepBy as s = hsep (punctuate s as) @@ -271,14 +274,38 @@ instance Pretty TPTP where pretty (TPTP us) = prettyList us +szsComment :: [Doc ann] -> Doc ann +szsComment = comment . hsep . ("SZS":) +instance Pretty TSTP where + pretty (TSTP (SZS s d) us) = status <> dataform (prettyList us) + where + status = case s of + Nothing -> mempty + Just st -> szsComment ["status", pretty st] + dataform p = case d of + Nothing -> p + Just df -> szsComment ["output", "start", pretty df] + <> p + <> szsComment ["output", "end", pretty df] + + -- * Annotations instance Pretty Intro where pretty = pretty . name +instance Pretty Success where + pretty = pretty . name . SZSOntology + +instance Pretty NoSuccess where + pretty = pretty . name . SZSOntology + instance Pretty Status where - pretty = pretty . name + pretty = either pretty pretty + +instance Pretty Dataform where + pretty = pretty . name . SZSOntology instance Pretty (Either Var Atom) where pretty = either pretty pretty diff --git a/test-data/szs/fof/AGT004+2---Metis---2.4.THM-CRf.original.s b/test-data/szs/fof/AGT004+2---Metis---2.4.THM-CRf.original.s new file mode 100644 --- /dev/null +++ b/test-data/szs/fof/AGT004+2---Metis---2.4.THM-CRf.original.s @@ -0,0 +1,110 @@ +% Problem : AGT004+2 : TPTP v7.1.0. Bugfixed v3.1.0. +% Command : metis --show proof --show saturation %s +% Computer : n065.star.cs.uiowa.edu +% Model : x86_64 x86_64 +% CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz +% Memory : 32218.625MB +% OS : Linux 3.10.0-693.2.2.el7.x86_64 +% CPULimit : 300 +% DateTime : Tue Aug 28 09:30:41 CDT 2018 +% CPUTime : +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p + +% SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p +fof(a1_1, axiom, + (! [A, C, N, L] : + (accept_team(A, L, C, N) <=> + (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N))))). + +fof(deduced_13, axiom, + (~ accept_city(countryamedicalorganization, coastvillage))). + +fof(query_4, conjecture, + (~ + accept_team(countryamedicalorganization, + countryahumanitarianorganization, coastvillage, n5))). + +fof(subgoal_0, plain, + (~ + accept_team(countryamedicalorganization, + countryahumanitarianorganization, coastvillage, n5)), + inference(strip, [], [query_4])). + +fof(negate_0_0, plain, + (~ ~ + accept_team(countryamedicalorganization, + countryahumanitarianorganization, coastvillage, n5)), + inference(negate, [], [subgoal_0])). + +fof(normalize_0_0, plain, + (accept_team(countryamedicalorganization, + countryahumanitarianorganization, coastvillage, n5)), + inference(canonicalize, [], [negate_0_0])). + +fof(normalize_0_1, plain, + (! [A, C, L, N] : + (~ accept_team(A, L, C, N) <=> + (~ accept_city(A, C) | ~ accept_leader(A, L) | + ~ accept_number(A, N)))), inference(canonicalize, [], [a1_1])). + +fof(normalize_0_2, plain, + (! [A, C, L, N] : + (~ accept_team(A, L, C, N) <=> + (~ accept_city(A, C) | ~ accept_leader(A, L) | + ~ accept_number(A, N)))), + inference(specialize, [], [normalize_0_1])). + +fof(normalize_0_3, plain, + (! [A, C, L, N] : + ((~ accept_team(A, L, C, N) | accept_city(A, C)) & + (~ accept_team(A, L, C, N) | accept_leader(A, L)) & + (~ accept_team(A, L, C, N) | accept_number(A, N)) & + (~ accept_city(A, C) | ~ accept_leader(A, L) | + ~ accept_number(A, N) | accept_team(A, L, C, N)))), + inference(clausify, [], [normalize_0_2])). + +fof(normalize_0_4, plain, + (! [A, C, L, N] : (~ accept_team(A, L, C, N) | accept_city(A, C))), + inference(conjunct, [], [normalize_0_3])). + +fof(normalize_0_5, plain, + (~ accept_city(countryamedicalorganization, coastvillage)), + inference(canonicalize, [], [deduced_13])). + +cnf(refute_0_0, plain, + (accept_team(countryamedicalorganization, + countryahumanitarianorganization, coastvillage, n5)), + inference(canonicalize, [], [normalize_0_0])). + +cnf(refute_0_1, plain, (~ accept_team(A, L, C, N) | accept_city(A, C)), + inference(canonicalize, [], [normalize_0_4])). + +cnf(refute_0_2, plain, + (~ + accept_team(countryamedicalorganization, + countryahumanitarianorganization, coastvillage, n5) | + accept_city(countryamedicalorganization, coastvillage)), + inference(subst, [], + [refute_0_1 : + [bind(A, $fot(countryamedicalorganization)), + bind(C, $fot(coastvillage)), + bind(L, $fot(countryahumanitarianorganization)), + bind(N, $fot(n5))]])). + +cnf(refute_0_3, plain, + (accept_city(countryamedicalorganization, coastvillage)), + inference(resolve, + [$cnf(accept_team(countryamedicalorganization, + countryahumanitarianorganization, coastvillage, + n5))], [refute_0_0, refute_0_2])). + +cnf(refute_0_4, plain, + (~ accept_city(countryamedicalorganization, coastvillage)), + inference(canonicalize, [], [normalize_0_5])). + +cnf(refute_0_5, plain, ($false), + inference(resolve, + [$cnf(accept_city(countryamedicalorganization, + coastvillage))], [refute_0_3, refute_0_4])). +% SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p diff --git a/test-data/szs/fof/ALG043+1---Vampire---4.3.THM-Ref.original.s b/test-data/szs/fof/ALG043+1---Vampire---4.3.THM-Ref.original.s new file mode 100644 --- /dev/null +++ b/test-data/szs/fof/ALG043+1---Vampire---4.3.THM-Ref.original.s @@ -0,0 +1,996 @@ +% Problem : ALG043+1 : TPTP v7.1.0. Released v2.7.0. +% Command : vampire --mode casc -t %d %s +% Computer : n157.star.cs.uiowa.edu +% Model : x86_64 x86_64 +% CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz +% Memory : 32218.625MB +% OS : Linux 3.10.0-693.2.2.el7.x86_64 +% CPULimit : 300 +% DateTime : Wed Aug 29 18:25:56 CDT 2018 +% CPUTime : +% ott+1002_2_av=off:bd=preordered:irw=on:lma=on:nm=64:nwc=10:sp=reverse_arity:updr=off_2 on theBenchmark +% Refutation found. Thanks to Tanya! +% SZS status Theorem for theBenchmark +% SZS output start Proof for theBenchmark +fof(f2,axiom,( + e0 = op(e3,e3) & e1 = op(e3,e2) & e2 = op(e3,e1) & e3 = op(e3,e0) & e1 = op(e2,e3) & e0 = op(e2,e2) & e3 = op(e2,e1) & e2 = op(e2,e0) & e2 = op(e1,e3) & e3 = op(e1,e2) & e0 = op(e1,e1) & e1 = op(e1,e0) & e3 = op(e0,e3) & e2 = op(e0,e2) & e1 = op(e0,e1) & e0 = op(e0,e0)), + file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2)). +fof(f3,axiom,( + e0 = unit), + file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3)). +fof(f4,conjecture,( + (e3 = op(e3,e3) | e3 = op(e2,e3) | e3 = op(e1,e3) | e3 = op(e0,e3)) & (e3 = op(e3,e3) | e3 = op(e3,e2) | e3 = op(e3,e1) | e3 = op(e3,e0)) & (e2 = op(e3,e3) | e2 = op(e2,e3) | e2 = op(e1,e3) | e2 = op(e0,e3)) & (e2 = op(e3,e3) | e2 = op(e3,e2) | e2 = op(e3,e1) | e2 = op(e3,e0)) & (e1 = op(e3,e3) | e1 = op(e2,e3) | e1 = op(e1,e3) | e1 = op(e0,e3)) & (e1 = op(e3,e3) | e1 = op(e3,e2) | e1 = op(e3,e1) | e1 = op(e3,e0)) & (e0 = op(e3,e3) | e0 = op(e2,e3) | e0 = op(e1,e3) | e0 = op(e0,e3)) & (e0 = op(e3,e3) | e0 = op(e3,e2) | e0 = op(e3,e1) | e0 = op(e3,e0)) & (e3 = op(e3,e2) | e3 = op(e2,e2) | e3 = op(e1,e2) | e3 = op(e0,e2)) & (e3 = op(e2,e3) | e3 = op(e2,e2) | e3 = op(e2,e1) | e3 = op(e2,e0)) & (e2 = op(e3,e2) | e2 = op(e2,e2) | e2 = op(e1,e2) | e2 = op(e0,e2)) & (e2 = op(e2,e3) | e2 = op(e2,e2) | e2 = op(e2,e1) | e2 = op(e2,e0)) & (e1 = op(e3,e2) | e1 = op(e2,e2) | e1 = op(e1,e2) | e1 = op(e0,e2)) & (e1 = op(e2,e3) | e1 = op(e2,e2) | e1 = op(e2,e1) | e1 = op(e2,e0)) & (e0 = op(e3,e2) | e0 = op(e2,e2) | e0 = op(e1,e2) | e0 = op(e0,e2)) & (e0 = op(e2,e3) | e0 = op(e2,e2) | e0 = op(e2,e1) | e0 = op(e2,e0)) & (e3 = op(e3,e1) | e3 = op(e2,e1) | e3 = op(e1,e1) | e3 = op(e0,e1)) & (e3 = op(e1,e3) | e3 = op(e1,e2) | e3 = op(e1,e1) | e3 = op(e1,e0)) & (e2 = op(e3,e1) | e2 = op(e2,e1) | e2 = op(e1,e1) | e2 = op(e0,e1)) & (e2 = op(e1,e3) | e2 = op(e1,e2) | e2 = op(e1,e1) | e2 = op(e1,e0)) & (e1 = op(e3,e1) | e1 = op(e2,e1) | e1 = op(e1,e1) | e1 = op(e0,e1)) & (e1 = op(e1,e3) | e1 = op(e1,e2) | e1 = op(e1,e1) | e1 = op(e1,e0)) & (e0 = op(e3,e1) | e0 = op(e2,e1) | e0 = op(e1,e1) | e0 = op(e0,e1)) & (e0 = op(e1,e3) | e0 = op(e1,e2) | e0 = op(e1,e1) | e0 = op(e1,e0)) & (e3 = op(e3,e0) | e3 = op(e2,e0) | e3 = op(e1,e0) | e3 = op(e0,e0)) & (e3 = op(e0,e3) | e3 = op(e0,e2) | e3 = op(e0,e1) | e3 = op(e0,e0)) & (e2 = op(e3,e0) | e2 = op(e2,e0) | e2 = op(e1,e0) | e2 = op(e0,e0)) & (e2 = op(e0,e3) | e2 = op(e0,e2) | e2 = op(e0,e1) | e2 = op(e0,e0)) & (e1 = op(e3,e0) | e1 = op(e2,e0) | e1 = op(e1,e0) | e1 = op(e0,e0)) & (e1 = op(e0,e3) | e1 = op(e0,e2) | e1 = op(e0,e1) | e1 = op(e0,e0)) & (e0 = op(e3,e0) | e0 = op(e2,e0) | e0 = op(e1,e0) | e0 = op(e0,e0)) & (e0 = op(e0,e3) | e0 = op(e0,e2) | e0 = op(e0,e1) | e0 = op(e0,e0)) & (e3 = unit | e2 = unit | e1 = unit | e0 = unit) & e3 = op(e3,unit) & e3 = op(unit,e3) & e2 = op(e2,unit) & e2 = op(unit,e2) & e1 = op(e1,unit) & e1 = op(unit,e1) & e0 = op(e0,unit) & e0 = op(unit,e0) & (e3 = op(e3,e3) | e2 = op(e3,e3) | e1 = op(e3,e3) | e0 = op(e3,e3)) & (e3 = op(e3,e2) | e2 = op(e3,e2) | e1 = op(e3,e2) | e0 = op(e3,e2)) & (e3 = op(e3,e1) | e2 = op(e3,e1) | e1 = op(e3,e1) | e0 = op(e3,e1)) & (e3 = op(e3,e0) | e2 = op(e3,e0) | e1 = op(e3,e0) | e0 = op(e3,e0)) & (e3 = op(e2,e3) | e2 = op(e2,e3) | e1 = op(e2,e3) | e0 = op(e2,e3)) & (e3 = op(e2,e2) | e2 = op(e2,e2) | e1 = op(e2,e2) | e0 = op(e2,e2)) & (e3 = op(e2,e1) | e2 = op(e2,e1) | e1 = op(e2,e1) | e0 = op(e2,e1)) & (e3 = op(e2,e0) | e2 = op(e2,e0) | e1 = op(e2,e0) | e0 = op(e2,e0)) & (e3 = op(e1,e3) | e2 = op(e1,e3) | e1 = op(e1,e3) | e0 = op(e1,e3)) & (e3 = op(e1,e2) | e2 = op(e1,e2) | e1 = op(e1,e2) | e0 = op(e1,e2)) & (e3 = op(e1,e1) | e2 = op(e1,e1) | e1 = op(e1,e1) | e0 = op(e1,e1)) & (e3 = op(e1,e0) | e2 = op(e1,e0) | e1 = op(e1,e0) | e0 = op(e1,e0)) & (e3 = op(e0,e3) | e2 = op(e0,e3) | e1 = op(e0,e3) | e0 = op(e0,e3)) & (e3 = op(e0,e2) | e2 = op(e0,e2) | e1 = op(e0,e2) | e0 = op(e0,e2)) & (e3 = op(e0,e1) | e2 = op(e0,e1) | e1 = op(e0,e1) | e0 = op(e0,e1)) & (e3 = op(e0,e0) | e2 = op(e0,e0) | e1 = op(e0,e0) | e0 = op(e0,e0)) & ((e3 = op(e3,e3) & e3 = op(e2,e2) & e3 = op(e1,e1) & e3 = op(e0,e0)) | (e2 = op(e3,e3) & e2 = op(e2,e2) & e2 = op(e1,e1) & e2 = op(e0,e0)) | (e1 = op(e3,e3) & e1 = op(e2,e2) & e1 = op(e1,e1) & e1 = op(e0,e0)) | (e0 = op(e3,e3) & e0 = op(e2,e2) & e0 = op(e1,e1) & e0 = op(e0,e0)))), + file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)). +fof(f5,negated_conjecture,( + ~((e3 = op(e3,e3) | e3 = op(e2,e3) | e3 = op(e1,e3) | e3 = op(e0,e3)) & (e3 = op(e3,e3) | e3 = op(e3,e2) | e3 = op(e3,e1) | e3 = op(e3,e0)) & (e2 = op(e3,e3) | e2 = op(e2,e3) | e2 = op(e1,e3) | e2 = op(e0,e3)) & (e2 = op(e3,e3) | e2 = op(e3,e2) | e2 = op(e3,e1) | e2 = op(e3,e0)) & (e1 = op(e3,e3) | e1 = op(e2,e3) | e1 = op(e1,e3) | e1 = op(e0,e3)) & (e1 = op(e3,e3) | e1 = op(e3,e2) | e1 = op(e3,e1) | e1 = op(e3,e0)) & (e0 = op(e3,e3) | e0 = op(e2,e3) | e0 = op(e1,e3) | e0 = op(e0,e3)) & (e0 = op(e3,e3) | e0 = op(e3,e2) | e0 = op(e3,e1) | e0 = op(e3,e0)) & (e3 = op(e3,e2) | e3 = op(e2,e2) | e3 = op(e1,e2) | e3 = op(e0,e2)) & (e3 = op(e2,e3) | e3 = op(e2,e2) | e3 = op(e2,e1) | e3 = op(e2,e0)) & (e2 = op(e3,e2) | e2 = op(e2,e2) | e2 = op(e1,e2) | e2 = op(e0,e2)) & (e2 = op(e2,e3) | e2 = op(e2,e2) | e2 = op(e2,e1) | e2 = op(e2,e0)) & (e1 = op(e3,e2) | e1 = op(e2,e2) | e1 = op(e1,e2) | e1 = op(e0,e2)) & (e1 = op(e2,e3) | e1 = op(e2,e2) | e1 = op(e2,e1) | e1 = op(e2,e0)) & (e0 = op(e3,e2) | e0 = op(e2,e2) | e0 = op(e1,e2) | e0 = op(e0,e2)) & (e0 = op(e2,e3) | e0 = op(e2,e2) | e0 = op(e2,e1) | e0 = op(e2,e0)) & (e3 = op(e3,e1) | e3 = op(e2,e1) | e3 = op(e1,e1) | e3 = op(e0,e1)) & (e3 = op(e1,e3) | e3 = op(e1,e2) | e3 = op(e1,e1) | e3 = op(e1,e0)) & (e2 = op(e3,e1) | e2 = op(e2,e1) | e2 = op(e1,e1) | e2 = op(e0,e1)) & (e2 = op(e1,e3) | e2 = op(e1,e2) | e2 = op(e1,e1) | e2 = op(e1,e0)) & (e1 = op(e3,e1) | e1 = op(e2,e1) | e1 = op(e1,e1) | e1 = op(e0,e1)) & (e1 = op(e1,e3) | e1 = op(e1,e2) | e1 = op(e1,e1) | e1 = op(e1,e0)) & (e0 = op(e3,e1) | e0 = op(e2,e1) | e0 = op(e1,e1) | e0 = op(e0,e1)) & (e0 = op(e1,e3) | e0 = op(e1,e2) | e0 = op(e1,e1) | e0 = op(e1,e0)) & (e3 = op(e3,e0) | e3 = op(e2,e0) | e3 = op(e1,e0) | e3 = op(e0,e0)) & (e3 = op(e0,e3) | e3 = op(e0,e2) | e3 = op(e0,e1) | e3 = op(e0,e0)) & (e2 = op(e3,e0) | e2 = op(e2,e0) | e2 = op(e1,e0) | e2 = op(e0,e0)) & (e2 = op(e0,e3) | e2 = op(e0,e2) | e2 = op(e0,e1) | e2 = op(e0,e0)) & (e1 = op(e3,e0) | e1 = op(e2,e0) | e1 = op(e1,e0) | e1 = op(e0,e0)) & (e1 = op(e0,e3) | e1 = op(e0,e2) | e1 = op(e0,e1) | e1 = op(e0,e0)) & (e0 = op(e3,e0) | e0 = op(e2,e0) | e0 = op(e1,e0) | e0 = op(e0,e0)) & (e0 = op(e0,e3) | e0 = op(e0,e2) | e0 = op(e0,e1) | e0 = op(e0,e0)) & (e3 = unit | e2 = unit | e1 = unit | e0 = unit) & e3 = op(e3,unit) & e3 = op(unit,e3) & e2 = op(e2,unit) & e2 = op(unit,e2) & e1 = op(e1,unit) & e1 = op(unit,e1) & e0 = op(e0,unit) & e0 = op(unit,e0) & (e3 = op(e3,e3) | e2 = op(e3,e3) | e1 = op(e3,e3) | e0 = op(e3,e3)) & (e3 = op(e3,e2) | e2 = op(e3,e2) | e1 = op(e3,e2) | e0 = op(e3,e2)) & (e3 = op(e3,e1) | e2 = op(e3,e1) | e1 = op(e3,e1) | e0 = op(e3,e1)) & (e3 = op(e3,e0) | e2 = op(e3,e0) | e1 = op(e3,e0) | e0 = op(e3,e0)) & (e3 = op(e2,e3) | e2 = op(e2,e3) | e1 = op(e2,e3) | e0 = op(e2,e3)) & (e3 = op(e2,e2) | e2 = op(e2,e2) | e1 = op(e2,e2) | e0 = op(e2,e2)) & (e3 = op(e2,e1) | e2 = op(e2,e1) | e1 = op(e2,e1) | e0 = op(e2,e1)) & (e3 = op(e2,e0) | e2 = op(e2,e0) | e1 = op(e2,e0) | e0 = op(e2,e0)) & (e3 = op(e1,e3) | e2 = op(e1,e3) | e1 = op(e1,e3) | e0 = op(e1,e3)) & (e3 = op(e1,e2) | e2 = op(e1,e2) | e1 = op(e1,e2) | e0 = op(e1,e2)) & (e3 = op(e1,e1) | e2 = op(e1,e1) | e1 = op(e1,e1) | e0 = op(e1,e1)) & (e3 = op(e1,e0) | e2 = op(e1,e0) | e1 = op(e1,e0) | e0 = op(e1,e0)) & (e3 = op(e0,e3) | e2 = op(e0,e3) | e1 = op(e0,e3) | e0 = op(e0,e3)) & (e3 = op(e0,e2) | e2 = op(e0,e2) | e1 = op(e0,e2) | e0 = op(e0,e2)) & (e3 = op(e0,e1) | e2 = op(e0,e1) | e1 = op(e0,e1) | e0 = op(e0,e1)) & (e3 = op(e0,e0) | e2 = op(e0,e0) | e1 = op(e0,e0) | e0 = op(e0,e0)) & ((e3 = op(e3,e3) & e3 = op(e2,e2) & e3 = op(e1,e1) & e3 = op(e0,e0)) | (e2 = op(e3,e3) & e2 = op(e2,e2) & e2 = op(e1,e1) & e2 = op(e0,e0)) | (e1 = op(e3,e3) & e1 = op(e2,e2) & e1 = op(e1,e1) & e1 = op(e0,e0)) | (e0 = op(e3,e3) & e0 = op(e2,e2) & e0 = op(e1,e1) & e0 = op(e0,e0))))), + inference(negated_conjecture,[],[f4])). +fof(f6,plain,( + (e3 != op(e3,e3) & e3 != op(e2,e3) & e3 != op(e1,e3) & e3 != op(e0,e3)) | (e3 != op(e3,e3) & e3 != op(e3,e2) & e3 != op(e3,e1) & e3 != op(e3,e0)) | (e2 != op(e3,e3) & e2 != op(e2,e3) & e2 != op(e1,e3) & e2 != op(e0,e3)) | (e2 != op(e3,e3) & e2 != op(e3,e2) & e2 != op(e3,e1) & e2 != op(e3,e0)) | (e1 != op(e3,e3) & e1 != op(e2,e3) & e1 != op(e1,e3) & e1 != op(e0,e3)) | (e1 != op(e3,e3) & e1 != op(e3,e2) & e1 != op(e3,e1) & e1 != op(e3,e0)) | (e0 != op(e3,e3) & e0 != op(e2,e3) & e0 != op(e1,e3) & e0 != op(e0,e3)) | (e0 != op(e3,e3) & e0 != op(e3,e2) & e0 != op(e3,e1) & e0 != op(e3,e0)) | (e3 != op(e3,e2) & e3 != op(e2,e2) & e3 != op(e1,e2) & e3 != op(e0,e2)) | (e3 != op(e2,e3) & e3 != op(e2,e2) & e3 != op(e2,e1) & e3 != op(e2,e0)) | (e2 != op(e3,e2) & e2 != op(e2,e2) & e2 != op(e1,e2) & e2 != op(e0,e2)) | (e2 != op(e2,e3) & e2 != op(e2,e2) & e2 != op(e2,e1) & e2 != op(e2,e0)) | (e1 != op(e3,e2) & e1 != op(e2,e2) & e1 != op(e1,e2) & e1 != op(e0,e2)) | (e1 != op(e2,e3) & e1 != op(e2,e2) & e1 != op(e2,e1) & e1 != op(e2,e0)) | (e0 != op(e3,e2) & e0 != op(e2,e2) & e0 != op(e1,e2) & e0 != op(e0,e2)) | (e0 != op(e2,e3) & e0 != op(e2,e2) & e0 != op(e2,e1) & e0 != op(e2,e0)) | (e3 != op(e3,e1) & e3 != op(e2,e1) & e3 != op(e1,e1) & e3 != op(e0,e1)) | (e3 != op(e1,e3) & e3 != op(e1,e2) & e3 != op(e1,e1) & e3 != op(e1,e0)) | (e2 != op(e3,e1) & e2 != op(e2,e1) & e2 != op(e1,e1) & e2 != op(e0,e1)) | (e2 != op(e1,e3) & e2 != op(e1,e2) & e2 != op(e1,e1) & e2 != op(e1,e0)) | (e1 != op(e3,e1) & e1 != op(e2,e1) & e1 != op(e1,e1) & e1 != op(e0,e1)) | (e1 != op(e1,e3) & e1 != op(e1,e2) & e1 != op(e1,e1) & e1 != op(e1,e0)) | (e0 != op(e3,e1) & e0 != op(e2,e1) & e0 != op(e1,e1) & e0 != op(e0,e1)) | (e0 != op(e1,e3) & e0 != op(e1,e2) & e0 != op(e1,e1) & e0 != op(e1,e0)) | (e3 != op(e3,e0) & e3 != op(e2,e0) & e3 != op(e1,e0) & e3 != op(e0,e0)) | (e3 != op(e0,e3) & e3 != op(e0,e2) & e3 != op(e0,e1) & e3 != op(e0,e0)) | (e2 != op(e3,e0) & e2 != op(e2,e0) & e2 != op(e1,e0) & e2 != op(e0,e0)) | (e2 != op(e0,e3) & e2 != op(e0,e2) & e2 != op(e0,e1) & e2 != op(e0,e0)) | (e1 != op(e3,e0) & e1 != op(e2,e0) & e1 != op(e1,e0) & e1 != op(e0,e0)) | (e1 != op(e0,e3) & e1 != op(e0,e2) & e1 != op(e0,e1) & e1 != op(e0,e0)) | (e0 != op(e3,e0) & e0 != op(e2,e0) & e0 != op(e1,e0) & e0 != op(e0,e0)) | (e0 != op(e0,e3) & e0 != op(e0,e2) & e0 != op(e0,e1) & e0 != op(e0,e0)) | (e3 != unit & e2 != unit & e1 != unit & e0 != unit) | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | e0 != op(e0,unit) | e0 != op(unit,e0) | (e3 != op(e3,e3) & e2 != op(e3,e3) & e1 != op(e3,e3) & e0 != op(e3,e3)) | (e3 != op(e3,e2) & e2 != op(e3,e2) & e1 != op(e3,e2) & e0 != op(e3,e2)) | (e3 != op(e3,e1) & e2 != op(e3,e1) & e1 != op(e3,e1) & e0 != op(e3,e1)) | (e3 != op(e3,e0) & e2 != op(e3,e0) & e1 != op(e3,e0) & e0 != op(e3,e0)) | (e3 != op(e2,e3) & e2 != op(e2,e3) & e1 != op(e2,e3) & e0 != op(e2,e3)) | (e3 != op(e2,e2) & e2 != op(e2,e2) & e1 != op(e2,e2) & e0 != op(e2,e2)) | (e3 != op(e2,e1) & e2 != op(e2,e1) & e1 != op(e2,e1) & e0 != op(e2,e1)) | (e3 != op(e2,e0) & e2 != op(e2,e0) & e1 != op(e2,e0) & e0 != op(e2,e0)) | (e3 != op(e1,e3) & e2 != op(e1,e3) & e1 != op(e1,e3) & e0 != op(e1,e3)) | (e3 != op(e1,e2) & e2 != op(e1,e2) & e1 != op(e1,e2) & e0 != op(e1,e2)) | (e3 != op(e1,e1) & e2 != op(e1,e1) & e1 != op(e1,e1) & e0 != op(e1,e1)) | (e3 != op(e1,e0) & e2 != op(e1,e0) & e1 != op(e1,e0) & e0 != op(e1,e0)) | (e3 != op(e0,e3) & e2 != op(e0,e3) & e1 != op(e0,e3) & e0 != op(e0,e3)) | (e3 != op(e0,e2) & e2 != op(e0,e2) & e1 != op(e0,e2) & e0 != op(e0,e2)) | (e3 != op(e0,e1) & e2 != op(e0,e1) & e1 != op(e0,e1) & e0 != op(e0,e1)) | (e3 != op(e0,e0) & e2 != op(e0,e0) & e1 != op(e0,e0) & e0 != op(e0,e0)) | ((e3 != op(e3,e3) | e3 != op(e2,e2) | e3 != op(e1,e1) | e3 != op(e0,e0)) & (e2 != op(e3,e3) | e2 != op(e2,e2) | e2 != op(e1,e1) | e2 != op(e0,e0)) & (e1 != op(e3,e3) | e1 != op(e2,e2) | e1 != op(e1,e1) | e1 != op(e0,e0)) & (e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0)))), + inference(ennf_transformation,[],[f5])). +fof(f7,plain,( + ((e3 != op(e3,e3) | e3 != op(e2,e2) | e3 != op(e1,e1) | e3 != op(e0,e0)) & (e2 != op(e3,e3) | e2 != op(e2,e2) | e2 != op(e1,e1) | e2 != op(e0,e0)) & (e1 != op(e3,e3) | e1 != op(e2,e2) | e1 != op(e1,e1) | e1 != op(e0,e0)) & (e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0))) | ~sP0), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP0])])). +fof(f8,plain,( + (e3 != op(e0,e0) & e2 != op(e0,e0) & e1 != op(e0,e0) & e0 != op(e0,e0)) | ~sP1), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP1])])). +fof(f9,plain,( + (e3 != op(e0,e1) & e2 != op(e0,e1) & e1 != op(e0,e1) & e0 != op(e0,e1)) | ~sP2), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP2])])). +fof(f10,plain,( + (e3 != op(e0,e2) & e2 != op(e0,e2) & e1 != op(e0,e2) & e0 != op(e0,e2)) | ~sP3), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP3])])). +fof(f11,plain,( + (e3 != op(e0,e3) & e2 != op(e0,e3) & e1 != op(e0,e3) & e0 != op(e0,e3)) | ~sP4), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP4])])). +fof(f12,plain,( + (e3 != op(e1,e0) & e2 != op(e1,e0) & e1 != op(e1,e0) & e0 != op(e1,e0)) | ~sP5), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP5])])). +fof(f13,plain,( + (e3 != op(e1,e1) & e2 != op(e1,e1) & e1 != op(e1,e1) & e0 != op(e1,e1)) | ~sP6), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP6])])). +fof(f14,plain,( + (e3 != op(e1,e2) & e2 != op(e1,e2) & e1 != op(e1,e2) & e0 != op(e1,e2)) | ~sP7), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP7])])). +fof(f15,plain,( + (e3 != op(e1,e3) & e2 != op(e1,e3) & e1 != op(e1,e3) & e0 != op(e1,e3)) | ~sP8), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP8])])). +fof(f16,plain,( + (e3 != op(e2,e0) & e2 != op(e2,e0) & e1 != op(e2,e0) & e0 != op(e2,e0)) | ~sP9), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP9])])). +fof(f17,plain,( + (e3 != op(e2,e1) & e2 != op(e2,e1) & e1 != op(e2,e1) & e0 != op(e2,e1)) | ~sP10), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP10])])). +fof(f18,plain,( + (e3 != op(e2,e2) & e2 != op(e2,e2) & e1 != op(e2,e2) & e0 != op(e2,e2)) | ~sP11), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP11])])). +fof(f19,plain,( + (e3 != op(e2,e3) & e2 != op(e2,e3) & e1 != op(e2,e3) & e0 != op(e2,e3)) | ~sP12), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP12])])). +fof(f20,plain,( + (e3 != op(e3,e0) & e2 != op(e3,e0) & e1 != op(e3,e0) & e0 != op(e3,e0)) | ~sP13), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP13])])). +fof(f21,plain,( + (e3 != op(e3,e1) & e2 != op(e3,e1) & e1 != op(e3,e1) & e0 != op(e3,e1)) | ~sP14), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP14])])). +fof(f22,plain,( + (e3 != op(e3,e2) & e2 != op(e3,e2) & e1 != op(e3,e2) & e0 != op(e3,e2)) | ~sP15), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP15])])). +fof(f23,plain,( + (e3 != op(e3,e3) & e2 != op(e3,e3) & e1 != op(e3,e3) & e0 != op(e3,e3)) | ~sP16), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP16])])). +fof(f24,plain,( + (e3 != unit & e2 != unit & e1 != unit & e0 != unit) | ~sP17), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP17])])). +fof(f25,plain,( + (e0 != op(e0,e3) & e0 != op(e0,e2) & e0 != op(e0,e1) & e0 != op(e0,e0)) | ~sP18), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP18])])). +fof(f26,plain,( + (e0 != op(e3,e0) & e0 != op(e2,e0) & e0 != op(e1,e0) & e0 != op(e0,e0)) | ~sP19), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP19])])). +fof(f27,plain,( + (e1 != op(e0,e3) & e1 != op(e0,e2) & e1 != op(e0,e1) & e1 != op(e0,e0)) | ~sP20), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP20])])). +fof(f28,plain,( + (e1 != op(e3,e0) & e1 != op(e2,e0) & e1 != op(e1,e0) & e1 != op(e0,e0)) | ~sP21), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP21])])). +fof(f29,plain,( + (e2 != op(e0,e3) & e2 != op(e0,e2) & e2 != op(e0,e1) & e2 != op(e0,e0)) | ~sP22), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP22])])). +fof(f30,plain,( + (e2 != op(e3,e0) & e2 != op(e2,e0) & e2 != op(e1,e0) & e2 != op(e0,e0)) | ~sP23), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP23])])). +fof(f31,plain,( + (e3 != op(e0,e3) & e3 != op(e0,e2) & e3 != op(e0,e1) & e3 != op(e0,e0)) | ~sP24), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP24])])). +fof(f32,plain,( + (e3 != op(e3,e0) & e3 != op(e2,e0) & e3 != op(e1,e0) & e3 != op(e0,e0)) | ~sP25), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP25])])). +fof(f33,plain,( + (e0 != op(e1,e3) & e0 != op(e1,e2) & e0 != op(e1,e1) & e0 != op(e1,e0)) | ~sP26), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP26])])). +fof(f34,plain,( + (e0 != op(e3,e1) & e0 != op(e2,e1) & e0 != op(e1,e1) & e0 != op(e0,e1)) | ~sP27), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP27])])). +fof(f35,plain,( + (e1 != op(e1,e3) & e1 != op(e1,e2) & e1 != op(e1,e1) & e1 != op(e1,e0)) | ~sP28), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP28])])). +fof(f36,plain,( + (e1 != op(e3,e1) & e1 != op(e2,e1) & e1 != op(e1,e1) & e1 != op(e0,e1)) | ~sP29), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP29])])). +fof(f37,plain,( + (e2 != op(e1,e3) & e2 != op(e1,e2) & e2 != op(e1,e1) & e2 != op(e1,e0)) | ~sP30), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP30])])). +fof(f38,plain,( + (e2 != op(e3,e1) & e2 != op(e2,e1) & e2 != op(e1,e1) & e2 != op(e0,e1)) | ~sP31), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP31])])). +fof(f39,plain,( + (e3 != op(e1,e3) & e3 != op(e1,e2) & e3 != op(e1,e1) & e3 != op(e1,e0)) | ~sP32), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP32])])). +fof(f40,plain,( + (e3 != op(e3,e1) & e3 != op(e2,e1) & e3 != op(e1,e1) & e3 != op(e0,e1)) | ~sP33), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP33])])). +fof(f41,plain,( + (e0 != op(e2,e3) & e0 != op(e2,e2) & e0 != op(e2,e1) & e0 != op(e2,e0)) | ~sP34), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP34])])). +fof(f42,plain,( + (e0 != op(e3,e2) & e0 != op(e2,e2) & e0 != op(e1,e2) & e0 != op(e0,e2)) | ~sP35), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP35])])). +fof(f43,plain,( + (e1 != op(e2,e3) & e1 != op(e2,e2) & e1 != op(e2,e1) & e1 != op(e2,e0)) | ~sP36), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP36])])). +fof(f44,plain,( + (e1 != op(e3,e2) & e1 != op(e2,e2) & e1 != op(e1,e2) & e1 != op(e0,e2)) | ~sP37), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP37])])). +fof(f45,plain,( + (e2 != op(e2,e3) & e2 != op(e2,e2) & e2 != op(e2,e1) & e2 != op(e2,e0)) | ~sP38), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP38])])). +fof(f46,plain,( + (e2 != op(e3,e2) & e2 != op(e2,e2) & e2 != op(e1,e2) & e2 != op(e0,e2)) | ~sP39), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP39])])). +fof(f47,plain,( + (e3 != op(e2,e3) & e3 != op(e2,e2) & e3 != op(e2,e1) & e3 != op(e2,e0)) | ~sP40), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP40])])). +fof(f48,plain,( + (e3 != op(e3,e2) & e3 != op(e2,e2) & e3 != op(e1,e2) & e3 != op(e0,e2)) | ~sP41), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP41])])). +fof(f49,plain,( + (e0 != op(e3,e3) & e0 != op(e3,e2) & e0 != op(e3,e1) & e0 != op(e3,e0)) | ~sP42), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP42])])). +fof(f50,plain,( + (e0 != op(e3,e3) & e0 != op(e2,e3) & e0 != op(e1,e3) & e0 != op(e0,e3)) | ~sP43), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP43])])). +fof(f51,plain,( + (e1 != op(e3,e3) & e1 != op(e3,e2) & e1 != op(e3,e1) & e1 != op(e3,e0)) | ~sP44), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP44])])). +fof(f52,plain,( + (e1 != op(e3,e3) & e1 != op(e2,e3) & e1 != op(e1,e3) & e1 != op(e0,e3)) | ~sP45), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP45])])). +fof(f53,plain,( + (e2 != op(e3,e3) & e2 != op(e3,e2) & e2 != op(e3,e1) & e2 != op(e3,e0)) | ~sP46), + introduced(predicate_definition_introduction,[new_symbols(naming,[sP46])])). +fof(f54,plain,( + (e3 != op(e3,e3) & e3 != op(e2,e3) & e3 != op(e1,e3) & e3 != op(e0,e3)) | (e3 != op(e3,e3) & e3 != op(e3,e2) & e3 != op(e3,e1) & e3 != op(e3,e0)) | (e2 != op(e3,e3) & e2 != op(e2,e3) & e2 != op(e1,e3) & e2 != op(e0,e3)) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | e0 != op(e0,unit) | e0 != op(unit,e0) | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0), + inference(definition_folding,[],[f6,f53,f52,f51,f50,f49,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7])). +fof(f55,plain,( + (e2 != op(e3,e3) & e2 != op(e3,e2) & e2 != op(e3,e1) & e2 != op(e3,e0)) | ~sP46), + inference(nnf_transformation,[],[f53])). +fof(f56,plain,( + (e1 != op(e3,e3) & e1 != op(e2,e3) & e1 != op(e1,e3) & e1 != op(e0,e3)) | ~sP45), + inference(nnf_transformation,[],[f52])). +fof(f57,plain,( + (e1 != op(e3,e3) & e1 != op(e3,e2) & e1 != op(e3,e1) & e1 != op(e3,e0)) | ~sP44), + inference(nnf_transformation,[],[f51])). +fof(f58,plain,( + (e0 != op(e3,e3) & e0 != op(e2,e3) & e0 != op(e1,e3) & e0 != op(e0,e3)) | ~sP43), + inference(nnf_transformation,[],[f50])). +fof(f59,plain,( + (e0 != op(e3,e3) & e0 != op(e3,e2) & e0 != op(e3,e1) & e0 != op(e3,e0)) | ~sP42), + inference(nnf_transformation,[],[f49])). +fof(f60,plain,( + (e3 != op(e3,e2) & e3 != op(e2,e2) & e3 != op(e1,e2) & e3 != op(e0,e2)) | ~sP41), + inference(nnf_transformation,[],[f48])). +fof(f61,plain,( + (e3 != op(e2,e3) & e3 != op(e2,e2) & e3 != op(e2,e1) & e3 != op(e2,e0)) | ~sP40), + inference(nnf_transformation,[],[f47])). +fof(f62,plain,( + (e2 != op(e3,e2) & e2 != op(e2,e2) & e2 != op(e1,e2) & e2 != op(e0,e2)) | ~sP39), + inference(nnf_transformation,[],[f46])). +fof(f63,plain,( + (e2 != op(e2,e3) & e2 != op(e2,e2) & e2 != op(e2,e1) & e2 != op(e2,e0)) | ~sP38), + inference(nnf_transformation,[],[f45])). +fof(f64,plain,( + (e1 != op(e3,e2) & e1 != op(e2,e2) & e1 != op(e1,e2) & e1 != op(e0,e2)) | ~sP37), + inference(nnf_transformation,[],[f44])). +fof(f65,plain,( + (e1 != op(e2,e3) & e1 != op(e2,e2) & e1 != op(e2,e1) & e1 != op(e2,e0)) | ~sP36), + inference(nnf_transformation,[],[f43])). +fof(f66,plain,( + (e0 != op(e3,e2) & e0 != op(e2,e2) & e0 != op(e1,e2) & e0 != op(e0,e2)) | ~sP35), + inference(nnf_transformation,[],[f42])). +fof(f67,plain,( + (e0 != op(e2,e3) & e0 != op(e2,e2) & e0 != op(e2,e1) & e0 != op(e2,e0)) | ~sP34), + inference(nnf_transformation,[],[f41])). +fof(f68,plain,( + (e3 != op(e3,e1) & e3 != op(e2,e1) & e3 != op(e1,e1) & e3 != op(e0,e1)) | ~sP33), + inference(nnf_transformation,[],[f40])). +fof(f69,plain,( + (e3 != op(e1,e3) & e3 != op(e1,e2) & e3 != op(e1,e1) & e3 != op(e1,e0)) | ~sP32), + inference(nnf_transformation,[],[f39])). +fof(f70,plain,( + (e2 != op(e3,e1) & e2 != op(e2,e1) & e2 != op(e1,e1) & e2 != op(e0,e1)) | ~sP31), + inference(nnf_transformation,[],[f38])). +fof(f71,plain,( + (e2 != op(e1,e3) & e2 != op(e1,e2) & e2 != op(e1,e1) & e2 != op(e1,e0)) | ~sP30), + inference(nnf_transformation,[],[f37])). +fof(f72,plain,( + (e1 != op(e3,e1) & e1 != op(e2,e1) & e1 != op(e1,e1) & e1 != op(e0,e1)) | ~sP29), + inference(nnf_transformation,[],[f36])). +fof(f73,plain,( + (e1 != op(e1,e3) & e1 != op(e1,e2) & e1 != op(e1,e1) & e1 != op(e1,e0)) | ~sP28), + inference(nnf_transformation,[],[f35])). +fof(f74,plain,( + (e0 != op(e3,e1) & e0 != op(e2,e1) & e0 != op(e1,e1) & e0 != op(e0,e1)) | ~sP27), + inference(nnf_transformation,[],[f34])). +fof(f75,plain,( + (e0 != op(e1,e3) & e0 != op(e1,e2) & e0 != op(e1,e1) & e0 != op(e1,e0)) | ~sP26), + inference(nnf_transformation,[],[f33])). +fof(f76,plain,( + (e3 != op(e3,e0) & e3 != op(e2,e0) & e3 != op(e1,e0) & e3 != op(e0,e0)) | ~sP25), + inference(nnf_transformation,[],[f32])). +fof(f77,plain,( + (e3 != op(e0,e3) & e3 != op(e0,e2) & e3 != op(e0,e1) & e3 != op(e0,e0)) | ~sP24), + inference(nnf_transformation,[],[f31])). +fof(f78,plain,( + (e2 != op(e3,e0) & e2 != op(e2,e0) & e2 != op(e1,e0) & e2 != op(e0,e0)) | ~sP23), + inference(nnf_transformation,[],[f30])). +fof(f79,plain,( + (e2 != op(e0,e3) & e2 != op(e0,e2) & e2 != op(e0,e1) & e2 != op(e0,e0)) | ~sP22), + inference(nnf_transformation,[],[f29])). +fof(f80,plain,( + (e1 != op(e3,e0) & e1 != op(e2,e0) & e1 != op(e1,e0) & e1 != op(e0,e0)) | ~sP21), + inference(nnf_transformation,[],[f28])). +fof(f81,plain,( + (e1 != op(e0,e3) & e1 != op(e0,e2) & e1 != op(e0,e1) & e1 != op(e0,e0)) | ~sP20), + inference(nnf_transformation,[],[f27])). +fof(f82,plain,( + (e0 != op(e3,e0) & e0 != op(e2,e0) & e0 != op(e1,e0) & e0 != op(e0,e0)) | ~sP19), + inference(nnf_transformation,[],[f26])). +fof(f83,plain,( + (e0 != op(e0,e3) & e0 != op(e0,e2) & e0 != op(e0,e1) & e0 != op(e0,e0)) | ~sP18), + inference(nnf_transformation,[],[f25])). +fof(f84,plain,( + (e3 != unit & e2 != unit & e1 != unit & e0 != unit) | ~sP17), + inference(nnf_transformation,[],[f24])). +fof(f85,plain,( + (e3 != op(e3,e3) & e2 != op(e3,e3) & e1 != op(e3,e3) & e0 != op(e3,e3)) | ~sP16), + inference(nnf_transformation,[],[f23])). +fof(f86,plain,( + (e3 != op(e3,e2) & e2 != op(e3,e2) & e1 != op(e3,e2) & e0 != op(e3,e2)) | ~sP15), + inference(nnf_transformation,[],[f22])). +fof(f87,plain,( + (e3 != op(e3,e1) & e2 != op(e3,e1) & e1 != op(e3,e1) & e0 != op(e3,e1)) | ~sP14), + inference(nnf_transformation,[],[f21])). +fof(f88,plain,( + (e3 != op(e3,e0) & e2 != op(e3,e0) & e1 != op(e3,e0) & e0 != op(e3,e0)) | ~sP13), + inference(nnf_transformation,[],[f20])). +fof(f89,plain,( + (e3 != op(e2,e3) & e2 != op(e2,e3) & e1 != op(e2,e3) & e0 != op(e2,e3)) | ~sP12), + inference(nnf_transformation,[],[f19])). +fof(f90,plain,( + (e3 != op(e2,e2) & e2 != op(e2,e2) & e1 != op(e2,e2) & e0 != op(e2,e2)) | ~sP11), + inference(nnf_transformation,[],[f18])). +fof(f91,plain,( + (e3 != op(e2,e1) & e2 != op(e2,e1) & e1 != op(e2,e1) & e0 != op(e2,e1)) | ~sP10), + inference(nnf_transformation,[],[f17])). +fof(f92,plain,( + (e3 != op(e2,e0) & e2 != op(e2,e0) & e1 != op(e2,e0) & e0 != op(e2,e0)) | ~sP9), + inference(nnf_transformation,[],[f16])). +fof(f93,plain,( + (e3 != op(e1,e3) & e2 != op(e1,e3) & e1 != op(e1,e3) & e0 != op(e1,e3)) | ~sP8), + inference(nnf_transformation,[],[f15])). +fof(f94,plain,( + (e3 != op(e1,e2) & e2 != op(e1,e2) & e1 != op(e1,e2) & e0 != op(e1,e2)) | ~sP7), + inference(nnf_transformation,[],[f14])). +fof(f95,plain,( + (e3 != op(e1,e1) & e2 != op(e1,e1) & e1 != op(e1,e1) & e0 != op(e1,e1)) | ~sP6), + inference(nnf_transformation,[],[f13])). +fof(f96,plain,( + (e3 != op(e1,e0) & e2 != op(e1,e0) & e1 != op(e1,e0) & e0 != op(e1,e0)) | ~sP5), + inference(nnf_transformation,[],[f12])). +fof(f97,plain,( + (e3 != op(e0,e3) & e2 != op(e0,e3) & e1 != op(e0,e3) & e0 != op(e0,e3)) | ~sP4), + inference(nnf_transformation,[],[f11])). +fof(f98,plain,( + (e3 != op(e0,e2) & e2 != op(e0,e2) & e1 != op(e0,e2) & e0 != op(e0,e2)) | ~sP3), + inference(nnf_transformation,[],[f10])). +fof(f99,plain,( + (e3 != op(e0,e1) & e2 != op(e0,e1) & e1 != op(e0,e1) & e0 != op(e0,e1)) | ~sP2), + inference(nnf_transformation,[],[f9])). +fof(f100,plain,( + (e3 != op(e0,e0) & e2 != op(e0,e0) & e1 != op(e0,e0) & e0 != op(e0,e0)) | ~sP1), + inference(nnf_transformation,[],[f8])). +fof(f101,plain,( + ((e3 != op(e3,e3) | e3 != op(e2,e2) | e3 != op(e1,e1) | e3 != op(e0,e0)) & (e2 != op(e3,e3) | e2 != op(e2,e2) | e2 != op(e1,e1) | e2 != op(e0,e0)) & (e1 != op(e3,e3) | e1 != op(e2,e2) | e1 != op(e1,e1) | e1 != op(e0,e0)) & (e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0))) | ~sP0), + inference(nnf_transformation,[],[f7])). +fof(f103,plain,( + e2 != op(e3,e1) | ~sP46), + inference(cnf_transformation,[],[f55])). +fof(f108,plain,( + e1 != op(e2,e3) | ~sP45), + inference(cnf_transformation,[],[f56])). +fof(f112,plain,( + e1 != op(e3,e2) | ~sP44), + inference(cnf_transformation,[],[f57])). +fof(f117,plain,( + e0 != op(e3,e3) | ~sP43), + inference(cnf_transformation,[],[f58])). +fof(f121,plain,( + e0 != op(e3,e3) | ~sP42), + inference(cnf_transformation,[],[f59])). +fof(f123,plain,( + e3 != op(e1,e2) | ~sP41), + inference(cnf_transformation,[],[f60])). +fof(f127,plain,( + e3 != op(e2,e1) | ~sP40), + inference(cnf_transformation,[],[f61])). +fof(f130,plain,( + e2 != op(e0,e2) | ~sP39), + inference(cnf_transformation,[],[f62])). +fof(f134,plain,( + e2 != op(e2,e0) | ~sP38), + inference(cnf_transformation,[],[f63])). +fof(f141,plain,( + e1 != op(e3,e2) | ~sP37), + inference(cnf_transformation,[],[f64])). +fof(f145,plain,( + e1 != op(e2,e3) | ~sP36), + inference(cnf_transformation,[],[f65])). +fof(f148,plain,( + e0 != op(e2,e2) | ~sP35), + inference(cnf_transformation,[],[f66])). +fof(f152,plain,( + e0 != op(e2,e2) | ~sP34), + inference(cnf_transformation,[],[f67])). +fof(f156,plain,( + e3 != op(e2,e1) | ~sP33), + inference(cnf_transformation,[],[f68])). +fof(f160,plain,( + e3 != op(e1,e2) | ~sP32), + inference(cnf_transformation,[],[f69])). +fof(f165,plain,( + e2 != op(e3,e1) | ~sP31), + inference(cnf_transformation,[],[f70])). +fof(f169,plain,( + e2 != op(e1,e3) | ~sP30), + inference(cnf_transformation,[],[f71])). +fof(f170,plain,( + e1 != op(e0,e1) | ~sP29), + inference(cnf_transformation,[],[f72])). +fof(f174,plain,( + e1 != op(e1,e0) | ~sP28), + inference(cnf_transformation,[],[f73])). +fof(f179,plain,( + e0 != op(e1,e1) | ~sP27), + inference(cnf_transformation,[],[f74])). +fof(f183,plain,( + e0 != op(e1,e1) | ~sP26), + inference(cnf_transformation,[],[f75])). +fof(f189,plain,( + e3 != op(e3,e0) | ~sP25), + inference(cnf_transformation,[],[f76])). +fof(f193,plain,( + e3 != op(e0,e3) | ~sP24), + inference(cnf_transformation,[],[f77])). +fof(f196,plain,( + e2 != op(e2,e0) | ~sP23), + inference(cnf_transformation,[],[f78])). +fof(f200,plain,( + e2 != op(e0,e2) | ~sP22), + inference(cnf_transformation,[],[f79])). +fof(f203,plain,( + e1 != op(e1,e0) | ~sP21), + inference(cnf_transformation,[],[f80])). +fof(f207,plain,( + e1 != op(e0,e1) | ~sP20), + inference(cnf_transformation,[],[f81])). +fof(f210,plain,( + e0 != op(e0,e0) | ~sP19), + inference(cnf_transformation,[],[f82])). +fof(f214,plain,( + e0 != op(e0,e0) | ~sP18), + inference(cnf_transformation,[],[f83])). +fof(f218,plain,( + e0 != unit | ~sP17), + inference(cnf_transformation,[],[f84])). +fof(f222,plain,( + e0 != op(e3,e3) | ~sP16), + inference(cnf_transformation,[],[f85])). +fof(f227,plain,( + e1 != op(e3,e2) | ~sP15), + inference(cnf_transformation,[],[f86])). +fof(f232,plain,( + e2 != op(e3,e1) | ~sP14), + inference(cnf_transformation,[],[f87])). +fof(f237,plain,( + e3 != op(e3,e0) | ~sP13), + inference(cnf_transformation,[],[f88])). +fof(f239,plain,( + e1 != op(e2,e3) | ~sP12), + inference(cnf_transformation,[],[f89])). +fof(f242,plain,( + e0 != op(e2,e2) | ~sP11), + inference(cnf_transformation,[],[f90])). +fof(f249,plain,( + e3 != op(e2,e1) | ~sP10), + inference(cnf_transformation,[],[f91])). +fof(f252,plain,( + e2 != op(e2,e0) | ~sP9), + inference(cnf_transformation,[],[f92])). +fof(f256,plain,( + e2 != op(e1,e3) | ~sP8), + inference(cnf_transformation,[],[f93])). +fof(f261,plain,( + e3 != op(e1,e2) | ~sP7), + inference(cnf_transformation,[],[f94])). +fof(f262,plain,( + e0 != op(e1,e1) | ~sP6), + inference(cnf_transformation,[],[f95])). +fof(f267,plain,( + e1 != op(e1,e0) | ~sP5), + inference(cnf_transformation,[],[f96])). +fof(f273,plain,( + e3 != op(e0,e3) | ~sP4), + inference(cnf_transformation,[],[f97])). +fof(f276,plain,( + e2 != op(e0,e2) | ~sP3), + inference(cnf_transformation,[],[f98])). +fof(f279,plain,( + e1 != op(e0,e1) | ~sP2), + inference(cnf_transformation,[],[f99])). +fof(f282,plain,( + e0 != op(e0,e0) | ~sP1), + inference(cnf_transformation,[],[f100])). +fof(f286,plain,( + e0 != op(e3,e3) | e0 != op(e2,e2) | e0 != op(e1,e1) | e0 != op(e0,e0) | ~sP0), + inference(cnf_transformation,[],[f101])). +fof(f291,plain,( + e3 != op(e0,e3) | e3 != op(e3,e0) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | e0 != op(e0,unit) | e0 != op(unit,e0) | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0), + inference(cnf_transformation,[],[f54])). +fof(f354,plain,( + e0 = unit), + inference(cnf_transformation,[],[f3])). +fof(f361,plain,( + e0 = op(e0,e0)), + inference(cnf_transformation,[],[f2])). +fof(f362,plain,( + e1 = op(e0,e1)), + inference(cnf_transformation,[],[f2])). +fof(f363,plain,( + e2 = op(e0,e2)), + inference(cnf_transformation,[],[f2])). +fof(f364,plain,( + e3 = op(e0,e3)), + inference(cnf_transformation,[],[f2])). +fof(f365,plain,( + e1 = op(e1,e0)), + inference(cnf_transformation,[],[f2])). +fof(f366,plain,( + e0 = op(e1,e1)), + inference(cnf_transformation,[],[f2])). +fof(f367,plain,( + e3 = op(e1,e2)), + inference(cnf_transformation,[],[f2])). +fof(f368,plain,( + e2 = op(e1,e3)), + inference(cnf_transformation,[],[f2])). +fof(f369,plain,( + e2 = op(e2,e0)), + inference(cnf_transformation,[],[f2])). +fof(f370,plain,( + e3 = op(e2,e1)), + inference(cnf_transformation,[],[f2])). +fof(f371,plain,( + e0 = op(e2,e2)), + inference(cnf_transformation,[],[f2])). +fof(f372,plain,( + e1 = op(e2,e3)), + inference(cnf_transformation,[],[f2])). +fof(f373,plain,( + e3 = op(e3,e0)), + inference(cnf_transformation,[],[f2])). +fof(f374,plain,( + e2 = op(e3,e1)), + inference(cnf_transformation,[],[f2])). +fof(f375,plain,( + e1 = op(e3,e2)), + inference(cnf_transformation,[],[f2])). +fof(f376,plain,( + e0 = op(e3,e3)), + inference(cnf_transformation,[],[f2])). +fof(f380,plain,( + op(e3,e3) != unit | ~sP43), + inference(definition_unfolding,[],[f117,f354])). +fof(f384,plain,( + op(e3,e3) != unit | ~sP42), + inference(definition_unfolding,[],[f121,f354])). +fof(f390,plain,( + e2 != op(unit,e2) | ~sP39), + inference(definition_unfolding,[],[f130,f354])). +fof(f391,plain,( + e2 != op(e2,unit) | ~sP38), + inference(definition_unfolding,[],[f134,f354])). +fof(f395,plain,( + op(e2,e2) != unit | ~sP35), + inference(definition_unfolding,[],[f148,f354])). +fof(f399,plain,( + op(e2,e2) != unit | ~sP34), + inference(definition_unfolding,[],[f152,f354])). +fof(f406,plain,( + e1 != op(unit,e1) | ~sP29), + inference(definition_unfolding,[],[f170,f354])). +fof(f407,plain,( + e1 != op(e1,unit) | ~sP28), + inference(definition_unfolding,[],[f174,f354])). +fof(f410,plain,( + op(e1,e1) != unit | ~sP27), + inference(definition_unfolding,[],[f179,f354])). +fof(f414,plain,( + op(e1,e1) != unit | ~sP26), + inference(definition_unfolding,[],[f183,f354])). +fof(f416,plain,( + e3 != op(e3,unit) | ~sP25), + inference(definition_unfolding,[],[f189,f354])). +fof(f420,plain,( + e3 != op(unit,e3) | ~sP24), + inference(definition_unfolding,[],[f193,f354])). +fof(f425,plain,( + e2 != op(e2,unit) | ~sP23), + inference(definition_unfolding,[],[f196,f354])). +fof(f429,plain,( + e2 != op(unit,e2) | ~sP22), + inference(definition_unfolding,[],[f200,f354])). +fof(f434,plain,( + e1 != op(e1,unit) | ~sP21), + inference(definition_unfolding,[],[f203,f354])). +fof(f438,plain,( + e1 != op(unit,e1) | ~sP20), + inference(definition_unfolding,[],[f207,f354])). +fof(f443,plain,( + op(unit,unit) != unit | ~sP19), + inference(definition_unfolding,[],[f210,f354,f354,f354])). +fof(f447,plain,( + op(unit,unit) != unit | ~sP18), + inference(definition_unfolding,[],[f214,f354,f354,f354])). +fof(f448,plain,( + unit != unit | ~sP17), + inference(definition_unfolding,[],[f218,f354])). +fof(f449,plain,( + op(e3,e3) != unit | ~sP16), + inference(definition_unfolding,[],[f222,f354])). +fof(f452,plain,( + e3 != op(e3,unit) | ~sP13), + inference(definition_unfolding,[],[f237,f354])). +fof(f457,plain,( + op(e2,e2) != unit | ~sP11), + inference(definition_unfolding,[],[f242,f354])). +fof(f460,plain,( + e2 != op(e2,unit) | ~sP9), + inference(definition_unfolding,[],[f252,f354])). +fof(f465,plain,( + op(e1,e1) != unit | ~sP6), + inference(definition_unfolding,[],[f262,f354])). +fof(f468,plain,( + e1 != op(e1,unit) | ~sP5), + inference(definition_unfolding,[],[f267,f354])). +fof(f470,plain,( + e3 != op(unit,e3) | ~sP4), + inference(definition_unfolding,[],[f273,f354])). +fof(f475,plain,( + e2 != op(unit,e2) | ~sP3), + inference(definition_unfolding,[],[f276,f354])). +fof(f480,plain,( + e1 != op(unit,e1) | ~sP2), + inference(definition_unfolding,[],[f279,f354])). +fof(f485,plain,( + op(unit,unit) != unit | ~sP1), + inference(definition_unfolding,[],[f282,f354,f354,f354])). +fof(f489,plain,( + op(e3,e3) != unit | op(e2,e2) != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0), + inference(definition_unfolding,[],[f286,f354,f354,f354,f354,f354,f354])). +fof(f552,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e3 != op(e3,unit) | e3 != op(unit,e3) | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0), + inference(definition_unfolding,[],[f291,f354,f354,f354,f354,f354,f354])). +fof(f557,plain,( + op(e3,e3) = unit), + inference(definition_unfolding,[],[f376,f354])). +fof(f558,plain,( + e3 = op(e3,unit)), + inference(definition_unfolding,[],[f373,f354])). +fof(f559,plain,( + op(e2,e2) = unit), + inference(definition_unfolding,[],[f371,f354])). +fof(f560,plain,( + e2 = op(e2,unit)), + inference(definition_unfolding,[],[f369,f354])). +fof(f561,plain,( + op(e1,e1) = unit), + inference(definition_unfolding,[],[f366,f354])). +fof(f562,plain,( + e1 = op(e1,unit)), + inference(definition_unfolding,[],[f365,f354])). +fof(f563,plain,( + e3 = op(unit,e3)), + inference(definition_unfolding,[],[f364,f354])). +fof(f564,plain,( + e2 = op(unit,e2)), + inference(definition_unfolding,[],[f363,f354])). +fof(f565,plain,( + e1 = op(unit,e1)), + inference(definition_unfolding,[],[f362,f354])). +fof(f566,plain,( + op(unit,unit) = unit), + inference(definition_unfolding,[],[f361,f354,f354,f354])). +fof(f568,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | sP17 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0), + inference(duplicate_literal_removal,[],[f552])). +fof(f631,plain,( + ~sP17), + inference(trivial_inequality_removal,[],[f448])). +fof(f1912,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP1 | sP0), + inference(subsumption_resolution,[],[f568,f631])). +fof(f1913,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | sP18 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0), + inference(subsumption_resolution,[],[f1912,f485])). +fof(f1914,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | sP19 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0), + inference(subsumption_resolution,[],[f1913,f447])). +fof(f1915,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP29 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0), + inference(subsumption_resolution,[],[f1914,f443])). +fof(f1916,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | sP20 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0), + inference(subsumption_resolution,[],[f1915,f406])). +fof(f1917,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP2 | sP0), + inference(subsumption_resolution,[],[f1916,f438])). +fof(f1918,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP28 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP0), + inference(subsumption_resolution,[],[f1917,f480])). +fof(f1919,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | sP21 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP0), + inference(subsumption_resolution,[],[f1918,f407])). +fof(f1920,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP5 | sP4 | sP3 | sP0), + inference(subsumption_resolution,[],[f1919,f434])). +fof(f1921,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP39 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP3 | sP0), + inference(subsumption_resolution,[],[f1920,f468])). +fof(f1922,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | sP22 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP3 | sP0), + inference(subsumption_resolution,[],[f1921,f390])). +fof(f1923,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP3 | sP0), + inference(subsumption_resolution,[],[f1922,f429])). +fof(f1924,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP38 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP0), + inference(subsumption_resolution,[],[f1923,f475])). +fof(f1925,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | sP23 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP0), + inference(subsumption_resolution,[],[f1924,f391])). +fof(f1926,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP9 | sP8 | sP7 | sP6 | sP4 | sP0), + inference(subsumption_resolution,[],[f1925,f425])). +fof(f1927,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP30 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP8 | sP7 | sP6 | sP4 | sP0), + inference(subsumption_resolution,[],[f1926,f460])). +fof(f1928,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP8 | sP7 | sP6 | sP4 | sP0), + inference(subsumption_resolution,[],[f1927,f169])). +fof(f1929,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP25 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0), + inference(subsumption_resolution,[],[f1928,f256])). +fof(f1930,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP13 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0), + inference(subsumption_resolution,[],[f1929,f416])). +fof(f1931,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | sP24 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0), + inference(subsumption_resolution,[],[f1930,f452])). +fof(f1932,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP4 | sP0), + inference(subsumption_resolution,[],[f1931,f420])). +fof(f1933,plain,( + e3 != op(unit,e3) | e3 != op(e3,unit) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f1932,f470])). +fof(f1963,plain,( + unit != unit | ~sP43), + inference(backward_demodulation,[],[f557,f380])). +fof(f1964,plain,( + unit != unit | ~sP42), + inference(backward_demodulation,[],[f557,f384])). +fof(f1965,plain,( + unit != unit | ~sP16), + inference(backward_demodulation,[],[f557,f449])). +fof(f1969,plain,( + unit != unit | op(e2,e2) != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0), + inference(backward_demodulation,[],[f557,f489])). +fof(f1981,plain,( + op(e2,e2) != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0), + inference(trivial_inequality_removal,[],[f1969])). +fof(f1982,plain,( + ~sP16), + inference(trivial_inequality_removal,[],[f1965])). +fof(f1983,plain,( + ~sP42), + inference(trivial_inequality_removal,[],[f1964])). +fof(f1984,plain,( + ~sP43), + inference(trivial_inequality_removal,[],[f1963])). +fof(f1986,plain,( + e1 != e1 | ~sP44), + inference(backward_demodulation,[],[f375,f112])). +fof(f1989,plain,( + e1 != e1 | ~sP37), + inference(backward_demodulation,[],[f375,f141])). +fof(f1990,plain,( + e1 != e1 | ~sP15), + inference(backward_demodulation,[],[f375,f227])). +fof(f2000,plain,( + ~sP15), + inference(trivial_inequality_removal,[],[f1990])). +fof(f2001,plain,( + ~sP37), + inference(trivial_inequality_removal,[],[f1989])). +fof(f2002,plain,( + ~sP44), + inference(trivial_inequality_removal,[],[f1986])). +fof(f2003,plain,( + e2 != e2 | ~sP46), + inference(backward_demodulation,[],[f374,f103])). +fof(f2006,plain,( + e2 != e2 | ~sP31), + inference(backward_demodulation,[],[f374,f165])). +fof(f2009,plain,( + e2 != e2 | ~sP14), + inference(backward_demodulation,[],[f374,f232])). +fof(f2018,plain,( + ~sP14), + inference(trivial_inequality_removal,[],[f2009])). +fof(f2019,plain,( + ~sP31), + inference(trivial_inequality_removal,[],[f2006])). +fof(f2020,plain,( + ~sP46), + inference(trivial_inequality_removal,[],[f2003])). +fof(f2035,plain,( + e3 != e3 | e3 != op(unit,e3) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(backward_demodulation,[],[f558,f1933])). +fof(f2036,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP46 | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(trivial_inequality_removal,[],[f2035])). +fof(f2069,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP44 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2036,f2020])). +fof(f2070,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP43 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2069,f2002])). +fof(f2071,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP42 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2070,f1984])). +fof(f2072,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP37 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2071,f1983])). +fof(f2073,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP31 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2072,f2001])). +fof(f2074,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP16 | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2073,f2019])). +fof(f2075,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP15 | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2074,f1982])). +fof(f2076,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP14 | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2075,f2000])). +fof(f2077,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(e2,unit) | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2076,f2018])). +fof(f2078,plain,( + e1 != e1 | ~sP45), + inference(backward_demodulation,[],[f372,f108])). +fof(f2081,plain,( + e1 != e1 | ~sP36), + inference(backward_demodulation,[],[f372,f145])). +fof(f2082,plain,( + e1 != e1 | ~sP12), + inference(backward_demodulation,[],[f372,f239])). +fof(f2091,plain,( + ~sP12), + inference(trivial_inequality_removal,[],[f2082])). +fof(f2092,plain,( + ~sP36), + inference(trivial_inequality_removal,[],[f2081])). +fof(f2093,plain,( + ~sP45), + inference(trivial_inequality_removal,[],[f2078])). +fof(f2103,plain,( + unit != unit | ~sP35), + inference(backward_demodulation,[],[f559,f395])). +fof(f2104,plain,( + unit != unit | ~sP34), + inference(backward_demodulation,[],[f559,f399])). +fof(f2105,plain,( + unit != unit | ~sP11), + inference(backward_demodulation,[],[f559,f457])). +fof(f2114,plain,( + unit != unit | op(e1,e1) != unit | op(unit,unit) != unit | ~sP0), + inference(backward_demodulation,[],[f559,f1981])). +fof(f2115,plain,( + op(e1,e1) != unit | op(unit,unit) != unit | ~sP0), + inference(trivial_inequality_removal,[],[f2114])). +fof(f2116,plain,( + ~sP11), + inference(trivial_inequality_removal,[],[f2105])). +fof(f2117,plain,( + ~sP34), + inference(trivial_inequality_removal,[],[f2104])). +fof(f2118,plain,( + ~sP35), + inference(trivial_inequality_removal,[],[f2103])). +fof(f2119,plain,( + e3 != e3 | ~sP40), + inference(backward_demodulation,[],[f370,f127])). +fof(f2122,plain,( + e3 != e3 | ~sP33), + inference(backward_demodulation,[],[f370,f156])). +fof(f2127,plain,( + e3 != e3 | ~sP10), + inference(backward_demodulation,[],[f370,f249])). +fof(f2135,plain,( + ~sP10), + inference(trivial_inequality_removal,[],[f2127])). +fof(f2136,plain,( + ~sP33), + inference(trivial_inequality_removal,[],[f2122])). +fof(f2137,plain,( + ~sP40), + inference(trivial_inequality_removal,[],[f2119])). +fof(f2152,plain,( + e2 != e2 | e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(backward_demodulation,[],[f560,f2077])). +fof(f2153,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP45 | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(trivial_inequality_removal,[],[f2152])). +fof(f2159,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP40 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2153,f2093])). +fof(f2160,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP36 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2159,f2137])). +fof(f2161,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP35 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2160,f2092])). +fof(f2162,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP34 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2161,f2118])). +fof(f2163,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP33 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2162,f2117])). +fof(f2164,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP12 | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2163,f2136])). +fof(f2165,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP11 | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2164,f2091])). +fof(f2166,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP10 | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2165,f2116])). +fof(f2167,plain,( + e3 != op(unit,e3) | e2 != op(e1,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2166,f2135])). +fof(f2178,plain,( + e2 != e2 | e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0), + inference(backward_demodulation,[],[f368,f2167])). +fof(f2179,plain,( + e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(e1,unit) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0), + inference(trivial_inequality_removal,[],[f2178])). +fof(f2182,plain,( + e3 != e3 | ~sP41), + inference(backward_demodulation,[],[f367,f123])). +fof(f2185,plain,( + e3 != e3 | ~sP32), + inference(backward_demodulation,[],[f367,f160])). +fof(f2190,plain,( + e3 != e3 | ~sP7), + inference(backward_demodulation,[],[f367,f261])). +fof(f2194,plain,( + ~sP7), + inference(trivial_inequality_removal,[],[f2190])). +fof(f2195,plain,( + ~sP32), + inference(trivial_inequality_removal,[],[f2185])). +fof(f2196,plain,( + ~sP41), + inference(trivial_inequality_removal,[],[f2182])). +fof(f2206,plain,( + unit != unit | ~sP27), + inference(backward_demodulation,[],[f561,f410])). +fof(f2207,plain,( + unit != unit | ~sP26), + inference(backward_demodulation,[],[f561,f414])). +fof(f2208,plain,( + unit != unit | ~sP6), + inference(backward_demodulation,[],[f561,f465])). +fof(f2209,plain,( + unit != unit | op(unit,unit) != unit | ~sP0), + inference(backward_demodulation,[],[f561,f2115])). +fof(f2210,plain,( + op(unit,unit) != unit | ~sP0), + inference(trivial_inequality_removal,[],[f2209])). +fof(f2211,plain,( + ~sP6), + inference(trivial_inequality_removal,[],[f2208])). +fof(f2212,plain,( + ~sP26), + inference(trivial_inequality_removal,[],[f2207])). +fof(f2213,plain,( + ~sP27), + inference(trivial_inequality_removal,[],[f2206])). +fof(f2226,plain,( + e1 != e1 | e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0), + inference(backward_demodulation,[],[f562,f2179])). +fof(f2227,plain,( + e3 != op(unit,e3) | sP41 | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0), + inference(trivial_inequality_removal,[],[f2226])). +fof(f2231,plain,( + e3 != op(unit,e3) | sP32 | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2227,f2196])). +fof(f2232,plain,( + e3 != op(unit,e3) | sP27 | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2231,f2195])). +fof(f2233,plain,( + e3 != op(unit,e3) | sP26 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2232,f2213])). +fof(f2234,plain,( + e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP7 | sP6 | sP0), + inference(subsumption_resolution,[],[f2233,f2212])). +fof(f2235,plain,( + e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP6 | sP0), + inference(subsumption_resolution,[],[f2234,f2194])). +fof(f2236,plain,( + e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit | sP0), + inference(subsumption_resolution,[],[f2235,f2211])). +fof(f2237,plain,( + e3 != op(unit,e3) | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit), + inference(subsumption_resolution,[],[f2236,f2210])). +fof(f2248,plain,( + e3 != e3 | e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit), + inference(backward_demodulation,[],[f563,f2237])). +fof(f2249,plain,( + e2 != op(unit,e2) | e1 != op(unit,e1) | op(unit,unit) != unit), + inference(trivial_inequality_removal,[],[f2248])). +fof(f2264,plain,( + e2 != e2 | e1 != op(unit,e1) | op(unit,unit) != unit), + inference(backward_demodulation,[],[f564,f2249])). +fof(f2265,plain,( + e1 != op(unit,e1) | op(unit,unit) != unit), + inference(trivial_inequality_removal,[],[f2264])). +fof(f2281,plain,( + e1 != e1 | op(unit,unit) != unit), + inference(backward_demodulation,[],[f565,f2265])). +fof(f2282,plain,( + op(unit,unit) != unit), + inference(trivial_inequality_removal,[],[f2281])). +fof(f2286,plain,( + $false), + inference(subsumption_resolution,[],[f566,f2282])). +% SZS output end Proof for theBenchmark +% ------------------------------ +% Version: Vampire 4.2.2 (commit 552c234 on 2018-07-02 14:53:33 +0100) +% Termination reason: Refutation + +% Memory used [KB]: 1535 +% Time elapsed: 0.178 s +% ------------------------------ +% ------------------------------ +% Success in time 0.214 s diff --git a/test-data/szs/tff/AGT004+2---Z3---4.4.1.THM-Prf.original.s b/test-data/szs/tff/AGT004+2---Z3---4.4.1.THM-Prf.original.s new file mode 100644 --- /dev/null +++ b/test-data/szs/tff/AGT004+2---Z3---4.4.1.THM-Prf.original.s @@ -0,0 +1,101 @@ +% Problem : AGT004+2 : TPTP v6.4.0. Bugfixed v3.1.0. +% Command : z3_tptp -proof -model -t:%d -file:%s +% Computer : n099.star.cs.uiowa.edu +% Model : x86_64 x86_64 +% CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz +% Memory : 32218.75MB +% OS : Linux 3.10.0-327.10.1.el7.x86_64 +% CPULimit : 300 +% DateTime : Thu Jul 21 10:50:24 CDT 2016 +% CPUTime : +% SZS status Theorem +% SZS output start Proof +tff(accept_number_type, type, ( + accept_number: ( $i * $i ) > $o)). +tff(n5_type, type, ( + n5: $i)). +tff(countryamedicalorganization_type, type, ( + countryamedicalorganization: $i)). +tff(accept_leader_type, type, ( + accept_leader: ( $i * $i ) > $o)). +tff(countryahumanitarianorganization_type, type, ( + countryahumanitarianorganization: $i)). +tff(accept_city_type, type, ( + accept_city: ( $i * $i ) > $o)). +tff(coastvillage_type, type, ( + coastvillage: $i)). +tff(accept_team_type, type, ( + accept_team: ( $i * $i * $i * $i ) > $o)). +tff(1,axiom,((~accept_city(countryamedicalorganization, coastvillage))), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax','deduced_13')). +tff(2,plain, + ((((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5))) | accept_city(countryamedicalorganization, coastvillage))), + inference(tautology,[status(thm)],[])). +tff(3,plain, + (((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5)))), + inference(unit_resolution,[status(thm)],[2, 1])). +tff(4,plain, + (((~(~accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5))) <=> accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5))), + inference(rewrite,[status(thm)],[])). +tff(5,axiom,((~(~accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','query_4')). +tff(6,plain, + (accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5)), + inference(modus_ponens,[status(thm)],[5, 4])). +tff(7,plain, + (((~(accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5) <=> (~((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5)))))) | (~accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5)) | (~((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5)))))), + inference(tautology,[status(thm)],[])). +tff(8,plain, + ((~(accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5) <=> (~((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5))))))), + inference(unit_resolution,[status(thm)],[7, 6, 3])). +tff(9,plain, + (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_team(X4, X1, X3, X2) <=> (~((~accept_city(X4, X3)) | (~accept_leader(X4, X1)) | (~accept_number(X4, X2))))) <=> (accept_team(X4, X1, X3, X2) <=> (~((~accept_city(X4, X3)) | (~accept_leader(X4, X1)) | (~accept_number(X4, X2))))))), + inference(reflexivity,[status(thm)],[])). +tff(10,plain, + ((![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N))))) <=> ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N))))))), + inference(quant_intro,[status(thm)],[9])). +tff(11,plain, + (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2)) <=> (~((~accept_city(X4, X3)) | (~accept_leader(X4, X1)) | (~accept_number(X4, X2)))))), + inference(rewrite,[status(thm)],[])). +tff(12,plain, + (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_team(X4, X1, X3, X2) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2))) <=> (accept_team(X4, X1, X3, X2) <=> (~((~accept_city(X4, X3)) | (~accept_leader(X4, X1)) | (~accept_number(X4, X2))))))), + inference(monotonicity,[status(thm)],[11])). +tff(13,plain, + ((![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N))) <=> ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N))))))), + inference(quant_intro,[status(thm)],[12])). +tff(14,plain, + (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_team(X4, X1, X3, X2) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2))) <=> (accept_team(X4, X1, X3, X2) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2))))), + inference(rewrite,[status(thm)],[])). +tff(15,plain, + ((![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N))) <=> ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N))))), + inference(quant_intro,[status(thm)],[14])). +tff(16,plain, + (![X4: $i, X3: $i, X2: $i, X1: $i] : (((accept_city(X4, X3) & accept_leader(X4, X1)) & accept_number(X4, X2)) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2)))), + inference(rewrite,[status(thm)],[])). +tff(17,plain, + (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_team(X4, X1, X3, X2) <=> ((accept_city(X4, X3) & accept_leader(X4, X1)) & accept_number(X4, X2))) <=> (accept_team(X4, X1, X3, X2) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2))))), + inference(monotonicity,[status(thm)],[16])). +tff(18,plain, + ((![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> ((accept_city(A, C) & accept_leader(A, L)) & accept_number(A, N))) <=> ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N))))), + inference(quant_intro,[status(thm)],[17])). +tff(19,axiom,(![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> ((accept_city(A, C) & accept_leader(A, L)) & accept_number(A, N)))), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax','a1_1')). +tff(20,plain, + (![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N)))), + inference(modus_ponens,[status(thm)],[19, 18])). +tff(21,plain, + (![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N)))), + inference(modus_ponens,[status(thm)],[20, 15])). +tff(22,plain,( + ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N)))), + inference(nnf,[status(sab)],[21])). +tff(23,plain, + (![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N)))))), + inference(modus_ponens,[status(thm)],[22, 13])). +tff(24,plain, + (![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N)))))), + inference(modus_ponens,[status(thm)],[23, 10])). +tff(25,plain, + (((~![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N)))))) | (accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5) <=> (~((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5))))))), + inference(quant_inst,[status(thm)],[])). +tff(26,plain, + ($false), + inference(unit_resolution,[status(thm)],[25, 24, 8])). +% SZS output end Proof diff --git a/test-data/szs/tff/ALG039+1---Z3---4.4.1.THM-Prf.original.s b/test-data/szs/tff/ALG039+1---Z3---4.4.1.THM-Prf.original.s new file mode 100644 --- /dev/null +++ b/test-data/szs/tff/ALG039+1---Z3---4.4.1.THM-Prf.original.s @@ -0,0 +1,126 @@ +% Problem : ALG039+1 : TPTP v6.4.0. Released v2.7.0. +% Command : z3_tptp -proof -model -t:%d -file:%s +% Computer : n088.star.cs.uiowa.edu +% Model : x86_64 x86_64 +% CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz +% Memory : 32218.75MB +% OS : Linux 3.10.0-327.10.1.el7.x86_64 +% CPULimit : 300 +% DateTime : Thu Jul 21 10:50:10 CDT 2016 +% CPUTime : +% SZS status Theorem +% SZS output start Proof +tff(e3_type, type, ( + e3: $i)). +tff(op_type, type, ( + op: ( $i * $i ) > $i)). +tff(e2_type, type, ( + e2: $i)). +tff(e1_type, type, ( + e1: $i)). +tff(e0_type, type, ( + e0: $i)). +tff(1,plain, + (((~$true) <=> $false)), + inference(rewrite,[status(thm)],[])). +tff(2,plain, + (((~$false) <=> $true)), + inference(rewrite,[status(thm)],[])). +tff(3,plain, + ((((((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2)) | ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3))) & (~(((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2)) | ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3))))) <=> $false)), + inference(rewrite,[status(thm)],[])). +tff(4,plain, + ((((((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2))) | ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3))) <=> (((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2)) | ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3))))), + inference(rewrite,[status(thm)],[])). +tff(5,plain, + (((((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3)) & (op(e3, e3) = e3)) <=> ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3)))), + inference(rewrite,[status(thm)],[])). +tff(6,plain, + (((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) <=> ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3)))), + inference(rewrite,[status(thm)],[])). +tff(7,plain, + ((((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3)) <=> (((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3)) & (op(e3, e3) = e3)))), + inference(monotonicity,[status(thm)],[6])). +tff(8,plain, + ((((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3)) <=> ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3)))), + inference(transitivity,[status(thm)],[7, 5])). +tff(9,plain, + ((((((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1))) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2))) <=> (((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2))))), + inference(rewrite,[status(thm)],[])). +tff(10,plain, + (((((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2)) & (op(e3, e3) = e2)) <=> ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2)))), + inference(rewrite,[status(thm)],[])). +tff(11,plain, + (((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) <=> ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2)))), + inference(rewrite,[status(thm)],[])). +tff(12,plain, + ((((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2)) <=> (((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2)) & (op(e3, e3) = e2)))), + inference(monotonicity,[status(thm)],[11])). +tff(13,plain, + ((((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2)) <=> ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2)))), + inference(transitivity,[status(thm)],[12, 10])). +tff(14,plain, + (((((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1)) & (op(e3, e3) = e1)) <=> ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)))), + inference(rewrite,[status(thm)],[])). +tff(15,plain, + (((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) <=> ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1)))), + inference(rewrite,[status(thm)],[])). +tff(16,plain, + ((((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1)) <=> (((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1)) & (op(e3, e3) = e1)))), + inference(monotonicity,[status(thm)],[15])). +tff(17,plain, + ((((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1)) <=> ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)))), + inference(transitivity,[status(thm)],[16, 14])). +tff(18,plain, + (((((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) <=> ((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)))), + inference(rewrite,[status(thm)],[])). +tff(19,plain, + (((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) <=> ((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0)))), + inference(rewrite,[status(thm)],[])). +tff(20,plain, + ((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) <=> (((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)))), + inference(monotonicity,[status(thm)],[19])). +tff(21,plain, + ((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) <=> ((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)))), + inference(transitivity,[status(thm)],[20, 18])). +tff(22,plain, + (((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) <=> (((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1))))), + inference(monotonicity,[status(thm)],[21, 17])). +tff(23,plain, + ((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) <=> ((((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1))) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2))))), + inference(monotonicity,[status(thm)],[22, 13])). +tff(24,plain, + ((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) <=> (((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2))))), + inference(transitivity,[status(thm)],[23, 9])). +tff(25,plain, + (((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))) <=> ((((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2))) | ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3))))), + inference(monotonicity,[status(thm)],[24, 8])). +tff(26,plain, + (((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))) <=> (((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2)) | ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3))))), + inference(transitivity,[status(thm)],[25, 4])). +tff(27,plain, + (((~(((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3)))) <=> (~(((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2)) | ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3)))))), + inference(monotonicity,[status(thm)],[26])). +tff(28,plain, + ((((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))) & (~(((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))))) <=> ((((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2)) | ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3))) & (~(((op(e0, e0) = e0) & (op(e1, e1) = e0) & (op(e2, e2) = e0) & (op(e3, e3) = e0)) | ((op(e0, e0) = e1) & (op(e1, e1) = e1) & (op(e2, e2) = e1) & (op(e3, e3) = e1)) | ((op(e0, e0) = e2) & (op(e1, e1) = e2) & (op(e2, e2) = e2) & (op(e3, e3) = e2)) | ((op(e0, e0) = e3) & (op(e1, e1) = e3) & (op(e2, e2) = e3) & (op(e3, e3) = e3))))))), + inference(monotonicity,[status(thm)],[26, 27])). +tff(29,plain, + ((((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))) & (~(((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))))) <=> $false)), + inference(transitivity,[status(thm)],[28, 3])). +tff(30,plain, + (((~((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))) & (~(((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3)))))) <=> (~$false))), + inference(monotonicity,[status(thm)],[29])). +tff(31,plain, + (((~((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))) & (~(((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3)))))) <=> $true)), + inference(transitivity,[status(thm)],[30, 2])). +tff(32,plain, + (((~(~((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))) & (~(((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))))))) <=> (~$true))), + inference(monotonicity,[status(thm)],[31])). +tff(33,plain, + (((~(~((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))) & (~(((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))))))) <=> $false)), + inference(transitivity,[status(thm)],[32, 1])). +tff(34,axiom,((~(~((((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3))) & (~(((((((op(e0, e0) = e0) & (op(e1, e1) = e0)) & (op(e2, e2) = e0)) & (op(e3, e3) = e0)) | ((((op(e0, e0) = e1) & (op(e1, e1) = e1)) & (op(e2, e2) = e1)) & (op(e3, e3) = e1))) | ((((op(e0, e0) = e2) & (op(e1, e1) = e2)) & (op(e2, e2) = e2)) & (op(e3, e3) = e2))) | ((((op(e0, e0) = e3) & (op(e1, e1) = e3)) & (op(e2, e2) = e3)) & (op(e3, e3) = e3)))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','co1')). +tff(35,plain, + ($false), + inference(modus_ponens,[status(thm)],[34, 33])). +% SZS output end Proof diff --git a/test/QuickCheckSpec/Generators.hs b/test/QuickCheckSpec/Generators.hs --- a/test/QuickCheckSpec/Generators.hs +++ b/test/QuickCheckSpec/Generators.hs @@ -216,15 +216,32 @@ arbitrary = genericArbitraryU shrink (TPTP us) = TPTP <$> shrinkList shrink us +deriving instance Generic TSTP +instance Arbitrary TSTP where + arbitrary = genericArbitraryU + shrink (TSTP szs us) = TSTP <$> shrink szs <*> shrinkList shrink us + -- * Annotations deriving instance Generic Intro instance Arbitrary Intro where arbitrary = genericArbitraryU -deriving instance Generic Status -instance Arbitrary Status where +deriving instance Generic SZS +instance Arbitrary SZS where + arbitrary = genericArbitraryU + +deriving instance Generic Success +instance Arbitrary Success where + arbitrary = genericArbitraryU + +deriving instance Generic NoSuccess +instance Arbitrary NoSuccess where + arbitrary = genericArbitraryU + +deriving instance Generic Dataform +instance Arbitrary Dataform where arbitrary = genericArbitraryU deriving instance Generic Info diff --git a/test/QuickCheckSpec/Main.hs b/test/QuickCheckSpec/Main.hs --- a/test/QuickCheckSpec/Main.hs +++ b/test/QuickCheckSpec/Main.hs @@ -126,6 +126,9 @@ prop_ipp_TPTP :: TPTP -> Property prop_ipp_TPTP = ippModulo normalizeTPTP tptp +prop_ipp_TSTP :: TSTP -> Property +prop_ipp_TSTP = ippModulo normalizeTSTP tstp + -- ** Annotations diff --git a/test/QuickCheckSpec/Normalizers.hs b/test/QuickCheckSpec/Normalizers.hs --- a/test/QuickCheckSpec/Normalizers.hs +++ b/test/QuickCheckSpec/Normalizers.hs @@ -17,11 +17,14 @@ normalizeType, normalizeUnit, normalizeTPTP, + normalizeTSTP, normalizeSource, normalizeInfo, normalizeParent ) where +import Data.Bifunctor (bimap) + import Data.TPTP @@ -64,12 +67,15 @@ normalizeUnit :: Unit -> Unit normalizeUnit = \case Include f ns -> Include f ns - Unit n d a -> Unit n (normalizeDeclaration d) (normalizeAnn a) + Unit n d a -> Unit n (normalizeDeclaration d) (fmap normalizeAnn a) where - normalizeAnn = fmap $ \(s, i) -> (normalizeSource s, fmap (fmap normalizeInfo) i) + normalizeAnn = bimap normalizeSource (fmap (fmap normalizeInfo)) normalizeTPTP :: TPTP -> TPTP normalizeTPTP (TPTP us) = TPTP (fmap normalizeUnit us) + +normalizeTSTP :: TSTP -> TSTP +normalizeTSTP (TSTP szs us) = TSTP szs (fmap normalizeUnit us) -- * Annotations diff --git a/test/UnitTests.hs b/test/UnitTests.hs --- a/test/UnitTests.hs +++ b/test/UnitTests.hs @@ -39,7 +39,7 @@ readTestFile f = Text.IO.readFile (testDataDir ++ "/" ++ f) parseFile :: FilePath -> IO Result -parseFile path = buildResult . parseTPTPOnly <$> readTestFile path +parseFile path = buildResult . parseTSTPOnly <$> readTestFile path where buildResult (Left e) = Error e buildResult (Right _) = Pass diff --git a/tptp.cabal b/tptp.cabal --- a/tptp.cabal +++ b/tptp.cabal @@ -1,15 +1,16 @@ cabal-version: 2.4 name: tptp -version: 0.1.0.3 +version: 0.1.1.0 synopsis: A parser and a pretty printer for the TPTP language description: (Thousands of Problems for Theorem Provers) is the standard language of problems, proofs, and models, used by automated theorem provers. . - This library provides definitions of data types, a pretty printer and an - parser for - (currently, a subset of) the TPTP language. + This library provides definitions of data types, a + and an + parser for the + CNF, FOF, TFF0 and TFF1 subsets of the TPTP language. homepage: https://github.com/aztek/tptp bug-reports: https://github.com/aztek/tptp/issues license: GPL-3.0-only @@ -23,12 +24,14 @@ GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, - GHC == 8.6.5 + GHC == 8.6.5, + GHC == 8.8.1 extra-source-files: CHANGELOG.md test/*.hs test/**/*.hs + test-data/szs/**/*.s test-data/tptp/**/*.ax test-data/tptp/**/*.p test-data/tstp/**/*.s @@ -40,6 +43,7 @@ flag Werror default: False manual: True + description: Build with -Werror library hs-source-dirs: src @@ -59,7 +63,7 @@ text >= 1.2.3 && < 1.3, attoparsec >= 0.13.2 && < 0.14, scientific >= 0.3.6 && < 0.4, - prettyprinter >= 1.2.1 && < 1.3, + prettyprinter >= 1.2.1 && < 1.5 if impl(ghc < 8) ghc-options: -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns @@ -128,9 +132,8 @@ -Wall -threaded if flag(Werror) ghc-options: -Werror - -- TODO: Make it work for older GHCs - if impl(ghc < 8.4) - buildable: False + -- TODO: Make it work + buildable: False build-depends: base, QuickCheck,