diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm
index ab00fe9..70486ac 100644
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -82,8 +82,8 @@ getRules env ps = Search.pure (List.concatMap (.rules) env.sections, ps)
 getUnificationState : Prover UnificationState
 getUnificationState env ps = Search.pure (ps.unificationState, ps)
 
-burn : Prover ()
-burn env ps = if ps.gas > 0 then Search.pure ((), { ps | gas = ps.gas - 1}) else Search.fail
+burn : Prover a -> Prover a
+burn p env ps = if ps.gas > 0 then Search.map (\(a, psp) -> (a, { psp | gas = ps.gas })) (p env { ps | gas = ps.gas - 1 }) else Search.fail
 
 liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
 liftInstantiation f a env ps =
@@ -171,9 +171,9 @@ proveTerm : Term UnificationVar -> Prover ProofTree
 proveTerm t =
     map (reify t) getUnificationState
     |> andThen (\tp ->
-        burn
-        |> andThen (\() -> getRules)
-        |> andThen (List.foldl (\r -> interleave (yield (rule tp r))) (builtinRules tp)))
+        burn (
+            getRules
+            |> andThen (List.foldr (\r -> interleave ((rule tp r))) (builtinRules tp))))
 
 prove : Term Metavariable -> Prover ProofTree
 prove mt =
@@ -182,6 +182,6 @@ prove mt =
 
 single : RuleEnv -> Prover a -> Maybe a
 single env p =
-    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 1000 }
+    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 30 }
     |> Search.one
     |> Maybe.map (Tuple.first << Tuple.first)