diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,21 @@
 # Revision history for tptp
 
+## 0.1.2.0 -- 2020-04-03
+
+* Consume leading whitespace in the TSTP parser.
+
+* Do not pretty print parenthesis in negated equality literals.
+
+* Parse superfluous parenthesis in types, terms and clauses.
+
+* Add a helper function 'unitClause'.
+
+* Add more tests and improve documentation.
+
+* Set more accurate lower bounds of the base and scientific dependencies.
+
+* Support compilation with GHC 8.8.3 and 8.10.1.
+
 ## 0.1.1.0 -- 2019-12-07
 
 * Parse SZS ontology information in the TSTP input.
diff --git a/src/Data/TPTP.hs b/src/Data/TPTP.hs
--- a/src/Data/TPTP.hs
+++ b/src/Data/TPTP.hs
@@ -56,6 +56,7 @@
   Literal(..),
   Sign(..),
   Clause(..),
+  unitClause,
   clause,
   Quantifier(..),
   Connective(..),
@@ -106,10 +107,15 @@
 import Data.Text (Text)
 
 #if !MIN_VERSION_base(4, 8, 0)
+import Data.Monoid (Monoid(..))
 import Data.Foldable (Foldable)
 import Data.Traversable (Traversable, traverse)
 #endif
 
+#if !MIN_VERSION_base(4, 11, 0)
+import Data.Semigroup (Semigroup(..))
+#endif
+
 -- $setup
 -- >>> :set -XOverloadedStrings
 -- >>> :load Data.TPTP.Pretty
@@ -158,6 +164,9 @@
 newtype Atom = Atom Text
   deriving (Eq, Show, Ord, IsString)
 
+instance Semigroup Atom where
+  Atom t <> Atom s = Atom (t <> s)
+
 -- | Check whether a given character is in the ASCII range 0x20 to 0x7E.
 isAsciiPrint :: Char -> Bool
 isAsciiPrint c = isAscii c && isPrint c
@@ -184,6 +193,9 @@
 newtype Var = Var Text
   deriving (Eq, Show, Ord, IsString)
 
+instance Semigroup Var where
+  Var v <> Var w = Var (v <> w)
+
 -- | Check whether a given character matches the regular expression
 -- @[a-zA-Z0-9_]@.
 isAlphaNumeric :: Char -> Bool
@@ -229,6 +241,13 @@
 newtype DistinctObject = DistinctObject Text
   deriving (Eq, Show, Ord, IsString)
 
+instance Semigroup DistinctObject where
+  DistinctObject d <> DistinctObject b = DistinctObject (d <> b)
+
+instance Monoid DistinctObject where
+  mempty = DistinctObject mempty
+  mappend = (<>)
+
 -- | Check whether a given string is a valid distinct object.
 --
 -- >>> isValidDistinctObject ""
@@ -312,25 +331,26 @@
 
 -- | The standard function symbol in TPTP.
 -- Represents an operation in a first-order theory of arithmetic.
+-- See <http://www.tptp.org/TPTP/TR/TPTPTR.shtml#arithmetic> for details.
 data Function
-  = Uminus
-  | Sum
-  | Difference
-  | Product
-  | Quotient
-  | QuotientE
-  | QuotientT
-  | QuotientF
-  | RemainderE
-  | RemainderT
-  | RemainderF
-  | Floor
-  | Ceiling
-  | Truncate
-  | Round
-  | ToInt
-  | ToRat
-  | ToReal
+  = Uminus     -- ^ @$uminus@ - Unary minus of a number.
+  | Sum        -- ^ @$sum@ - Sum of two numbers.
+  | Difference -- ^ @$difference@ - Difference between two numbers.
+  | Product    -- ^ @$product@ - Product of two numbers.
+  | Quotient   -- ^ @$quotient@ - Exact quotient of two @$rat@ or @$real@ numbers.
+  | QuotientE  -- ^ @$quotient_e@ - Integral quotient of two numbers.
+  | QuotientT  -- ^ @$quotient_t@ - Integral quotient of two numbers.
+  | QuotientF  -- ^ @$quotient_f@ - Integral quotient of two numbers.
+  | RemainderE -- ^ @$remainder_e@ - Remainder after integral division of two numbers.
+  | RemainderT -- ^ @$remainder_t@ - Remainder after integral division of two numbers.
+  | RemainderF -- ^ @$remainder_f@ - Remainder after integral division of two numbers.
+  | Floor      -- ^ @$floor@ - Floor of a number.
+  | Ceiling    -- ^ @$ceiling@ - Ceiling of a number.
+  | Truncate   -- ^ @$truncate@ - Truncation of a number.
+  | Round      -- ^ @$round@ - Rounding of a number.
+  | ToInt      -- ^ @$to_int@ - Coercion of a number to @$int@.
+  | ToRat      -- ^ @$to_rat@ - Coercion of a number to @$rat@.
+  | ToReal     -- ^ @$to_real@ - Coercion of a number to @$real@.
   deriving (Eq, Show, Ord, Enum, Bounded)
 
 instance Named Function where
@@ -355,16 +375,17 @@
     ToReal     -> "to_real"
 
 -- | The standard predicate symbol in TPTP.
+-- See <http://www.tptp.org/TPTP/TR/TPTPTR.shtml#arithmetic> for details.
 data Predicate
-  = Tautology
-  | Falsum
-  | Distinct
-  | Less
-  | Lesseq
-  | Greater
-  | Greatereq
-  | IsInt
-  | IsRat
+  = Tautology -- ^ @$true@ - Logical tautology.
+  | Falsum    -- ^ @$false@ - Logical falsum.
+  | Distinct  -- ^ @$distinct@ - Denotes that its arguments are unequal to each other.
+  | Less      -- ^ @$less@ - Less-than comparison of two numbers.
+  | Lesseq    -- ^ @$lesseq@ - Less-than-or-equal-to comparison of two numbers.
+  | Greater   -- ^ @$greater@ - Greater-than comparison of two numbers.
+  | Greatereq -- ^ @$greatereq@ - Greater-than-or-equal-to comparison of two numbers.
+  | IsInt     -- ^ @$is_nat@ - Test for coincidence with an integer.
+  | IsRat     -- ^ @$is_rat@ - Test for coincidence with a rational.
   deriving (Eq, Show, Ord, Enum, Bounded)
 
 instance Named Predicate where
@@ -406,11 +427,11 @@
 
 -- | The standard sort in TPTP.
 data Sort
-  = I    -- ^ The sort of individuals.
-  | O    -- ^ The sort of booleans.
-  | Int  -- ^ The sort of integers.
-  | Real -- ^ The sort of real numbers.
-  | Rat  -- ^ The sort of rational numbers.
+  = I    -- ^ @$i@ - The sort of individuals.
+  | O    -- ^ @$o@ - The sort of booleans.
+  | Int  -- ^ @$int@ - The sort of integers.
+  | Real -- ^ @$real@ - The sort of real numbers.
+  | Rat  -- ^ @$rat@ - The sort of rational numbers.
   deriving (Eq, Show, Ord, Enum, Bounded)
 
 instance Named Sort where
@@ -459,7 +480,10 @@
 
 -- | A smart constructor of a TFF1 type. 'tff1Type' constructs a TFF0 type with
 -- its arguments, if it is possible, and otherwise constructs a TFF1 type.
-tff1Type :: [Var] -> [TFF1Sort] -> TFF1Sort -> Type
+tff1Type :: [Var]      -- ^ Quantified type variables.
+         -> [TFF1Sort] -- ^ Sort arguments.
+         -> TFF1Sort   -- ^ Return sort.
+         -> Type
 tff1Type [] ss s
   | Just ss' <- traverse monomorphizeTFF1Sort ss
   , Just s'  <- monomorphizeTFF1Sort s = Type ss' s'
@@ -523,13 +547,20 @@
 newtype Clause = Clause (NonEmpty (Sign, Literal))
   deriving (Eq, Show, Ord)
 
+instance Semigroup Clause where
+  Clause ls <> Clause ks = Clause (ls <> ks)
+
+-- | Construct a unit clause from a given signed literal.
+unitClause :: (Sign, Literal) -> Clause
+unitClause l = Clause (l :| [])
+
 -- | A smart constructor for 'Clause'. 'clause' constructs a clause from a
 -- possibly empty list of signed literals. If the provided list is empty,
 -- the unit clause @$false@ is constructed instead.
 clause :: [(Sign, Literal)] -> Clause
 clause ls
   | Just ls' <- nonEmpty ls = Clause ls'
-  | otherwise = Clause ((Positive, falsum) :| [])
+  | otherwise = unitClause (Positive, falsum)
   where
     falsum = Predicate (Reserved (Standard Falsum)) []
 
@@ -546,14 +577,14 @@
 
 -- | The connective in full first-order logic.
 data Connective
-  = Conjunction
-  | Disjunction
-  | Implication
-  | Equivalence
-  | ExclusiveOr
-  | NegatedConjunction
-  | NegatedDisjunction
-  | ReversedImplication
+  = Conjunction         -- ^ @&@.
+  | Disjunction         -- ^ @|@.
+  | Implication         -- ^ @=>@.
+  | Equivalence         -- ^ @<=>@.
+  | ExclusiveOr         -- ^ @<~>@ - XOR.
+  | NegatedConjunction  -- ^ @~&@ - NAND.
+  | NegatedDisjunction  -- ^ @~|@ - NOR.
+  | ReversedImplication -- ^ @<=@.
   deriving (Eq, Show, Ord, Enum, Bounded)
 
 -- | Check associativity of a given connective.
@@ -727,6 +758,13 @@
 newtype TPTP = TPTP {
   units :: [Unit]
 } deriving (Eq, Show, Ord)
+
+instance Semigroup TPTP where
+  TPTP us <> TPTP ys = TPTP (us <> ys)
+
+instance Monoid TPTP where
+  mempty = TPTP mempty
+  mappend = (<>)
 
 -- | The TSTP output - zero or more TSTP units, possibly annotated with the
 -- status of the proof search and the resulting dataform.
diff --git a/src/Data/TPTP/Parse/Combinators.hs b/src/Data/TPTP/Parse/Combinators.hs
--- a/src/Data/TPTP/Parse/Combinators.hs
+++ b/src/Data/TPTP/Parse/Combinators.hs
@@ -1,5 +1,6 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE CPP #-}
 
@@ -68,7 +69,9 @@
 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(..))
+import Data.Semigroup (Semigroup(..), sconcat)
+#else
+import Data.Semigroup (sconcat)
 #endif
 
 import qualified Data.Scientific as Sci (base10Exponent, coefficient)
@@ -153,7 +156,7 @@
 {-# INLINE parens #-}
 
 optionalParens :: Parser a -> Parser a
-optionalParens p = parens p <|> p
+optionalParens p = p <|> parens (optionalParens p)
 {-# INLINE optionalParens #-}
 
 brackets :: Parser a -> Parser a
@@ -170,7 +173,7 @@
 {-# INLINE bracketList1 #-}
 
 application :: Parser f -> Parser a -> Parser (f, [a])
-application f a = (,) <$> f <*> option [] (parens (a `sepBy1` op ','))
+application f a = (,) <$> f <*> option [] (parens (optionalParens a `sepBy1` op ','))
 {-# INLINE application #-}
 
 labeled :: Text -> Parser a -> Parser a
@@ -280,8 +283,8 @@
      <?> "type"
   where
     prefix = token "!>" *> bracketList1 sortVar <* op ':'
-    sortVar = var <* op ':' <* token "$tType"
-    matrix = optionalParens (mapping tff1Sort)
+    sortVar = var <* op ':' <* optionalParens (token "$tType")
+    matrix = optionalParens (mapping (optionalParens tff1Sort))
 
 
 -- ** First-order logic
@@ -297,41 +300,50 @@
       | otherwise = RealConstant n
 
 -- | Parse a term.
+--
+-- @term@ supports parsing superfluous parenthesis around arguments
+-- of the function application, which are not present in the TPTP grammar.
 term :: Parser Term
-term =  parens term
-    <|> uncurry Function <$> application function term
+term =  uncurry Function <$> application function term
     <|> Variable         <$> var
     <|> Number           <$> number
     <|> DistinctTerm     <$> distinctObject
     <?> "term"
 
--- | Parse the equality and the unequality sign.
+-- | Parse the equality and the inequality sign.
 eq :: Parser Sign
 eq = enum <?> "eq"
 {-# INLINE eq #-}
 
 -- | Parse a literal.
+--
+-- @literal@ supports parsing superfluous parenthesis around arguments
+-- of the predicate application, which are not present in the TPTP grammar.
 literal :: Parser Literal
-literal =  parens literal
-       <|> Equality <$> term <*> eq <*> term
+literal =  Equality <$> optionalParens term <*> eq <*> optionalParens term
        <|> uncurry Predicate <$> application predicate term
        <?> "literal"
 
--- | Parse the negation sign.
-sign :: Parser Sign
-sign = option Positive (op '~' $> Negative)
-{-# INLINE sign #-}
-
 -- | Parse a signed literal.
+--
+-- @signedLiteral@ supports parsing superfluous parenthesis around the literal
+-- under the negation sign, which are not present in the TPTP grammar.
 signedLiteral :: Parser (Sign, Literal)
-signedLiteral = (,) <$> sign <*> literal <?> "signed literal"
+signedLiteral =  fmap (Negative,) (op '~' *> optionalParens literal)
+             <|> fmap (Positive,) literal
+             <?> "signed literal"
 {-# INLINE signedLiteral #-}
 
 -- | Parse a clause.
+--
+-- @clause@ supports parsing superfluous parenthesis around any of the
+-- subclauses of the clause, which are not present in the TPTP grammar.
 clause :: Parser Clause
-clause =  parens clause
-      <|> Clause . NEL.fromList <$> signedLiteral `sepBy1` op '|'
-      <?> "clause"
+clause = sconcat . NEL.fromList <$> subclause `sepBy1` op '|'
+  where
+    subclause =  unitClause <$> signedLiteral
+             <|> parens clause
+             <?> "subclause"
 
 -- | Parse a quantifier.
 quantifier :: Parser Quantifier
@@ -349,10 +361,10 @@
   f <- unitary
   option f (Connected f <$> connective <*> firstOrder p)
   where
-    unitary =  parens (firstOrder p)
-           <|> Atomic     <$> literal
-           <|> Quantified <$> quantifier <*> vs <* op ':' <*> unitary
+    unitary =  Atomic     <$> literal
            <|> Negated    <$> (op '~' *> unitary)
+           <|> Quantified <$> quantifier <*> vs <* op ':' <*> unitary
+           <|> parens (firstOrder p)
            <?> "unitary first order"
 
     vs = bracketList1 $ (,) <$> var <*> p
@@ -363,7 +375,7 @@
   where unsorted = pure (Unsorted ()) <?> "unsorted"
 
 sorted :: Parser s -> Parser (Sorted s)
-sorted s = Sorted <$> optional (op ':' *> s) <?> "sorted"
+sorted s = Sorted <$> optional (op ':' *> optionalParens s) <?> "sorted"
 
 -- | An alias for 'monomorphicFirstOrder'.
 sortedFirstOrder :: Parser SortedFirstOrder
@@ -414,11 +426,11 @@
 -- | Parse a declaration with the @type@ role - either a typing relation or
 -- a sort declaration.
 typeDeclaration :: Parser Declaration
-typeDeclaration =  Sort   <$> atom <* op ':' <*> arity
-               <|> Typing <$> atom <* op ':' <*> type_
+typeDeclaration =  Sort   <$> atom <* op ':' <*> optionalParens arity
+               <|> Typing <$> atom <* op ':' <*> optionalParens type_
                <?> "type declaration"
   where
-    arity = genericLength . fst <$> mapping (token "$tType")
+    arity = genericLength . fst <$> mapping (optionalParens (token "$tType"))
 
 -- | Parse a unit name.
 unitName :: Parser (Either Atom Integer)
@@ -455,7 +467,8 @@
 
 -- | Parse a TSTP input.
 tstp :: Parser TSTP
-tstp = TSTP <$> szs <*> manyTill unit endOfInput <* endOfInput <?> "tstp"
+tstp =  skipSpace *> (TSTP <$> szs <*> manyTill unit endOfInput) <* endOfInput
+    <?> "tstp"
 
 
 -- ** Annotations
@@ -524,8 +537,8 @@
 
 -- | Parse and expression
 expr :: Parser Expression
-expr =  char '$' *> (labeled "fot" (Term <$> term)
-                <|>  Logical <$> (language >>= parens . formula))
+expr =  char '$' *> (labeled "fot" (Term <$> optionalParens term)
+                <|>  Logical <$> (language >>= parens . optionalParens . formula))
     <?> "expression"
 
 -- | Parse a parent.
diff --git a/src/Data/TPTP/Pretty.hs b/src/Data/TPTP/Pretty.hs
--- a/src/Data/TPTP/Pretty.hs
+++ b/src/Data/TPTP/Pretty.hs
@@ -18,6 +18,7 @@
 ) where
 
 #if !MIN_VERSION_base(4, 8, 0)
+import Data.Foldable (Foldable)
 import Data.Functor ((<$>))
 import Data.Monoid (mempty)
 #endif
@@ -27,9 +28,9 @@
 #endif
 
 import Data.Char (isAsciiLower, isAsciiUpper, isDigit)
-import Data.List (genericReplicate)
-import Data.List.NonEmpty (NonEmpty)
-import qualified Data.List.NonEmpty as NEL (nonEmpty, toList)
+import qualified Data.Foldable as Foldable (toList)
+import Data.List (genericReplicate, intersperse)
+import qualified Data.List.NonEmpty as NEL (nonEmpty)
 import Data.Maybe (maybeToList)
 import Data.Text (Text)
 import qualified Data.Text as Text (
@@ -37,7 +38,7 @@
   )
 import Data.Text.Prettyprint.Doc (
     Doc, Pretty(..),
-    hsep, sep, (<+>), brackets, parens, punctuate, comma, space, line
+    hsep, sep, (<+>), parens, brackets, punctuate, space, comma, line
   )
 
 import Data.TPTP
@@ -48,21 +49,18 @@
 comment :: Doc ann -> Doc ann
 comment c = "%" <+> c <> line
 
-sepBy :: [Doc ann] -> Doc ann -> Doc ann
-sepBy as s = hsep (punctuate s as)
-
-sepBy1 :: NonEmpty (Doc ann) -> Doc ann -> Doc ann
-sepBy1 as s = hsep (punctuate s (NEL.toList as))
+sepBy :: Foldable f => f (Doc ann) -> Doc ann -> Doc ann
+sepBy as s = hsep (intersperse s (Foldable.toList as))
 
 application :: Pretty f => f -> [Doc ann] -> Doc ann
 application f [] = pretty f
-application f as = pretty f <> parens (as `sepBy` comma)
+application f as = pretty f <> parens (hsep (punctuate comma as))
 
-bracketList :: Pretty a => [a] -> Doc ann
-bracketList as = brackets (fmap pretty as `sepBy` comma)
+list :: Foldable f => f (Doc ann) -> Doc ann
+list = brackets . hsep . punctuate comma . Foldable.toList
 
-bracketList1 :: Pretty a => NonEmpty a -> Doc ann
-bracketList1 as = brackets (fmap pretty as `sepBy1` comma)
+bracketList :: (Pretty a, Functor f, Foldable f) => f a -> Doc ann
+bracketList = list . fmap pretty
 
 
 -- * Names
@@ -135,7 +133,7 @@
     args = case as of
       []  -> mempty
       [a] -> pretty a <+> ">" <> space
-      _   -> parens (fmap pretty as `sepBy` (space <> "*")) <+> ">" <> space
+      _   -> parens (fmap pretty as `sepBy` "*") <+> ">" <> space
 
 instance Pretty Type where
   pretty = \case
@@ -143,9 +141,8 @@
     TFF1Type vs as r -> prefix <> if null as then matrix else parens matrix
       where
         prefix = case NEL.nonEmpty vs of
-          Nothing  -> mempty
-          Just vs' -> "!>" <+> brackets (vars vs') <> ":" <> space
-        vars vs' = fmap prettyVar vs' `sepBy1` comma
+          Nothing -> mempty
+          Just{}  -> "!>" <+> list (fmap prettyVar vs) <> ":" <> space
         prettyVar v = pretty v <> ":" <+> pretty tType
         matrix = prettyMapping as r
 
@@ -175,10 +172,15 @@
 
 instance Pretty Clause where
   pretty = \case
-    Clause ls -> fmap p ls `sepBy1` (space <> pretty Disjunction)
+    Clause ls -> fmap p ls `sepBy` pretty Disjunction
       where
         p (Positive, l) = pretty l
-        p (Negative, l) = "~" <+> parens (pretty l)
+        -- TPTP v7.3.0.0 doesn't allow for wrapping atom in parentesis in
+        -- a negated atom in CNF formulas. I.e. for example ~ (X = Y) is
+        -- not allowed. See http://www.tptp.org/TPTP/SyntaxBNF.html#cnf_formula
+        -- TODO: implement AB-test comparing this parser against some canonical
+        -- implementation of the parser of TPTP BNF (like tptp4X).
+        p (Negative, l) = "~" <+> pretty l
 
 instance Pretty Quantifier where
   pretty = pretty . name
@@ -207,24 +209,24 @@
   Quantified{} -> True
   Connected{}  -> False
 
-pretty' :: Pretty s => FirstOrder s -> Doc ann
-pretty' f
-  | unitary f = pretty f
-  | otherwise = parens (pretty f)
+ppretty :: Pretty s => (FirstOrder s -> Bool) -> FirstOrder s -> Doc ann
+ppretty skipParens f
+  | skipParens f = pretty f
+  | otherwise    = parens (pretty f)
 
+under :: Connective -> FirstOrder s -> Bool
+under c = \case
+  Connected _ c' _ -> c' == c && isAssociative c
+  f -> unitary f
+
 instance Pretty s => Pretty (FirstOrder s) where
   pretty = \case
     Atomic l -> pretty l
-    Negated f -> "~" <+> pretty' f
-    Connected f c g -> pretty'' f <+> pretty c <+> pretty'' g
-      where
-        -- Nested applications of associative connectives do not require
-        -- parenthesis. Otherwise, the connectives do not have precedence
-        pretty'' e@(Connected _ c' _) | c' == c && isAssociative c = pretty e
-        pretty'' e = pretty' e
-    Quantified q vs f -> pretty q <+> vs' <> ":" <+> pretty' f
+    Negated f -> "~" <+> ppretty unitary f
+    Connected f c g -> ppretty (under c) f <+> pretty c <+> ppretty (under c) g
+    Quantified q vs f -> pretty q <+> list vs' <> ":" <+> ppretty unitary f
       where
-        vs' = brackets (fmap var vs `sepBy1` comma)
+        vs' = fmap var (Foldable.toList vs)
         var (v, s) = pretty v <> pretty s
 
 
@@ -255,7 +257,7 @@
   pretty = \case
     Include (Atom f) ns -> application (Atom "include") args <> "."
       where
-        args = pretty (SingleQuoted f) : maybeToList (fmap bracketList1 ns)
+        args = pretty (SingleQuoted f) : maybeToList (fmap bracketList ns)
     Unit nm decl a -> application (declarationLanguage decl) args <> "."
       where
         args = pretty nm : role : pretty decl : ann
@@ -286,7 +288,7 @@
       dataform p = case d of
         Nothing -> p
         Just df -> szsComment ["output", "start", pretty df]
-                <> p
+                <> p <> line
                 <> szsComment ["output", "end", pretty df]
 
 
@@ -316,7 +318,7 @@
     Description    a -> application (Atom "description") [pretty a]
     Iquote         a -> application (Atom "iquote")      [pretty a]
     Status         s -> application (Atom "status")      [pretty s]
-    Assumptions    u -> application (Atom "assumptions") [bracketList1 u]
+    Assumptions    u -> application (Atom "assumptions") [bracketList u]
     NewSymbols  n ss -> application (Atom "new_symbols") [pretty n, prettyList ss]
     Refutation     a -> application (Atom "refutation")  [pretty a]
     Bind         v e -> application (Atom "bind")        [pretty v, pretty e]
diff --git a/test-data/szs/fof/group-theory---E.s b/test-data/szs/fof/group-theory---E.s
new file mode 100644
--- /dev/null
+++ b/test-data/szs/fof/group-theory---E.s
@@ -0,0 +1,25 @@
+
+# Proof found!
+# SZS status Theorem
+# SZS output start CNFRefutation
+fof(3, axiom, ![X3, X1, X2]:mult(mult(X3,X1),X2)=mult(X3,mult(X1,X2)), file('<stdin>', 3)).
+fof(4, axiom, ![X2]:mult(X2,X2)=e, file('<stdin>', 4)).
+fof(1, axiom, ![X2]:mult(e,X2)=X2, file('<stdin>', 1)).
+fof(0, conjecture, ![X1, X2]:mult(X1,X2)=mult(X2,X1), file('<stdin>', 0)).
+fof(c_0_4, plain, ![X8, X9, X10]:mult(mult(X8,X9),X10)=mult(X8,mult(X9,X10)), inference(variable_rename,[status(thm)],[3])).
+fof(c_0_5, plain, ![X11]:mult(X11,X11)=e, inference(variable_rename,[status(thm)],[4])).
+fof(c_0_6, plain, ![X6]:mult(e,X6)=X6, inference(variable_rename,[status(thm)],[1])).
+cnf(c_0_7, plain, (mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))), inference(split_conjunct,[status(thm)],[c_0_4])).
+cnf(c_0_8, plain, (mult(X1,X1)=e), inference(split_conjunct,[status(thm)],[c_0_5])).
+cnf(c_0_9, plain, (mult(e,X1)=X1), inference(split_conjunct,[status(thm)],[c_0_6])).
+cnf(c_0_10, plain, (mult(X1,mult(X1,X2))=X2), inference(rw,[status(thm)],[inference(pm,[status(thm)],[c_0_7, c_0_8]), c_0_9])).
+fof(c_0_11, negated_conjecture, ~(![X1, X2]:mult(X1,X2)=mult(X2,X1)), inference(assume_negation,[status(cth)],[0])).
+cnf(c_0_12, plain, (mult(X1,mult(X2,mult(X1,X2)))=e), inference(pm,[status(thm)],[c_0_8, c_0_7])).
+cnf(c_0_13, plain, (mult(X1,e)=X1), inference(pm,[status(thm)],[c_0_10, c_0_8])).
+fof(c_0_14, negated_conjecture, mult(esk1_0,esk2_0)!=mult(esk2_0,esk1_0), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])).
+cnf(c_0_15, plain, (mult(X1,mult(X2,X1))=X2), inference(rw,[status(thm)],[inference(pm,[status(thm)],[c_0_10, c_0_12]), c_0_13])).
+cnf(c_0_16, negated_conjecture, (mult(esk1_0,esk2_0)!=mult(esk2_0,esk1_0)), inference(split_conjunct,[status(thm)],[c_0_14])).
+cnf(c_0_17, plain, (mult(X1,X2)=mult(X2,X1)), inference(pm,[status(thm)],[c_0_10, c_0_15])).
+cnf(c_0_18, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_17])]), ['proof']).
+# SZS output end CNFRefutation
+# Training examples: 0 positive, 0 negative
diff --git a/test-data/szs/fof/group-theory---Vampire.s b/test-data/szs/fof/group-theory---Vampire.s
new file mode 100644
--- /dev/null
+++ b/test-data/szs/fof/group-theory---Vampire.s
@@ -0,0 +1,97 @@
+% Refutation found. Thanks to Tanya!
+% SZS status Theorem for 
+% SZS output start Proof for 
+fof(f276,plain,(
+  $false),
+  inference(trivial_inequality_removal,[],[f275])).
+fof(f275,plain,(
+  mult(sK0,sK1) != mult(sK0,sK1)),
+  inference(superposition,[],[f16,f131])).
+fof(f131,plain,(
+  ( ! [X2,X3] : (mult(X2,X3) = mult(X3,X2)) )),
+  inference(superposition,[],[f27,f96])).
+fof(f96,plain,(
+  ( ! [X4,X3] : (mult(X4,mult(X3,X4)) = X3) )),
+  inference(forward_demodulation,[],[f81,f33])).
+fof(f33,plain,(
+  ( ! [X2] : (mult(inverse(X2),e) = X2) )),
+  inference(superposition,[],[f27,f18])).
+fof(f18,plain,(
+  ( ! [X0] : (e = mult(inverse(X0),X0)) )),
+  inference(cnf_transformation,[],[f9])).
+fof(f9,plain,(
+  ! [X0] : e = mult(inverse(X0),X0)),
+  inference(rectify,[],[f4])).
+fof(f4,axiom,(
+  ! [X1] : e = mult(inverse(X1),X1)),
+  file(unknown,unknown)).
+fof(f81,plain,(
+  ( ! [X4,X3] : (mult(X4,mult(X3,X4)) = mult(inverse(X3),e)) )),
+  inference(superposition,[],[f28,f25])).
+fof(f25,plain,(
+  ( ! [X0,X1] : (e = mult(X0,mult(X1,mult(X0,X1)))) )),
+  inference(superposition,[],[f19,f20])).
+fof(f20,plain,(
+  ( ! [X0] : (e = mult(X0,X0)) )),
+  inference(cnf_transformation,[],[f12])).
+fof(f12,plain,(
+  ! [X0] : e = mult(X0,X0)),
+  inference(rectify,[],[f6])).
+fof(f6,axiom,(
+  ! [X1] : e = mult(X1,X1)),
+  file(unknown,unknown)).
+fof(f19,plain,(
+  ( ! [X2,X0,X1] : (mult(mult(X0,X1),X2) = mult(X0,mult(X1,X2))) )),
+  inference(cnf_transformation,[],[f11])).
+fof(f11,plain,(
+  ! [X0,X1,X2] : mult(mult(X0,X1),X2) = mult(X0,mult(X1,X2))),
+  inference(flattening,[],[f10])).
+fof(f10,plain,(
+  ! [X0] : ! [X1] : ! [X2] : mult(mult(X0,X1),X2) = mult(X0,mult(X1,X2))),
+  inference(rectify,[],[f5])).
+fof(f5,axiom,(
+  ! [X2] : ! [X0] : ! [X1] : mult(mult(X2,X0),X1) = mult(X2,mult(X0,X1))),
+  file(unknown,unknown)).
+fof(f28,plain,(
+  ( ! [X4,X5] : (mult(inverse(X4),mult(X4,X5)) = X5) )),
+  inference(forward_demodulation,[],[f23,f17])).
+fof(f17,plain,(
+  ( ! [X0] : (mult(e,X0) = X0) )),
+  inference(cnf_transformation,[],[f8])).
+fof(f8,plain,(
+  ! [X0] : mult(e,X0) = X0),
+  inference(rectify,[],[f3])).
+fof(f3,axiom,(
+  ! [X1] : mult(e,X1) = X1),
+  file(unknown,unknown)).
+fof(f23,plain,(
+  ( ! [X4,X5] : (mult(inverse(X4),mult(X4,X5)) = mult(e,X5)) )),
+  inference(superposition,[],[f19,f18])).
+fof(f27,plain,(
+  ( ! [X2,X3] : (mult(X2,mult(X2,X3)) = X3) )),
+  inference(forward_demodulation,[],[f22,f17])).
+fof(f22,plain,(
+  ( ! [X2,X3] : (mult(X2,mult(X2,X3)) = mult(e,X3)) )),
+  inference(superposition,[],[f19,f20])).
+fof(f16,plain,(
+  mult(sK0,sK1) != mult(sK1,sK0)),
+  inference(cnf_transformation,[],[f15])).
+fof(f15,plain,(
+  mult(sK0,sK1) != mult(sK1,sK0)),
+  inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1])],[f13,f14])).
+fof(f14,plain,(
+  ? [X0,X1] : mult(X0,X1) != mult(X1,X0) => mult(sK0,sK1) != mult(sK1,sK0)),
+  introduced(choice_axiom,[])).
+fof(f13,plain,(
+  ? [X0,X1] : mult(X0,X1) != mult(X1,X0)),
+  inference(ennf_transformation,[],[f7])).
+fof(f7,plain,(
+  ~! [X0,X1] : mult(X0,X1) = mult(X1,X0)),
+  inference(flattening,[],[f2])).
+fof(f2,negated_conjecture,(
+  ~! [X0] : ! [X1] : mult(X0,X1) = mult(X1,X0)),
+  inference(negated_conjecture,[],[f1])).
+fof(f1,conjecture,(
+  ! [X0] : ! [X1] : mult(X0,X1) = mult(X1,X0)),
+  file(unknown,unknown)).
+% SZS output end Proof for 
diff --git a/test-data/szs/fof/syllogism---E.s b/test-data/szs/fof/syllogism---E.s
new file mode 100644
--- /dev/null
+++ b/test-data/szs/fof/syllogism---E.s
@@ -0,0 +1,17 @@
+
+# Proof found!
+# SZS status Theorem
+# SZS output start CNFRefutation
+fof(0, conjecture, mortal(socrates), file('<stdin>', 0)).
+fof(1, axiom, ![X1]:(human(X1)=>mortal(X1)), file('<stdin>', 1)).
+fof(2, axiom, human(socrates), file('<stdin>', 2)).
+fof(c_0_3, negated_conjecture, ~(mortal(socrates)), inference(assume_negation,[status(cth)],[0])).
+fof(c_0_4, plain, ![X2]:(~human(X2)|mortal(X2)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[1])])).
+fof(c_0_5, negated_conjecture, ~mortal(socrates), inference(fof_simplification,[status(thm)],[c_0_3])).
+cnf(c_0_6, plain, (mortal(X1)|~human(X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
+cnf(c_0_7, plain, (human(socrates)), inference(split_conjunct,[status(thm)],[2])).
+cnf(c_0_8, negated_conjecture, (~mortal(socrates)), inference(split_conjunct,[status(thm)],[c_0_5])).
+cnf(c_0_9, plain, (mortal(socrates)), inference(pm,[status(thm)],[c_0_6, c_0_7])).
+cnf(c_0_10, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_8, c_0_9])]), ['proof']).
+# SZS output end CNFRefutation
+# Training examples: 0 positive, 0 negative
diff --git a/test-data/szs/fof/syllogism---Vampire.s b/test-data/szs/fof/syllogism---Vampire.s
new file mode 100644
--- /dev/null
+++ b/test-data/szs/fof/syllogism---Vampire.s
@@ -0,0 +1,37 @@
+% Refutation found. Thanks to Tanya!
+% SZS status Theorem for 
+% SZS output start Proof for 
+fof(f11,plain,(
+  $false),
+  inference(subsumption_resolution,[],[f10,f7])).
+fof(f7,plain,(
+  ~mortal(socrates)),
+  inference(cnf_transformation,[],[f5])).
+fof(f5,plain,(
+  ~mortal(socrates)),
+  inference(flattening,[],[f2])).
+fof(f2,negated_conjecture,(
+  ~mortal(socrates)),
+  inference(negated_conjecture,[],[f1])).
+fof(f1,conjecture,(
+  mortal(socrates)),
+  file(unknown,unknown)).
+fof(f10,plain,(
+  mortal(socrates)),
+  inference(resolution,[],[f8,f9])).
+fof(f9,plain,(
+  human(socrates)),
+  inference(cnf_transformation,[],[f4])).
+fof(f4,axiom,(
+  human(socrates)),
+  file(unknown,unknown)).
+fof(f8,plain,(
+  ( ! [X0] : (~human(X0) | mortal(X0)) )),
+  inference(cnf_transformation,[],[f6])).
+fof(f6,plain,(
+  ! [X0] : (mortal(X0) | ~human(X0))),
+  inference(ennf_transformation,[],[f3])).
+fof(f3,axiom,(
+  ! [X0] : (human(X0) => mortal(X0))),
+  file(unknown,unknown)).
+% SZS output end Proof for 
diff --git a/test-data/tptp/fof/group-theory.p b/test-data/tptp/fof/group-theory.p
new file mode 100644
--- /dev/null
+++ b/test-data/tptp/fof/group-theory.p
@@ -0,0 +1,5 @@
+fof(0, conjecture, ! [Z]: ! [Y]: mult(Z, Y) = mult(Y, Z)).
+fof(1, axiom, ! [Y]: mult(e, Y) = Y).
+fof(2, axiom, ! [Y]: mult(inverse(Y), Y) = e).
+fof(3, axiom, ! [P]: ! [Z]: ! [Y]: mult(mult(P, Z), Y) = mult(P, mult(Z, Y))).
+fof(4, axiom, ! [Y]: mult(Y, Y) = e).
diff --git a/test-data/tptp/fof/syllogism.p b/test-data/tptp/fof/syllogism.p
new file mode 100644
--- /dev/null
+++ b/test-data/tptp/fof/syllogism.p
@@ -0,0 +1,3 @@
+fof(0, conjecture, mortal(socrates)).
+fof(1, axiom, ! [Y]: (human(Y) => mortal(Y))).
+fof(2, axiom, human(socrates)).
diff --git a/test/QuickCheckSpec/ArbitrarilyPretty.hs b/test/QuickCheckSpec/ArbitrarilyPretty.hs
new file mode 100644
--- /dev/null
+++ b/test/QuickCheckSpec/ArbitrarilyPretty.hs
@@ -0,0 +1,333 @@
+{-# LANGUAGE DeriveFunctor, DeriveTraversable, DeriveFoldable #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE CPP #-}
+
+-- |
+-- Module       : ArbitrarilyPretty
+-- Description  : Generators for randomized pretty outputs of TPTP expressions.
+-- Copyright    : (c) Evgenii Kotelnikov, 2020
+-- License      : GPL-3
+-- Maintainer   : evgeny.kotelnikov@gmail.com
+-- Stability    : experimental
+--
+-- Defines a class 'ArbitrarilyPretty' used for randomized pretty printing along
+-- with instances of this class implementing substandard ways to pretty print
+-- a TPTP expression.
+--
+
+module ArbitrarilyPretty (
+  ArbitrarilyPretty(..),
+  SuperfluousParenthesis(..),
+  randomSplit,
+  randomTree
+) where
+
+import Data.List.NonEmpty (NonEmpty(..))
+import qualified Data.List.NonEmpty as NEL (splitAt, fromList, length)
+
+#if MIN_VERSION_base(4, 8, 0)
+import Prelude hiding ((<$>), (<*>))
+#else
+import Prelude hiding (mapM)
+import Data.Foldable (Foldable)
+import Data.Traversable (Traversable, mapM)
+import Data.Monoid (mempty)
+#endif
+
+import qualified Data.Foldable as F (toList)
+import Data.List (genericReplicate, intersperse)
+import Data.Maybe (maybeToList)
+import Data.Text (Text)
+
+#if !MIN_VERSION_base(4, 11, 0)
+import Data.Semigroup ((<>))
+#endif
+
+import Control.Applicative ((<$>), (<*>))
+
+import Test.QuickCheck (Gen, choose, frequency)
+
+import Data.Text.Prettyprint.Doc (
+    Doc, (<+>), parens, brackets, punctuate, surround, hsep, space, comma
+  )
+
+import Data.TPTP
+import Data.TPTP.Pretty
+
+
+-- | The class whose instances provide various ways of randomly pretty print
+-- an expression.
+class ArbitrarilyPretty e where
+  apretty :: forall a. e -> Gen (Doc a)
+
+
+-- * Helpers
+
+(&) :: (a -> b) -> (b -> c) -> a -> c
+(&) = flip (.)
+
+-- | Randomply split a non-empty list into two lists.
+randomSplit :: NonEmpty a -> Gen ([a], NonEmpty a)
+randomSplit lst = do
+  index <- choose (0, NEL.length lst - 1)
+  let (prefix, suffix) = NEL.splitAt index lst
+  return (prefix, NEL.fromList suffix)
+
+-- | Randomly split a non-empty list into a binary tree such that collecting
+-- the leafs of that tree from left to right results in the original list.
+--
+-- This splitting is used to generate randomly nested disjunctions with
+-- superfluous parenthesis compared to an equivalent clause.
+randomTree :: NonEmpty a -> Gen (BinTree a)
+randomTree = \case
+  a :| [] -> return (Leaf a)
+  a :| a' : as -> do
+    (prefix, suffix) <- randomSplit (a' :| as)
+    Fork <$> randomTree (a :| prefix) <*> randomTree suffix
+
+star, arrow, tType, colon, negation :: Text
+star = "*"
+arrow = ">"
+tType = "$tType"
+colon = ":"
+negation = "~"
+
+
+-- * Superfluous parenthesis
+
+-- | An auxiliary wrapper used to generate pretty printed TPTP expressions
+-- with superfluous parenthesis.
+newtype SuperfluousParenthesis a = SuperfluousParenthesis {
+  unSuperfluousParenthesis :: a
+} deriving (Eq, Show, Ord, Functor, Traversable, Foldable)
+
+-- | Randomly pretty print a TPTP expression with superflouous parenthesis
+-- somewhere inside the expression but not on the outer level.
+sppretty :: ArbitrarilyPretty (SuperfluousParenthesis e)
+         => e -> forall a. Gen (Doc a)
+sppretty = apretty . SuperfluousParenthesis
+
+-- | Map a given 'Doc' generator to a one that randomly wraps the document
+-- in zero, one or two pairs of parenthesis.
+superfluousParenthesis :: Gen (Doc a) -> Gen (Doc a)
+superfluousParenthesis g = frequency [
+    (2, g),
+    (2, parens <$> g),
+    (1, parens . parens <$> g)
+  ]
+
+
+-- ** SuperfluousParenthesis instances for common types
+
+instance (ArbitrarilyPretty (SuperfluousParenthesis a),
+          ArbitrarilyPretty (SuperfluousParenthesis b)) =>
+          ArbitrarilyPretty (SuperfluousParenthesis (Either a b)) where
+  apretty = either sppretty sppretty . unSuperfluousParenthesis
+
+instance ArbitrarilyPretty (SuperfluousParenthesis Text) where
+  apretty = return . pretty . unSuperfluousParenthesis
+
+
+-- ** Auxiliary data types and their SuperfluousParenthesis instances
+
+-- | An auxiliary wrapper used to pretty print applications of function and
+-- predicate symbols with superfluous parenthesis.
+data Application s e = Application_ s [e]
+  deriving (Eq, Ord, Show)
+
+-- | Pretty print an application of a symbol to a list of arguments.
+application :: Pretty f => f -> [Doc a] -> Doc a
+application f [] = pretty f
+application f as = pretty f <> parens (hsep (punctuate comma as))
+
+instance (ArbitrarilyPretty (SuperfluousParenthesis e), Pretty s) =>
+          ArbitrarilyPretty (SuperfluousParenthesis (Application s e)) where
+  apretty = unSuperfluousParenthesis & \case
+    Application_ s ts -> application s
+                     <$> mapM (superfluousParenthesis . sppretty) ts
+
+-- | An auxiliary wrapper used to pretty print applications of infix operators
+-- with superfluous parenthesis.
+data Infix e o = Infix o e e
+  deriving (Eq, Ord, Show)
+
+instance (ArbitrarilyPretty (SuperfluousParenthesis e), Pretty o) =>
+          ArbitrarilyPretty (SuperfluousParenthesis (Infix e o)) where
+  apretty = unSuperfluousParenthesis & \case
+    Infix o a b -> surround (space <> pretty o <> space)
+               <$> superfluousParenthesis (sppretty a)
+               <*> superfluousParenthesis (sppretty b)
+
+-- | An auxiliary wrapper used to pretty print applications of prefix operators
+-- with superfluous parenthesis.
+data Prefix e o = Prefix o e
+  deriving (Eq, Ord, Show)
+
+instance (ArbitrarilyPretty (SuperfluousParenthesis e), Pretty o) =>
+          ArbitrarilyPretty (SuperfluousParenthesis (Prefix e o)) where
+  apretty = unSuperfluousParenthesis & \case
+    Prefix o e -> (pretty o <+>) <$> superfluousParenthesis (sppretty e)
+
+-- | An auxiliary wrapper used to pretty print expressions with superfluous
+-- parenthesis with a condition that mandates at least one pair of parenthesis.
+data ParensUnless e = ParensUnless Bool e
+  deriving (Show, Eq, Ord)
+
+instance ArbitrarilyPretty (SuperfluousParenthesis e) =>
+         ArbitrarilyPretty (SuperfluousParenthesis (ParensUnless e)) where
+  apretty = unSuperfluousParenthesis & \case
+    ParensUnless p e -> if p then sppretty e else parens <$> sppretty e
+
+-- | An auxiliary data structure used to pretty print a binary tree of disjunctions.
+data BinTree t
+  = Leaf t
+  | Fork (BinTree t) (BinTree t)
+  deriving (Eq, Ord, Show, Functor, Traversable, Foldable)
+
+instance ArbitrarilyPretty (SuperfluousParenthesis l) =>
+         ArbitrarilyPretty (SuperfluousParenthesis (BinTree l)) where
+  apretty = unSuperfluousParenthesis & \case
+    Leaf   l -> sppretty l
+    Fork a b -> sppretty (Infix Disjunction a b)
+
+-- | An auxiliary wrapper used to pretty print a typing of a symbol or a variable
+-- with superfluous parenthesis around the type.
+data Typing a t = Typing_ a t
+  deriving (Eq, Show, Ord)
+
+instance (ArbitrarilyPretty (SuperfluousParenthesis t), Pretty a) =>
+          ArbitrarilyPretty (SuperfluousParenthesis (Typing a t)) where
+  apretty = unSuperfluousParenthesis & \case
+    Typing_ a t -> (pretty a <>) <$> sppretty (Prefix colon t)
+
+-- | An auxiliary wrapper used to pretty print a mapping type with superfluous
+-- parenthesis around the argument type and the return type.
+data Mapping s = Mapping [s] s
+  deriving (Eq, Show, Ord, Functor, Traversable, Foldable)
+
+instance ArbitrarilyPretty (SuperfluousParenthesis s) =>
+         ArbitrarilyPretty (SuperfluousParenthesis (Mapping s)) where
+  apretty = unSuperfluousParenthesis & \case
+    Mapping [] s -> sppretty s
+    m -> do
+      Mapping as s <- mapM (superfluousParenthesis . sppretty) m
+      let starSeparated = hsep . intersperse (pretty star)
+      return (parens (starSeparated as) <+> pretty arrow <+> s)
+
+
+-- ** First-order logic
+
+instance ArbitrarilyPretty (SuperfluousParenthesis Term) where
+  apretty = unSuperfluousParenthesis & \case
+    Function  f ts -> sppretty (Application_ f ts)
+    Variable     v -> return (pretty v)
+    Number       i -> return (pretty i)
+    DistinctTerm d -> return (pretty d)
+
+instance ArbitrarilyPretty (SuperfluousParenthesis Literal) where
+  apretty = unSuperfluousParenthesis & \case
+    Predicate p ts -> sppretty (Application_ p ts)
+    Equality a s b -> sppretty (Infix s a b)
+
+instance ArbitrarilyPretty (SuperfluousParenthesis (Sign, Literal)) where
+  apretty = unSuperfluousParenthesis & \case
+    (Positive, l) -> sppretty l
+    (Negative, l) -> sppretty (Prefix negation l)
+
+instance ArbitrarilyPretty (SuperfluousParenthesis Clause) where
+  apretty = unSuperfluousParenthesis & \case
+    Clause ls -> randomTree ls >>= sppretty
+
+unitary :: FirstOrder s -> Bool
+unitary = \case
+  Atomic{}     -> True
+  Negated{}    -> True
+  Quantified{} -> True
+  Connected{}  -> False
+
+under :: Connective -> FirstOrder s -> Bool
+under c = \case
+  Connected _ c' _ -> c' == c && isAssociative c
+  f -> unitary f
+
+instance ArbitrarilyPretty (SuperfluousParenthesis s) =>
+         ArbitrarilyPretty (SuperfluousParenthesis (FirstOrder s)) where
+  apretty = unSuperfluousParenthesis & \case
+    Atomic  l -> sppretty l
+    Negated g -> sppretty (Prefix negation (ParensUnless (unitary g) g))
+    Connected g c h -> sppretty (Infix c (ParensUnless (under c g) g)
+                                         (ParensUnless (under c h) h))
+    Quantified q vs g -> do
+      let var (v, s) = (pretty v <>) <$> sppretty s
+      vs' <- mapM var (F.toList vs)
+      g' <- sppretty (Prefix colon (ParensUnless (unitary g) g))
+      return (pretty q <+> brackets (hsep (punctuate comma vs')) <> g')
+
+
+-- ** Sorts and types
+
+instance ArbitrarilyPretty (SuperfluousParenthesis Unsorted) where
+  apretty = return . pretty . unSuperfluousParenthesis
+
+instance ArbitrarilyPretty (SuperfluousParenthesis s) =>
+         ArbitrarilyPretty (SuperfluousParenthesis (Sorted s)) where
+  apretty = unSuperfluousParenthesis & \case
+    Sorted Nothing  -> return mempty
+    Sorted (Just s) -> sppretty (Prefix colon s)
+
+instance ArbitrarilyPretty (SuperfluousParenthesis (Name Sort)) where
+  apretty = return . pretty . unSuperfluousParenthesis
+
+instance ArbitrarilyPretty (SuperfluousParenthesis QuantifiedSort) where
+  apretty = return . pretty . unSuperfluousParenthesis
+
+instance ArbitrarilyPretty (SuperfluousParenthesis TFF1Sort) where
+  apretty = unSuperfluousParenthesis & \case
+    SortVariable v -> return (pretty v)
+    TFF1Sort  f ss -> sppretty (Application_ f ss)
+
+instance ArbitrarilyPretty (SuperfluousParenthesis Type) where
+  apretty = unSuperfluousParenthesis & \case
+    Type        as r -> sppretty (Mapping as r)
+    TFF1Type [] as r -> sppretty (Mapping as r)
+    TFF1Type vs as r -> do
+      vs' <- mapM sppretty (fmap (flip Typing_ tType) vs)
+      t' <- sppretty (Prefix colon (ParensUnless (null as) (TFF1Type [] as r)))
+      return ("!>" <+> brackets (hsep (punctuate comma vs')) <> t')
+
+
+-- ** Units
+
+instance ArbitrarilyPretty (SuperfluousParenthesis Formula) where
+  apretty = unSuperfluousParenthesis & \case
+    CNF  c -> sppretty c
+    FOF  g -> sppretty g
+    TFF0 g -> sppretty g
+    TFF1 g -> sppretty g
+
+instance ArbitrarilyPretty (SuperfluousParenthesis Declaration) where
+  apretty = unSuperfluousParenthesis & \case
+    Formula _ f -> sppretty f
+    Typing  s t -> sppretty (Typing_ s t)
+    Sort    s n -> sppretty (Typing_ s (Mapping (genericReplicate n tType) tType))
+
+instance ArbitrarilyPretty (SuperfluousParenthesis Unit) where
+  apretty = unSuperfluousParenthesis & \case
+    i@Include{} -> return (pretty i)
+    Unit nm decl a -> do
+      decl' <- superfluousParenthesis (sppretty decl)
+      let args = pretty nm : prettyRole decl : decl' : ann
+      return (application (declarationLanguage decl) args <> ".")
+      where
+        prettyRole = \case
+          Sort{}      -> "type"
+          Typing{}    -> "type"
+          Formula r _ -> pretty (name r)
+
+        ann = case a of
+          Just (s, i) -> pretty s : maybeToList (fmap prettyList i)
+          Nothing -> []
diff --git a/test/QuickCheckSpec/Generators.hs b/test/QuickCheckSpec/Generators.hs
--- a/test/QuickCheckSpec/Generators.hs
+++ b/test/QuickCheckSpec/Generators.hs
@@ -204,7 +204,7 @@
 
 deriving instance Generic Unit
 instance Arbitrary Unit where
-  arbitrary = genericArbitraryU
+  arbitrary = genericArbitraryRec (1 % 10 % ())
   shrink = \case
     Include f ns -> Include f <$> shrink ns
     Unit   n d a -> Unit    n <$> shrink d <*> shrinkAnnotation a
diff --git a/test/QuickCheckSpec/Main.hs b/test/QuickCheckSpec/Main.hs
--- a/test/QuickCheckSpec/Main.hs
+++ b/test/QuickCheckSpec/Main.hs
@@ -1,5 +1,8 @@
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE CPP #-}
 
 -- |
@@ -20,40 +23,90 @@
 #endif
 
 import Control.Applicative ((<*))
+import Control.Monad (unless)
+import Data.Foldable (toList)
+import Data.List.NonEmpty (NonEmpty)
+import qualified Data.List.NonEmpty as NEL (cons)
+import Data.Text (Text)
 
 import Data.Attoparsec.Text (Parser, parseOnly, endOfInput)
-import Data.Text.Prettyprint.Doc (layoutPretty, defaultLayoutOptions)
+import Data.Text.Prettyprint.Doc (Doc, layoutPretty, defaultLayoutOptions)
 import Data.Text.Prettyprint.Doc.Render.Text (renderStrict)
-import Test.QuickCheck (Property, Args(..), stdArgs, (===), whenFail,
-                        forAllProperties, quickCheckWithResult)
+import Test.QuickCheck (Gen, Property, Args(..), stdArgs, (===), whenFail,
+                        forAll, forAllProperties, quickCheckWithResult)
+import Test.QuickCheck.Poly (A)
 
+import System.Exit (exitFailure)
+
 import Data.TPTP hiding (clause)
 import Data.TPTP.Parse.Combinators
 import Data.TPTP.Pretty
 
+import ArbitrarilyPretty
 import Generators ()
 import Normalizers
 
+
 -- * Helper functions
 
--- | Idempotent parsing / pretty printing modulo normalization
-ippModulo :: (Show a, Eq a, Pretty a) => (a -> a) -> Parser a -> a -> Property
-ippModulo normalize p a =
-  whenFail (print t) $ case parseOnly (p <* endOfInput) t of
-    Left err -> whenFail (putStrLn $ "Parsing error: " ++ err) False
-    Right a' -> normalize a' === normalize a
-  where
-    t = renderStrict $ layoutPretty defaultLayoutOptions (pretty a)
+-- | Generalized idempotent parsing / pretty printing.
+ippWith :: (Show e, Show e', Eq e')
+        => (e -> Gen (Doc a))  -- ^ Pretty printer.
+        -> (Doc a -> Gen Text) -- ^ Renderer.
+        -> Parser e            -- ^ Parser.
+        -> (e -> e')           -- ^ Normalizer.
+        -> e -> Property
+ippWith pprint render parse normalize expr =
+  forAll (pprint expr) $ \doc  ->
+  forAll (render doc)  $ \text ->
+    case parseOnly (parse <* endOfInput) text of
+      Left err    -> whenFail (putStrLn $ "Parsing error: " ++ err) False
+      Right expr' -> normalize expr' === normalize expr
 
--- | Idempotent parsing / pretty printing
-ipp :: (Show a, Eq a, Pretty a) => Parser a -> a -> Property
-ipp = ippModulo id
+defaultRender :: Doc a -> Gen Text
+defaultRender = return . renderStrict . layoutPretty defaultLayoutOptions
 
+defaultNormalize :: e -> e
+defaultNormalize = id
 
+-- | Idempotent parsing / pretty printing modulo normalization.
+ippModulo :: (Show e, Eq e, Pretty e) => (e -> e) -> Parser e -> e -> Property
+ippModulo = flip $ ippWith (return . pretty) defaultRender
+
+-- | Idempotent parsing / pretty printing.
+ipp :: (Show e, Eq e, Pretty e) => Parser e -> e -> Property
+ipp = ippModulo defaultNormalize
+
+-- | Idempotent arbitrary parsing / pretty printing modulo normalization.
+aippModulo :: (Show e, Eq e, ArbitrarilyPretty e, Show e', Eq e')
+           => (e -> e') -> Parser e -> e -> Property
+aippModulo = flip $ ippWith apretty defaultRender
+
+-- | Idempotent parsing / pretty printing.
+aipp :: (Show e, Eq e, ArbitrarilyPretty e) => Parser e -> e -> Property
+aipp = aippModulo defaultNormalize
+
+-- | Idempotent parsing / pretty printing with superfluous parenthesis
+-- modulo normalization.
+spAippModulo :: (Show e, Eq e, ArbitrarilyPretty (SuperfluousParenthesis e))
+             => (e -> e) -> Parser e -> e -> Property
+spAippModulo normalize parser expr =
+  aippModulo (normalize . unSuperfluousParenthesis)
+             (fmap SuperfluousParenthesis parser)
+             (SuperfluousParenthesis expr)
+
+-- | Idempotent parsing / pretty printing with superfluous parenthesis.
+spAipp :: (Show e, Eq e, ArbitrarilyPretty (SuperfluousParenthesis e))
+       => Parser e -> e -> Property
+spAipp = spAippModulo defaultNormalize
+
+
 -- * Properties
 
 -- ** Generators
 
+-- *** Well-formed names
+
 prop_validAtom :: Atom -> Bool
 prop_validAtom (Atom t) = isValidAtom t
 
@@ -63,7 +116,19 @@
 prop_validDistinctObject :: DistinctObject -> Bool
 prop_validDistinctObject (DistinctObject t) = isValidDistinctObject t
 
+-- *** Auxiliary data structures
 
+prop_randomSplit :: NonEmpty A -> Property
+prop_randomSplit list = forAll (randomSplit list)
+                      $ \(prefix, suffix) -> appendr prefix suffix === list
+  where
+    appendr l nel = foldr NEL.cons nel l
+
+prop_randomTree :: NonEmpty A -> Property
+prop_randomTree list = forAll (randomTree list)
+                     $ \tree -> toList tree === toList list
+
+
 -- ** Names
 
 prop_ipp_Atom :: Atom -> Property
@@ -90,10 +155,16 @@
 prop_ipp_TFF1Sort :: TFF1Sort -> Property
 prop_ipp_TFF1Sort = ipp tff1Sort
 
+prop_ipp_sp_TFF1Sort :: TFF1Sort -> Property
+prop_ipp_sp_TFF1Sort = spAipp tff1Sort
+
 prop_ipp_Type :: Type -> Property
 prop_ipp_Type = ippModulo normalizeType type_
 
+prop_ipp_sp_Type :: Type -> Property
+prop_ipp_sp_Type = spAippModulo normalizeType type_
 
+
 -- ** First-order logic
 
 prop_ipp_Number :: Number -> Property
@@ -102,27 +173,48 @@
 prop_ipp_Term :: Term -> Property
 prop_ipp_Term = ipp term
 
+prop_ipp_sp_Term :: Term -> Property
+prop_ipp_sp_Term = spAipp term
+
 prop_ipp_Literal :: Literal -> Property
 prop_ipp_Literal = ipp literal
 
+prop_ipp_sp_Literal :: Literal -> Property
+prop_ipp_sp_Literal = spAipp literal
+
 prop_ipp_Clause :: Clause -> Property
 prop_ipp_Clause = ipp clause
 
+prop_ipp_sp_Clause :: Clause -> Property
+prop_ipp_sp_Clause = spAipp clause
+
 prop_ipp_UnsortedFO :: UnsortedFirstOrder -> Property
 prop_ipp_UnsortedFO = ippModulo reassociate unsortedFirstOrder
 
+prop_ipp_sp_UnsortedFO :: UnsortedFirstOrder -> Property
+prop_ipp_sp_UnsortedFO = spAippModulo reassociate unsortedFirstOrder
+
 prop_ipp_MonomorphicFO :: MonomorphicFirstOrder -> Property
 prop_ipp_MonomorphicFO = ippModulo reassociate monomorphicFirstOrder
 
+prop_ipp_sp_MonomorphicFO :: MonomorphicFirstOrder -> Property
+prop_ipp_sp_MonomorphicFO = spAippModulo reassociate monomorphicFirstOrder
+
 prop_ipp_PolymorphicFO :: PolymorphicFirstOrder -> Property
 prop_ipp_PolymorphicFO = ippModulo reassociate polymorphicFirstOrder
 
+prop_ipp_sp_PolymorphicFO :: PolymorphicFirstOrder -> Property
+prop_ipp_sp_PolymorphicFO = spAippModulo reassociate polymorphicFirstOrder
 
+
 -- ** Units
 
 prop_ipp_Unit :: Unit -> Property
 prop_ipp_Unit = ippModulo normalizeUnit unit
 
+prop_ipp_sp_Unit :: Unit -> Property
+prop_ipp_sp_Unit = spAippModulo normalizeUnit unit
+
 prop_ipp_TPTP :: TPTP -> Property
 prop_ipp_TPTP = ippModulo normalizeTPTP tptp
 
@@ -146,5 +238,8 @@
 
 return []
 
-main :: IO Bool
-main = $forAllProperties $ quickCheckWithResult stdArgs{maxSuccess=1000}
+main :: IO ()
+main = do
+  success <- $forAllProperties $ quickCheckWithResult stdArgs{maxSuccess=1000}
+  unless success exitFailure
+
diff --git a/test/UnitTests.hs b/test/UnitTests.hs
--- a/test/UnitTests.hs
+++ b/test/UnitTests.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TupleSections #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE CPP #-}
 
 -- |
@@ -13,59 +14,81 @@
 
 module UnitTests (tests) where
 
-import Distribution.TestSuite (Test(..), TestInstance(..),
-                               Progress(..), Result(..))
-
-import System.Directory (listDirectory)
-
+import Control.Monad.Extra (concatMapM)
 #if !MIN_VERSION_base(4, 8, 0)
 import Data.Functor ((<$>))
 #endif
-
 import Data.Text (Text)
 import qualified Data.Text.IO as Text.IO (readFile)
-import Data.List (intercalate)
-import Control.Monad.Extra (concatMapM)
 
-import Data.TPTP.Parse.Text
+import System.Directory (listDirectory)
+import System.FilePath.Posix (joinPath, (</>))
 
+import Distribution.TestSuite (Test(..), TestInstance(..),
+                               Progress(..), Result(..))
+
+import Data.TPTP (TPTP(..), TSTP(..), SZS(..))
+import Data.TPTP.Parse.Text (parseTPTPOnly, parseTSTPOnly)
+
+
 testDataDir :: FilePath
 testDataDir = "test-data"
 
 listTestDirectory :: FilePath -> IO [FilePath]
-listTestDirectory d = listDirectory (testDataDir ++ "/" ++ d)
+listTestDirectory d = listDirectory (testDataDir </> d)
 
 readTestFile :: FilePath -> IO Text
-readTestFile f = Text.IO.readFile (testDataDir ++ "/" ++ f)
+readTestFile f = Text.IO.readFile (testDataDir </> f)
 
-parseFile :: FilePath -> IO Result
-parseFile path = buildResult . parseTSTPOnly <$> readTestFile path
+testParsingTPTP :: FilePath -> IO Result
+testParsingTPTP path = buildResult . parseTPTPOnly <$> readTestFile path
   where
-    buildResult (Left e)  = Error e
-    buildResult (Right _) = Pass
+    buildResult = \case
+      Left e -> Error e
+      Right (TPTP []) -> Error "empty list of parsed units"
+      Right _ -> Pass
 
+testParsingTSTP :: FilePath -> IO Result
+testParsingTSTP path = buildResult . parseTSTPOnly <$> readTestFile path
+  where
+    buildResult = \case
+      Left e -> Error e
+      Right (TSTP _ []) -> Error "empty list of parsed units"
+      Right (TSTP (SZS (Just _) (Just _)) _) -> Pass
+      Right (TSTP _ _) -> Error "failed to parse SZS ontology"
+
 type TestCase = (FilePath, FilePath, FilePath)
 
+testCasePath :: TestCase -> FilePath
+testCasePath (space, lang, file) = joinPath [space, lang, file]
+
+runTestCase :: (FilePath, FilePath, FilePath) -> IO Result
+runTestCase testCase@(space, _, _) = test (testCasePath testCase)
+  where
+    test = case space of
+      "szs" -> testParsingTSTP
+      _     -> testParsingTPTP
+
 testFile :: TestCase -> Test
-testFile (space, lang, file) = Test $ TestInstance {
-  run = Finished <$> parseFile path,
-  name = path,
-  tags = [space, lang],
-  options = [],
+testFile testCase@(space, lang, _) = Test $ TestInstance {
+  run       = Finished <$> runTestCase testCase,
+  name      = testCasePath testCase,
+  tags      = [space, lang],
+  options   = [],
   setOption = const . const $ Left "not supported"
-} where path = intercalate "/" [space, lang, file]
+}
 
 listSpaces :: IO [FilePath]
-listSpaces = listTestDirectory ""
+listSpaces = listDirectory testDataDir
 
 listLangs :: FilePath -> IO [(FilePath, FilePath)]
 listLangs s = fmap (s,) <$> listTestDirectory s
 
 listFiles :: (FilePath, FilePath) -> IO [(FilePath, FilePath, FilePath)]
-listFiles (s, l) = fmap (s, l,) <$> listTestDirectory (s ++ "/" ++ l)
+listFiles (s, l) = fmap (s, l,) <$> listTestDirectory (s </> l)
 
 cases :: IO [TestCase]
 cases = listSpaces >>= concatMapM listLangs >>= concatMapM listFiles
 
 tests :: IO [Test]
-tests =  fmap testFile <$> cases
+tests = fmap testFile <$> cases
diff --git a/tptp.cabal b/tptp.cabal
--- a/tptp.cabal
+++ b/tptp.cabal
@@ -1,7 +1,7 @@
 cabal-version: 2.4
 name: tptp
-version: 0.1.1.0
-synopsis: A parser and a pretty printer for the TPTP language
+version: 0.1.2.0
+synopsis: Parser and 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
@@ -10,7 +10,7 @@
   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.
+  CNF, FOF, TFF0 and TFF1 subsets of TPTP.
 homepage: https://github.com/aztek/tptp
 bug-reports: https://github.com/aztek/tptp/issues
 license: GPL-3.0-only
@@ -25,7 +25,8 @@
   GHC == 8.2.2,
   GHC == 8.4.4,
   GHC == 8.6.5,
-  GHC == 8.8.1
+  GHC == 8.8.3,
+  GHC == 8.10.1
 
 extra-source-files:
   CHANGELOG.md
@@ -59,16 +60,16 @@
   if flag(Werror)
     ghc-options: -Werror
   build-depends:
-    base          >= 4.5    && < 5.0,
+    base          >= 4.7    && < 5.0,
     text          >= 1.2.3  && < 1.3,
     attoparsec    >= 0.13.2 && < 0.14,
-    scientific    >= 0.3.6  && < 0.4,
+    scientific    >= 0.3.1  && < 0.4,
     prettyprinter >= 1.2.1  && < 1.5
   if impl(ghc < 8)
     ghc-options:
       -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns
     build-depends:
-      semigroups  >= 0.16.1 && < 0.19
+      semigroups  >= 0.16.1 && < 1.0
   if impl(ghc >= 8)
     ghc-options:
       -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns
@@ -80,6 +81,7 @@
   default-language: Haskell2010
   main-is: Main.hs
   other-modules:
+    ArbitrarilyPretty
     Generators
     Normalizers
   ghc-options:
@@ -121,6 +123,7 @@
     Cabal     >= 1.16.0,
     extra     >= 1.4.4 && < 1.7,
     directory >= 1.2.5 && < 1.4,
+    filepath  >= 1.3   && < 1.5,
     tptp
 
 test-suite doctests