{-# language TypeApplications #-}

import Ersatz
import Prelude hiding (and,or, not, (||),(&&))
import Ersatz.Solver
import Ersatz.Solver.Minisat

main = do
  result <- solveWith minisat $ do
    p <- exists @Bit
    q <- exists @Bit
    assert $ (p || not q) && (not p || q)
    return (p,q)
  case result of
    (Satisfied, Just (p,q)) -> do
      print (p,q)