diff options
Diffstat (limited to 'source/Test')
| -rw-r--r-- | source/Test/All.hs | 14 | ||||
| -rw-r--r-- | source/Test/Golden.hs | 141 | ||||
| -rw-r--r-- | source/Test/Unit.hs | 15 | ||||
| -rw-r--r-- | source/Test/Unit/Symdiff.hs | 96 |
4 files changed, 266 insertions, 0 deletions
diff --git a/source/Test/All.hs b/source/Test/All.hs new file mode 100644 index 0000000..7fb5bd3 --- /dev/null +++ b/source/Test/All.hs @@ -0,0 +1,14 @@ +module Test.All where + + +import Base +import Test.Golden +import Test.Unit +import Test.Tasty + + +runTests :: IO () +runTests = defaultMain =<< tests + +tests :: IO TestTree +tests = testGroup "all tests" <$> sequence [goldenTests, return unitTests] diff --git a/source/Test/Golden.hs b/source/Test/Golden.hs new file mode 100644 index 0000000..705aaa5 --- /dev/null +++ b/source/Test/Golden.hs @@ -0,0 +1,141 @@ +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE RecordWildCards #-} + +module Test.Golden where + + +import Api qualified +import Provers qualified +import Tptp.UnsortedFirstOrder (toText) +import Base +import Provers (defaultTimeLimit) + +import Control.Monad.Logger +import Control.Monad.Reader +import Data.Text qualified as Text +import Data.Text.IO qualified as TextIO +import Data.Text.Lazy.IO qualified as LazyTextIO +import System.Directory +import System.FilePath +import Test.Tasty +import Test.Tasty.Golden (goldenVsFile, findByExtension) +import Text.Pretty.Simple (pShowNoColor) +import UnliftIO +import UnliftIO.Environment +import Api (Options(withDumpPremselTraining)) + +testOptions :: Api.Options +testOptions = Api.Options + { Api.withDumpPremselTraining = Api.WithoutDumpPremselTraining + , Api.withCache = Api.WithoutCache + , Api.withFilter = Api.WithoutFilter + , inputPath = error "testOptions: no inputPath" + , withDump = Api.WithoutDump + , withLogging = Api.WithoutLogging + , withMemoryLimit = Provers.defaultMemoryLimit + , withOmissions = Api.WithOmissions + , withParseOnly = Api.WithoutParseOnly + , withProver = Api.WithDefaultProver + , withTimeLimit = Provers.defaultTimeLimit + , withVersion = Api.WithoutVersion + , withMegalodon = Api.WithoutMegalodon + } + +goldenTests :: IO TestTree +goldenTests = runReaderT goldenTestGroup testOptions + +goldenTestGroup :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree +goldenTestGroup = testGroup "golden tests" <$> sequence + [ tokenizing + , scanning + , parsing + , glossing + , generatingTasks + , encodingTasks + , verification + ] + + +-- | A testing triple consists of a an 'input' file, which is proccesed, resulting +-- in 'output' file, which is then compared to a 'golden' file. +data Triple = Triple + { input :: FilePath + , output :: FilePath + , golden :: FilePath + } + deriving (Show, Eq) + + +-- | Gathers all the files for the test. We test all examples and everything in @test/pass/@. +-- The golden files for all tests are stored in @test/pass/@, so we need to adjust the filepath +-- of the files from @examples/@. +gatherTriples :: MonadIO io => String -> io [Triple] +gatherTriples stage = do + inputs <- liftIO (findByExtension [".tex"] "test/examples") + pure $ + [ Triple{..} + | input <- inputs + , let input' = "test" </> "golden" </> takeBaseName input </> stage + , let golden = input' <.> "golden" + , let output = input' <.> "out" + ] + +createTripleDirectoriesIfMissing :: MonadIO io => Triple -> io () +createTripleDirectoriesIfMissing Triple{..} = liftIO $ + createDirectoryIfMissing True (takeDirectory output) + +makeGoldenTest :: (MonadUnliftIO io, MonadReader Api.Options io) => String -> (Triple -> io ()) -> io TestTree +makeGoldenTest stage action = do + triples <- gatherTriples stage + for triples createTripleDirectoriesIfMissing + runInIO <- askRunInIO + pure $ testGroup stage + [ goldenVsFile + (takeBaseName input) -- test name + golden + output + (runInIO (action triple)) + | triple@Triple{..} <- triples + ] + +tokenizing :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree +tokenizing = makeGoldenTest "tokenizing" $ \Triple{..} -> do + tokenStream <- Api.tokenize input + liftIO (LazyTextIO.writeFile output (pShowNoColor (Api.simpleStream tokenStream))) + + +scanning :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree +scanning = makeGoldenTest "scanning" $ \Triple{..} -> do + lexicalItems <- Api.scan input + liftIO (LazyTextIO.writeFile output (pShowNoColor lexicalItems)) + +parsing :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree +parsing = makeGoldenTest "parsing" $ \Triple{..} -> do + (parseResult, _) <- Api.parse input + liftIO (LazyTextIO.writeFile output (pShowNoColor parseResult)) + + +glossing :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree +glossing = makeGoldenTest "glossing" $ \Triple{..} -> do + (interpretationResult, _) <- Api.gloss input + liftIO (LazyTextIO.writeFile output (pShowNoColor interpretationResult)) + + +generatingTasks :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree +generatingTasks = makeGoldenTest "generating tasks" $ \Triple{..} -> do + (tasks, _) <- Api.generateTasks input + liftIO $ LazyTextIO.writeFile output (pShowNoColor tasks) + + +encodingTasks :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree +encodingTasks = makeGoldenTest "encoding tasks" $ \Triple{..} -> do + tasks <- Api.encodeTasks input + liftIO (TextIO.writeFile output (Text.intercalate "\n------------------\n" (toText <$> tasks))) + + +verification :: (MonadUnliftIO io, MonadReader Api.Options io) => io TestTree +verification = makeGoldenTest "verification" $ \Triple{..} -> do + vampirePathPath <- (?? "vampire") <$> lookupEnv "NAPROCHE_VAMPIRE" + let defaultProverInstance = Provers.vampire vampirePathPath Provers.Silent Provers.defaultTimeLimit Provers.defaultMemoryLimit + answers <- runNoLoggingT (Api.verify defaultProverInstance input) + liftIO (LazyTextIO.writeFile output (pShowNoColor answers)) diff --git a/source/Test/Unit.hs b/source/Test/Unit.hs new file mode 100644 index 0000000..e98c33c --- /dev/null +++ b/source/Test/Unit.hs @@ -0,0 +1,15 @@ +module Test.Unit where + + +import Test.Tasty +import Test.Tasty.HUnit +import Test.Unit.Symdiff qualified as Symdiff + + +unitTests :: TestTree +unitTests = testGroup "unit tests" [testCase "filter" filtersWell] + + +filtersWell :: Assertion +filtersWell = do + assertBool "Filter works on symdiff problem" Symdiff.filtersWell diff --git a/source/Test/Unit/Symdiff.hs b/source/Test/Unit/Symdiff.hs new file mode 100644 index 0000000..583004f --- /dev/null +++ b/source/Test/Unit/Symdiff.hs @@ -0,0 +1,96 @@ +module Test.Unit.Symdiff where + +import Base +import Bound.Scope +import Bound.Var +import Syntax.Internal +import Filter + +import Data.Text qualified as Text + +filtersWell :: Bool +filtersWell = badFact `notElem` (snd <$> taskHypotheses (filterTask symdiff)) + + +badFact :: ExprOf a +badFact = Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "FreshReplacementVar")), TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Quantified Existentially (Scope (Connected Conjunction (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (B (NamedVar "A"))))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "b")), TermVar (F (TermVar (B (NamedVar "B"))))])) (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (F (TermVar (B (NamedVar "FreshReplacementVar")))), TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))]])))))) + + +symdiff :: Task +symdiff = + Task + { taskDirectness = + Direct + , taskConjectureLabel = Marker "symdiff_test" + , taskHypotheses = zipWith (,) (Marker . Text.pack . show <$> ([1..] :: [Int])) + [ Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "A"))], TermVar (B (NamedVar "A"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "A")), TermSymbol (SymbolMixfix [Just (Command "emptyset")]) []], TermSymbol (SymbolMixfix [Just (Command "emptyset")]) []])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "x")), TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "x")), TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "C"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "A")), TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "C"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "x"))], TermSymbol (SymbolMixfix [Just (Command "emptyset")]) []])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))]], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermSymbol (SymbolMixfix [Just (Command "emptyset")]) []], TermVar (B (NamedVar "x"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "symdiff"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "x"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]], TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))], TermVar (B (NamedVar "Z"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))], TermVar (B (NamedVar "Z"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "A"))], TermVar (B (NamedVar "A"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "A")), TermSymbol (SymbolMixfix [Just (Command "emptyset")]) []], TermVar (B (NamedVar "A"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "x")), TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "z"))]], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "z"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "C"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "A")), TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "C"))]]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Just (Command "inters"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermSymbol (SymbolMixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "A"))]], TermSymbol (SymbolMixfix [Just (Command "emptyset")]) []])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Just (Command "unions"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermSymbol (SymbolMixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "A"))]], TermVar (B (NamedVar "A"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))]], TermVar (B (NamedVar "a"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))]], TermVar (B (NamedVar "b"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "A")), TermSymbol (SymbolMixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "A"))]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "x")), TermSymbol (SymbolMixfix [Just (Command "Cons"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermSymbol (SymbolMixfix [Just (Command "emptyset")]) [], TermSymbol (SymbolMixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "A"))]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "neq"))) [TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))], TermVar (B (NamedVar "a"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "neq"))) [TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))], TermVar (B (NamedVar "b"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "A"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "A")), TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "A"))])) + , Quantified Universally (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermSymbol (SymbolMixfix [Just (Command "emptyset")]) [], TermVar (B (NamedVar "a"))])) + , Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "disjoint"), Just (Word "from"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "disjoint"), Just (Word "from"), Nothing])) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))]))) + , Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "B"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]))) + , Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]))) + , Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Not (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))])))) + , Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))]]) (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "Y"))])))) + , Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "neq"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (Quantified Existentially (Scope (Connected ExclusiveOr (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "c")), TermVar (F (TermVar (B (NamedVar "A"))))]) (Not (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "c")), TermVar (F (TermVar (B (NamedVar "B"))))]))) (Connected Conjunction (Not (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "c")), TermVar (F (TermVar (B (NamedVar "A"))))])) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "c")), TermVar (F (TermVar (B (NamedVar "B"))))]))))))) + , Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "B"))]))) + , Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Z"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "Y")), TermVar (B (NamedVar "Z"))]]))) + , Quantified Universally (Scope (Connected Implication (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]) (Not (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))]))) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]))) + , Quantified Universally (Scope (Connected Implication (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "Y"))])) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))], TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))]]))) + , Quantified Universally (Scope (Connected Implication (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))])) (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]))) + , Quantified Universally (Scope (Connected Implication (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "C"))])) (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "C"))]))) + , Quantified Universally (Scope (Connected Implication (Connected Conjunction (PropositionalConstant IsTop) (PropositionalConstant IsTop)) (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Connected Disjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))]))))) + , Quantified Universally (Scope (Connected Implication (Connected Conjunction (Not (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "inhabited")])) [TermVar (B (NamedVar "x"))])) (Not (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "inhabited")])) [TermVar (B (NamedVar "y"))]))) (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))]))) + , Quantified Universally (Scope (Connected Implication (Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (B (NamedVar "A"))))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (B (NamedVar "B"))))])))) (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "disjoint"), Just (Word "from"), Nothing])) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (Quantified Universally (Scope (Not (Quantified Existentially (Scope (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "A"))))))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "B"))))))]))))))))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "inhabited")])) [TermVar (B (NamedVar "A"))]) (Quantified Universally (Scope (Quantified Existentially (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "A"))))))]))))))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "inhabited")])) [TermVar (B (NamedVar "A"))]) (Not (Not (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "inhabited")])) [TermVar (B (NamedVar "A"))]))))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "b"))], TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "aprime")), TermVar (B (NamedVar "bprime"))]]) (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "aprime"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (B (NamedVar "b")), TermVar (B (NamedVar "bprime"))])))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "a")), TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "b")), TermVar (B (NamedVar "c"))]], TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "aprime")), TermSymbol (SymbolMixfix [Just (Word "pair")]) [TermVar (B (NamedVar "bprime")), TermVar (B (NamedVar "cprime"))]]]) (Connected Conjunction (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "aprime"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (B (NamedVar "b")), TermVar (B (NamedVar "bprime"))])) (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (B (NamedVar "c")), TermVar (B (NamedVar "cprime"))])))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "B")), TermSymbol (SymbolMixfix [Just (Command "Pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "A"))]]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "B")), TermVar (B (NamedVar "A"))]))) + , badFact + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))])))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]]) (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "A"))]) (Not (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (B (NamedVar "B"))]))))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "x")), TermSymbol (SymbolMixfix [Just (Command "Cons"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "y")), TermVar (B (NamedVar "X"))]]) (Connected Disjunction (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "y"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))])))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "z")), TermSymbol (SymbolMixfix [Just (Command "inters"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "X"))]]) (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "inhabited")])) [TermVar (B (NamedVar "X"))]) (Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "Y")), TermVar (F (TermVar (B (NamedVar "X"))))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (F (TermVar (B (NamedVar "z")))), TermVar (B (NamedVar "Y"))]))))))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "z")), TermSymbol (SymbolMixfix [Just (Command "unions"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "X"))]]) (Quantified Existentially (Scope (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "Y")), TermVar (F (TermVar (B (NamedVar "X"))))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (F (TermVar (B (NamedVar "z")))), TermVar (B (NamedVar "Y"))])))))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "subset"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (Quantified Universally (Scope (Connected Conjunction (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (F (TermVar (B (NamedVar "A")))), TermVar (F (TermVar (B (NamedVar "B"))))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "neq"))) [TermVar (F (TermVar (B (NamedVar "A")))), TermVar (F (TermVar (B (NamedVar "B"))))])))))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "="))) [TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))], TermVar (B (NamedVar "A"))]))) + , Quantified Universally (Scope (Connected Equivalence (TermSymbol (SymbolPredicate (PredicateRelation (Command "subseteq"))) [TermVar (B (NamedVar "A")), TermVar (B (NamedVar "B"))]) (Quantified Universally (Scope (Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "A"))))))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermVar (F (TermVar (F (TermVar (B (NamedVar "B"))))))])))))))) + , Quantified Universally (Scope (Connected Equivalence (Not (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "inhabited")])) [TermSymbol (SymbolMixfix [Nothing, Just (Command "times"), Nothing]) [TermVar (B (NamedVar "X")), TermVar (B (NamedVar "Y"))]])) (Connected Disjunction (Not (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "inhabited")])) [TermVar (B (NamedVar "X"))])) (Not (TermSymbol (SymbolPredicate (PredicateAdj [Just (Word "inhabited")])) [TermVar (B (NamedVar "Y"))]))))) + , Quantified Universally (Scope (Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (F (TermVar (B (NamedVar "y")))), TermVar (B (NamedVar "X"))]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (F (TermVar (B (NamedVar "y")))), TermSymbol (SymbolMixfix [Just (Command "Cons"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR]) [TermVar (B (NamedVar "x")), TermVar (B (NamedVar "X"))]]))))) + , Quantified Universally (Scope (Not (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (NamedVar "a")), TermSymbol (SymbolMixfix [Just (Command "emptyset")]) []]))) + ] + , taskConjecture = + Quantified Universally (Scope (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (FreshVar 0)), TermSymbol (SymbolMixfix [Nothing, Just (Command "setminus"), Nothing]) [TermSymbol (SymbolMixfix [Nothing, Just (Command "union"), Nothing]) [TermVar (F (TermVar (NamedVar "x"))), TermVar (F (TermVar (NamedVar "y")))], TermSymbol (SymbolMixfix [Nothing, Just (Command "inter"), Nothing]) [TermVar (F (TermVar (NamedVar "y"))), TermVar (F (TermVar (NamedVar "x")))]]]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (B (FreshVar 0)), TermSymbol (SymbolMixfix [Nothing, Just (Command "symdiff"), Nothing]) [TermVar (F (TermVar (NamedVar "x"))), TermVar (F (TermVar (NamedVar "y")))]]))) + } |