diff --git a/Codec/TPTP/Base.hs b/Codec/TPTP/Base.hs
--- a/Codec/TPTP/Base.hs
+++ b/Codec/TPTP/Base.hs
@@ -287,6 +287,7 @@
                  | GNumber Rational
                  | GDistinctObject String
                  | GFormulaData String Formula
+                 | GFormulaTerm String Term
                    deriving (Eq,Ord,Show,Read,Data,Typeable)
 
 -- | Metadata (the /general_term/ rule in TPTP's grammar)
@@ -502,9 +503,38 @@
                            ,arbNum GNumber
 
                            ,GDistinctObject <$> arbPrintable
-                           ,GFormulaData `fmap` ((:) '$' `fmap` arbLowerWord) `ap` (sized (\n -> resize (n `div` 2) arbitrary))
+                           ,oneof
+                            [ GFormulaData "$fof" `fmap` sized (\n -> resize (n `div` 2) arbitrary)
+                            , GFormulaData "$cnf" `fmap` sized (\n -> resize (n `div` 2) arbCNF)
+                            , GFormulaTerm "$fot" `fmap` sized (\n -> resize (n `div` 2) arbitrary)
+                            ]
                            ]
 
+arbCNF :: Gen Formula
+arbCNF = do
+    (xs :: [Formula]) <- liftArbitrary arbLiteral `suchThat` (not . Prelude.null)
+    return $ foldl1 (.|.) xs
+
+
+arbLiteral :: Gen Formula
+arbLiteral = oneof
+    [
+      do
+            p <- arbitrary
+            x <- arbAtomicFormula
+            return $ if p then x else (.~.) x
+    , do
+            x1 <- arbitrary
+            x2 <- arbitrary
+            return $ F $ point $ InfixPred x1 (:!=:) x2
+    ]
+
+
+arbAtomicFormula :: Gen Formula
+arbAtomicFormula = fmap (F . point) $ do
+    x1 <- arbitrary
+    x2 <- argsFreq vector
+    return (PredApp x1 x2)
 
 
 instance Arbitrary GTerm
diff --git a/Codec/TPTP/Export.hs b/Codec/TPTP/Export.hs
--- a/Codec/TPTP/Export.hs
+++ b/Codec/TPTP/Export.hs
@@ -141,7 +141,18 @@
    GVar x -> toTPTP x
    GNumber x -> showsRational x
    GDistinctObject x -> showString (tptpQuote x)
+   GFormulaData str@"$cnf" formu -> s str . s "(" . cnfToTPTP formu . s ")"
+     where
+       cnfToTPTP :: Formula -> ShowS
+       cnfToTPTP (F (Identity (BinOp l (:|:) r))) = cnfToTPTP l . s " | " . cnfToTPTP r
+       cnfToTPTP (F (Identity ((:~:) x@(F (Identity (PredApp _ _)))))) = s "~ " . toTPTP x
+       cnfToTPTP x@(F (Identity (PredApp _ _))) = toTPTP x
+       -- We do not call toTPTP directly on the formula in InfixPred case, because parenthesis should not be printed.
+       cnfToTPTP (F (Identity (InfixPred x1 (:!=:) x2))) = toTPTP x1 . s " != " . toTPTP x2
+       cnfToTPTP x = error $ show x ++ " is not a literal"
+
    GFormulaData str formu -> s str . s "(" . toTPTP formu . s ")"
+   GFormulaTerm str term -> s str . s "(" . toTPTP term . s ")"
 
 tptpQuote :: [Char] -> [Char]
 tptpQuote x = "\"" ++ concatMap go x ++ "\""
diff --git a/Codec/TPTP/Pretty.hs b/Codec/TPTP/Pretty.hs
--- a/Codec/TPTP/Pretty.hs
+++ b/Codec/TPTP/Pretty.hs
@@ -220,6 +220,7 @@
     pretty (GApp x []) = fsym x
     pretty (GApp x args) = fsym x <+> prettyargs args
     pretty (GFormulaData s f) = text s <> align (parens (pretty f))
+    pretty (GFormulaTerm s t) = text s <> align (parens (pretty t))
     pretty (GVar x) = pretty x
 
 instance Pretty AtomicWord where
diff --git a/Parser.y b/Parser.y
--- a/Parser.y
+++ b/Parser.y
@@ -54,6 +54,10 @@
  tok_cnf                { LowerWord "cnf" }
  tok_include_           { LowerWord "include" }
 
+ tok_fd_fof             { DollarWord "$fof" }
+ tok_fd_cnf             { DollarWord "$cnf" }
+ tok_fd_fot             { DollarWord "$fot" }
+
  tok_single_quoted      { SingleQuoted $$ }
  tok_distinct_object    { DoubleQuoted $$ }
  tok_dollar_word        { DollarWord $$ }
@@ -365,15 +369,17 @@
 
 general_data  :: {GData}
 general_data  :  atomic_word  { GWord $1 }
+               | formula_data  { $1 }
                | atomic_word  lp general_terms  rp { GApp $1 $3 }
                | variable  { GVar $1 }
                | number  { GNumber $1 }
                | distinct_object { GDistinctObject (stripQuotes '"' $1) }
-               | formula_data  { $1 }
 
+
 formula_data :: {GData}
-formula_data  : dollar_word lp fof_formula  rp { GFormulaData $1 $3 }
-              -- too ambiguous | dollar_word lp cnf_formula  rp { GFormulaData $1 $3 }
+formula_data  :  tok_fd_fof lp fof_formula  rp { GFormulaData "$fof" $3 }
+               | tok_fd_cnf lp cnf_formula  rp { GFormulaData "$cnf" $3 }
+               | tok_fd_fot lp term rp         { GFormulaTerm "$fot" $3 }
 
 general_list  :: {[GTerm]}
 general_list  : lbra rbra {[]}
diff --git a/ParserC.y b/ParserC.y
--- a/ParserC.y
+++ b/ParserC.y
@@ -55,6 +55,10 @@
  tok_cnf                { LowerWord "cnf" }
  tok_include_           { LowerWord "include" }
 
+ tok_fd_fof             { DollarWord "$fof" }
+ tok_fd_cnf             { DollarWord "$cnf" }
+ tok_fd_fot             { DollarWord "$fot" }
+
  tok_single_quoted      { SingleQuoted $$ }
  tok_distinct_object    { DoubleQuoted $$ }
  tok_dollar_word        { DollarWord $$ }
@@ -373,8 +377,9 @@
                | formula_data  { $1 }
 
 formula_data :: {GData}
-formula_data  : dollar_word lp fof_formula  rp { GFormulaData $1 (forgetFC $3) }
-              -- too ambiguous | dollar_word lp cnf_formula  rp { GFormulaData $1 $3 }
+formula_data  :  tok_fd_fof lp fof_formula  rp { GFormulaData "$fof" (forgetFC $3) }
+               | tok_fd_cnf lp cnf_formula  rp { GFormulaData "$cnf" (forgetFC $3) }
+               | tok_fd_fot lp term rp         { GFormulaTerm "$fot" (forgetTC $3) }
 
 general_list  :: {[GTerm]}
 general_list  : lbra rbra {[]}
diff --git a/changelog.markdown b/changelog.markdown
--- a/changelog.markdown
+++ b/changelog.markdown
@@ -1,3 +1,13 @@
+## 0.5.0.0
+
+* Add `GFormulaTerm` constructor to `GData` and support `$fot` `formula_data` (#1, #2, #19, thanks to @agomezl)
+* Produce valid `$cnf` `formula_data` (#23)
+* Improve test suites
+
+## 0.4.7.0
+
+* Fix to work with happy >=1.19.10
+
 ## 0.4.6.0
 
 * Add Semigroup instances for Monoids and fix cabal-version warning (Thanks to @msakai)
diff --git a/logic-TPTP.cabal b/logic-TPTP.cabal
--- a/logic-TPTP.cabal
+++ b/logic-TPTP.cabal
@@ -1,5 +1,5 @@
 name: logic-TPTP
-version: 0.4.7.0
+version: 0.5.0.0
 cabal-version: >= 1.8
 build-type: Simple
 license: GPL
@@ -96,6 +96,7 @@
  build-depends:     logic-TPTP
                   , base
                   , ansi-wl-pprint
+                  , optparse-applicative >=0.11 && <0.16
                   , pcre-light
                   , semigroups
  if impl(ghc <7.10)
diff --git a/testing/ParseRandom.hs b/testing/ParseRandom.hs
--- a/testing/ParseRandom.hs
+++ b/testing/ParseRandom.hs
@@ -1,5 +1,4 @@
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-{-# LANGUAGE PackageImports #-}
 
 module Main where
 
@@ -25,7 +24,7 @@
 import Common
 import SimpleArgs
 
-import "logic-TPTP" Codec.TPTP
+import Codec.TPTP
 
 infilename = getArgs
 parseRes = return . parse =<< readFile =<< infilename
diff --git a/testing/PrettyPrintFile.hs b/testing/PrettyPrintFile.hs
--- a/testing/PrettyPrintFile.hs
+++ b/testing/PrettyPrintFile.hs
@@ -1,5 +1,4 @@
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-{-# LANGUAGE PackageImports #-}
 
 module Main where
 
@@ -24,7 +23,7 @@
 import System.Exit
 import Text.Regex.PCRE.Light.Char8
 
-import "logic-TPTP" Codec.TPTP
+import Codec.TPTP
 import SimpleArgs
 
 main = putStrLn . prettySimple . parse =<< readFile =<< getArgs
diff --git a/testing/TestImportExportImportFile.hs b/testing/TestImportExportImportFile.hs
--- a/testing/TestImportExportImportFile.hs
+++ b/testing/TestImportExportImportFile.hs
@@ -1,39 +1,61 @@
 {-# OPTIONS_GHC -Wall #-}
-{-# LANGUAGE PackageImports #-}
 module Main where
 
 import Control.Monad
 import Data.Monoid
-import Text.PrettyPrint.ANSI.Leijen
+import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 import System.Exit
 import Common
-import SimpleArgs
+import Options.Applicative
 
-import "logic-TPTP" Codec.TPTP
+import Codec.TPTP
 
+data Options
+  = Options
+  { optPrintExport :: Bool
+  , optPrintFailureOnly :: Bool
+  }
 
+optionsParser :: Parser Options
+optionsParser = Options <$> printExportOption <*> printFailureOnlyOption
+  where
+    printExportOption = argument auto
+      $  metavar "True|False"
+      <> help ("print exported result")
+    printFailureOnlyOption = switch
+      $  long "print-failure-only"
+      <> help ("print failure only")
+
+parserInfo :: ParserInfo Options
+parserInfo = info (helper <*> optionsParser) $ mconcat
+  [ fullDesc
+  ]
+
 -- Note: This test expects a list of .p files (one per line) through stdin
 
 main ::  IO ()
 main = do
   files <- lines `fmap` getContents
   --print (length files)
-  print_export <- getArgs
-  forM_ files (diff_once_twice print_export)
+  Options print_export print_failure_only <- execParser parserInfo
+  forM_ files (diff_once_twice print_export print_failure_only)
   exitWith ExitSuccess
 
-diff_once_twice ::  Bool -> String -> IO ()
-diff_once_twice print_export infilename'  = do
+diff_once_twice ::  Bool -> Bool -> String -> IO ()
+diff_once_twice print_export print_failure_only infilename'  = do
   --let tmp = "/tmp/tmp.tptp"
-  putStrLn infilename'
+  unless print_failure_only $ putStrLn infilename'
   input <- readFile infilename'
   case findUnsupportedFormulaType input of
-     Just x -> putStrLn . prettySimple . yellow . text $ ("Skipping unsupported formula type "++x)
+     Just x -> do
+       unless print_failure_only $ 
+         putStrLn . prettySimple . yellow . text $ ("Skipping unsupported formula type "++x)
      Nothing -> do
 
       let once = parse input
       let tptp = toTPTP' once
-      when print_export (putStrLn $ "new tptp = " ++tptp)
+      when (print_export && not print_failure_only) $
+        putStrLn $ "new tptp = " ++tptp
       let twice = parse tptp
       let dif = mconcat (zipWith diffAFormula once twice)
       let success = (putStrLn . prettySimple . dullgreen . text $ "Ok")
@@ -46,7 +68,9 @@
       --     exitWith (ExitFailure 1)
 
       if once==twice
-         then success
+         then do
+           unless print_failure_only $ success
          else do
+           when print_failure_only $ putStrLn infilename'
            putStrLn . prettySimple $ dif
            exitWith (ExitFailure 1)
diff --git a/testing/TestImportExportRandom.hs b/testing/TestImportExportRandom.hs
--- a/testing/TestImportExportRandom.hs
+++ b/testing/TestImportExportRandom.hs
@@ -1,12 +1,11 @@
 {-# OPTIONS_GHC -Wall #-}
-{-# LANGUAGE PackageImports #-}
 module Main where
 
 import Test.QuickCheck
 import Common
 import Data.Functor.Identity
 
-import "logic-TPTP" Codec.TPTP
+import Codec.TPTP
 
 main ::  IO ()
 main = quickCheckWith (stdArgs { maxSuccess = 5000 }) prop_test_ie
@@ -20,10 +19,9 @@
 
           dif = diffAFormula f g
        in
-          whenFail
-          (putStrLn . prettySimple $ dif)
-
-           (f==g)
+          counterexample tptp $
+           whenFail (putStrLn . prettySimple $ dif) $
+            (f==g)
 
           -- (case dif of
           --    OtherSame -> True