diff --git a/executable/Main.hs b/executable/Main.hs
index 7799bf5..7ac1347 100644
--- a/executable/Main.hs
+++ b/executable/Main.hs
@@ -589,10 +589,14 @@ main = do
       -- hack: get --quiet and --no-proof options to appear before --tstp
     forAllFilesBox <*>
       (readProblemBox =>>=
-       expert (toFof <$> clausifyBox <*> pure (tags True)) =>>=
        expert clausifyBox =>>=
        forAllConjecturesBox <*>
-         (combine <$> pure (hornToUnitIO (HornFlags False)) <*>
+         (combine <$>
+           (pure (hornToUnitIO (HornFlags False)) =>>=
+            toFormulasBox =>>=
+            expert (toFof <$> clausifyBox <*> pure (tags True)) =>>=
+            clausifyBox =>>=
+            oneConjectureBox) <*>
            (runTwee <$> globalFlags <*> tstpFlags <*> parseMainFlags <*> parseConfig <*> parsePrecedence)))
   where
     combine horn prove later prob =