tptp 0.1.0.3 → 0.1.1.0

raw patch · 15 files changed

+1825/−80 lines, 15 filesdep ~prettyprinterPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: prettyprinter

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• src/Data/TPTP.hs +265/−14
• src/Data/TPTP/Parse/Combinators.hs +101/−22
• src/Data/TPTP/Parse/Text.hs +30/−16
• src/Data/TPTP/Parse/Text/Lazy.hs +14/−12
• src/Data/TPTP/Pretty.hs +29/−2
• test-data/szs/fof/AGT004+2---Metis---2.4.THM-CRf.original.s +110/−0
• test-data/szs/fof/ALG043+1---Vampire---4.3.THM-Ref.original.s +996/−0
• test-data/szs/tff/AGT004+2---Z3---4.4.1.THM-Prf.original.s +101/−0
• test-data/szs/tff/ALG039+1---Z3---4.4.1.THM-Prf.original.s +126/−0
• test/QuickCheckSpec/Generators.hs +19/−2
• test/QuickCheckSpec/Main.hs +3/−0
• test/QuickCheckSpec/Normalizers.hs +8/−2
• test/UnitTests.hs +1/−1
• tptp.cabal +12/−9

@@ -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.

@@ -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 <http://www.tptp.org/Seminars/SZSOntologies/Summary.html The SZS Ontologies>+-- | 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+-- <http://www.tptp.org/Seminars/SZSOntologies/Summary.html The SZS Ontologies> -- 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+-- <http://www.tptp.org/Seminars/SZSOntologies/Summary.html The SZS Ontologies>+-- 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+-- <http://www.tptp.org/Seminars/SZSOntologies/Summary.html The SZS Ontologies>+-- 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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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 

@@ -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

@@ -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

@@ -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:   <http://www.tptp.org TPTP> (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-  <http://hackage.haskell.org/package/attoparsec attoparsec> parser for-  (currently, a subset of) the TPTP language.+  This library provides definitions of data types, a+  <https://hackage.haskell.org/package/prettyprinter pretty printer> and an+  <https://hackage.haskell.org/package/attoparsec attoparsec> 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,