diff --git a/API.hs b/API.hs
index 2ac811d..ba64449 100644
--- a/API.hs
+++ b/API.hs
@@ -1,4 +1,4 @@
-module API where
+module Jukebox.API where
 
 -- this is not actual code, it is just for writing down ideas
 
diff --git a/Graph.hs b/Graph.hs
index b34f2d3..97f11a0 100644
--- a/Graph.hs
+++ b/Graph.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TemplateHaskell #-}
-module Graph where
+module Jukebox.Graph where
 
 import Data.Map as M
 import Data.Set as S
diff --git a/Clausify.hs b/Jukebox/Clausify.hs
similarity index 97%
rename from Clausify.hs
rename to Jukebox/Clausify.hs
index cc69714..a1a50fd 100644
--- a/Clausify.hs
+++ b/Jukebox/Clausify.hs
@@ -1,22 +1,22 @@
 {-# LANGUAGE TypeOperators, BangPatterns #-}
-module Clausify where
+module Jukebox.Clausify where
 
-import Form
-import qualified Form
-import Name
+import Jukebox.Form
+import qualified Jukebox.Form as Form
+import Jukebox.Name
 import Data.List( maximumBy, sortBy, partition )
 import Data.Ord
 import Control.Monad.Reader
 import Control.Monad.State.Strict
-import qualified Seq as S
-import Seq(Seq)
-import qualified NameMap
-import NameMap(NameMap)
-import qualified Map
+import qualified Jukebox.Seq as S
+import Jukebox.Seq(Seq)
+import qualified Jukebox.NameMap as NameMap
+import Jukebox.NameMap(NameMap)
+import qualified Jukebox.Map as Map
 import qualified Data.HashSet as Set
 import qualified Data.ByteString.Char8 as BS
-import Utils
-import Options
+import Jukebox.Utils
+import Jukebox.Options
 import Control.Applicative
 
 newtype ClausifyFlags = ClausifyFlags { splitting :: Bool } deriving Show
diff --git a/Form.hs b/Jukebox/Form.hs
similarity index 98%
rename from Form.hs
rename to Jukebox/Form.hs
index c408821..ac11f50 100644
--- a/Form.hs
+++ b/Jukebox/Form.hs
@@ -3,21 +3,21 @@
 -- "Show" instances for several of these types are found in TPTP.Print.
 
 {-# LANGUAGE DeriveDataTypeable, FlexibleContexts, Rank2Types, GADTs, TypeOperators, ScopedTypeVariables, BangPatterns, PatternGuards #-}
-module Form where
+module Jukebox.Form where
 
 import Prelude hiding (sequence, mapM)
-import qualified Seq as S
-import Seq(Seq)
+import qualified Jukebox.Seq as S
+import Jukebox.Seq(Seq)
 import Data.Hashable
-import qualified Map
-import NameMap(NameMap)
-import qualified NameMap
+import qualified Jukebox.Map as Map
+import Jukebox.NameMap(NameMap)
+import qualified Jukebox.NameMap as NameMap
 import Data.Ord
 import qualified Data.ByteString.Char8 as BS
-import Name
+import Jukebox.Name
 import Control.Monad.State.Strict hiding (sequence, mapM)
 import Data.List hiding (nub)
-import Utils
+import Jukebox.Utils
 import Data.Typeable(Typeable)
 import Data.Monoid
 import Data.Traversable
diff --git a/GuessModel.hs b/Jukebox/GuessModel.hs
similarity index 95%
rename from GuessModel.hs
rename to Jukebox/GuessModel.hs
index 3f3cd20..7c78680 100644
--- a/GuessModel.hs
+++ b/Jukebox/GuessModel.hs
@@ -1,14 +1,14 @@
 {-# LANGUAGE GADTs, PatternGuards #-}
-module GuessModel where
+module Jukebox.GuessModel where
 
 import Control.Monad
 import qualified Data.ByteString.Char8 as BS
-import Name
-import Form
-import Clausify hiding (cnf)
-import TPTP.Print
-import TPTP.ParseSnippet
-import Utils
+import Jukebox.Name
+import Jukebox.Form
+import Jukebox.Clausify hiding (cnf)
+import Jukebox.TPTP.Print
+import Jukebox.TPTP.ParseSnippet
+import Jukebox.Utils
 
 data Universe = Peano | Trees
 
diff --git a/HighSat.hs b/Jukebox/HighSat.hs
similarity index 94%
rename from HighSat.hs
rename to Jukebox/HighSat.hs
index a17db60..8e84955 100644
--- a/HighSat.hs
+++ b/Jukebox/HighSat.hs
@@ -1,13 +1,13 @@
 {-# LANGUAGE BangPatterns, GeneralizedNewtypeDeriving #-}
-module HighSat where
+module Jukebox.HighSat where
 
 import MiniSat hiding (neg)
 import qualified MiniSat
-import qualified Seq as Seq
-import Seq(Seq, List)
-import Form(Signed(..), neg)
-import qualified Map
-import Map(Map)
+import qualified Jukebox.Seq as Seq
+import Jukebox.Seq(Seq, List)
+import Jukebox.Form(Signed(..), neg)
+import qualified Jukebox.Map as Map
+import Jukebox.Map(Map)
 import Control.Monad.State.Strict
 import Control.Monad.Reader
 import Control.Monad.Trans
diff --git a/InferTypes.hs b/Jukebox/InferTypes.hs
similarity index 93%
rename from InferTypes.hs
rename to Jukebox/InferTypes.hs
index fb79358..caf796a 100644
--- a/InferTypes.hs
+++ b/Jukebox/InferTypes.hs
@@ -1,12 +1,12 @@
 {-# LANGUAGE TypeOperators, GADTs #-}
-module InferTypes where
+module Jukebox.InferTypes where
 
 import Control.Monad
-import Form
-import Name
-import qualified NameMap
-import NameMap(NameMap)
-import UnionFind hiding (rep)
+import Jukebox.Form
+import Jukebox.Name
+import qualified Jukebox.NameMap as NameMap
+import Jukebox.NameMap(NameMap)
+import Jukebox.UnionFind hiding (rep)
 
 type Function' = Name ::: ([Type'], Type')
 type Variable' = Name ::: Type'
diff --git a/Map.hs b/Jukebox/Map.hs
similarity index 95%
rename from Map.hs
rename to Jukebox/Map.hs
index b9c6418..3409734 100644
--- a/Map.hs
+++ b/Jukebox/Map.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
-module Map where
+module Jukebox.Map where
 
 import qualified Data.HashMap.Lazy as H
 
diff --git a/Monotonox/Monotonicity.hs b/Jukebox/Monotonox/Monotonicity.hs
similarity index 92%
rename from Monotonox/Monotonicity.hs
rename to Jukebox/Monotonox/Monotonicity.hs
index 30ea94d..3b7538a 100644
--- a/Monotonox/Monotonicity.hs
+++ b/Jukebox/Monotonox/Monotonicity.hs
@@ -1,12 +1,12 @@
 {-# LANGUAGE TypeOperators #-}
-module Monotonox.Monotonicity where
+module Jukebox.Monotonox.Monotonicity where
 
 import Prelude hiding (lookup)
-import Name
-import Form hiding (Form, clause, true, false, conj, disj)
-import HighSat
-import NameMap
-import Utils
+import Jukebox.Name
+import Jukebox.Form hiding (Form, clause, true, false, conj, disj)
+import Jukebox.HighSat
+import Jukebox.NameMap as NameMap
+import Jukebox.Utils
 import Data.Hashable
 import Control.Monad
 
diff --git a/Monotonox/ToFOF.hs b/Jukebox/Monotonox/ToFOF.hs
similarity index 97%
rename from Monotonox/ToFOF.hs
rename to Jukebox/Monotonox/ToFOF.hs
index 5b085d8..5f46a9f 100644
--- a/Monotonox/ToFOF.hs
+++ b/Jukebox/Monotonox/ToFOF.hs
@@ -1,11 +1,11 @@
 {-# LANGUAGE GADTs, PatternGuards #-}
-module Monotonox.ToFOF where
+module Jukebox.Monotonox.ToFOF where
 
-import Clausify(split, removeEquiv, run, withName)
-import Name
-import qualified NameMap
-import Form
-import Options
+import Jukebox.Clausify(split, removeEquiv, run, withName)
+import Jukebox.Name
+import qualified Jukebox.NameMap as NameMap
+import Jukebox.Form
+import Jukebox.Options
 import qualified Data.ByteString.Char8 as BS
 import Control.Monad hiding (guard)
 import Data.Monoid
diff --git a/Name.hs b/Jukebox/Name.hs
similarity index 98%
rename from Name.hs
rename to Jukebox/Name.hs
index 473adee..c6724ae 100644
--- a/Name.hs
+++ b/Jukebox/Name.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeOperators, GeneralizedNewtypeDeriving, FlexibleInstances, DeriveDataTypeable #-}
-module Name(
+module Jukebox.Name(
   Name, uniqueId, base,
   stringBaseName,
   unsafeMakeName,
@@ -11,8 +11,8 @@ module Name(
 
 import qualified Data.ByteString.Char8 as BS
 import Data.Hashable
-import qualified Map
-import Utils
+import qualified Jukebox.Map as Map
+import Jukebox.Utils
 import Data.List
 import Data.Ord
 import Data.Int
diff --git a/NameMap.hs b/Jukebox/NameMap.hs
similarity index 82%
rename from NameMap.hs
rename to Jukebox/NameMap.hs
index 8a28acb..97f2e5c 100644
--- a/NameMap.hs
+++ b/Jukebox/NameMap.hs
@@ -1,11 +1,11 @@
-module NameMap(NameMap, lookup, lookup_, insert, member, delete, (!), fromList, toList, singleton) where
+module Jukebox.NameMap(NameMap, lookup, lookup_, insert, member, delete, (!), fromList, toList, singleton) where
 
 import Prelude hiding (lookup)
-import Name
-import Map(Map)
-import qualified Map
+import Jukebox.Name
+import Jukebox.Map(Map)
+import qualified Jukebox.Map as Map
 import Data.Int
-import qualified Seq as S
+import qualified Jukebox.Seq as S
 
 type NameMap a = Map Int64 a
 
diff --git a/Options.hs b/Jukebox/Options.hs
similarity index 99%
rename from Options.hs
rename to Jukebox/Options.hs
index 9484438..e4a207b 100644
--- a/Options.hs
+++ b/Jukebox/Options.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE FlexibleContexts #-}
-module Options where
+module Jukebox.Options where
 
 import Control.Arrow((***))
 import Control.Applicative
diff --git a/ProgressBar.hs b/Jukebox/ProgressBar.hs
similarity index 95%
rename from ProgressBar.hs
rename to Jukebox/ProgressBar.hs
index af6c9c4..abcadfb 100644
--- a/ProgressBar.hs
+++ b/Jukebox/ProgressBar.hs
@@ -1,4 +1,4 @@
-module ProgressBar(ProgressBar(..), tickOnRead, withProgressBar) where
+module Jukebox.ProgressBar(ProgressBar(..), tickOnRead, withProgressBar) where
 
 import System.IO
 import Data.IORef
diff --git a/Provers/E.hs b/Jukebox/Provers/E.hs
similarity index 89%
rename from Provers/E.hs
rename to Jukebox/Provers/E.hs
index b994d2c..06841b7 100644
--- a/Provers/E.hs
+++ b/Jukebox/Provers/E.hs
@@ -1,23 +1,23 @@
 {-# LANGUAGE GADTs #-}
-module Provers.E where
+module Jukebox.Provers.E where
 
-import Form hiding (tag, Or)
-import Name
-import Options
+import Jukebox.Form hiding (tag, Or)
+import Jukebox.Name
+import Jukebox.Options
 import Control.Applicative hiding (Const)
 import Control.Monad
-import Utils
-import TPTP.Parsec
-import TPTP.ClauseParser hiding (newFunction, Term)
-import TPTP.Print
-import TPTP.Lexer hiding (Normal, keyword, Axiom, name, Var)
+import Jukebox.Utils
+import Jukebox.TPTP.Parsec
+import Jukebox.TPTP.ClauseParser hiding (newFunction, Term)
+import Jukebox.TPTP.Print
+import Jukebox.TPTP.Lexer hiding (Normal, keyword, Axiom, name, Var)
 import Text.PrettyPrint.HughesPJ hiding (parens)
 import Data.Maybe
 import qualified Data.ByteString.Char8 as BS
 import qualified Data.ByteString.Lazy.Char8 as BSL
-import qualified Seq as S
-import qualified Map
-import Map(Map)
+import qualified Jukebox.Seq as S
+import qualified Jukebox.Map as Map
+import Jukebox.Map(Map)
 import Data.Hashable
 
 data EFlags = EFlags {
@@ -109,4 +109,4 @@ extractAnswer prob str = fromMaybe (Left status) (fmap Right answer)
           bracks (term `sepBy1` punct Comma)
           <|> return []
         lookup :: (Ord a, Hashable a) => Map BS.ByteString a -> BS.ByteString -> a
-        lookup m x = Map.findWithDefault (error "runE: result from E mentions free names") x m
\ No newline at end of file
+        lookup m x = Map.findWithDefault (error "runE: result from E mentions free names") x m
diff --git a/Sat.hs b/Jukebox/Sat.hs
similarity index 98%
rename from Sat.hs
rename to Jukebox/Sat.hs
index 8253c79..240902c 100644
--- a/Sat.hs
+++ b/Jukebox/Sat.hs
@@ -1,4 +1,4 @@
-module Sat
+module Jukebox.Sat
   ( Solver
   , newSolver
   , deleteSolver
diff --git a/Sat3.hs b/Jukebox/Sat3.hs
similarity index 96%
rename from Sat3.hs
rename to Jukebox/Sat3.hs
index d9a2bf8..c6e19b4 100644
--- a/Sat3.hs
+++ b/Jukebox/Sat3.hs
@@ -1,6 +1,6 @@
-module Sat3 where
+module Jukebox.Sat3 where
 
-import Sat
+import Jukebox.Sat
 
 --------------------------------------------------------------------------------
 
diff --git a/SatEq.hs b/Jukebox/SatEq.hs
similarity index 95%
rename from SatEq.hs
rename to Jukebox/SatEq.hs
index 2d77b42..5298af9 100644
--- a/SatEq.hs
+++ b/Jukebox/SatEq.hs
@@ -1,8 +1,8 @@
-module SatEq where
+module Jukebox.SatEq where
 
-import Sat
-import Sat3
-import SatMin
+import Jukebox.Sat
+import Jukebox.Sat3
+import Jukebox.SatMin
 
 import Data.IORef
 import Data.Map as M
diff --git a/SatMin.hs b/Jukebox/SatMin.hs
similarity index 95%
rename from SatMin.hs
rename to Jukebox/SatMin.hs
index 3d5073d..72bf1eb 100644
--- a/SatMin.hs
+++ b/Jukebox/SatMin.hs
@@ -1,6 +1,6 @@
-module SatMin where
+module Jukebox.SatMin where
 
-import Sat
+import Jukebox.Sat
 
 solveLocalMin :: SatSolver s => s -> [Lit] -> [Lit] -> IO Bool
 solveLocalMin s as ms =
diff --git a/Seq.hs b/Jukebox/Seq.hs
similarity index 99%
rename from Seq.hs
rename to Jukebox/Seq.hs
index ec1c71b..f6e0339 100644
--- a/Seq.hs
+++ b/Jukebox/Seq.hs
@@ -1,5 +1,5 @@
 -- Strict lists with efficient append.
-module Seq where
+module Jukebox.Seq where
 
 import Prelude hiding (concat, concatMap, length, mapM, mapM_)
 import Control.Monad hiding (mapM, mapM_)
diff --git a/TPTP/ClauseParser.hs b/Jukebox/TPTP/ClauseParser.hs
similarity index 96%
rename from TPTP/ClauseParser.hs
rename to Jukebox/TPTP/ClauseParser.hs
index 669b5dd..df93211 100644
--- a/TPTP/ClauseParser.hs
+++ b/Jukebox/TPTP/ClauseParser.hs
@@ -1,30 +1,30 @@
 -- Parse and typecheck TPTP clauses, stopping at include-clauses.
 
 {-# LANGUAGE BangPatterns, MultiParamTypeClasses, ImplicitParams, FlexibleInstances, TypeOperators, TypeFamilies #-}
-module TPTP.ClauseParser where
+module Jukebox.TPTP.ClauseParser where
 
-import TPTP.Parsec
+import Jukebox.TPTP.Parsec
 import Control.Applicative
 import Control.Monad
 import qualified Data.ByteString.Lazy.Char8 as BSL
 import qualified Data.ByteString.Char8 as BS
-import qualified Map
-import Map(Map)
-import qualified Seq as S
-import Seq(Seq)
+import qualified Jukebox.Map as Map
+import Jukebox.Map(Map)
+import qualified Jukebox.Seq as S
+import Jukebox.Seq(Seq)
 import Data.List
-import TPTP.Print
-import Name hiding (name)
-import qualified NameMap
+import Jukebox.TPTP.Print
+import Jukebox.Name hiding (name)
+import qualified Jukebox.NameMap as NameMap
 
-import TPTP.Lexer hiding
+import Jukebox.TPTP.Lexer hiding
   (Pos, Error, Include, Var, Type, Not, ForAll,
    Exists, And, Or, Type, Apply, Implies, Follows, Xor, Nand, Nor,
    keyword, defined, kind)
-import qualified TPTP.Lexer as L
-import qualified Form
-import Form hiding (tag, kind, Axiom, Conjecture, Question, newFunction, TypeOf(..))
-import qualified Name
+import qualified Jukebox.TPTP.Lexer as L
+import qualified Jukebox.Form as Form
+import Jukebox.Form hiding (tag, kind, Axiom, Conjecture, Question, newFunction, TypeOf(..))
+import qualified Jukebox.Name as Name
 
 -- The parser monad
 
diff --git a/TPTP/FindFile.hs b/Jukebox/TPTP/FindFile.hs
similarity index 94%
rename from TPTP/FindFile.hs
rename to Jukebox/TPTP/FindFile.hs
index f394b6c..cc161d1 100644
--- a/TPTP/FindFile.hs
+++ b/Jukebox/TPTP/FindFile.hs
@@ -1,4 +1,4 @@
-module TPTP.FindFile where
+module Jukebox.TPTP.FindFile where
 
 import System.FilePath
 import System.Directory(doesFileExist)
@@ -7,7 +7,7 @@ import Control.Applicative
 import Control.Exception
 import Control.Monad
 import Prelude hiding (catch)
-import Options
+import Jukebox.Options
 import Data.Traversable(sequenceA)
 
 findFile :: [FilePath] -> FilePath -> IO (Maybe FilePath)
@@ -38,4 +38,4 @@ findFileFlags =
       []
       argFiles,
     io getTPTPDirs
-    ]
\ No newline at end of file
+    ]
diff --git a/TPTP/Lexer.x b/Jukebox/TPTP/Lexer.x
similarity index 99%
rename from TPTP/Lexer.x
rename to Jukebox/TPTP/Lexer.x
index c5ea7f4..b23c068 100644
--- a/TPTP/Lexer.x
+++ b/Jukebox/TPTP/Lexer.x
@@ -4,7 +4,7 @@
 {
 {-# OPTIONS_GHC -O2 -fno-warn-deprecated-flags #-}
 {-# LANGUAGE BangPatterns #-}
-module TPTP.Lexer(
+module Jukebox.TPTP.Lexer(
   scan,
   Pos(..),
   Token(..),
diff --git a/TPTP/ParseProblem.hs b/Jukebox/TPTP/ParseProblem.hs
similarity index 91%
rename from TPTP/ParseProblem.hs
rename to Jukebox/TPTP/ParseProblem.hs
index 066c8e0..b96353e 100644
--- a/TPTP/ParseProblem.hs
+++ b/Jukebox/TPTP/ParseProblem.hs
@@ -1,22 +1,22 @@
 {-# LANGUAGE ScopedTypeVariables #-}
-module TPTP.ParseProblem where
+module Jukebox.TPTP.ParseProblem where
 
-import ProgressBar
-import TPTP.FindFile
-import TPTP.ClauseParser
-import TPTP.Lexer hiding (Include, Error)
-import TPTP.Parsec
-import TPTP.Print
-import qualified TPTP.Lexer as L
+import Jukebox.ProgressBar
+import Jukebox.TPTP.FindFile
+import Jukebox.TPTP.ClauseParser
+import Jukebox.TPTP.Lexer hiding (Include, Error)
+import Jukebox.TPTP.Parsec
+import Jukebox.TPTP.Print
+import qualified Jukebox.TPTP.Lexer as L
 import Control.Monad.Error
-import Form hiding (Pos)
+import Jukebox.Form hiding (Pos)
 import qualified Data.ByteString.Lazy.Char8 as BSL
 import qualified Data.ByteString.Char8 as BS
 import Control.Monad.Identity
 import Control.Exception
 import Prelude hiding (catch)
 import Data.List
-import Name
+import Jukebox.Name
 
 parseProblem :: [FilePath] -> FilePath -> IO (Either String (Problem Form))
 parseProblem dirs name = withProgressBar $ \pb -> parseProblemWith (findFileTPTP dirs) pb name
diff --git a/TPTP/ParseSnippet.hs b/Jukebox/TPTP/ParseSnippet.hs
similarity index 86%
rename from TPTP/ParseSnippet.hs
rename to Jukebox/TPTP/ParseSnippet.hs
index c30c49d..5c7e20b 100644
--- a/TPTP/ParseSnippet.hs
+++ b/Jukebox/TPTP/ParseSnippet.hs
@@ -1,16 +1,16 @@
 -- Parse little bits of TPTP, e.g. a prelude for a particular tool.
 
-module TPTP.ParseSnippet where
+module Jukebox.TPTP.ParseSnippet where
 
-import TPTP.ClauseParser
-import TPTP.Parsec
-import TPTP.Lexer
-import Name
-import Form
+import Jukebox.TPTP.ClauseParser as TPTP.ClauseParser
+import Jukebox.TPTP.Parsec as TPTP.Parsec
+import Jukebox.TPTP.Lexer
+import Jukebox.Name
+import Jukebox.Form
 import qualified Data.ByteString.Lazy.Char8 as BSL
 import qualified Data.ByteString.Char8 as BS
 import Control.Applicative
-import qualified Map
+import qualified Jukebox.Map as Map
 import Data.List
 
 tff, cnf :: [(String, Type)] -> [(String, Function)] -> String -> NameM Form
diff --git a/TPTP/Parsec.hs b/Jukebox/TPTP/Parsec.hs
similarity index 99%
rename from TPTP/Parsec.hs
rename to Jukebox/TPTP/Parsec.hs
index 1f4c203..e182533 100644
--- a/TPTP/Parsec.hs
+++ b/Jukebox/TPTP/Parsec.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE RankNTypes, BangPatterns, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, TypeFamilies #-}
-module TPTP.Parsec where
+module Jukebox.TPTP.Parsec where
 
 import Control.Applicative
 import Control.Monad
diff --git a/TPTP/Print.hs b/Jukebox/TPTP/Print.hs
similarity index 95%
rename from TPTP/Print.hs
rename to Jukebox/TPTP/Print.hs
index d9d296a..1b7caef 100644
--- a/TPTP/Print.hs
+++ b/Jukebox/TPTP/Print.hs
@@ -1,19 +1,19 @@
 -- Pretty-printing of formulae. WARNING: icky code inside!
 {-# LANGUAGE FlexibleContexts, TypeSynonymInstances, TypeOperators, FlexibleInstances #-}
-module TPTP.Print(prettyShow, chattyShow, prettyFormula, prettyProblem, Level(..), Pretty)
+module Jukebox.TPTP.Print(prettyShow, chattyShow, prettyFormula, prettyProblem, Level(..), Pretty)
        where
 
 import qualified Data.ByteString.Char8 as BS
 import Data.Char
 import Text.PrettyPrint.HughesPJ
-import qualified TPTP.Lexer as L
-import Form
+import qualified Jukebox.TPTP.Lexer as L
+import Jukebox.Form
 import Data.List
-import qualified Map
-import qualified Seq as S
-import qualified NameMap
-import NameMap(NameMap)
-import Name
+import qualified Jukebox.Map as Map
+import qualified Jukebox.Seq as S
+import qualified Jukebox.NameMap as NameMap
+import Jukebox.NameMap(NameMap)
+import Jukebox.Name
 
 data Level = Normal | Chatty deriving (Eq, Ord)
 
diff --git a/Toolbox.hs b/Jukebox/Toolbox.hs
similarity index 94%
rename from Toolbox.hs
rename to Jukebox/Toolbox.hs
index faedf33..da2bcc3 100644
--- a/Toolbox.hs
+++ b/Jukebox/Toolbox.hs
@@ -1,23 +1,23 @@
-module Toolbox where
+module Jukebox.Toolbox where
 
-import Options
+import Jukebox.Options
 import qualified Data.ByteString.Char8 as BS
-import Form
-import Name
-import qualified NameMap
-import TPTP.Print
+import Jukebox.Form
+import Jukebox.Name
+import qualified Jukebox.NameMap as NameMap
+import Jukebox.TPTP.Print
 import Control.Monad
 import Control.Applicative
-import Clausify
-import TPTP.ParseProblem
-import Monotonox.Monotonicity hiding (guards)
-import Monotonox.ToFOF
+import Jukebox.Clausify
+import Jukebox.TPTP.ParseProblem
+import Jukebox.Monotonox.Monotonicity hiding (guards)
+import Jukebox.Monotonox.ToFOF
 import System.Exit
 import System.IO
-import TPTP.FindFile
+import Jukebox.TPTP.FindFile
 import Text.PrettyPrint.HughesPJ
-import GuessModel
-import InferTypes
+import Jukebox.GuessModel
+import Jukebox.InferTypes
 
 (=>>=) :: (Monad m, Applicative f) => f (a -> m b) -> f (b -> m c) -> f (a -> m c)
 f =>>= g = (>=>) <$> f <*> g
@@ -199,4 +199,4 @@ printInferredBox = pure $ \(prob, rep) -> do
   return prob
 
 equinoxBox :: OptionParser (Problem Clause -> IO Answer)
-equinoxBox = pure (\f -> return (NoAnswer GaveUp)) -- A highly sophisticated proof method. We are sure to win CASC! :)
\ No newline at end of file
+equinoxBox = pure (\f -> return (NoAnswer GaveUp)) -- A highly sophisticated proof method. We are sure to win CASC! :)
diff --git a/UnionFind.hs b/Jukebox/UnionFind.hs
similarity index 90%
rename from UnionFind.hs
rename to Jukebox/UnionFind.hs
index 5b62703..6a1f2b7 100644
--- a/UnionFind.hs
+++ b/Jukebox/UnionFind.hs
@@ -1,10 +1,10 @@
-module UnionFind(UF, Replacement((:>)), (=:=), rep, evalUF, execUF, runUF, S, isRep, initial, reps) where
+module Jukebox.UnionFind(UF, Replacement((:>)), (=:=), rep, evalUF, execUF, runUF, S, isRep, initial, reps) where
 
 import Prelude hiding (min)
 import Control.Monad.State.Strict
 import Data.Hashable
-import Map(Map)
-import qualified Map
+import Jukebox.Map(Map)
+import qualified Jukebox.Map as Map
 
 type S a = Map a a
 type UF a = State (S a)
diff --git a/Utils.hs b/Jukebox/Utils.hs
similarity index 94%
rename from Utils.hs
rename to Jukebox/Utils.hs
index 2f3fbb3..b77cb30 100644
--- a/Utils.hs
+++ b/Jukebox/Utils.hs
@@ -1,7 +1,7 @@
-module Utils where
+module Jukebox.Utils where
 
 import Data.List
-import qualified Seq as Seq
+import qualified Jukebox.Seq as Seq
 import qualified Data.HashSet as Set
 import Data.Hashable
 import System.Process
diff --git a/Main.hs b/Main.hs
index 0eab6c4..9de238c 100644
--- a/Main.hs
+++ b/Main.hs
@@ -1,10 +1,10 @@
 module Main where
 
 import Control.Monad
-import Options
+import Jukebox.Options
 import Control.Applicative
 import Data.Monoid
-import Toolbox
+import Jukebox.Toolbox
 
 tools = mconcat [fof, cnf, monotonox, justparser, guessmodel, equinox]
 
diff --git a/UniverseTH.hs b/UniverseTH.hs
deleted file mode 100644
index 257d170..0000000
--- a/UniverseTH.hs
+++ /dev/null
@@ -1,59 +0,0 @@
--- Template Haskell stuff to help with the Symbolic class.
-
-{-# LANGUAGE TemplateHaskell #-}
-module UniverseTH where
-
-import Language.Haskell.TH
-import Control.Monad
-import Data.List
-
-data Constructor = C Name [TyVarBndr] Cxt Type deriving Show
-
-constructors :: Name -> Q [Constructor]
-constructors ty = do
-  TyConI (DataD _ _  _ cons _) <- reify ty
-  let name (NormalC x _) = x
-      name (ForallC _ _ x) = name x
-      norm n (ForallT tvs ctx (AppT _ ty)) = C n tvs ctx ty
-      norm n (AppT _ ty) = C n [] [] ty
-  forM cons $ \x -> do
-    DataConI n t _ _ <- reify (name x)
-    return (norm n t)
-
-symbolicInstances :: Name -> Name -> Name -> Q [Dec]
-symbolicInstances ty cls typeRep = do
-  cs <- constructors ty
-  forM cs $ \(C n tvs ctx ty) -> do
-    let con = return (ConE n)
-    decl <- [d| typeRep _ = $(con) |]
-    return (InstanceD ctx (AppT (ConT cls) ty) decl)
-
-mkUnpack :: Name -> ExpQ -> ExpQ -> ExpQ
-mkUnpack ty unpack typeRep = do
-  cs <- constructors ty
-  let constructor (C n tvs cxt ty) = do
-        e <- unpack
-        return (Match (ConP n []) (NormalB e) [])
-  liftM2 CaseE typeRep (mapM constructor cs)
-
-specialiseSymbolic :: Name -> Name -> [Q Type] -> Q [Dec]
-specialiseSymbolic cls f tys = aux -- `recover` error "Couldn't specialise symbolic function"
-  where
-    aux = do
-      VarI _ ty@(ForallT _ ctx _) _ _ <- reify f
-      tys' <- sequence tys
-      let sym = [ v | ClassP cls' [v] <- ctx, cls == cls' ]
-          instances = sequence [ [ (v, ty) | ty <- tys' ] | v <- sym ]
-          subst s (ForallT tys ctx ty) =
-            ForallT (tys \\ [ PlainTV v | (VarT v, _) <- s ])
-                    (ctx \\ [ ClassP cls [v] | (v, _) <- s ])
-                    (subst s ty)
-          subst s ty@VarT{} =
-            case lookup ty s of
-              Nothing -> ty
-              Just ty' -> ty'
-          subst s (SigT ty k) = SigT (subst s ty) k
-          subst s (AppT t u) = AppT (subst s t) (subst s u)
-          subst s ty = ty
-      return [ PragmaD (SpecialiseP f (subst inst ty) Nothing)
-             | inst <- instances ]
diff --git a/jukebox.cabal b/jukebox.cabal
index 4ffbbc8..725704d 100644
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,6 +1,6 @@
 Name: jukebox
 Version: 0
-Cabal-version: >= 1.2
+Cabal-version: >= 1.8
 Build-type: Simple
 
 Extra-Source-Files: build scripts/fetch-minisat scripts/install-minisat scripts/gcc-static-minisat
@@ -12,31 +12,48 @@ Flag static
 Library
   Build-depends: bytestring, base >= 4 && < 5, array, mtl, directory,
     filepath, pretty, hashable, minisat,
-    binary, unordered-containers, process
+    binary, unordered-containers, process, containers
   Build-tools: alex
   Ghc-options: -funfolding-use-threshold=500
   if flag(static)
     Ghc-options: -pgml scripts/gcc-static-minisat
   Exposed-modules:
-    Clausify
-    Form
-    HighSat
-    InferTypes
-    Monotonox.Monotonicity
-    Monotonox.ToFOF
-    Name
-    NameMap
-    Options
-    ProgressBar
-    Seq
-    Toolbox
-    TPTP.ClauseParser
-    TPTP.FindFile
-    TPTP.Lexer
-    TPTP.Parsec
-    TPTP.ParseProblem
-    TPTP.Print
-    Utils
+    Jukebox.Clausify
+    Jukebox.Form
+    Jukebox.GuessModel
+    Jukebox.HighSat
+    Jukebox.InferTypes
+    Jukebox.Map
+    Jukebox.Monotonox.Monotonicity
+    Jukebox.Monotonox.ToFOF
+    Jukebox.Name
+    Jukebox.NameMap
+    Jukebox.Options
+    Jukebox.ProgressBar
+    Jukebox.Provers.E
+    Jukebox.Sat3
+    Jukebox.SatEq
+    Jukebox.Sat
+    Jukebox.SatMin
+    Jukebox.Seq
+    Jukebox.Toolbox
+    Jukebox.TPTP.ClauseParser
+    Jukebox.TPTP.FindFile
+    Jukebox.TPTP.Lexer
+    Jukebox.TPTP.Parsec
+    Jukebox.TPTP.ParseProblem
+    Jukebox.TPTP.ParseSnippet
+    Jukebox.TPTP.Print
+    Jukebox.UnionFind
+    Jukebox.Utils
 
 Executable jukebox
-  Main-is: Main.hs
\ No newline at end of file
+  Main-is: Main.hs
+  Build-depends: bytestring, base >= 4 && < 5, array, mtl, directory,
+    filepath, pretty, hashable, minisat,
+    binary, unordered-containers, process, containers,
+    jukebox
+  Build-tools: alex
+  Ghc-options: -funfolding-use-threshold=500
+  if flag(static)
+    Ghc-options: -pgml scripts/gcc-static-minisat
diff --git a/scripts/make-tarball b/scripts/make-tarball
index ae90f08..94d2442 100755
--- a/scripts/make-tarball
+++ b/scripts/make-tarball
@@ -20,6 +20,6 @@ mv scratch/jukebox.tar.gz .
 rm -r scratch
 
 if [ x$1 = xupload ]; then
-    scp jukebox.tar.gz nicsma@remote12.chalmers.se:www/www.cse.chalmers.se
-    ssh nicsma@remote12.chalmers.se chmod a+r www/www.cse.chalmers.se/jukebox.tar.gz
+    scp jukebox.tar.gz nicsma@remote12.chalmers.se:www/www.cse.chalmers.se/files
+    ssh nicsma@remote12.chalmers.se chmod a+r www/www.cse.chalmers.se/files/jukebox.tar.gz
 fi