diff --git a/packages.dhall b/packages.dhall
index 8744915..eefbced 100644
--- a/packages.dhall
+++ b/packages.dhall
@@ -104,7 +104,7 @@ let upstream =
 
 in  upstream
     with logict.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/logict.git"
-    with logict.version = "2facde23774a6d47c45bb20425645cfafc3179e5"
+    with logict.version = "a2d2b10e86beb2769245502e7f5dec4592bb2a2a"
     with logict.dependencies = [ "control", "lists", "maybe", "prelude", "transformers", "tuples" ]
     with unifyt.repo = "https://dev.danilafe.com/Everything-I-Know-About-Types/unifyt.git"
     with unifyt.version = "590306964c59b8828b66b8d020283c8efaf2170b"
diff --git a/src/Language/Bergamot/Syntax.purs b/src/Language/Bergamot/Syntax.purs
index d895dd9..91030ce 100644
--- a/src/Language/Bergamot/Syntax.purs
+++ b/src/Language/Bergamot/Syntax.purs
@@ -1,6 +1,6 @@
 module Language.Bergamot.Syntax where
 
-import Prelude (Unit, ($), (<<<), unit, (/=), const, flip, (+))
+import Prelude
 
 import Control.Plus (class Plus, empty)
 import Control.Monad (class Monad)
@@ -12,7 +12,7 @@ import Control.Alternative (class Alternative)
 import Control.Applicative (class Applicative, pure, (*>))
 import Control.Bind (class Bind, bind, join, (>>=))
 import Control.MonadPlus (class MonadPlus)
-import Control.Monad.Reader.Class (class MonadReader, class MonadAsk, local, ask)
+import Control.Monad.Reader.Class (class MonadReader, class MonadAsk, local, ask, asks)
 import Control.Monad.Logic.Class (class MonadLogic, msplit, interleave)
 import Control.Monad.Unify.Class (class MonadUnify, class Unifiable, class UnificationVariable, Stream(..), squash, alongside, ComparisonAction(..), fresh, unify, reify)
 import Control.Monad.Reader.Trans (ReaderT, runReaderT)
@@ -79,7 +79,8 @@ derive instance Functor Rule
 derive instance Foldable Rule
 derive instance Traversable Rule
 
-newtype Unifier a = MkUnifier (UnifyT IntVar Expr (ReaderT (Array (Rule Metavariable)) (SFKT List)) a)
+type UnifierEnv = { rules :: Array (Rule Metavariable), fuel :: Int }
+newtype Unifier a = MkUnifier (UnifyT IntVar Expr (ReaderT UnifierEnv (SFKT Maybe)) a)
 
 derive instance Newtype (Unifier a) _
 derive newtype instance Functor Unifier
@@ -94,11 +95,11 @@ derive newtype instance MonadPlus Unifier
 derive newtype instance MonadUnify IntVar Expr Unifier
 
 -- >:(
-instance MonadAsk (Array (Rule Metavariable)) Unifier where
+instance MonadAsk UnifierEnv Unifier where
     ask = MkUnifier $ MkUnifyT ask
 
 -- >:(
-instance MonadReader (Array (Rule Metavariable)) Unifier where
+instance MonadReader UnifierEnv Unifier where
     local f m = MkUnifier $ MkUnifyT $ StateT $ \s -> local f (runStateT (un MkUnifyT $ un MkUnifier m) s)
 
 -- >:(
@@ -106,6 +107,11 @@ instance MonadLogic Unifier where
     msplit m = MkUnifier $ MkUnifyT $ map (map (rmap (MkUnifier <<< MkUnifyT))) $ msplit $ un MkUnifyT $ un MkUnifier m
     interleave = over2 MkUnifier (over2 MkUnifyT interleave)
 
+spend :: forall a. Unifier a -> Unifier a
+spend m = do
+    n <- asks _.fuel
+    if n > 0 then local (_ { fuel = n - 1}) m else empty
+
 type Metavariable = String
 type Metavariables k = Map Metavariable k
 
@@ -124,7 +130,7 @@ newtype ProofTree k = MkProofTree { claim :: Expr k, rule :: Rule Metavariable,
 match :: Array (Rule Metavariable) -> Expr IntVar -> Unifier (ProofTree IntVar)
 match rs e = oneOf $ map (matchSingle e) rs
     where
-      matchSingle e' rule = do
+      matchSingle e' rule = spend $ do
          MkRule {head, tail} <- instantiate rule
          _ <- unify e' head
          witnesses <- traverse (match rs) tail
@@ -137,7 +143,7 @@ reifyProofTree (MkProofTree {claim, rule, witnesses}) = do
     pure $ MkProofTree $ { claim: claim', rule: rule, witnesses: witnesses' }
 
 query :: Expr Metavariable -> Unifier (ProofTree IntVar)
-query e = (join $ lift2 match ask (instantiate e)) >>= reifyProofTree
+query e = (join $ lift2 match (asks _.rules) (instantiate e)) >>= reifyProofTree
 
-runUnifier :: forall a. Array (Rule Metavariable) -> Unifier a -> List a
-runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) rs))
+runUnifier :: forall a. Array (Rule Metavariable) -> Unifier a -> Maybe a
+runUnifier rs m = runSFKTOnce (fst <$> (runReaderT (runUnifyT $ un MkUnifier m) { rules: rs, fuel: 10 }))
diff --git a/test/Main.purs b/test/Main.purs
index 1bbe04e..db781a9 100644
--- a/test/Main.purs
+++ b/test/Main.purs
@@ -61,5 +61,6 @@ toLatexExpr (Var _) = "?"
 toLatexProofTree :: ProofTree IntVar -> String
 toLatexProofTree (MkProofTree {claim, witnesses}) = "\\cfrac{" <> intercalate "\\quad" (toLatexProofTree <$> witnesses) <> "}{" <> toLatexExpr claim <> "}"
 
-main :: List String
-main = map toLatexProofTree $ runUnifier rules $ query $ tType (tSndExpr (tProdExpr tStringExpr (tPlusExpr tIntExpr tIntExpr))) (Var "T")
+main :: Maybe String
+main = map toLatexProofTree $ runUnifier rules $ query $ tType (Var "e") (tProd tInt (tProd tInt tString))
+-- main = map toLatexProofTree $ runUnifier rules $ query $ tType (tSndExpr (tProdExpr tStringExpr (tPlusExpr tIntExpr tIntExpr))) (Var "T")