module Data.Logic.ATP
    ( module Data.Logic.ATP.Lib
    , module Data.Logic.ATP.Pretty
    , module Data.Logic.ATP.Formulas
    , module Data.Logic.ATP.Lit
    , module Data.Logic.ATP.Prop
    , module Data.Logic.ATP.PropExamples
    , module Data.Logic.ATP.DefCNF
    , module Data.Logic.ATP.DP
    , module Data.Logic.ATP.Term
    , module Data.Logic.ATP.Apply
    , module Data.Logic.ATP.Equate
    , module Data.Logic.ATP.Quantified
    , module Data.Logic.ATP.Parser
    , module Data.Logic.ATP.FOL
    , module Data.Logic.ATP.Skolem
    , module Data.Logic.ATP.Herbrand
    , module Data.Logic.ATP.Unif
    , module Data.Logic.ATP.Tableaux
    , module Data.Logic.ATP.Resolution
    , module Data.Logic.ATP.Prolog
    , module Data.Logic.ATP.Meson
    , module Data.Logic.ATP.Equal
    , module Text.PrettyPrint.HughesPJClass
    , module Test.HUnit
    ) where

import Data.String ({-instances-})
import Text.PrettyPrint.HughesPJClass hiding ((<>))

import Data.Logic.ATP.Lib
import Data.Logic.ATP.Pretty
import Data.Logic.ATP.Formulas
import Data.Logic.ATP.Lit hiding (Atom, T, F, Not)
import Data.Logic.ATP.Prop hiding (Atom, nnf, T, F, Not, And, Or, Imp, Iff)
import Data.Logic.ATP.PropExamples hiding (K)
import Data.Logic.ATP.DefCNF
import Data.Logic.ATP.DP
import Data.Logic.ATP.Term
import Data.Logic.ATP.Apply
import Data.Logic.ATP.Equate
import Data.Logic.ATP.Quantified
import Data.Logic.ATP.Parser
import Data.Logic.ATP.FOL
import Data.Logic.ATP.Skolem
import Data.Logic.ATP.Herbrand
import Data.Logic.ATP.Unif
import Data.Logic.ATP.Tableaux hiding (K)
import Data.Logic.ATP.Resolution
import Data.Logic.ATP.Prolog
import Data.Logic.ATP.Meson
import Data.Logic.ATP.Equal
import Test.HUnit