From 9aac1a22c4ff4b4be16800b86e34a94d358b0deb Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 16 Jul 2025 12:36:32 +0200
Subject: Add quantified calcs and relax tokenization

Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems.
---
 source/CommandLine.hs | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'source/CommandLine.hs')

diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index b8c170e..3502b9a 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -18,7 +18,6 @@ import UnliftIO
 import UnliftIO.Directory
 import UnliftIO.Environment (lookupEnv)
 import System.FilePath.Posix
-import qualified Tptp.UnsortedFirstOrder as Syntax.Internal
 
 runCommandLine :: IO ()
 runCommandLine = do
@@ -94,7 +93,7 @@ run = do
                             Text.putStrLn task
                             Text.putStrLn err
                             Text.putStrLn tptp
-                            
+
                 WithFailList -> liftIO case result of
                     VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m"
                     VerificationFailure [] -> error "Empty verification fail"
@@ -187,4 +186,4 @@ withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to M
 
 withFailListParser :: Parser WithFailList
 withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.")
-    <|> pure WithoutFailList -- Default to using the cache.
\ No newline at end of file
+    <|> pure WithoutFailList -- Default to using the cache.
-- 
cgit v1.2.3