diff --git a/LojbanTools.hs b/LojbanTools.hs
deleted file mode 100644
--- a/LojbanTools.hs
+++ /dev/null
@@ -1,46 +0,0 @@
-module LojbanTools (
-	getSentences,
-	headTerms,
-	bridiTail,
-	selbri,
-	tailTerms,
-	snd3
-) where
-
-import Language.Lojban.Parser hiding (LA, Brivla, KOhA, GOhA, NA, LerfuString)
-import qualified Language.Lojban.Parser as P
-import System.Environment
-import Data.Maybe
-import Data.Either
-import Data.List
-
-getSentences :: Sentence -> [Sentence]
-getSentences (TopText _ _ _ _ (Just t) _) = getSentences t
-getSentences (IText_1 _ _ _ _ (Just t)) = getSentences t
-getSentences (StatementI s1 ss) = s1 : catMaybes (map (\(_, _, s) -> s) ss)
-getSentences tbt@(TermsBridiTail _ _ _ _) = [tbt]
-getSentences o = error $ show o
-
-headTerms :: Sentence -> [Sumti]
-headTerms (TermsBridiTail ts _ _ _) = ts
-headTerms _ = []
-
-bridiTail :: Sentence -> Sentence
-bridiTail (TermsBridiTail _ _ _ bt) = bt
-bridiTail o = o
-
-selbri :: Sentence -> Selbri
-selbri (Selbri s) = s
-selbri (SelbriTailTerms s _ _ _) = s
-selbri t = error $ show t -- P.Brivla ([], "", []) []
-
-tailTerms :: Sentence -> [Sumti]
-tailTerms (SelbriTailTerms _ ts _ _) = ts
-tailTerms _ = []
-
-readSumtiTail :: SumtiTail -> String
-readSumtiTail (SelbriRelativeClauses (P.Brivla (_, n, _) _) _) = n
-readSumtiTail st = show st
-
-snd3 :: (a, b, c) -> b
-snd3 (_, y, _) = y
diff --git a/NotUnif.hs b/NotUnif.hs
deleted file mode 100644
--- a/NotUnif.hs
+++ /dev/null
@@ -1,81 +0,0 @@
-module NotUnif (
-	checkAll,
-	checkNot,
-	deleteFromNot,
-	notUnification
-) where
-
-import Unif
-import Control.Applicative
-import Data.Maybe
-
--- checkAll :: [([Term], Maybe Term)] -> [Maybe [(Term, Term)]] -> Bool
-checkAll r [] = True
-checkAll r (Nothing : nots) = checkAll r nots
-checkAll r (Just [] : nots) = checkAll r nots
-checkAll r (Just n : nots) =
-	checkNot r (deleteFromNot r n) && checkAll r nots
-
--- deleteFromNot :: [([Term], Maybe Term)] -> [(Term, Term)] -> [(Term, Term)]
-deleteFromNot _ [] = []
-deleteFromNot r ((t@(Var _ _), u@(Var _ _)) : ps)
-	| null $ filter ((t `elem`) . fst) r = deleteFromNot r ps
-	| null $ filter ((u `elem`) . fst) r = deleteFromNot r ps
-	| otherwise = (t, u) : deleteFromNot r ps
-deleteFromNot r ((t, u) : ps) = (t, u) : deleteFromNot r ps
-
--- checkNot :: [([Term], Maybe Term)] -> [(Term, Term)] -> Bool
-checkNot _ [] = False
-checkNot r ((t@(Var _ _), u@(Var _ _)) : ps)
-	= null (filter ((\vs -> t `elem` vs && u `elem` vs) . fst) r) ||
---		null (filter ((t `elem`) .fst) r) ||
---		null (filter ((u `elem`) .fst) r) ||
-		checkNot r ps
-checkNot r ((t@(Var _ _), u) : ps)
-	= snd (head $ filter ((t `elem`) . fst) r) /= Just u || checkNot r ps
-
--- notUnification :: 
-notUnification ts us = simplify <$> notUnifies ts us
-
--- notUnify :: Term -> Term -> Maybe (Maybe (Term, Term))
-notUnify t u | t == u = Nothing
-notUnify t@(Con _) u@(Con _) = Just Nothing
-notUnify t u = Just $ Just (t, u)
-
--- notUnifies :: [Term] -> [Term] -> Maybe [(Term, Term)]
-notUnifies [] [] = Nothing
-notUnifies [t] [u] = maybeToList <$> notUnify t u
-notUnifies (t : ts) (u : us) = case notUnify t u of
-	Nothing -> notUnifies ts us
-	Just Nothing -> Just []
-	Just (Just p) -> case notUnifies ts us of
-		Nothing -> Just [p]
-		Just [] -> Just []
-		Just ps -> Just $ p : ps
-notUnifies _ _ = Just []
-
--- simplify :: [(Term, Term)] -> [(Term, Term)]
-simplify :: (Eq sc, Eq s) =>
-	[(Term sc s, Term sc s)] -> [(Term sc s, Term sc s)]
-simplify = checkSame . map (uncurry order)
-
--- checkSame :: [(Term, Term)] -> [(Term, Term)]
-checkSame :: (Eq sc, Eq s) =>
-	[(Term sc s, Term sc s)] -> [(Term sc s, Term sc s)]
-checkSame [] = []
-checkSame (p : ps) = catMaybes (map (isSame p) ps) ++ p : checkSame ps
-
--- isSame :: (Term, Term) -> (Term, Term) -> Maybe (Term, Term)
-isSame :: Eq a => (a, a) -> (a, a) -> Maybe (a, a)
-isSame (x, y) (z, w)
-	| x == z = Just (y, w)
-	| y == w = Just (x, z)
-	| x == w = Just (y, z)
-	| y == z = Just (x, w)
-	| otherwise = Nothing
-
--- order :: Term -> Term -> (Term, Term)
-order (Con _) (Con _) = error "not occur"
-order t@(Var _ _) u@(Con _) = (t, u)
-order t@(Con _) u@(Var _ _) = (u, t)
-order t u = (t, u)
diff --git a/Prolog2.hs b/Prolog2.hs
deleted file mode 100644
--- a/Prolog2.hs
+++ /dev/null
@@ -1,31 +0,0 @@
-module Prolog2 (
-	ask,
-	Fact,
---	Unify(..),
-	Rule(..),
-	Term(..),
-	TwoD(..),
-	Result
-) where
-
-import PrologTools
-import Unif
-import Data.Maybe
-
-ask :: (TwoD sc, Eq sc, Eq s) =>
-	sc -> Result sc s -> Fact sc s -> [Rule sc s] -> [Result sc s]
-ask sc ret q rs =
-	concat $ zipWith (\sc r -> askrule sc ret q r rs) (iterate next $ down sc) rs
-
-askrule :: (TwoD sc, Eq sc, Eq s) =>
-	sc -> Result sc s -> Fact sc s -> Rule sc s -> [Rule sc s] -> [Result sc s]
-askrule sc ret q r@(Rule fact _ facts notFacts) rs =
-	filter (flip checkAll nots) ret'
-	where
-	ret' = foldl (\rets (sc', f) -> rets >>= \r -> ask sc' r f rs) r0 $ zip (iterate next sc0) $
-		map (const . ($ sc0)) facts
-	sc0 = down sc
-	r0 = case (q sc) `unification` (fact sc0) of
-		Nothing -> []
-		Just r0' -> maybeToList $ ret `merge` r0'
-	nots = concat $ map ((flip (notAsk sc0) rs) . const . ($sc0)) notFacts
diff --git a/PrologTools.hs b/PrologTools.hs
deleted file mode 100644
--- a/PrologTools.hs
+++ /dev/null
@@ -1,48 +0,0 @@
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE FlexibleInstances #-}
-
-module PrologTools (
-	TwoD(..),
-	Fact,
-	NotFact,
-	Rule(..),
-	notAsk,
-	checkAll
-) where
-
-import Unif
-import NotUnif
-import Control.Applicative
-
-class TwoD td where
-	next :: td -> td
-	down :: td -> td
-
-type Fact sc s = sc -> [Term sc s]
-type NotFact sc s = Fact sc s
-data Unify sc s
-	= Unify (Term sc s) (Term sc s)
-	| NotUnify (Term sc s) (Term sc s)
-	deriving Show
-data Rule sc s = Rule (Fact sc s) [Unify sc s] [Fact sc s] [NotFact sc s]
-
-notAsk :: (TwoD sc, Eq sc, Eq s) => sc ->
-	Fact sc s -> [Rule sc s] -> [Maybe [(Term sc s, Term sc s)]]
-notAsk sc q rs = zipWith (\sc r -> notAskRule sc q r rs) (iterate next $ down sc) rs
-
-notAskRule :: (TwoD sc, Eq sc, Eq s) => sc ->
-	Fact sc s -> Rule sc s -> [Rule sc s] -> Maybe [(Term sc s, Term sc s)]
-notAskRule sc q r@(Rule fact unify facts notFacts) rs = liftA concat $
-	case match of
-		Nothing -> Just []
-		Just _ ->
-			liftA2 (:) start $ maybeOut $ concat $
-				map ((flip (notAsk sc) rs) . const . ($ sc)) facts
-	where
-	start = notUnification (q sc) $ fact sc
-	match = unification [head $ q sc] [head $ fact sc]
-
-maybeOut :: [Maybe a] -> Maybe [a]
-maybeOut [] = Just []
-maybeOut (Nothing : xs) = Nothing
-maybeOut (Just x : xs) = maybe Nothing (Just . (x :)) $ maybeOut xs
diff --git a/Unif.hs b/Unif.hs
deleted file mode 100644
--- a/Unif.hs
+++ /dev/null
@@ -1,180 +0,0 @@
-module Unif (
-	unification,
-	merge,
-	Term(..),
-	checkSimple2,
-	simplify2All,
-	Result
-) where
-
-import Control.Applicative
-import Data.List hiding (deleteBy)
-import Data.Maybe
-
-data Term sc s = Con s | Var sc s deriving (Eq, Show)
-
-type Result sc s = [([Term sc s], Maybe (Term sc s))]
-
-merge :: (Eq sc, Eq s) => Result sc s -> Result sc s -> Maybe (Result sc s)
-merge [] uss = Just $ simplify2All uss
-merge (tsv@(ts, v1) : tss) uss = case us of
-	[] -> merge tss $ tsv : uss
-	(us, v2) : rest -> case mergeValue v1 v2 of
-		Nothing -> Nothing
-		Just v	| not $ allEqual $ v2 : map snd rest -> Nothing
-			| otherwise -> merge tss $
-				(foldr union (union ts us) $ map fst rest, v) : uss'
-	where
-	us = filterElems ts uss
-	uss' = deleteElems' ts uss
-
-allEqual :: Eq a => [a] -> Bool
-allEqual [x] = True
-allEqual (x : y : xs) = x == y && allEqual (y : xs)
-
-mergeValue :: Eq a => Maybe a -> Maybe a -> Maybe (Maybe a)
-mergeValue x@(Just _) y@(Just _)
-	| x == y = Just x
-	| otherwise = Nothing
-mergeValue x@(Just _) _ = Just x
-mergeValue _ y = Just y
-
-unification :: (Eq sc, Eq s) => [Term sc s] -> [Term sc s] -> Maybe (Result sc s)
-unification ts us = simplify2All <$> (simplify =<< unifies ts us)
--- unification ts us = (simplify =<< unifies ts us)
-
--- unify :: Term -> Term -> Maybe (Maybe (Term, Term))
-unify t u | t == u = Just Nothing
-unify t@(Con _) u@(Con _) = Nothing
-unify t u = Just $ Just (t, u)
-
--- unifies :: [Term] -> [Term] -> Maybe [(Term, Term)]
-unifies [] [] = Just []
-unifies (t : ts) (u : us) = case unify t u of
-	Nothing -> Nothing
-	Just Nothing -> unifies ts us
-	Just (Just p) -> (p :) <$> unifies ts us
-unifies _ _ = Nothing
-
--- before form is bellow
--- [(X, A), (A, Y), (B, Z), (hoge, B)] -- no (hoge, hage) or (B, B)
--- (Var _, Var _), (Con _, Var _), (Var _, Con _)
--- simplified form is bellow
--- [([X, A, Y], Nothing), ([Z, B], Just hoge)]
-
--- test data
--- a, b, x, y, hoge :: Term
-a = Var "" "A"
-b = Var "" "B"
-x = Var "" "X"
-y = Var "" "Y"
-z = Var "" "Z"
-hoge = Con "hoge"
--- before :: [(Term, Term)]
-before = [(x, a), (a, y), (b, z), (hoge, b)]
-
-simplify2All :: (Eq sc, Eq s) => Result sc s -> Result sc s
-simplify2All ps
-	| checkSimple2 ps = ps
-	| otherwise = simplify2All $ simplify2 ps
-
-checkSimple2 :: (Eq sc, Eq s) => Result sc s -> Bool
-checkSimple2 = notDup' . map snd
-
-notDup' :: Eq a => [Maybe a] -> Bool
-notDup' [] = True
-notDup' (Nothing : xs) = notDup' xs
-notDup' (Just x : xs)
-	| x `elem` (catMaybes xs) = False
-	| otherwise = notDup' xs
-
-notDup :: Eq a => [a] -> Bool
-notDup [] = True
-notDup (x : xs)
-	| x `elem` xs = False
-	| otherwise = notDup xs
-
-simplify2 [] = []
-simplify2 ((ts, v@(Just _)) : ps) = (maybe ts (ts ++) ts', v) : simplify2 ps'
-	where
-	ts' = lookupSnd v ps
-	ps' = deleteSnd v ps
-simplify2 (p : ps) = p : simplify2 ps
-
-lookupSnd :: Eq b => b -> [(a, b)] -> Maybe a
-lookupSnd x = lookup x . map (\(y, z) -> (z, y))
-
-deleteSnd :: Eq b => b -> [(a, b)] -> [(a, b)]
-deleteSnd x = filter ((/= x) . snd)
-
--- simplify :: [(Term, Term)] -> Maybe [([Term], Maybe Term)]
-simplify [] = Just []
-simplify ((Con _, Con _) : _) = error "bad before data"
-simplify ((t@(Var _ _), u@(Var _ _)) : ps) = case simplify ps of
-	Nothing -> Nothing
-	Just ps' -> case (lookupElem t ps', lookupElem u ps') of
-		(Just (ts, Just v1), Just (us, Just v2))
-			| v1 == v2 -> Just $ (union ts us, Just v1) :
-				deleteElem t (deleteElem u ps')
-			| otherwise -> Nothing
-		(Just (ts, Just v1), Just (us, _)) ->
-			Just $ (union ts us, Just v1) :
-				deleteElem t (deleteElem u ps')
-		(Just (ts, _), Just (us, v2)) ->
-			Just $ (union ts us, v2) :
-				deleteElem t (deleteElem u ps')
-		(Just (ts, v1), _) -> Just $ (u : ts, v1) : deleteElem t ps'
-		(_, Just (us, v2)) -> Just $ (t : us, v2) : deleteElem u ps'
-		(_, _) -> Just $ ([t, u], Nothing) : ps'
-simplify ((t@(Var _ _), u) : ps) = case simplify ps of
-	Nothing -> Nothing
-	Just ps' -> case lookupElem t ps' of
-		Just (ts, Just v1)
-			| u == v1 -> Just ps'
-			| otherwise -> Nothing
-		Just (ts, _) -> Just $ (ts, Just u) : deleteElem t ps'
-		_ -> Just $ ([t], Just u) : ps'
-simplify ((t, u) : ps) = case simplify ps of
-	Nothing -> Nothing
-	Just ps' -> case lookupElem u ps' of
-		Just (us, Just v2)
-			| t == v2 -> Just ps'
-			| otherwise -> Nothing
-		Just (us, _) -> Just $ (us, Just t) : deleteElem u ps'
-		_ -> Just $ ([u], Just t) : ps'
-
-deleteElems :: Eq a => [a] -> [([a], b)] -> [([a], b)]
-deleteElems = deleteBy $ \x y -> not $ null $ intersect x y
-
-deleteElems' :: Eq a => [a] -> [([a], b)] -> [([a], b)]
-deleteElems' xs = filter $ \ys -> null $ intersect xs $ fst ys
-
-deleteBy :: (a -> b -> Bool) -> a -> [(b, c)] -> [(b, c)]
-deleteBy _ _ [] = []
-deleteBy p x ((y, z) : ps)
-	| p x y = ps
-	| otherwise = (y, z) : deleteBy p x ps
-
-deleteElem :: Eq a => a -> [([a], b)] -> [([a], b)]
-deleteElem _ [] = []
-deleteElem x ((xs, y) : ps)
-	| x `elem` xs = ps
-	| otherwise = (xs, y) : deleteElem x ps
-
-filterElems :: Eq a => [a] -> [([a], b)] -> [([a], b)]
-filterElems xs = filter (\ys -> not $ null $ intersect xs $ fst ys)
-
-lookupElems :: Eq a => [a] -> [([a], b)] -> Maybe ([a], b)
-lookupElems = lookupBy $ \x y -> not $ null $ intersect x y
-
-lookupBy :: (a -> b -> Bool) -> a -> [(b, c)] -> Maybe (b, c)
-lookupBy _ _ [] = Nothing
-lookupBy p x ((y, z) :ps)
-	| p x y = Just (y, z)
-	| otherwise = lookupBy p x ps
-
-lookupElem :: Eq a => a -> [([a], b)] -> Maybe ([a], b)
-lookupElem _ [] = Nothing
-lookupElem x ((xs, y) : ps)
-	| x `elem` xs = Just (xs, y)
-	| otherwise = lookupElem x ps
diff --git a/examples/gugde.jbo b/examples/gugde.jbo
deleted file mode 100644
--- a/examples/gugde.jbo
+++ /dev/null
@@ -1,19 +0,0 @@
-.i lo kamxu'e cu drata lo kamri'o
-.i lo kamxu'e cu drata lo kambla
-
-.i lo kamri'o cu drata lo kamxu'e
-.i lo kamri'o cu drata lo kambla
-
-.i lo kambla cu drata lo kamxu'e
-.i lo kambla cu drata lo kamri'o
-
-.i alabam. bu toldu'o misisip. bu boi joji'as. bu boi tenesis. bu boi florid. bu
-.ijanai tu'e
-	misisip. bu drata tenesis. bu .i
-	misisip. bu drata alabam. bu .i
-	alabam. bu drata tenesis. bu .i
-	alabam. bu drata misisip. bu .i
-	alabam. bu drata joji'as. bu .i
-	alabam. bu drata florid. bu .i
-	joji'as. bu drata florid. bu .i
-	joji'as. bu drata tenesis. bu
diff --git a/examples/patfu.jbo b/examples/patfu.jbo
--- a/examples/patfu.jbo
+++ b/examples/patfu.jbo
@@ -1,5 +1,5 @@
 .i la zeb. cu patfu la jon.bois.sr.
-.i la jon.bois.sr cu patfu la jon.bois.jr.
+.i la jon.bois.sr. cu patfu la jon.bois.jr.
 
 .i da dzena de .ijanai tu'e
 	da patfu de
diff --git a/examples/pendo.jbo b/examples/pendo.jbo
--- a/examples/pendo.jbo
+++ b/examples/pendo.jbo
@@ -1,5 +1,8 @@
-.i do du do
-.i la ualeis. cu nelci lo cirla
+.i da du da
+.i la .ualeis. cu nelci lo cirla
 .i la gromit. cu nelci lo cirla
-.i la uendolen. cu nelci lo lanme
-.i da pendo de .ijanai tu'e da nadu de .i da nelci di .i de nelci di
+.i la .uendolen. cu nelci lo lanme
+.i da pendo de .ijanai tu'e
+	da nadu de .i
+	da nelci di .i
+	de nelci di
diff --git a/examples/skari.jbo b/examples/skari.jbo
new file mode 100644
--- /dev/null
+++ b/examples/skari.jbo
@@ -0,0 +1,19 @@
+.i lo kamxu'e cu drata lo kamri'o
+.i lo kamxu'e cu drata lo kambla
+
+.i lo kamri'o cu drata lo kamxu'e
+.i lo kamri'o cu drata lo kambla
+
+.i lo kambla cu drata lo kamxu'e
+.i lo kambla cu drata lo kamri'o
+
+.i alabam. bu toldu'o misisip. bu boi joji'as. bu boi tenesis. bu boi florid. bu
+.ijanai tu'e
+	misisip. bu drata tenesis. bu .i
+	misisip. bu drata alabam. bu .i
+	alabam. bu drata tenesis. bu .i
+	alabam. bu drata misisip. bu .i
+	alabam. bu drata joji'as. bu .i
+	alabam. bu drata florid. bu .i
+	joji'as. bu drata florid. bu .i
+	joji'as. bu drata tenesis. bu
diff --git a/lojysamban.cabal b/lojysamban.cabal
--- a/lojysamban.cabal
+++ b/lojysamban.cabal
@@ -2,8 +2,8 @@
 cabal-version:		>= 1.6
 
 name:			lojysamban
-version:		0.0.7
-stability:		experimental
+version:		0.0.8
+stability:		alpha
 author:			.iocikun.juj. <PAF01143@nifty.ne.jp>
 maintainer:		.iocikun.juj. <PAF01143@nifty.ne.jp>
 homepage:		http://homepage3.nifty.com/salamander/myblog/lojysamban.html
@@ -30,7 +30,7 @@
     > .i la gromit
     > .i co'o
     >
-    > lojysamban example/gugde.jbo
+    > lojysamban example/skari.jbo
     > .i alabam. bu toldu'o misisip. bu boi joji'as. bu boi tenesis. bu boi florid. bu
     > .i tu'e alabam bu du lo kambla .ije joji'as. bu du lo kamxu'e .ije misisip bu
     > du lo kamxu'e .ije tenesis bu du lo kamri'o .ije florid bu du lo kamri'o tu'u
@@ -42,7 +42,7 @@
     > .i la jon.bois.sr .a la zeb
     > .i co'o
     .
-extra-source-files:	examples/pendo.jbo, examples/gugde.jbo, examples/patfu.jbo
+extra-source-files:	examples/pendo.jbo, examples/skari.jbo, examples/patfu.jbo
     examples/cidja.jbo, examples/mlatu.jbo
 
 source-repository	head
@@ -50,6 +50,9 @@
     location:		git://github.com/YoshikuniJujo/lojysamban.git
 
 executable		lojysamban
-    main-is:		lojysamban2.hs
-    other-modules:	LojbanTools, Prolog2, PrologTools, NotUnif, Unif
-    build-depends:	base > 3 && < 5, lojbanParser
+    hs-source-dirs:	src
+    main-is:		lojysamban.hs
+    other-modules:	LojysambanLib, LojbanTools, Prolog2, PrologTools,
+        NotUnif, Unif
+    build-depends:	base > 3 && < 5, lojbanParser >= 0.1.2, yjtools >= 0.9.16
+    ghc-options:	-Wall
diff --git a/lojysamban2.hs b/lojysamban2.hs
deleted file mode 100644
--- a/lojysamban2.hs
+++ /dev/null
@@ -1,181 +0,0 @@
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TupleSections #-}
-
-module Main where
-
-import LojbanTools
-import Prolog2
-import Language.Lojban.Parser hiding (LA, Brivla, KOhA, GOhA, NA, LerfuString)
-import qualified Language.Lojban.Parser as P
-import System.Environment
-import Data.Maybe
-import Data.Either
-import Data.List
-import Control.Monad
-import Control.Arrow
-import Control.Applicative
-import System.IO
-
-main :: IO ()
-main = do
-	args <- getArgs
-	src <- case args of
-		[] -> readFacts
-		[fn] -> readFile fn
-	let	Right p = parse src
-		rules = map readSentence $ getSentences p
-	whileJust getAsk $ flip ask1 rules
-
-readFacts :: IO String
-readFacts = do
-	l <- getLine
-	if "fa'o" `isInfixOf` l then return l else do
-		ls <- readFacts
-		return $ l ++ ls
-
-whileJust :: IO (Maybe a) -> (a -> IO b) -> IO ()
-whileJust test action = do
-	p <- test
-	case p of
-		Just x -> action x >> whileJust test action
-		Nothing -> return ()
-
-getAsk :: IO (Maybe (Fact Scope Atom))
-getAsk = do
-	putStr ".i "
-	hFlush stdout
-	p <- (either (error . show) id . parse) `fmap` getLine
-	let	Left q = readSentenceFact p
-	return $ if isCOhO p then Nothing else Just q
-
-isCOhO (TopText _ _ [VocativeSumti [(_, "co'o", _)] _ _] _ _ _) = True
-isCOhO _ = False
-
-ask1 :: Fact Scope Atom -> [Rule Scope Atom] -> IO ()
-ask1 q rules = do
-	let	answer = ask [] [] q rules
-	let	answer2_1 = unwords $ intersperse ".ija" $ map unwords $ filter ((> 2) . length) $
-			map ((\ret -> intersperse ".ije" ret) . map showPair . filter (not . isMA . fst) . regularization . onlyTopVars) answer
-		answer2 = unwords $ intersperse ".ija" $ map unwords $ filter ((> 2) . length) $
-			map ((\ret -> "tu'e" : intersperse ".ije" ret ++ ["tu'u"]) . map showPair . filter (not . isMA . fst) . regularization . onlyTopVars) answer
-	putStr ".i "
-	putStr $ case answer of
-		[] -> "nago'i\n"
-		_ -> case intersperse ".a" $ catMaybes $ (flip map) (map maValue answer) $ (showAtom <$>) of
-			[] -> if null answer2 then "go'i\n" else ""
-			m -> unwords m ++ "\n"
-	if null answer2 then return () else
-		if length answer == 1 then putStrLn answer2_1 else putStrLn answer2
-
-showAtom :: Atom -> String
-showAtom (LA n) = "la " ++ n
-showAtom (LO n) = "lo " ++ n
-
-maValue :: Result Scope Atom -> Maybe Atom
-maValue r = case filter (not . null . fst) $ map (first $ filter isMA) r of
-	[] -> Nothing
-	((_, tv) : _) -> (\(Con v) -> v) <$> tv
-
-isMA :: Term Scope Atom -> Bool
-isMA (Var [_] (KOhA "ma")) = True
-isMA _ = False
-
-showAnswerAll a = if null a then "nago'i" else
-	intercalate " .a " $ map showAnswer $ map (lookupMA . onlyTop) a
-
-showPair :: (Term Scope Atom, Term Scope Atom) -> String
-showPair (Var _ (KOhA k), Con (LO n)) = k ++ " du lo " ++ n
-showPair (Var _ (LerfuString l), Con (LO n)) = l ++ " du lo " ++ n
-showPair (Var _ (KOhA k), Con (LA n)) = k ++ " du la " ++ n
-showPair (Var _ (LerfuString l), Con (LA n)) = l ++ " du la " ++ n
-
-regularization :: Result sc s -> [(Term sc s, Term sc s)]
-regularization [] = []
-regularization ((_, Nothing) : rest) = regularization rest
-regularization ((vars, Just val) : rest) = map (, val) vars ++ regularization rest
-
-onlyTopVars :: Result Scope s -> Result Scope s
-onlyTopVars = filter (not . null . fst) . map (first $ filter isTopVar)
-
-isTopVar :: Term Scope s -> Bool
-isTopVar (Var [_] _) = True
-isTopVar _ = False
-
-lookupMA = map snd . filter ((Var "top" (KOhA "ma") `elem`) . fst)
-
-showAnswer as = if null as then "go'i" else showLA $ head as
-
-showLA (Just (Con (LA n))) = "la " ++ n
-showLA (Just (Con (LO n))) = "lo " ++ n
-
-onlyTop = filter (not . null . fst) .
-	map (\(vars, val) -> (filter isTop vars, val))
-
-isTop :: Term String s -> Bool
-isTop (Var "top" _) = True
-isTop _ = False
-
-data Atom
-	= LA String
-	| LO String
-	| KOhA String
-	| Brivla String
-	| GOhA String
-	| LerfuString String
-	deriving (Show, Eq)
-
-type Scope = [Int]
-
-instance TwoD [Int] where
-	next (n : ns) = n + 1 : ns
-	down ns = 0 : ns
-
-readSumti :: Scope -> Sumti -> Term Scope Atom
-readSumti sc (P.LA (_, "la", _) _ _ ns _) = Con $ LA $ intercalate "." $ map snd3 ns
-readSumti sc (P.LALE (_, "lo", _) _ st _ _) = Con $ LO $ readSumtiTail st
-readSumti sc (P.KOhA (_, k, _) _) = Var sc $ KOhA k
-readSumti sc (P.LerfuString s _ _) = Var sc $ LerfuString $ concatMap snd3 s
-
-readSumtiTail :: SumtiTail -> String
-readSumtiTail (SelbriRelativeClauses (P.Brivla (_, n, _) _) _) = n
-readSumtiTail st = show st
-
-readSelbriAtom (P.GOhA (_, n, _) _ _) = GOhA n
-
-readSelbri :: Selbri -> Either (Term Scope Atom) (Term Scope Atom)
-readSelbri (P.Brivla (_, n, _) _) = Left $ Con $ Brivla n
-readSelbri (P.GOhA (_, n, _) _ _) = Left $ Con $ GOhA n
-readSelbri (P.NA (_, "na", _) _ s) = Right $ Con $ readSelbriAtom s
-
-readSentenceFact :: Sentence -> Either (Fact Scope Atom) (Fact Scope Atom)
-readSentenceFact s@(TermsBridiTail _ _ _ _) =
-	either (\lf -> Left $ \sc -> lf : (h sc ++ t sc))
-		(\rf -> Right $ \sc -> rf : (h sc ++ t sc)) f
-	where
-	h sc = map (readSumti sc) $ headTerms s
-	f = readSelbri $ selbri $ bridiTail s
-	t sc = map (readSumti sc) $ tailTerms $ bridiTail s
-readSentenceFact (TopText _ _ _ _ (Just s) _) = readSentenceFact s
-readSentenceFact o = error $ show o
-
-readSentence :: Sentence -> Rule Scope Atom
-readSentence s@(TermsBridiTail _ _ _ _) = Rule (\sc -> f : h sc ++ t sc) [] [] []
-	where
-	h sc = map (readSumti sc) $ headTerms s
-	Left f = readSelbri $ selbri $ bridiTail s
-	t sc = map (readSumti sc) $ tailTerms $ bridiTail s
-readSentence (IJoikJek s [r]) = Rule f [] (getRule r) (getNotRule r)
-	where
-	Left f = readSentenceFact s
-
-getRule (_, Jek _ _ (_, "ja", _) (Just (_, "nai", _)), _, Just t) =
-	lefts $ readRule t
-getNotRule (_, Jek _ _ (_, "ja", _) (Just (_, "nai", _)), _, Just t) =
-	rights $ readRule t
-
-readRule t@(TUhE _ _ _ _ _ _) = readTUhE t
-readRule t = [readSentenceFact t]
-
-readTUhE (TUhE _ _ _ t _ _) = map readSentenceFact $ getSentences t
-readTUhE o = error $ show o
diff --git a/src/LojbanTools.hs b/src/LojbanTools.hs
new file mode 100644
--- /dev/null
+++ b/src/LojbanTools.hs
@@ -0,0 +1,44 @@
+module LojbanTools (
+	getSentences,
+	headTerms,
+	bridiTail,
+	selbri,
+	tailTerms,
+	snd3
+) where
+
+import Language.Lojban.Parser hiding (LA, Brivla, KOhA, GOhA, NA, LerfuString)
+import Data.Maybe
+
+getSentences :: Sentence -> [Sentence]
+getSentences (TopText _ _ _ _ (Just t) _) = getSentences t
+getSentences (IText_1 _ _ _ _ (Just t)) = getSentences t
+getSentences (StatementI s1 ss) = s1 : mapMaybe (\(_, _, s) -> s) ss
+getSentences tbt@(TermsBridiTail{}) = [tbt]
+getSentences o = error $ "getSentences: " ++ show o
+
+headTerms :: Sentence -> [Sumti]
+headTerms (TermsBridiTail ts _ _ _) = ts
+headTerms _ = []
+
+bridiTail :: Sentence -> Sentence
+bridiTail (TermsBridiTail _ _ _ bt) = bt
+bridiTail o = o
+
+selbri :: Sentence -> Selbri
+selbri (Selbri s) = s
+selbri (SelbriTailTerms s _ _ _) = s
+selbri t = error $ show t -- P.Brivla ([], "", []) []
+
+tailTerms :: Sentence -> [Sumti]
+tailTerms (SelbriTailTerms _ ts _ _) = ts
+tailTerms _ = []
+
+{-
+readSumtiTail :: SumtiTail -> String
+readSumtiTail (SelbriRelativeClauses (P.Brivla (_, n, _) _) _) = n
+readSumtiTail st = show st
+-}
+
+snd3 :: (a, b, c) -> b
+snd3 (_, y, _) = y
diff --git a/src/LojysambanLib.hs b/src/LojysambanLib.hs
new file mode 100644
--- /dev/null
+++ b/src/LojysambanLib.hs
@@ -0,0 +1,256 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE PatternGuards #-}
+
+module LojysambanLib (ask, readRules, end) where
+
+import LojbanTools
+import Prolog2 hiding (ask)
+import qualified Prolog2 as P
+import Language.Lojban.Parser hiding (LA, Brivla, KOhA, GOhA, NA, LerfuString, LI)
+import qualified Language.Lojban.Parser as P
+import Data.Maybe
+import Data.Either
+import Data.List
+import Control.Arrow
+import Control.Applicative
+
+end :: String -> Bool
+end = isFAhO
+ask :: String -> [Rule Scope Atom] -> Maybe String
+ask = question
+
+isFAhO :: String -> Bool
+isFAhO src
+	| Right (TopText _ _ _ _ _ (Just (_, "fa'o"))) <- parse src = True
+	| otherwise = False
+
+readRules :: String -> [Rule Scope Atom]
+readRules = map readSentence . getSentences . (\(Right p) -> p) . parse
+
+readQuestion :: String -> Fact Scope Atom
+readQuestion =
+	(\(Left q) -> q) . readSentenceFact . either (error . show) id . parse
+
+isCOhO :: String -> Bool
+isCOhO = isCOhO' . either (error . show) id . parse
+
+isCOhO' :: Sentence -> Bool
+isCOhO' (TopText _ _ [VocativeSumti [(_, "co'o", _)] _ _] _ _ _) = True
+isCOhO' _ = False
+
+question :: String -> [Rule Scope Atom] -> Maybe String
+question q r = if isCOhO q then Nothing else Just $ question' q r
+
+question' :: String -> [Rule Scope Atom] -> String
+question' = ask1 . readQuestion
+
+ask1 :: Fact Scope Atom -> [Rule Scope Atom] -> String
+ask1 q rules =
+	let	answer = P.ask [] [] q rules
+		answer2_1 = unwords $ intersperse ".ija" $ map unwords $ filter ((> 2) . length) $
+			map (intersperse ".ije" . map showPair .
+			filter (not . isMA . fst) . regularization . onlyTopVars) answer
+		answer2 = unwords $ intersperse ".ija" $ map unwords $ filter ((> 2) . length) $
+			map ((\ret -> "tu'e" : intersperse ".ije" ret ++ ["tu'u"]) .
+				map showPair . filter (not . isMA . fst) .
+					regularization . onlyTopVars) answer
+--	print answer
+--	print answer2_1
+--	print answer2
+--	putStr ".i "
+		result1 = ".i " ++ case answer of
+			[] -> "nago'i"
+			_ -> case intersperse ".a" $ mapMaybe
+				((showAtom <$>) . maValue) answer of
+				[] -> if null answer2 then "go'i" else ""
+				m -> unwords m
+	in
+--	show answer ++ "\n" ++
+--	show (q []) ++
+	result1 ++ if null answer2 then "" else
+		if length answer == 1 then answer2_1 else answer2
+
+showAtom :: Atom -> String
+showAtom (LA n) = "la " ++ n
+showAtom (LO n) = "lo " ++ n
+showAtom (LI n) = "li " ++ show n
+showAtom (ListA []) = "lo kunti"
+showAtom (ListA ns) = unwords $ intersperse "ce'o" $ map showAtom ns
+showAtom o = error $ "showAtom: " ++ show o
+
+maValue :: Result Scope Atom -> Maybe Atom
+maValue r = case filter (not . null . fst) $ map (first $ filter isMA) r of
+	[] -> Nothing
+	((_, tv) : _) -> flip (<$>) tv $ \tv' -> case tv' of
+		Con v -> v
+		List vs -> ListA $ map (\(Con v) -> v) vs
+		c@(Cons _ _) -> ListA $ map (\(Con v) -> v) $
+			(\(List vs) -> vs) $ getList c r
+{-
+		Cons v (List vs) -> ListA $
+			(\(Con v) -> v) (lookupValue v r) : map (\(Con v) -> v) vs
+		Cons v vs@(Var _ _) -> ListA $
+			(\(Con v) -> v) (lookupValue v r) : map (\(Con v) -> v)
+				((\(List l) -> l) $ lookupValue vs r)
+-}
+		o -> error $ "maValue: " ++ show o ++ " r = " ++ show r
+
+getList :: (Eq sc, Eq s) => Term sc s -> Result sc s -> Term sc s
+getList l@(List _) _ = l
+getList (Cons v var@(Var _ _)) r
+	| List vs <- lookupValue var r = List $
+		lookupValue v r : map (flip lookupValue r) vs
+	| c@(Cons _ _) <- lookupValue var r,
+		List vs <- getList c r = List $ lookupValue v r : vs
+getList _ _ = error "not implemented"
+
+isMA :: Term Scope Atom -> Bool
+isMA (Var [_] (KOhA "ma")) = True
+isMA _ = False
+
+showPair :: (Term Scope Atom, Term Scope Atom) -> String
+showPair (Var _ (KOhA k), Con (LO n)) = k ++ " du lo " ++ n
+showPair (Var _ (LerfuString l), Con (LO n)) = l ++ " du lo " ++ n
+showPair (Var _ (KOhA k), Con (LA n)) = k ++ " du la " ++ n
+showPair (Var _ (LerfuString l), Con (LA n)) = l ++ " du la " ++ n
+showPair (Var _ (KOhA k), Con (LI n)) = k ++ " du li " ++ show n
+showPair (Var _ (LerfuString l), Con (LI n)) = l ++ " du li " ++ show n
+showPair (Var _ (LerfuString l), List vs) = l ++ " du " ++ unwords (intersperse "ce'o" $ map showTerm vs)
+showPair o = show o
+
+showTerm :: Term Scope Atom -> String
+showTerm (Con (LI n)) = "li " ++ show n
+showTerm (Con (LA n)) = "la " ++ n
+showTerm o = error $ "showTerm: " ++ show o
+
+regularization :: Result sc s -> [(Term sc s, Term sc s)]
+regularization [] = []
+regularization ((_, Nothing) : rest) = regularization rest
+regularization ((vars, Just val) : rest) = map (, val) vars ++ regularization rest
+
+onlyTopVars :: Result Scope s -> Result Scope s
+onlyTopVars = filter (not . null . fst) . map (first $ filter isTopVar)
+
+isTopVar :: Term Scope s -> Bool
+isTopVar (Var [_] _) = True
+isTopVar _ = False
+
+data Atom
+	= LA String
+	| LO String
+	| KOhA String
+	| Brivla String
+	| GOhA String
+	| LerfuString String
+	| LI Int
+	| ListA [Atom]
+	deriving (Show, Eq)
+
+addLI, divLI :: Atom -> Atom -> Atom
+addLI (LI x) (LI y) = LI $ x + y
+addLI _ _ = error "not number"
+divLI (LI x) (LI y) = LI $ x `div` y
+divLI _ _ = error "not number"
+
+type Scope = [Int]
+
+readSumti :: Scope -> Sumti -> Term Scope Atom
+readSumti _ (P.LA (_, "la", _) _ _ ns _) = Con $ LA $ intercalate "." $ map snd3 ns
+readSumti sc (P.LALE (_, "lo", _) _ (SelbriRelativeClauses (Linkargs (P.Brivla
+	(_, "terziljmina", _) _) (BE (_, "be", _) _ s1
+	(Just (BEI (_, "bei", _) _ s2 _)) _ _)) _) _ _) =
+	ApplyOp addLI (readSumti sc s1) (readSumti sc s2)
+readSumti sc (P.LALE (_, "lo", _) _ (SelbriRelativeClauses (Linkargs (P.Brivla
+	(_, "dilcu", _) _) (BE (_, "be", _) _ s1
+	(Just (BEI (_, "bei", _) _ s2 _)) _ _)) _) _ _) =
+	ApplyOp divLI (readSumti sc s1) (readSumti sc s2)
+readSumti _ (P.LALE (_, "lo", _) _ (SelbriRelativeClauses
+	(P.Brivla (_, "kunti", _) _) _) _ _) = List []
+readSumti sc (P.LALE (_, "lo", _) _ (SelbriRelativeClauses (Linkargs (P.Brivla
+	(_, "selzilvi'u", _) _) (BE (_, "be", _) _ s1
+	(Just (BEI (_, "bei", _) _ s2 _)) _ _)) _) _ _) =
+	Cons (readSumti sc s1) (readSumti sc s2)
+readSumti _ (P.LALE (_, "lo", _) _ st _ _) = Con $ LO $ readSumtiTail st
+readSumti sc (P.KOhA (_, k, _) _) = Var sc $ KOhA k
+readSumti sc (P.LerfuString s _ _) = Var sc $ LerfuString $ concatMap snd3 s
+readSumti _ (P.LI (_, "li", _) _ (Number ns _ _) _ _) = Con $ LI $ readNumber ns
+readSumti sc (JoikEkSumti s ss) = List $ readSumti sc s : readCEhOTail sc ss
+readSumti _ o = error $ show o
+
+readCEhOTail :: Scope -> [(JoikJek, [Free], Sumti)] -> [Term Scope Atom]
+readCEhOTail _ [] = []
+readCEhOTail sc ((JOI _ (_, "ce'o", _) _, _, s) : rest) =
+	readSumti sc s : readCEhOTail sc rest
+readCEhOTail _ o = error $ "readCEhOTail: " ++ show o
+
+readNumber :: [([String], String, [[([String], String)]])] -> Int
+readNumber = readTen 0 . map snd3
+
+paList :: [(String, Int)]
+paList = [
+	("no", 0), ("pa", 1), ("re", 2), ("ci", 3), ("vo", 4),
+	("0", 0), ("1", 1), ("2", 2), ("3", 3), ("4", 4)]
+
+readTen :: Int -> [String] -> Int
+readTen = foldl (\r n -> r * 10 + fromJust (lookup n paList))
+
+readSumtiTail :: SumtiTail -> String
+readSumtiTail (SelbriRelativeClauses (P.Brivla (_, "terziljmina", _) _) _) =
+	error "readSumtiTail: terziljmina"
+readSumtiTail (SelbriRelativeClauses (P.Brivla (_, n, _) _) _) = n
+readSumtiTail st = show st
+
+readSelbriAtom :: Selbri -> Atom
+readSelbriAtom (P.GOhA (_, n, _) _ _) = GOhA n
+readSelbriAtom o = error $ "readSelbriAtom: " ++ show o
+
+readSelbri :: Selbri -> Either (Term Scope Atom) (Term Scope Atom)
+readSelbri (P.Brivla (_, "binxo", _) _) = Left Is
+readSelbri (P.Brivla (_, n, _) _) = Left $ Con $ Brivla n
+readSelbri (P.GOhA (_, n, _) _ _) = Left $ Con $ GOhA n
+readSelbri (P.NA (_, "na", _) _ s) = Right $ Con $ readSelbriAtom s
+readSelbri o = error $ "readSelbri: " ++ show o
+
+readSentenceFact :: Sentence -> Either (Fact Scope Atom) (Fact Scope Atom)
+readSentenceFact s@(TermsBridiTail{}) =
+	either (\lf -> Left $ \sc -> lf : (h sc ++ t sc))
+		(\rf -> Right $ \sc -> rf : (h sc ++ t sc)) f
+	where
+	h sc = map (readSumti sc) $ headTerms s
+	f = readSelbri $ selbri $ bridiTail s
+	t sc = map (readSumti sc) $ tailTerms $ bridiTail s
+readSentenceFact (TopText _ _ _ _ (Just s) _) = readSentenceFact s
+readSentenceFact o = error $ show o
+
+readSentence :: Sentence -> Rule Scope Atom
+readSentence s@(TermsBridiTail{}) = Rule (\sc -> f : h sc ++ t sc) [] [] []
+	where
+	h sc = map (readSumti sc) $ headTerms s
+	Left f = readSelbri $ selbri $ bridiTail s
+	t sc = map (readSumti sc) $ tailTerms $ bridiTail s
+readSentence (IJoikJek s [r]) = Rule f [] (getRule r) (getNotRule r)
+	where
+	Left f = readSentenceFact s
+readSentence o = error $ "readSentence: " ++ show o
+
+getRule :: (Show s, Show t) =>
+	(s, JoikJek, t, Maybe Sentence) -> [Fact Scope Atom]
+getRule (_, Jek _ _ (_, "ja", _) (Just (_, "nai", _)), _, Just t) =
+	lefts $ readRule t
+getRule o = error $ "getRule: " ++ show o
+
+getNotRule :: (Show s, Show t) =>
+	(s, JoikJek, t, Maybe Sentence) -> [Fact Scope Atom]
+getNotRule (_, Jek _ _ (_, "ja", _) (Just (_, "nai", _)), _, Just t) =
+	rights $ readRule t
+getNotRule o = error $ "getNotRule: " ++ show o
+
+readRule :: Sentence -> [Either (Fact Scope Atom) (Fact Scope Atom)]
+readRule t@(TUhE {}) = readTUhE t
+readRule t = [readSentenceFact t]
+
+readTUhE :: Sentence -> [Either (Fact Scope Atom) (Fact Scope Atom)]
+readTUhE (TUhE _ _ _ t _ _) = map readSentenceFact $ getSentences t
+readTUhE o = error $ show o
diff --git a/src/NotUnif.hs b/src/NotUnif.hs
new file mode 100644
--- /dev/null
+++ b/src/NotUnif.hs
@@ -0,0 +1,96 @@
+module NotUnif (
+	merge,
+	Result,
+	unification,
+	Term(..),
+	checkAll,
+	checkNot,
+	deleteFromNot,
+	notUnification,
+	apply,
+	lookupValue,
+) where
+
+import Unif
+import Control.Applicative
+import Data.Maybe
+
+checkAll :: (Eq sc, Eq s) =>
+	[([Term sc s], Maybe (Term sc s))] -> [Maybe [(Term sc s, Term sc s)]]
+		-> Bool
+checkAll _ [] = True
+checkAll r (Nothing : nots) = checkAll r nots
+checkAll r (Just [] : nots) = checkAll r nots
+checkAll r (Just n : nots) =
+	checkNot r (deleteFromNot r n) && checkAll r nots
+
+deleteFromNot :: (Eq sc, Eq s) =>
+	[([Term sc s], Maybe (Term sc s))] -> [(Term sc s, Term sc s)] ->
+		[(Term sc s, Term sc s)]
+deleteFromNot _ [] = []
+deleteFromNot r ((t@(Var _ _), u@(Var _ _)) : ps)
+	| not $ any ((t `elem`) . fst) r = deleteFromNot r ps
+	| not $ any ((u `elem`) . fst) r = deleteFromNot r ps
+	| otherwise = (t, u) : deleteFromNot r ps
+deleteFromNot r ((t, u) : ps) = (t, u) : deleteFromNot r ps
+
+checkNot :: (Eq sc, Eq s) =>
+	[([Term sc s], Maybe (Term sc s))] -> [(Term sc s, Term sc s)] -> Bool
+checkNot _ [] = False
+checkNot r ((t@(Var _ _), u@(Var _ _)) : ps)
+	= not (any ((\vs -> t `elem` vs && u `elem` vs) . fst) r) ||
+--		null (filter ((t `elem`) .fst) r) ||
+--		null (filter ((u `elem`) .fst) r) ||
+		checkNot r ps
+checkNot r ((t@(Var _ _), u) : ps)
+	= snd (head $ filter ((t `elem`) . fst) r) /= Just u || checkNot r ps
+checkNot _ _ = error "bad"
+
+notUnification :: (Eq sc, Eq s) =>
+	[Term sc s] -> [Term sc s] -> Maybe [(Term sc s, Term sc s)]
+notUnification ts us = simplify <$> notUnifies ts us
+
+notUnify :: (Eq sc, Eq s) =>
+	Term sc s -> Term sc s -> Maybe (Maybe (Term sc s, Term sc s))
+notUnify t u | t == u = Nothing
+notUnify (Con _) (Con _) = Just Nothing
+notUnify t u = Just $ Just (t, u)
+
+notUnifies :: (Eq sc, Eq s) =>
+	[Term sc s] -> [Term sc s] -> Maybe [(Term sc s, Term sc s)]
+notUnifies [] [] = Nothing
+notUnifies [t] [u] = maybeToList <$> notUnify t u
+notUnifies (t : ts) (u : us) = case notUnify t u of
+	Nothing -> notUnifies ts us
+	Just Nothing -> Just []
+	Just (Just p) -> case notUnifies ts us of
+		Nothing -> Just [p]
+		Just [] -> Just []
+		Just ps -> Just $ p : ps
+notUnifies _ _ = Just []
+
+-- simplify :: [(Term, Term)] -> [(Term, Term)]
+simplify :: (Eq sc, Eq s) =>
+	[(Term sc s, Term sc s)] -> [(Term sc s, Term sc s)]
+simplify = checkSame . map (uncurry order)
+
+-- checkSame :: [(Term, Term)] -> [(Term, Term)]
+checkSame :: (Eq sc, Eq s) =>
+	[(Term sc s, Term sc s)] -> [(Term sc s, Term sc s)]
+checkSame [] = []
+checkSame (p : ps) = mapMaybe (isSame p) ps ++ p : checkSame ps
+
+-- isSame :: (Term, Term) -> (Term, Term) -> Maybe (Term, Term)
+isSame :: Eq a => (a, a) -> (a, a) -> Maybe (a, a)
+isSame (x, y) (z, w)
+	| x == z = Just (y, w)
+	| y == w = Just (x, z)
+	| x == w = Just (y, z)
+	| y == z = Just (x, w)
+	| otherwise = Nothing
+
+order :: Term sc s -> Term sc s -> (Term sc s, Term sc s)
+order (Con _) (Con _) = error "not occur"
+order t@(Var _ _) u@(Con _) = (t, u)
+order t@(Con _) u@(Var _ _) = (u, t)
+order t u = (t, u)
diff --git a/src/Prolog2.hs b/src/Prolog2.hs
new file mode 100644
--- /dev/null
+++ b/src/Prolog2.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE PatternGuards #-}
+
+module Prolog2 (
+	ask,
+	Fact,
+	Rule(..),
+	Term(..),
+	TwoD(..),
+	Result,
+	lookupValue
+) where
+
+import PrologTools
+import Data.Maybe
+
+ask :: (TwoD sc, Eq sc, Eq s) =>
+	sc -> Result sc s -> Fact sc s -> [Rule sc s] -> [Result sc s]
+ask sc ret q rs
+	| [Is, t, u] <- q sc =
+		maybeToList $ [([t], Just $ apply u ret)] `merge` ret
+	| otherwise = concat $ zipWith ar (iterate next $ down sc) rs
+	where
+	ar sc' r = askrule sc' ret q r rs
+--		| [Is, t, u] <- q sc =
+--			maybeToList $ [([t], Just $ apply u ret)] `merge` ret
+--		| (Is : _) <- q sc' = error "debug: Is"
+
+askrule :: (TwoD sc, Eq sc, Eq s) =>
+	sc -> Result sc s -> Fact sc s -> Rule sc s -> [Rule sc s] -> [Result sc s]
+askrule sc ret q (Rule fact _ facts notFacts) rs
+--	| [Is, t, u] <- fact (next sc) = maybeToList $ [([t], Just u)] `merge` ret
+	| [Is, _, _] <- fact (next sc) = error "not implemented"
+	| otherwise = filter (`checkAll` nots) ret'
+	where
+	ret' = foldl (\rets (sc', f) -> rets >>= \r' -> ask sc' r' f rs) r0 $
+		zip (iterate next sc0) $ map (const . ($ sc0)) facts
+	sc0 = down sc
+	r0 = case q sc `unification` fact sc0 of
+		Nothing -> []
+		Just r0' -> maybeToList $ ret `merge` r0'
+	nots = concatMap (flip (notAsk sc0) rs . const . ($sc0)) notFacts
diff --git a/src/PrologTools.hs b/src/PrologTools.hs
new file mode 100644
--- /dev/null
+++ b/src/PrologTools.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module PrologTools (
+	Term(..),
+	merge,
+	unification,
+	Result,
+	TwoD(..),
+	Fact,
+	NotFact,
+	Rule(..),
+	notAsk,
+	checkAll,
+	apply,
+	lookupValue
+) where
+
+import NotUnif
+import Control.Applicative
+
+class TwoD td where
+	next :: td -> td
+	down :: td -> td
+
+instance TwoD [Int] where
+	next (n : ns) = n + 1 : ns
+	next _ = error "empty"
+	down ns = 0 : ns
+
+type Fact sc s = sc -> [Term sc s]
+type NotFact sc s = Fact sc s
+data Unify sc s
+	= Unify (Term sc s) (Term sc s)
+	| NotUnify (Term sc s) (Term sc s)
+	deriving Show
+data Rule sc s = Rule (Fact sc s) [Unify sc s] [Fact sc s] [NotFact sc s]
+
+notAsk :: (TwoD sc, Eq sc, Eq s) => sc ->
+	Fact sc s -> [Rule sc s] -> [Maybe [(Term sc s, Term sc s)]]
+notAsk sc q rs = zipWith (\sc' r -> notAskRule sc' q r rs) (iterate next $ down sc) rs
+
+notAskRule :: (TwoD sc, Eq sc, Eq s) => sc ->
+	Fact sc s -> Rule sc s -> [Rule sc s] -> Maybe [(Term sc s, Term sc s)]
+notAskRule sc q (Rule fact _ facts _) rs = liftA concat $
+	case match of
+		Nothing -> Just []
+		Just _ ->
+			liftA2 (:) start $ maybeOut $ concatMap
+				(flip (notAsk sc) rs . const . ($ sc)) facts
+	where
+	start = notUnification (q sc) $ fact sc
+	match = unification [head $ q sc] [head $ fact sc]
+
+maybeOut :: [Maybe a] -> Maybe [a]
+maybeOut [] = Just []
+maybeOut (Nothing : _) = Nothing
+maybeOut (Just x : xs) = fmap (x :) $ maybeOut xs
diff --git a/src/Unif.hs b/src/Unif.hs
new file mode 100644
--- /dev/null
+++ b/src/Unif.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE PatternGuards #-}
+
+module Unif (Term(..), Result, merge, unification, unify, apply, lookupValue) where
+
+import Data.List(intersect, union)
+import Control.Monad(foldM)
+
+data Term sc s
+	= Con s | Var sc s | List [Term sc s] | Cons (Term sc s) (Term sc s)
+	| ApplyOp (s -> s -> s) (Term sc s) (Term sc s)
+	| Is
+
+instance (Show sc, Show s) => Show (Term sc s) where
+	show (Con x) = "Con " ++ show x
+	show (Var sc x) = "Var " ++ show sc ++ " " ++ show x
+	show (List ts) = "List " ++ show ts
+	show (Cons h t) = "Cons (" ++ show h ++ ") (" ++ show t ++ ")"
+	show (ApplyOp{}) = "ApplyOp _ _ _"
+	show Is = "Is"
+
+instance (Eq sc, Eq s) => Eq (Term sc s) where
+	Con x == Con y = x == y
+	Var sc x == Var sc' y = sc == sc' && x == y
+	List xs == List ys = xs == ys
+	Cons h t == Cons i u = h == i && t == u
+	ApplyOp{} == ApplyOp{} = error "can't compare applys"
+	_ == _ = False
+
+type Result sc s = [([Term sc s], Maybe (Term sc s))]
+
+merge :: (Eq sc, Eq s) => Result sc s -> Result sc s -> Maybe (Result sc s)
+merge ps qs = foldM (flip merge1) qs ps
+
+merge1 :: (Eq sc, Eq s) =>
+	([Term sc s], Maybe (Term sc s)) -> Result sc s -> Maybe (Result sc s)
+merge1 (ts, mv) r
+	| [(us, mv')] <- filter (isDefFor ts) r = do
+		(vv, m) <- case (mv, mv') of
+			(Just v, Just v') -> do
+				(vv', m) <- unify v v'
+				return (Just vv', m)
+			(v, Nothing) -> return (v, [])
+			(_, v') -> return (v', [])
+		merge m $ (ts `union` us, vv) `add` notSames
+	| [] <- filter (isDefFor ts) r = return $ (ts, mv) `add` notSames
+	| [(us1, mv'1), (us2, mv'2)] <- filter (isDefFor ts) r = do
+		ret1 <- fun (us1, mv'1) (ts, mv) notSames
+		fun (us2, mv'2) (ts `union` us1, mv) ret1
+	| err <- filter (isDefFor ts) r = error $ show $ length err
+	where
+	notSames = filter (not . isDefFor ts) r
+	fun (_, mv') (tsss, mvvv) hoge = do
+		(vv, m) <- case (mvvv, mv') of
+			(Just v, Just v') -> do
+				(vv', m) <- unify v v'
+				return (Just vv', m)
+			(v, Nothing) -> return (v, [])
+			(_, v') -> return (v', [])
+		merge m $ (tsss, vv) `add` hoge
+
+add :: (Eq sc, Eq s) =>
+	([Term sc s], Maybe (Term sc s)) -> Result sc s -> Result sc s
+add (ts, v@(Just _)) rs = (foldr union ts sames, v) : notSames
+	where
+	sames = map fst $ filter ((== v) . snd) rs
+	notSames = filter ((/= v) . snd) rs
+add r1 rs = r1 : rs
+
+isDefFor :: (Eq sc, Eq s) => [Term sc s] -> ([Term sc s], Maybe (Term sc s)) -> Bool
+isDefFor ts (us, _) = not $ null $ ts `intersect` us
+
+unification :: (Eq sc, Eq s) => [Term sc s] -> [Term sc s] -> Maybe (Result sc s)
+unification = unifies
+
+unify :: (Eq sc, Eq s) => Term sc s -> Term sc s -> Maybe (Term sc s, Result sc s)
+unify t u | t == u = Just (t, [])
+unify (Con _) (Con _) = Nothing
+unify t@(Var _ _) u@(Var _ _) = Just (t, [([t, u], Nothing)])
+unify t@(Var _ _) u = Just (u, [([t], Just u)])
+unify t u@(Var _ _) = Just (t, [([u], Just t)])
+unify (List ts) (List us) = do
+	rs <- unification ts us
+	return (List $ map (`lookupValue` rs) ts, rs)
+unify (Cons h t) (List (u : us)) = do
+	rs <- unification [h, t] [u, List us]
+	return (Cons (lookupValue h rs) (lookupValue t rs), rs)
+unify (Cons _ _) (List []) = Nothing
+unify (Cons h1 t1) (Cons h2 t2) = do
+	rs <- unification [h1, t1] [h2, t2]
+	return (Cons (lookupValue h1 rs) (lookupValue t1 rs), rs)
+unify t u@(Cons _ _) = unify u t
+unify Is Is = Just (Is, [])
+unify Is _ = Nothing
+unify _ Is = Nothing
+unify (Cons _ _) (Con _) = Nothing -- error "Cons with Con"
+unify (Cons _ _) _ = error "Cons with _"
+unify (ApplyOp{}) (List _) = error "AppOp with List"
+unify (Con _) (List _) = Nothing -- error "Con with List"
+unify _ _ = error "not implemented"
+
+unifies :: (Eq sc, Eq s) => [Term sc s] -> [Term sc s] -> Maybe (Result sc s)
+unifies [] [] = Just []
+unifies (t : ts) (u : us) = do
+	(_, ret) <- unify t u
+	rets <- unifies ts us
+	merge ret rets
+unifies _ _ = Nothing
+
+lookupValue :: (Eq sc, Eq s) => Term sc s -> Result sc s -> Term sc s
+lookupValue t rs =
+	case f of
+		[] -> t
+		[(_, Nothing)] -> t
+		[(_, Just t')] -> t'
+		_ -> error "cannot occur"
+	where
+	f = filter ((t `elem`) . fst) rs
+
+apply :: (Eq s, Eq sc) => Term sc s -> Result sc s -> Term sc s
+apply (ApplyOp op t u) rs
+	| Con x <- lookupValue t rs, Con y <- lookupValue u rs =
+		Con $ op x y
+	| otherwise = error "cannot apply"
+apply x rs = lookupValue x rs
diff --git a/src/lojysamban.hs b/src/lojysamban.hs
new file mode 100644
--- /dev/null
+++ b/src/lojysamban.hs
@@ -0,0 +1,20 @@
+module Main where
+
+import System.IO(hFlush, stdout)
+import System.Environment(getArgs)
+import System.Exit(exitFailure)
+import Control.Applicative((<$>))
+import Control.Arrow((&&&))
+import Control.Monad.Tools(doWhile, doWhile_)
+import LojysambanLib(ask, readRules, end)
+
+main :: IO ()
+main = do
+	args <- getArgs
+	rules <- readRules <$> case args of
+		[] -> doWhile "" $ \s -> (id &&& not . end) . (s ++) <$> getLine
+		[fp] -> readFile fp
+		_ -> putStrLn "Usage: lojysamban [FILEPATH]" >> exitFailure
+	doWhile_ $ do
+		q <- putStr ".i " >> hFlush stdout >> getLine
+		maybe (return False) ((>> return True) . putStrLn) $ ask q rules