{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, MonoLocalBinds, NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies  #-}
{-# OPTIONS -fno-warn-name-shadowing -fno-warn-missing-signatures #-}
module Data.Logic.Tests.Data
    ( tests
    , allFormulas
    , proofs
{-
    , formulas
    , animalKB
    , animalConjectures
    , chang43KB
    , chang43Conjecture
    , chang43ConjectureRenamed
-}
    ) where

import Data.Boolean.SatSolver (Literal(..))
--import Data.Generics (Data, Typeable)
import Data.Logic.Classes.Combine (Combinable(..))
import Data.Logic.Classes.Constants (Constants(..))
import Data.Logic.Classes.Equals (AtomEq, (.=.), pApp, pApp2)
import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), for_all', exists')
import Data.Logic.Classes.Negate ((.~.))
import Data.Logic.Classes.Term (Term(..))
import Data.Logic.Classes.Skolem (Skolem(toSkolem))
--import Data.Logic.Classes.Negate (Negatable(..))
--import qualified Data.Logic.Classes.Literal as N
import qualified Data.Logic.Instances.Chiou as C
import Data.Logic.KnowledgeBase (WithId(WithId, wiItem, wiIdent), Proof(..), ProofResult(..))
import Data.Logic.Normal.Implicative (ImplicativeForm(INF), makeINF')
import Data.Logic.Tests.Common (TestFormula(..), TestProof(..), Expected(..), ProofExpected(..), doTest, doProof,
                                TFormula, TAtom, TTerm, V, Pr, AtomicFunction, TTestFormula, TTestProof)
--import Data.Logic.Types.FirstOrder (Predicate(..), PTerm(..))
import Data.Map (fromList)
import qualified Data.Set as S
import Data.String (IsString)
import Test.HUnit

{-
:m +Data.Logic.Test
:m +Data.Logic.Types.FirstOrder
:m +Data.Set
runNormal (clauseNormalForm (true :: Formula V Pr AtomicFunction)) :: Set (Set (Formula V Pr AtomicFunction))
runNormal (skolemNormalForm (true :: Formula V Pr AtomicFunction)) :: Formula V Pr AtomicFunction
:m +Data.Logic.Normal.Prenex
prenexNormalForm true :: Formula V Pr AtomicFunction
:m +Data.Logic.Normal.Skolem
:m +Data.Logic.Normal.Negation
-}

tests :: [TTestFormula] -> [TTestProof] -> Test
tests fs ps =
    TestLabel "Test.Data" $ TestList (map doTest fs ++ map doProof ps)

allFormulas :: [TTestFormula]
allFormulas = (formulas ++
               concatMap snd [animalKB, chang43KB] ++
               animalConjectures ++
               [chang43Conjecture, chang43ConjectureRenamed])

formulas :: [TTestFormula]
formulas =
    let n = (.~.)
        p = pApp "p"
        q = pApp "q"
        r = pApp "r"
        s = pApp "s"
        t = pApp "t"
        p0 = p []
        q0 = q []
        r0 = r []
        s0 = s []
        t0 = t []
        (x, y, z, u, v, w) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm, vt "w" :: TTerm)
        z2 = vt "z2" :: TTerm in
    
    [ 
      TestFormula
      { formula = p0 .|. q0 .&. r0 .|. n s0 .&. n t0
      , name = "operator precedence"
      , expected = [ FirstOrderFormula (p0 .|. (q0 .&. r0) .|. ((n s0) .&. (n t0))) ] }
    , TestFormula
      { formula = pApp (fromBool True) []
      , name = "True"
      , expected = [ClauseNormalForm  (toSS [])] }
    , TestFormula
      { formula = pApp (fromBool False) []
      , name = "False"
      , expected = [ClauseNormalForm  (toSS [[]])] }
    , TestFormula
      { formula = pApp "p" []
      , name = "p"
      , expected = [ClauseNormalForm  (toSS [[pApp "p" []]])] }
    , let p = pApp "p" [] in
      TestFormula
      { formula = p .&. ((.~.) (p))
      , name = "p&~p"
      , expected = [ PrenexNormalForm ((pApp ("p") []) .&. (((.~.) (pApp ("p") []))))
                   , ClauseNormalForm (toSS [[(p)], [((.~.) (p))]])
                   ] }
    , TestFormula
      { formula = pApp "p" [vt "x"]
      , name = "p[x]"
      , expected = [ClauseNormalForm  (toSS [[pApp "p" [x]]])] }
    , let f = pApp "f"
          q = pApp "q" in
      TestFormula
      { name = "iff"
      , formula = for_all "x" (for_all "y" (q [x, y] .<=>. for_all "z" (f [z, x] .<=>. f [z, y])))
      , expected = [ PrenexNormalForm
                     (for_all "x"
                      (for_all "y"
                       (for_all "z"
                        (exists "z2"
                         (((((q [x,y])) .&.
                            ((((((f [z,x])) .&.
                                ((f [z,y])))) .|.
                              (((((.~.) (f [z,x]))) .&.
                                (((.~.) (f [z,y]))))))))) .|.
                          (((((.~.) (q [x,y]))) .&.
                            ((((((f [z2,x])) .&.
                                (((.~.) (f [z2,y]))))) .|.
                              (((((.~.) (f [z2,x]))) .&.
                                ((f [z2,y])))))))))))))
                   , ClauseNormalForm 
                     (toSS [[(pApp2 ("f") (vt ("z")) (vt ("x"))),
                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),
                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),
                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y"))))],
                            [(pApp2 ("f") (vt ("z")) (vt ("x"))),
                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y")))),
                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),
                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))],
                            [(pApp2 ("f") (vt ("z")) (vt ("x"))),
                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y")))),
                             ((.~.) (pApp2 ("q") (vt ("x")) (vt ("y"))))],
                            [(pApp2 ("f") (vt ("z")) (vt ("y"))),
                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),
                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),
                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x"))))],
                            [(pApp2 ("f") (vt ("z")) (vt ("y"))),
                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x")))),
                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),
                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))],
                            [(pApp2 ("f") (vt ("z")) (vt ("y"))),
                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x")))),
                             ((.~.) (pApp2 ("q") (vt ("x")) (vt ("y"))))],
                            [(pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),
                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),
                             (pApp2 ("q") (vt ("x")) (vt ("y")))],
                            [(pApp2 ("q") (vt ("x")) (vt ("y"))),
                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),
                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))]])
                   ]
      }
    , TestFormula
      { name = "move quantifiers out"
      , formula = (for_all "x" (pApp "p" [x]) .&. (pApp "q" [x]))
      , expected = [PrenexNormalForm (for_all "x2" ((pApp "p" [vt ("x2")]) .&. ((pApp "q" [vt ("x")]))))]
      }
    , TestFormula
      { name = "skolemize2"
      , formula = exists "x" (for_all "y" (pApp "loves" [x, y]))
      , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem "x") [],y])]
      }
    , TestFormula
      { name = "skolemize3"
      , formula = for_all "y" (exists "x" (pApp "loves" [x, y]))
      , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem "x") [y],y])]
      }
    , TestFormula
      { formula = exists "x" (for_all' ["y", "z"]
                              (exists "u"
                               (for_all "v"
                                (exists "w"
                                 (pApp "P" [x, y, z, u, v, w])))))
      , name = "chang example 4.1"
      , expected = [ SkolemNormalForm (pApp "P" [fApp (toSkolem "x") [],
                                                 vt ("y"),
                                                 vt ("z"),
                                                 fApp (toSkolem "u") [vt ("y"),vt ("z")],
                                                 vt ("v"),
                                                 fApp (toSkolem "w") [vt ("v"), vt ("y"),vt ("z")]]) ]
      }
    , TestFormula
      { name = "chang example 4.2"
      -- ∀x ∃y∃z ~P(x,y) & Q(x,z) | R(x,y,z)
      , formula = for_all "x" (exists' ["y", "z"] (((((.~.) (pApp "P" [x, y])) .&. pApp "Q" [x, z]) .|. pApp "R" [x, y, z])))
      -- ∀x ~P(x,Sk1[x]) | R(x,Sk1[x],Sk2[x]) & Q(x,Sk2[x]) | R(x,Sk1[x],Sk2[x])
      , expected = [ SkolemNormalForm
                     ((((.~.) (pApp ("P") [vt ("x"),vt ("y")])) .&.
                       ((pApp ("Q") [vt ("x"),vt ("z")]))) .|.
                      ((pApp ("R") [vt ("x"),vt ("y"),vt ("z")])))
                   , ClauseNormalForm
                     (toSS 
                      [[((.~.) (pApp ("P") [vt ("x"),vt ("y")])),
                       (pApp ("R") [vt ("x"),vt ("y"),vt ("z")])],
                      [(pApp ("Q") [vt ("x"),vt ("z")]),
                       (pApp ("R") [vt ("x"),vt ("y"),vt ("z")])]]) ]
      }
    , TestFormula
      { formula = n p0 .|. q0 .&. p0 .|. r0 .&. n q0 .&. n r0
      , name = "chang 7.2.1a - unsat"
      , expected = [ SatSolverSat False ] }
    , TestFormula
      { formula = p0 .|. q0 .|. r0 .&. n p0 .&. n q0 .&. n r0 .|. s0 .&. n s0
      , name = "chang 7.2.1b - unsat"
      , expected = [ SatSolverSat False ] }
    , TestFormula
      { formula = p0 .|. q0 .&. q0 .|. r0 .&. r0 .|. s0 .&. n r0 .|. n p0 .&. n s0 .|. n q0 .&. n q0 .|. n r0
      , name = "chang 7.2.1c - unsat"
      , expected = [ SatSolverSat False ] }
    , let q = pApp "q"
          f = pApp "f"
          sk1 = f [fApp (toSkolem "x") [x,x,y,z],y]
          sk2 = f [fApp (toSkolem "x") [x,x,y,z],x] in
      TestFormula
      { name = "distribute bug test"
      , formula = ((((.~.) (q [x,y])) .|.
                    ((((.~.) (sk2)) .|. (sk1)) .&.
                     (((.~.) (sk1)) .|. (sk2)))) .&.
                   ((((sk2) .&.
                      ((.~.) (sk1))) .|. ((sk1) .&.
                      ((.~.) (sk2)))) .|. (q [x,y])))
      , expected = [ClauseNormalForm
                    (toSS
                     [[sk2,sk1,pApp ("q") [x,y]],
                      [sk2,((.~.) (sk1)),((.~.) (q [x,y]))],
                      [sk1,((.~.) (sk2)),((.~.) (q [x,y]))],
                      [q [x,y], ((.~.) sk2),((.~.) sk1)]])]
      }
    , let x = vt "x" :: TTerm
          y = vt "y" :: TTerm
          x' = vt "x" :: C.CTerm V AtomicFunction
          y' = vt "y" :: C.CTerm V AtomicFunction in
      TestFormula
      { name = "convert to Chiou 1"
      , formula = exists "x" (x .=. y)
      , expected = [ConvertToChiou (exists "x" (x' .=. y') :: C.Sentence V Pr AtomicFunction)]
      }
    , let s = pApp "s"
          s' = pApp "s"
          x' = vt "x"
          y' = vt "y" in
      TestFormula
      { name = "convert to Chiou 2"
      , formula = s [fApp ("a") [x, y]]
      , expected = [ConvertToChiou (s' [fApp "a" [x', y']])]
      }
    , let s = pApp "s"
          h = pApp "h"
          m = pApp "m"
          s' = pApp "s"
          h' = pApp "h"
          m' = pApp "m"
          x' = vt "x" in
      TestFormula
      { name = "convert to Chiou 3"
      , formula = for_all "x" (((s [x] .=>. h [x]) .&. (h [x] .=>. m [x])) .=>. (s [x] .=>. m [x]))
      , expected = [ConvertToChiou (for_all "x" (((s' [x'] .=>. h' [x']) .&. (h' [x'] .=>. m' [x'])) .=>. (s' [x'] .=>. m' [x'])))]
      }
    , let taller a b = pApp "taller" [a, b]
          wise a = pApp "wise" [a] in
      TestFormula
      { name = "cnf test 1"
      , formula = for_all "y" (for_all "x" (taller y x .|. wise x) .=>. wise y)
      , expected = [ClauseNormalForm
                    (toSS
                     [[(pApp ("wise") [vt ("y")]),
                       ((.~.) (pApp ("taller") [vt ("y"),fApp (toSkolem "x") [vt ("y")]]))],
                      [(pApp ("wise") [vt ("y")]),
                       ((.~.) (pApp ("wise") [fApp (toSkolem "x") [vt ("y")]]))]])]
      }
    , TestFormula
      { name = "cnf test 2"
      , formula = ((.~.) (exists "x" (pApp "s" [x] .&. pApp "q" [x])))
      , expected = [ ClauseNormalForm (toSS 
                                       [[((.~.) (pApp ("q") [vt ("x")])),
                                         ((.~.) (pApp ("s") [vt ("x")]))]])
                   , PrenexNormalForm (for_all "x"
                                       (((.~.) (pApp ("s") [vt ("x")])) .|.
                                        (((.~.) (pApp ("q") [vt ("x")])))))
                                     {- [[((.~.) (pApp "s" [vt "x"])),
                                        ((.~.) (pApp "q" [vt "x"]))]] -}
                   ]
      }
    , TestFormula
      { name = "cnf test 3"
      , formula = (for_all "x" (p [x] .=>. (q [x] .|. r [x])))
      , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "p" [vt "x"])),(pApp "q" [vt "x"]),(pApp "r" [vt "x"])]])]
      }
    , TestFormula
      { name = "cnf test 4"
      , formula = ((.~.) (exists "x" (p [x] .=>. exists "y" (q [y]))))
      , expected = [ClauseNormalForm (toSS [[(pApp "p" [vt "x"])],[((.~.) (pApp "q" [vt "y"]))]])]
      }
    , TestFormula
      { name = "cnf test 5"
      , formula = (for_all "x" (q [x] .|. r [x] .=>. s [x]))
      , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "q" [vt "x"])),(pApp "s" [vt "x"])],[((.~.) (pApp "r" [vt "x"])),(pApp "s" [vt "x"])]])]
      }
    , TestFormula
      { name = "cnf test 6"
      , formula = (exists "x" (p0 .=>. pApp "f" [x]))
      , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "p" [])),(pApp "f" [fApp (toSkolem "x") []])]])]
      }
    , let p = pApp "p" []
          f' = pApp "f" [x]
          f = pApp "f" [fApp (toSkolem "x") []] in
      TestFormula
      { name = "cnf test 7"
      , formula = exists "x" (p .<=>. f')
      , expected = [ PrenexNormalForm (exists "x" ((p .&. f') .|. ((((.~.) p) .&. (((.~.) f'))))))
                   , SkolemNormalForm ((p .&. f) .|. (((.~.) p) .&. (((.~.) f))))
                   , TrivialClauses [(False,S.fromList [((.~.) (pApp ("p") [])),(pApp ("f") [fApp (toSkolem "x") []])]),
                                     (False,S.fromList [((.~.) (pApp ("f") [fApp (toSkolem "x") []])),(pApp ("p") [])])]
                   , ClauseNormalForm (toSS [[(f), ((.~.) p)], [p, ((.~.) f)]])]
      }
    , TestFormula
      { name = "cnf test 8"
      , formula = (for_all "z" (exists "y" (for_all "x" (pApp "f" [x, y] .<=>. (pApp "f" [x, z] .&. ((.~.) (pApp "f" [x, x])))))))
      , expected = [ClauseNormalForm 
                    (toSS [[((.~.) (pApp "f" [vt "x",fApp (toSkolem "y") [vt "z"]])),(pApp "f" [vt "x",vt "z"])],
                           [((.~.) (pApp "f" [vt "x",fApp (toSkolem "y") [vt "z"]])),((.~.) (pApp "f" [vt "x",vt "x"]))],
                           [((.~.) (pApp "f" [vt "x",vt "z"])),(pApp "f" [vt "x",vt "x"]),(pApp "f" [vt "x",fApp (toSkolem "y") [vt "z"]])]])]
      }
    , let f = pApp "f" 
          q = pApp "q"
          (x, y, z) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm) in
      TestFormula
      { name = "cnf test 9"
      , formula = (for_all "x" (for_all "x" (for_all "y" (q [x, y] .<=>. for_all "z" (f [z, x] .<=>. f [z, y])))))
      , expected = [ClauseNormalForm
                    (toSS
                     [[(pApp2 ("f") (vt ("z")) (vt ("x"))),
                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),
                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),
                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y"))))],
                      [(pApp2 ("f") (vt ("z")) (vt ("x"))),
                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y")))),
                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),
                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))],
                      [(pApp2 ("f") (vt ("z")) (vt ("x"))),
                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y")))),
                       ((.~.) (pApp2 ("q") (vt ("x")) (vt ("y"))))],
                      [(pApp2 ("f") (vt ("z")) (vt ("y"))),
                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),
                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),((.~.) (pApp2 ("f") (vt ("z")) (vt ("x"))))],
                      [(pApp2 ("f") (vt ("z")) (vt ("y"))),
                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x")))),
                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),
                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))],
                      [(pApp2 ("f") (vt ("z")) (vt ("y"))),
                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x")))),
                       ((.~.) (pApp2 ("q") (vt ("x")) (vt ("y"))))],
                      [(pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),
                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),
                       (pApp2 ("q") (vt ("x")) (vt ("y")))],
                      [(pApp2 ("q") (vt ("x")) (vt ("y"))),
                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),
                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))]])
                   ]
      }
    , TestFormula
      { name = "cnf test 10"
      , formula = (for_all "x" (exists "y" ((p [x, y] .<=. for_all "x" (exists "z" (q [y, x, z]) .=>. r [y])))))
      , expected = [ClauseNormalForm
                    (toSS 
                     [[(pApp ("p") [vt ("x"),fApp (toSkolem "y") [vt ("x")]]),
                       (pApp ("q") [fApp (toSkolem "y") [vt "x"],fApp (toSkolem "x2") [vt "x"],fApp (toSkolem "z") [vt "x"]])],
                      [(pApp ("p") [vt ("x"),fApp (toSkolem "y") [vt ("x")]]),
                       ((.~.) (pApp ("r") [fApp (toSkolem "y") [vt "x"]]))]])
                   ]
      }
    , TestFormula
      { name = "cnf test 11"
      , formula = (for_all "x" (for_all "z" (p [x, z] .=>. exists "y" ((.~.) (q [x, y] .|. ((.~.) (r [y, z])))))))
      , expected = [ClauseNormalForm
                    (toSS 
                    [[((.~.) (pApp "p" [vt "x",vt "z"])),((.~.) (pApp "q" [vt "x",fApp (toSkolem "y") [vt "x",vt "z"]]))],
                     [((.~.) (pApp "p" [vt "x",vt "z"])),(pApp "r" [fApp (toSkolem "y") [vt "x",vt "z"],vt "z"])]])]
      }
    , TestFormula
      { name = "cnf test 12"
      , formula = ((p0 .=>. q0) .=>. (((.~.) r0) .=>. (s0 .&. t0)))
      , expected = [ClauseNormalForm
                    (toSS
                    [[(pApp "p" []),(pApp "r" []),(pApp "s" [])],
                     [((.~.) (pApp "q" [])),(pApp "r" []),(pApp "s" [])],
                     [(pApp "p" []),(pApp "r" []),(pApp "t" [])],
                     [((.~.) (pApp "q" [])),(pApp "r" []),(pApp "t" [])]])]
      }
    , let p = pApp "p" []
          true = pApp (fromBool True) []
          false = pApp (fromBool False) [] in
      TestFormula
      { name = "psimplify 50"
      , formula = true .=>. (p .<=>. (p .<=>. false))
      , expected = [ SimplifiedForm (p .<=>. (.~.) p) ] }
    , let true = pApp (fromBool True) []
          false = pApp (fromBool False) [] in
      TestFormula
      { name = "psimplify 51"
      , formula = (((pApp "x" [] .=>. pApp "y" []) .=>. true) .|. false)
      , expected = [ SimplifiedForm (pApp (fromBool True) []) ] }
    , let false = pApp (fromBool False) []
          q = pApp "q" [] in
      TestFormula
      { name = "simplify 140.3"
      , formula = (for_all "x"
                   (for_all "y"
                    (pApp "p" [vt "x"] .|. (pApp "p" [vt "y"] .&. false))) .=>.
                   (exists "z" q))
      , expected = [ SimplifiedForm ((for_all "x" (pApp "p" [vt "x"])) .=>.
                                        (pApp "q" [])) ] }
    , TestFormula
      { name = "nnf 141.1"
      , formula = ((for_all "x" (pApp "p" [vt "x"])) .=>. ((exists "y" (pApp "q" [vt "y"])) .<=>. (exists "z" (pApp "p" [vt "z"] .&. pApp "q" [vt "z"]))))
      , expected = [ NegationNormalForm 
                     ((exists "x" ((.~.) (pApp "p" [vt "x"]))) .|.
                      ((((exists "y" (pApp "q" [vt "y"])) .&. ((exists "z" ((pApp "p" [vt "z"]) .&. ((pApp "q" [vt "z"])))))) .|.
                        (((for_all "y" ((.~.) (pApp "q" [vt "y"]))) .&.
                          ((for_all "z" (((.~.) (pApp "p" [vt "z"])) .|. (((.~.) (pApp "q" [vt "z"]))))))))))) ] }
    , TestFormula
      { name = "pnf 144.1"
      , formula = (for_all "x" (pApp "p" [vt "x"] .|. pApp "r" [vt "y"]) .=>.
                   (exists "y" (exists "z" (pApp "q" [vt "y"] .|. ((.~.) (exists "z" (pApp "p" [vt "z"] .&. pApp "q" [vt "z"])))))))
      , expected = [ PrenexNormalForm 
                     (exists "x" 
                      (for_all "z"
                       ((((.~.) (pApp "p" [vt "x"])) .&. (((.~.) (pApp "r" [vt "y"])))) .|.
                        (((pApp "q" [vt "x"]) .|. ((((.~.) (pApp "p" [vt "z"])) .|. (((.~.) (pApp "q" [vt "z"])))))))))) ] }
    , let (x, y, u, v) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm)
          fv = fApp (toSkolem "v") [u,x]
          fy = fApp (toSkolem "y") [x] in
      TestFormula
      { name = "snf 150.1"
      , formula = (exists "y" (pApp "<" [x, y] .=>. for_all "u" (exists "v" (pApp "<" [fApp "*" [x, u], fApp "*" [y, v]]))))
      , expected = [ SkolemNormalForm (((.~.) (pApp "<" [x, fy])) .|. pApp "<" [fApp "*" [x, u], fApp "*" [fy, fv]]) ] }
    , let p x = pApp "p" [x]
          q x = pApp "q" [x]
          (x, y, z) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm) in
      TestFormula
      { name = "snf 150.2"
      , formula = (for_all "x" (p x .=>. (exists "y" (exists "z" (q y .|. (.~.) (exists "z" (p z .&. (q z))))))))
      , expected = [ SkolemNormalForm (((.~.) (p x)) .|. (q (fApp (toSkolem "y") []) .|. (((.~.) (p z)) .|. ((.~.) (q z))))) ] }
    ]

animalKB :: (String, [TTestFormula])
animalKB =
    let x = vt "x"
        y = vt "y"
        dog = pApp "Dog"
        cat = pApp "Cat"
        owns = pApp "Owns"
        kills = pApp "Kills"
        animal = pApp "Animal"
        animalLover = pApp "AnimalLover"
        jack = fApp "Jack" []
        tuna = fApp "Tuna" []
        curiosity = fApp "Curiosity" [] in
    ("animal"
    , [ TestFormula
       { formula = exists "x" (dog [x] .&. owns [jack, x]) -- [[Pos 1],[Pos 2]]
       , name = "jack owns a dog"
       , expected = [ClauseNormalForm (toSS [[(pApp "Dog" [fApp (toSkolem "x") []])],[(pApp "Owns" [fApp "Jack" [],fApp (toSkolem "x") []])]])]
       -- owns(jack,sK0)
       -- dog (SK0)
                   }
     , TestFormula
       { formula = for_all "x" ((exists "y" (dog [y] .&. (owns [x, y]))) .=>. (animalLover [x])) -- [[Neg 1,Neg 2,Pos 3]]
       , name = "dog owners are animal lovers"
       , expected = [ PrenexNormalForm (for_all "x" (for_all "y" ((((.~.) (pApp "Dog" [vt "y"])) .|.
                                                                           (((.~.) (pApp "Owns" [vt "x",vt "y"])))) .|.
                                                                          ((pApp "AnimalLover" [vt "x"])))))
                    , ClauseNormalForm (toSS [[((.~.) (pApp "Dog" [vt "y"])),((.~.) (pApp "Owns" [vt "x",vt "y"])),(pApp "AnimalLover" [vt "x"])]]) ]
       -- animalLover(X0) | ~owns(X0,sK1(X0)) | ~dog(sK1(X0))
       }
     , TestFormula
       { formula = for_all "x" (animalLover [x] .=>. (for_all "y" ((animal [y]) .=>. ((.~.) (kills [x, y]))))) -- [[Neg 3,Neg 4,Neg 5]]
       , name = "animal lovers don't kill animals"
       , expected = [ClauseNormalForm  (toSS [[((.~.) (pApp "AnimalLover" [vt "x"])),((.~.) (pApp "Animal" [vt "y"])),((.~.) (pApp "Kills" [vt "x",vt "y"]))]])]
       -- ~kills(X0,X2) | ~animal(X2) | ~animalLover(sK2(X0))
       }
     , TestFormula
       { formula = (kills [jack, tuna]) .|. (kills [curiosity, tuna]) -- [[Pos 5,Pos 5]]
       , name = "Either jack or curiosity kills tuna"
       , expected = [ClauseNormalForm  (toSS [[(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []]),(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []])]])]
       -- kills(curiosity,tuna) | kills(jack,tuna)
       }
     , TestFormula
       { formula = cat [tuna] -- [[Pos 6]]
       , name = "tuna is a cat"
       , expected = [ClauseNormalForm  (toSS [[(pApp "Cat" [fApp "Tuna" []])]])]
       -- cat(tuna)
       }
     , TestFormula
       { formula = for_all "x" ((cat [x]) .=>. (animal [x])) -- [[Neg 6,Pos 4]]
       , name = "a cat is an animal"
       , expected = [ClauseNormalForm  (toSS [[((.~.) (pApp "Cat" [vt "x"])),(pApp "Animal" [vt "x"])]])]
       -- animal(X0) | ~cat(X0)
       }
     ])

animalConjectures :: [TTestFormula]
animalConjectures =
    let kills = pApp "Kills"
        jack = fApp "Jack" []
        tuna = fApp "Tuna" []
        curiosity = fApp "Curiosity" [] in

    map (withKB animalKB) $
     [ TestFormula
       { formula = kills [jack, tuna]             -- False
       , name = "jack kills tuna"
       , expected =
           [ FirstOrderFormula ((.~.) (((exists "x" ((pApp "Dog" [vt ("x")]) .&. ((pApp "Owns" [fApp ("Jack") [],vt ("x")])))) .&.
                                        (((for_all "x" ((exists "y" ((pApp "Dog" [vt ("y")]) .&. ((pApp "Owns" [vt ("x"),vt ("y")])))) .=>.
                                                          ((pApp "AnimalLover" [vt ("x")])))) .&.
                                          (((for_all "x" ((pApp "AnimalLover" [vt ("x")]) .=>.
                                                            ((for_all "y" ((pApp "Animal" [vt ("y")]) .=>.
                                                                             (((.~.) (pApp "Kills" [vt ("x"),vt ("y")])))))))) .&.
                                            ((((pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]) .|. ((pApp "Kills" [fApp ("Curiosity") [],fApp ("Tuna") []]))) .&.
                                              (((pApp "Cat" [fApp ("Tuna") []]) .&.
                                                ((for_all "x" ((pApp "Cat" [vt ("x")]) .=>.
                                                                 ((pApp "Animal" [vt ("x")])))))))))))))) .=>.
                                       ((pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]))))

           , PrenexNormalForm
             (for_all "x"
              (for_all "y"
               (exists "x2"
                ((((pApp ("Dog") [vt ("x2")]) .&.
                   ((pApp ("Owns") [fApp ("Jack") [],vt ("x2")]))) .&.
                  ((((((.~.) (pApp ("Dog") [vt ("y")])) .|.
                      (((.~.) (pApp ("Owns") [vt ("x"),vt ("y")])))) .|.
                     ((pApp ("AnimalLover") [vt ("x")]))) .&.
                    (((((.~.) (pApp ("AnimalLover") [vt ("x")])) .|.
                       ((((.~.) (pApp ("Animal") [vt ("y")])) .|.
                         (((.~.) (pApp ("Kills") [vt ("x"),vt ("y")])))))) .&.
                      ((((pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []]) .|.
                         ((pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]))) .&.
                        (((pApp ("Cat") [fApp ("Tuna") []]) .&.
                          ((((.~.) (pApp ("Cat") [vt ("x")])) .|.
                            ((pApp ("Animal") [vt ("x")]))))))))))))) .&.
                 (((.~.) (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])))))))
           , ClauseNormalForm
             (toSS
              [[(pApp ("Animal") [vt ("x")]),
                ((.~.) (pApp ("Cat") [vt ("x")]))],
               [(pApp ("AnimalLover") [vt ("x")]),
                ((.~.) (pApp ("Dog") [vt ("y")])),
                ((.~.) (pApp ("Owns") [vt ("x"),vt ("y")]))],
               [(pApp ("Cat") [fApp ("Tuna") []])],
               [(pApp ("Dog") [fApp (toSkolem "x") []])],
               [(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),
                (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])],
               [(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x") []])],
               [((.~.) (pApp ("Animal") [vt ("y")])),
                ((.~.) (pApp ("AnimalLover") [vt ("x")])),
                ((.~.) (pApp ("Kills") [vt ("x"),vt ("y")]))],
               [((.~.) (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []]))]])
           , ChiouKB1
             (Proof
              Invalid
              (S.fromList 
               [makeINF' ([]) ([(pApp ("Cat") [fApp ("Tuna") []])]),
                makeINF' ([]) ([(pApp ("Dog") [fApp (toSkolem "x") []])]),
                makeINF' ([]) ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),
                makeINF' ([]) ([(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x") []])]),
                makeINF' ([(pApp ("Animal") [vt ("y")]),(pApp ("AnimalLover") [vt ("x")]),(pApp ("Kills") [vt ("x"),vt ("y")])]) ([]),
                makeINF' ([(pApp ("Cat") [vt ("x")])]) ([(pApp ("Animal") [vt ("x")])]),
                makeINF' ([(pApp ("Dog") [vt ("y")]),(pApp ("Owns") [vt ("x"),vt ("y")])]) ([(pApp ("AnimalLover") [vt ("x")])]),
                makeINF' ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]) ([])]))
           ]
       }
     , TestFormula
       { formula = kills [curiosity, tuna]        -- True
       , name = "curiosity kills tuna"
       , expected =
           [ ClauseNormalForm
             (toSS
             [[(pApp "Dog" [fApp (toSkolem "x") []])],
              [(pApp "Owns" [fApp ("Jack") [],fApp (toSkolem "x") []])],
              [((.~.) (pApp "Dog" [vt ("y")])),
               ((.~.) (pApp "Owns" [vt ("x"),vt ("y")])),
               (pApp "AnimalLover" [vt ("x")])],
              [((.~.) (pApp "AnimalLover" [vt ("x")])),
               ((.~.) (pApp "Animal" [vt ("y")])),
               ((.~.) (pApp "Kills" [vt ("x"),vt ("y")]))],
              [(pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]),
               (pApp "Kills" [fApp ("Curiosity") [],fApp ("Tuna") []])],
              [(pApp "Cat" [fApp ("Tuna") []])],
              [((.~.) (pApp "Cat" [vt ("x")])),
               (pApp "Animal" [vt ("x")])],
              [((.~.) (pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]))]])
           , PropLogicSat True
{-
           , SatSolverCNF [ [Neg 1,Neg 2,Neg 3]    -- animallover(x)|animal(y)|kills(x,y)
                          , [Neg 4,Pos 5]          -- ~cat(x)|animal(x)
                          , [Neg 6,Neg 7,Pos 2]    -- ~dog(y)|~owns(x,y)|animallover(x)
                          , [Neg 8]                -- ~kills(curisity,tuna)
                          , [Pos 8,Pos 11]         -- kills(curiosity,tuna)|kills(jack,tuna)
                          , [Pos 9]                -- cat(tuna)
                          , [Pos 10]               -- owns(jack,sk1)
                          , [Pos 12]               -- dog(sk1)
                          ]
-}
           -- I haven't tried to figure out if this is correct, it
           -- probably is because things are working.
           , SatSolverCNF [[Neg 2,Pos 1],[Neg 3,Neg 11,Neg 12],[Neg 4,Neg 5,Pos 3],[Neg 8],[Pos 6],[Pos 7],[Pos 8,Pos 9],[Pos 10]]
           -- It seems like this should be True.
           , SatSolverSat False
           ]
       }
     ]

socratesKB =
    let x = vt "x"
        socrates x = pApp "Socrates" [x]
        human x = pApp "Human" [x]
        mortal x = pApp "Mortal" [x] in
    ("socrates"
    , [ TestFormula
       { name = "all humans are mortal"
       , formula = for_all "x" (human x .=>. mortal x)
       , expected = [ClauseNormalForm  (toSS [[((.~.) (human x)), mortal x]])] }
     , TestFormula
       { name = "socrates is human"
       , formula = for_all "x" (socrates x .=>. human x)
       , expected = [ClauseNormalForm  (toSS [[(.~.) (socrates x), human x]])] }
     ])

{-
socratesConjectures =
    map (withKB socratesKB)
     [ TestFormula
       { formula = for_all' [V "x"] (socrates x .=>. mortal x)
       , name = "socrates is mortal"
       , expected = [ FirstOrderFormula ((.~.) (((for_all' [V "x"] ((pApp "Human" [vt "x"]) .=>. ((pApp "Mortal" [vt "x"])))) .&.
                                                 ((for_all' [V "x"] ((pApp "Socrates" [vt "x"]) .=>. ((pApp "Human" [vt "x"])))))) .=>.
                                                ((for_all' [V "x"] ((pApp "Socrates" [vt "x"]) .=>. ((pApp "Mortal" [vt "x"])))))))
                    , ClauseNormalForm  [[((.~.) (pApp "Human" [vt "x2"])),(pApp "Mortal" [vt "x2"])],
                                          [((.~.) (pApp "Socrates" [vt "x2"])),(pApp "Human" [vt "x2"])],
                                          [(pApp "Socrates" [fApp (toSkolem "x") [vt "x2",vt "x2"]])],
                                          [((.~.) (pApp "Mortal" [fApp (toSkolem "x") [vt "x2",vt "x2"]]))]]
                    , SatPropLogic True ]
       }
     , TestFormula
       { formula = (.~.) (for_all' [V "x"] (socrates x .=>. mortal x))
       , name = "not (socrates is mortal)"
       , expected = [ SatPropLogic False
                    , FirstOrderFormula ((.~.) (((for_all' [V "x"] ((pApp "Human" [vt "x"]) .=>. ((pApp "Mortal" [vt "x"])))) .&.
                                                 ((for_all' [V "x"] ((pApp "Socrates" [vt "x"]) .=>. ((pApp "Human" [vt "x"])))))) .=>.
                                                (((.~.) (for_all' [V "x"] ((pApp "Socrates" [vt "x"]) .=>. ((pApp "Mortal" [vt "x"]))))))))
                    -- [~human(x) | mortal(x)], [~socrates(Sk1(x,y)) | human(Sk1(x,y))], socrates(Sk1(x,y)), ~mortal(Sk1(x,y))
                    -- ~1 | 2, ~3 | 4, 3, ~5?
                    , ClauseNormalForm [[((.~.) (pApp "Human" [x])), (pApp "Mortal" [x])],
                                         [((.~.) (pApp "Socrates" [fApp (toSkolem "x") [x,y]])), (pApp "Human" [fApp (toSkolem "x") [x,y]])],
                                         [(pApp "Socrates" [fApp (toSkolem "x") [x,y]])], [((.~.) (pApp "Mortal" [fApp (toSkolem "x") [x,y]]))]]
                    , ClauseNormalForm [[((.~.) (pApp "Human" [vt "x2"])), (pApp "Mortal" [vt "x2"])],
                                         [((.~.) (pApp "Socrates" [vt "x2"])), (pApp "Human" [vt "x2"])],
                                         [((.~.) (pApp "Socrates" [vt "x"])), (pApp "Mortal" [vt "x"])]] ]
       }
     ]
-}

chang43KB :: (String, [TTestFormula])
chang43KB = 
    let e = fApp "e" []
        (x, y, z, u, v, w) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm, vt "w" :: TTerm) in
    ("chang example 4.3"
    , [ TestFormula { name = "closure property"
                    , formula = for_all' ["x", "y"] (exists "z" (pApp "P" [x,y,z]))
                    , expected = [] }
      , TestFormula { name = "associativity property"
                    , formula = for_all' ["x", "y", "z", "u", "v", "w"] (pApp "P" [x, y, u] .&. pApp "P" [y, z, v] .&. pApp "P" [u, z, w] .=>. pApp "P" [x, v, w]) .&.
                                for_all' ["x", "y", "z", "u", "v", "w"] (pApp "P" [x, y, u] .&. pApp "P" [y, z, v] .&. pApp "P" [x, v, w] .=>. pApp "P" [u, z, w])
                    , expected = [] }
      , TestFormula { name = "identity property"
                    , formula = (for_all "x" (pApp "P" [x,e,x])) .&. (for_all "x" (pApp "P" [e,x,x]))
                    , expected = [] }
      , TestFormula { name = "inverse property"
                    , formula = (for_all "x" (pApp "P" [x,fApp "i" [x], e])) .&. (for_all "x" (pApp "P" [fApp "i" [x], x, e]))
                    , expected = [] }
      ])

chang43Conjecture :: TTestFormula
chang43Conjecture =
    let e = (fApp "e" [])
        (x, u, v, w) = (vt "x" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm, vt "w" :: TTerm) in
    withKB chang43KB $
    TestFormula { name = "G is commutative"
                , formula = for_all "x" (pApp "P" [x, x, e] .=>. (for_all' ["u", "v", "w"] (pApp "P" [u, v, w] .=>. pApp "P" [v, u, w]))) 
                , expected =
                    [ FirstOrderFormula 
                      ((.~.) (((for_all' ["x","y"] (exists "z" (pApp "P" [vt ("x"),vt ("y"),vt ("z")]))) .&. ((((for_all' ["x","y","z","u","v","w"] ((((pApp "P" [vt ("x"),vt ("y"),vt ("u")]) .&. ((pApp "P" [vt ("y"),vt ("z"),vt ("v")]))) .&. ((pApp "P" [vt ("u"),vt ("z"),vt ("w")]))) .=>. ((pApp "P" [vt ("x"),vt ("v"),vt ("w")])))) .&. ((for_all' ["x","y","z","u","v","w"] ((((pApp "P" [vt ("x"),vt ("y"),vt ("u")]) .&. ((pApp "P" [vt ("y"),vt ("z"),vt ("v")]))) .&. ((pApp "P" [vt ("x"),vt ("v"),vt ("w")]))) .=>. ((pApp "P" [vt ("u"),vt ("z"),vt ("w")])))))) .&. ((((for_all "x" (pApp "P" [vt ("x"),fApp ("e") [],vt ("x")])) .&. ((for_all "x" (pApp "P" [fApp ("e") [],vt ("x"),vt ("x")])))) .&. (((for_all "x" (pApp "P" [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []])) .&. ((for_all "x" (pApp "P" [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []])))))))))) .=>. ((for_all "x" ((pApp "P" [vt ("x"),vt ("x"),fApp ("e") []]) .=>. ((for_all' ["u","v","w"] ((pApp "P" [vt ("u"),vt ("v"),vt ("w")]) .=>. ((pApp "P" [vt ("v"),vt ("u"),vt ("w")]))))))))))
                      -- (∀x ∀y ∃z P(x,y,z)) &
                      -- (∀x∀y∀z∀u∀v∀w ~P(x,y,u) | ~P(y,z,v) | ~P(u,z,w) | P(x,v,w)) &
                      -- (∀x∀y∀z∀u∀v∀w ~P(x,y,u) | ~P(y,z,v) | ~P(x,v,w) | P(u,z,w)) &
                      -- (∀x P(x,e,x)) &
                      -- (∀x P(e,x,x)) &
                      -- (∀x P(x,i[x],e)) &
                      -- (∀x P(i[x],x,e)) &
                      -- (∃x P(x,x,e) & (∃u∃v∃w P(u,v,w) & ~P(v,u,w)))
                    , NegationNormalForm
                      (((for_all "x"
                         (for_all "y"
                          (exists "z"
                           (pApp ("P") [vt ("x"),vt ("y"),vt ("z")])))) .&.
                        ((((for_all "x"
                            (for_all "y"
                             (for_all "z"
                              (for_all "u"
                               (for_all "v"
                                (for_all "w"
                                 (((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.
                                    (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.
                                   (((.~.) (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])))) .|.
                                  ((pApp ("P") [vt ("x"),vt ("v"),vt ("w")]))))))))) .&.
                           ((for_all "x"
                             (for_all "y"
                              (for_all "z"
                               (for_all "u"
                                (for_all "v"
                                 (for_all "w"
                                  (((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.
                                     (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.
                                    (((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])))) .|.
                                   ((pApp ("P") [vt ("u"),vt ("z"),vt ("w")]))))))))))) .&.
                          ((((for_all "x" (pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")])) .&.
                             ((for_all "x" (pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")])))) .&.
                            (((for_all "x" (pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []])) .&.
                              ((for_all "x" (pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []])))))))))) .&.
                       ((exists "x"
                         ((pApp ("P") [vt ("x"),vt ("x"),fApp ("e") []]) .&.
                          ((exists "u"
                            (exists "v"
                             (exists "w"
                              ((pApp ("P") [vt ("u"),vt ("v"),vt ("w")]) .&.
                               (((.~.) (pApp ("P") [vt ("v"),vt ("u"),vt ("w")]))))))))))))
                    , PrenexNormalForm
                      (for_all "x"
                       (for_all "y"
                        (for_all "z"
                         (for_all "u"
                          (for_all "v"
                           (for_all "w"
                            (exists "z2"
                             (exists "x2"
                              (exists "u2"
                               (exists "v2"
                                (exists "w2"
                                 (((pApp ("P") [vt ("x"),vt ("y"),vt ("z2")]) .&.
                                   ((((((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.
                                         (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.
                                        (((.~.) (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])))) .|.
                                       ((pApp ("P") [vt ("x"),vt ("v"),vt ("w")]))) .&.
                                      ((((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.
                                          (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.
                                         (((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])))) .|.
                                        ((pApp ("P") [vt ("u"),vt ("z"),vt ("w")]))))) .&.
                                     ((((pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")]) .&.
                                        ((pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")]))) .&.
                                       (((pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []]) .&.
                                         ((pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []]))))))))) .&.
                                  (((pApp ("P") [vt ("x2"),vt ("x2"),fApp ("e") []]) .&.
                                    (((pApp ("P") [vt ("u2"),vt ("v2"),vt ("w2")]) .&.
                                      (((.~.) (pApp ("P") [vt ("v2"),vt ("u2"),vt ("w2")])))))))))))))))))))
                    , SkolemNormalForm
                      (((pApp ("P") [vt ("x"),vt ("y"),fApp (toSkolem "z") [vt ("x"),vt ("y")]]) .&.
                        ((((((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.
                              (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.
                             (((.~.) (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])))) .|.
                            ((pApp ("P") [vt ("x"),vt ("v"),vt ("w")]))) .&.
                           ((((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.
                               (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.
                              (((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])))) .|.
                             ((pApp ("P") [vt ("u"),vt ("z"),vt ("w")]))))) .&.
                          ((((pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")]) .&.
                             ((pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")]))) .&.
                            (((pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []]) .&.
                              ((pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []]))))))))) .&.
                       (((pApp ("P") [fApp (toSkolem "x") [],fApp (toSkolem "x") [],fApp ("e") []]) .&.
                         (((pApp ("P") [fApp (toSkolem "u") [],fApp (toSkolem "v") [],fApp (toSkolem "w") []]) .&.
                           (((.~.) (pApp ("P") [fApp (toSkolem "v") [],fApp (toSkolem "u") [],fApp (toSkolem "w") []]))))))))
                    , SkolemNumbers (S.fromList [toSkolem "u",toSkolem "v",toSkolem "w",toSkolem "x",toSkolem "z"])
                    -- From our algorithm

                    , ClauseNormalForm
                      (toSS 
                      [[(pApp ("P") [vt ("x"),vt ("y"),fApp (toSkolem "z") [vt ("x"),vt ("y")]])],
                       [((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])),
                        ((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])),
                        ((.~.) (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])),
                        (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])],
                       [((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])),
                        ((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])),
                        ((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])),
                        (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])],
                       [(pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")])],
                       [(pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")])],
                       [(pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []])],
                       [(pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []])],
                       [(pApp ("P") [fApp (toSkolem "x") [],fApp (toSkolem "x") [],fApp ("e") []])],
                       [(pApp ("P") [fApp (toSkolem "u") [],fApp (toSkolem "v") [],fApp (toSkolem "w") []])],
                       [((.~.) (pApp ("P") [fApp (toSkolem "v") [],fApp (toSkolem "u") [],fApp (toSkolem "w") []]))]])

                    -- From the book
{-
                    , let (a, b, c) = 
                              (fApp (toSkolem "x") [vt ("x"),vt ("y"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u"),vt ("v"),vt ("w"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u2"),vt ("v2"),vt ("w2"),vt ("x3"),vt ("x3"),vt ("x3"),vt ("x3")],
                               fApp (toSkolem "x") [vt ("x"),vt ("y"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u"),vt ("v"),vt ("w"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u2"),vt ("v2"),vt ("w2"),vt ("x3"),vt ("x3"),vt ("x3"),vt ("x3")],
                               fApp (toSkolem "x") [vt ("x"),vt ("y"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u"),vt ("v"),vt ("w"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u2"),vt ("v2"),vt ("w2"),vt ("x3"),vt ("x3"),vt ("x3"),vt ("x3")]) in
                      ClauseNormalForm
                      [[(pApp "P" [vt "x",vt "y",fApp (toSkolem "x") [vt "x",vt "y"]])],
                       [((.~.) (pApp "P" [vt "x",vt "y",vt "u"])),
                        ((.~.) (pApp "P" [vt "y",vt "z",vt "v"])),
                        ((.~.) (pApp "P" [vt "u",vt "z",vt "w"])),
                        (pApp "P" [vt "x",vt "v",vt "w"])],
                       [((.~.) (pApp "P" [vt "x",vt "y",vt "u"])),
                        ((.~.) (pApp "P" [vt "y",vt "z",vt "v"])),
                        ((.~.) (pApp "P" [vt "x",vt "v",vt "w"])),
                        (pApp "P" [vt "u",vt "z",vt "w"])],
                       [(pApp "P" [vt "x",fApp "e" [],vt "x"])],
                       [(pApp "P" [fApp "e" [],vt "x",vt "x"])],
                       [(pApp "P" [vt "x",fApp "i" [vt "x"],fApp "e" []])],
                       [(pApp "P" [fApp "i" [vt "x"],vt "x",fApp "e" []])],
                       [(pApp "P" [vt "x",
                                   vt "x",
                                   fApp "e" []])],
                       [(pApp "P" [a, b, c])],
                       [((.~.) (pApp "P" [b, a, c]))]]
-}
                    ]
                }

{-
% ghci
> :load Test/Data.hs
> :m +Logic.FirstOrder
> :m +Logic.Normal
> let f = (.~.) (conj (map formula (snd chang43KB)) .=>. formula chang43Conjecture)
> putStrLn (runNormal (cnfTrace f))
-}

chang43ConjectureRenamed :: TTestFormula
chang43ConjectureRenamed =
    let e = fApp "e" []
        (x, y, z, u, v, w) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm, vt "w" :: TTerm)
        (u2, v2, w2, x2, y2, z2, u3, v3, w3, x3, y3, z3, x4, x5, x6, x7, x8) =
            (vt "u2" :: TTerm, vt "v2" :: TTerm, vt "w2" :: TTerm, vt "x2" :: TTerm, vt "y2" :: TTerm, vt "z2" :: TTerm, vt "u3" :: TTerm, vt "v3" :: TTerm, vt "w3" :: TTerm, vt "x3" :: TTerm, vt "y3" :: TTerm, vt "z3" :: TTerm, vt "x4" :: TTerm, vt "x5" :: TTerm, vt "x6" :: TTerm, vt "x7" :: TTerm, vt "x8" :: TTerm) in
    TestFormula { name = "chang 43 renamed"
                , formula = (.~.) ((for_all' ["x", "y"] (exists "z" (pApp "P" [x,y,z])) .&.
                                    for_all' ["x2", "y2", "z2", "u", "v", "w"] (pApp "P" [x2, y2, u] .&. pApp "P" [y2, z2, v] .&. pApp "P" [u, z2, w] .=>. pApp "P" [x2, v, w]) .&.
                                    for_all' ["x3", "y3", "z3", "u2", "v2", "w2"] (pApp "P" [x3, y3, u2] .&. pApp "P" [y3, z3, v2] .&. pApp "P" [x3, v2, w2] .=>. pApp "P" [u2, z3, w2]) .&.
                                    for_all "x4" (pApp "P" [x4,e,x4]) .&.
                                    for_all "x5" (pApp "P" [e,x5,x5]) .&.
                                    for_all "x6" (pApp "P" [x6,fApp "i" [x6], e]) .&.
                                    for_all "x7" (pApp "P" [fApp "i" [x7], x7, e])) .=>.
                                   (for_all "x8" (pApp "P" [x8, x8, e] .=>. (for_all' ["u3", "v3", "w3"] (pApp "P" [u3, v3, w3] .=>. pApp "P" [v3, u3, w3])))))
                , expected =
                    [ FirstOrderFormula
                      ((.~.) ((((((((for_all' ["x","y"] (exists "z" (pApp "P" [vt "x",vt "y",vt "z"]))) .&.
                                    ((for_all' ["x2","y2","z2","u","v","w"] ((((pApp "P" [vt "x2",vt "y2",vt "u"]) .&.
                                                                                          ((pApp "P" [vt "y2",vt "z2",vt "v"]))) .&.
                                                                                         ((pApp "P" [vt "u",vt "z2",vt "w"]))) .=>.
                                                                                        ((pApp "P" [vt "x2",vt "v",vt "w"])))))) .&.
                                   ((for_all' ["x3","y3","z3","u2","v2","w2"] ((((pApp "P" [vt "x3",vt "y3",vt "u2"]) .&.
                                                                                            ((pApp "P" [vt "y3",vt "z3",vt "v2"]))) .&.
                                                                                           ((pApp "P" [vt "x3",vt "v2",vt "w2"]))) .=>.
                                                                                          ((pApp "P" [vt "u2",vt "z3",vt "w2"])))))) .&.
                                  ((for_all "x4" (pApp "P" [vt "x4",fApp "e" [],vt "x4"])))) .&.
                                 ((for_all "x5" (pApp "P" [fApp "e" [],vt "x5",vt "x5"])))) .&.
                                ((for_all "x6" (pApp "P" [vt "x6",fApp "i" [vt "x6"],fApp "e" []])))) .&.
                               ((for_all "x7" (pApp "P" [fApp "i" [vt "x7"],vt "x7",fApp "e" []])))) .=>.
                              ((for_all "x8" ((pApp "P" [vt "x8",vt "x8",fApp "e" []]) .=>.
                                                  ((for_all' ["u3","v3","w3"] ((pApp "P" [vt "u3",vt "v3",vt "w3"]) .=>.
                                                                                    ((pApp "P" [vt "v3",vt "u3",vt "w3"]))))))))))
                    , let a = fApp (toSkolem "u3") []
                          b = fApp (toSkolem "v3") []
                          c = fApp (toSkolem "w3") [] in
                      ClauseNormalForm
                      (toSS
                      [[(pApp ("P") [vt ("x"),vt ("y"),fApp (toSkolem "z") [vt ("x"),vt ("y")]])],
                       [((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])),
                        ((.~.) (pApp ("P") [vt ("y"),vt ("z2"),vt ("v")])),
                        ((.~.) (pApp ("P") [vt ("u"),vt ("z2"),vt ("w")])),
                        (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])],
                       [((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])),
                        ((.~.) (pApp ("P") [vt ("y"),vt ("z2"),vt ("v")])),
                        ((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])),
                        (pApp ("P") [vt ("u"),vt ("z2"),vt ("w")])],
                       [(pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")])],
                       [(pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")])],
                       [(pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []])],
                       [(pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []])],
                       [(pApp ("P") [fApp (toSkolem "x8") [],fApp (toSkolem "x8") [],fApp ("e") []])],
                       [(pApp ("P") [a,b,c])],
                       [((.~.) (pApp ("P") [b,a,c]))]])                      
                    ]
                }

withKB :: forall formula atom term v p f. (formula ~ TFormula, atom ~ TAtom, v ~ V, FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f) =>
          (String, [TestFormula formula atom v]) -> TestFormula formula atom v -> TestFormula formula atom v
withKB (kbName, knowledge) conjecture =
    conjecture { name = name conjecture ++ " with " ++ kbName ++ " knowledge base"
               -- Here we say that the conjunction of the knowledge
               -- base formula implies the conjecture.  We prove the
               -- theorem by showing that the negation is
               -- unsatisfiable.
               , formula = (.~.) (conj (map formula knowledge) .=>. formula conjecture)}
    where
      conj [] = error "conj []"
      conj [x] = x
      conj (x:xs) = x .&. conj xs

kbKnowledge :: forall formula atom term v p f. (formula ~ TFormula, atom ~ TAtom, v ~ V,
                                                FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f) =>
               (String, [TestFormula formula atom v]) -> (String, [formula])
kbKnowledge kb = (fst (kb :: (String, [TestFormula formula atom v])), map formula (snd kb))

proofs :: forall formula atom term v p f. (formula ~ TFormula, atom ~ TAtom, v ~ V,
                                           FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f, Ord formula, IsString v, IsString p, IsString f) =>
          [TestProof formula term v]
proofs =
    let -- dog = pApp "Dog" :: [term] -> formula
        -- cat = pApp "Cat" :: [term] -> formula
        -- owns = pApp "Owns" :: [term] -> formula
        kills = pApp "Kills"
        -- animal = pApp "Animal" :: [term] -> formula
        -- animalLover = pApp "AnimalLover" :: [term] -> formula
        socrates = pApp "Socrates"
        -- human = pApp "Human" :: [term] -> formula
        mortal = pApp "Mortal"

        jack = fApp "Jack" []
        tuna = fApp "Tuna" []
        curiosity = fApp "Curiosity" [] in

    [ TestProof
      { proofName = "prove jack kills tuna"
      , proofKnowledge = kbKnowledge animalKB
      , conjecture = kills [jack, tuna]
      , proofExpected = 
          [ ChiouKB (S.fromList
                     [WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Dog" [fApp (toSkolem "x") []])]), wiIdent = 1},
                      WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem "x") []])]), wiIdent = 1},
                      WithId {wiItem = INF (S.fromList [(pApp "Dog" [vt "y"]),(pApp "Owns" [vt "x",vt "y"])]) (S.fromList [(pApp "AnimalLover" [vt "x"])]), wiIdent = 2},
                      WithId {wiItem = INF (S.fromList [(pApp "Animal" [vt "y"]),(pApp "AnimalLover" [vt "x"]),(pApp "Kills" [vt "x",vt "y"])]) (S.fromList []), wiIdent = 3},
                      WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]),(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])]), wiIdent = 4},
                      WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Cat" [fApp "Tuna" []])]), wiIdent = 5},
                      WithId {wiItem = INF (S.fromList [(pApp "Cat" [vt "x"])]) (S.fromList [(pApp "Animal" [vt "x"])]), wiIdent = 6}])
          , ChiouResult (False,
                         (S.fromList
                          [(inf' [(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])] [],fromList []),
                           (inf' [] [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []])],fromList []),
                           (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "AnimalLover" [fApp "Curiosity" []])] [],fromList []),
                           (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "Dog" [vt "y"]),(pApp "Owns" [fApp "Curiosity" [],vt "y"])] [],fromList []),
                           (inf' [(pApp "AnimalLover" [fApp "Curiosity" []]),(pApp "Cat" [fApp "Tuna" []])] [],fromList []),
                           (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem "x") []])] [],fromList []),
                           (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Dog" [vt "y"]),(pApp "Owns" [fApp "Curiosity" [],vt "y"])] [],fromList []),
                           (inf' [(pApp "AnimalLover" [fApp "Curiosity" []])] [],fromList []),
                           (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem "x") []])] [],fromList []),
                           (inf' [(pApp "Dog" [vt "y"]),(pApp "Owns" [fApp "Curiosity" [],vt "y"])] [],fromList []),
                           (inf' [(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem "x") []])] [],fromList [])]))
          ]
      }
    , TestProof
      { proofName = "prove curiosity kills tuna"
      , proofKnowledge = kbKnowledge animalKB
      , conjecture = kills [curiosity, tuna]
      , proofExpected =
          [ ChiouKB (S.fromList
                     [WithId {wiItem = inf' []                                 [(pApp "Dog" [fApp (toSkolem "x") []])],                 wiIdent = 1},
                      WithId {wiItem = inf' []                                 [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem "x") []])], wiIdent = 1},
                      WithId {wiItem = inf' [(pApp "Dog" [vt "y"]),
                                             (pApp "Owns" [vt "x",vt "y"])]  [(pApp "AnimalLover" [vt "x"])],                      wiIdent = 2},
                      WithId {wiItem = inf' [(pApp "Animal" [vt "y"]),
                                             (pApp "AnimalLover" [vt "x"]),
                                             (pApp "Kills" [vt "x",vt "y"])] [], wiIdent = 3},
                      WithId {wiItem = inf' []                                 [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]),
                                                                                (pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])],      wiIdent = 4},
                      WithId {wiItem = inf' []                                 [(pApp "Cat" [fApp "Tuna" []])],                       wiIdent = 5},
                      WithId {wiItem = inf' [(pApp "Cat" [vt "x"])]           [(pApp "Animal" [vt "x"])],                           wiIdent = 6}])
          , ChiouResult (True,
                         S.fromList 
                         [(makeINF' ([]) ([]),fromList []),
                          (makeINF' ([]) ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),fromList []),
                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem "x") []])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x") []])]) ([]),fromList []),
                          (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),
                          (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []]),(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem "x") []])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x") []])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Dog") [vt ("y")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),
                          (makeINF' ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]) ([]),fromList [])])
          ]
      }
{-
  -- Seems not to terminate
    , let (x, u, v, w, e) = (vt "x", vt "u", vt "v", vt "w", vt "e") in
      TestProof
      { proofName = "chang example 4.3"
      , proofKnowledge = (fst chang43KB, map (convertFOF id id id . formula) (snd chang43KB))
      , conjecture = for_all' ["x"] (pApp "P" [x, x, e] .=>. (for_all' ["u", "v", "w"] (pApp "P" [u, v, w] .=>. pApp "P" [v, u, w])))
      , proofExpected =
          [ChiouResult (True, [])]
      }
-}
    , let x = vt "x" in
      TestProof
      { proofName = "socrates is mortal"
      , proofKnowledge = kbKnowledge (socratesKB)
      , conjecture = for_all "x" (socrates [x] .=>. mortal [x])
      , proofExpected = 
         [ ChiouKB (S.fromList
                    [WithId {wiItem = inf' [(pApp "Human" [vt "x"])] [(pApp "Mortal" [vt "x"])], wiIdent = 1},
                     WithId {wiItem = inf' [(pApp "Socrates" [vt "x"])] [(pApp "Human" [vt "x"])], wiIdent = 2}])
         , ChiouResult (True,
                        S.fromList 
                        [(makeINF' ([]) ([]),fromList []),
                         (makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem "x") []])]),fromList []),
                         (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem "x") []])]),fromList []),
                         (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem "x") []])]),fromList []),
                         (makeINF' ([(pApp ("Mortal") [fApp (toSkolem "x") []])]) ([]),fromList [])])]
      }
    , let x = vt "x" in
      TestProof
      { proofName = "socrates is not mortal"
      , proofKnowledge = kbKnowledge (socratesKB)
      , conjecture = (.~.) (for_all "x" (socrates [x] .=>. mortal [x]))
      , proofExpected = 
         [ ChiouKB (S.fromList
                    [WithId {wiItem = inf' [(pApp "Human" [vt "x"])] [(pApp "Mortal" [vt "x"])], wiIdent = 1},
                     WithId {wiItem = inf' [(pApp "Socrates" [vt "x"])] [(pApp "Human" [vt "x"])], wiIdent = 2}])
         , ChiouResult (False
                       ,(S.fromList [(inf' [(pApp "Socrates" [vt "x"])] [(pApp "Mortal" [vt "x"])],fromList [("x",vt "x")])]))]
      }
    , let x = vt "x" in
      TestProof
      { proofName = "socrates exists and is not mortal"
      , proofKnowledge = kbKnowledge (socratesKB)
      , conjecture = (.~.) (exists "x" (socrates [x]) .&. for_all "x" (socrates [x] .=>. mortal [x]))
      , proofExpected = 
         [ ChiouKB (S.fromList
                    [WithId {wiItem = inf' [(pApp "Human" [vt "x"])] [(pApp "Mortal" [vt "x"])], wiIdent = 1},
                     WithId {wiItem = inf' [(pApp "Socrates" [vt "x"])] [(pApp "Human" [vt "x"])], wiIdent = 2}])
         , ChiouResult (False,
                        S.fromList [(makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem "x") []])]),fromList []),
                                    (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem "x") []])]),fromList []),
                                    (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem "x") []])]),fromList []),
                                    (makeINF' ([(pApp ("Socrates") [vt ("x")])]) ([(pApp ("Mortal") [vt ("x")])]),fromList [("x",vt ("x"))])])
         ]
      }
    ]

inf' = makeINF'

toLL = map S.toList . S.toList
toSS = S.fromList . map S.fromList