diff --git a/README.md b/README.md
index 808aced3..a1a1faa5 100644
--- a/README.md
+++ b/README.md
@@ -105,6 +105,7 @@ The global options are common to all commands.
 |```--nparse <int>```                             |```-1```  |Search only N-best parse trees for each sentence (A negative value means all trees) |                      |
 |```--ntypecheck <int>```                         |```-1```  |Search only N-best diagrams for each type checking of a logical form (A negative value means all diagrams) |
 |```--nproof <int>```                             |```-1```  |Search only N-best diagrams for each proof search (A negative value means all diagrams) |
+|```--maxdepth <int>```                           |```9```   |Set the maximum search depth in proof search (default: 9) |
 |```--noTypeCheck```                              |          |If specified, show no type checking diagram for each sentence.|
 |```--noInference```                              |          |If specified, execute no inference for each discourse.|
 |```--time```                                     |          |Show the execution time in stderr.|
diff --git a/app/lightblueMain.hs b/app/lightblueMain.hs
index 7dce3c55..695890a5 100644
--- a/app/lightblueMain.hs
+++ b/app/lightblueMain.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE OverloadedStrings, RecordWildCards #-}
 
 import Options.Applicative hiding (style) --optparse-applicative
---import Data.Semigroup ((<>))              --semigroup
+import Control.Applicative (optional)     --base
 import Control.Monad (forM)               --base
 import ListT (toList)                     --list-t
 import qualified Data.Text.Lazy as T      --text
@@ -38,7 +38,7 @@ data Options =
   -- Version
   -- | Stat
   -- | Test
-  Options Command I.Style FilePath Juman.MorphAnalyzerName Int Int Int Int Bool Bool Bool Bool
+  Options Command I.Style FilePath Juman.MorphAnalyzerName Int Int Int Int Int Bool Bool Bool Bool
     deriving (Show, Eq)
 
 data Command =
@@ -178,6 +178,12 @@ optionParser =
       <> showDefault
       <> value (-1)
       <> metavar "INT" )
+    <*> option auto 
+      ( long "maxdepth"
+      <> help "Set the maximum search depth in proof search"
+      <> showDefault
+      <> value 9
+      <> metavar "INT" )
     <*> switch 
       ( long "noTypeCheck"
       <> help "If True, execute no type checking for LFs" )
@@ -239,7 +245,7 @@ lightblueMain :: Options -> IO()
 -- lightblueMain Version = showVersion
 -- lightblueMain Stat = showStat
 -- lightblueMain Test = test
-lightblueMain (Options commands style filepath morphaName beamW nParse nTypeCheck nProof noTypeCheck noInference iftime verbose) = do
+lightblueMain (Options commands style filepath morphaName beamW nParse nTypeCheck nProof maxDepth noTypeCheck noInference iftime verbose) = do
   start <- Time.getCurrentTime
   contents <- case filepath of
     "-" -> T.getContents
@@ -260,7 +266,7 @@ lightblueMain (Options commands style filepath morphaName beamW nParse nTypeChec
     lightblueMainLocal (Parse output proverName) lr contents = do
       let handle = S.stdout
           parseSetting = CP.ParseSetting jpOptions lr beamW nParse nTypeCheck nProof True Nothing Nothing noInference verbose
-          prover = NLI.getProver proverName $ QT.ProofSearchSetting Nothing Nothing (Just QT.Classical)
+          prover = NLI.getProver proverName $ QT.ProofSearchSetting (Just maxDepth) Nothing (Just QT.Classical) verbose
           parseResult = NLI.parseWithTypeCheck parseSetting prover [("dummy",DTT.Entity)] [] $ T.lines contents
           posTagOnly = case output of 
                          I.TREE -> False
@@ -281,7 +287,7 @@ lightblueMain (Options commands style filepath morphaName beamW nParse nTypeChec
             | otherwise = take nSample parsedJSeM'
           handle = S.stdout
           parseSetting = CP.ParseSetting jpOptions lr beamW nParse nTypeCheck nProof True Nothing Nothing noInference verbose
-          prover = NLI.getProver proverName $ QT.ProofSearchSetting Nothing Nothing (Just QT.Classical)
+          prover = NLI.getProver proverName $ QT.ProofSearchSetting (Just maxDepth) Nothing (Just QT.Classical) verbose
       S.hPutStrLn handle $ I.headerOf style
       pairs <- forM parsedJSeM'' $ \j -> do
         let title = "JSeM-ID " ++ (StrictT.unpack $ J.jsem_id j)
@@ -386,7 +392,7 @@ test = do
       termA = UDTT.Sigma (UDTT.Con "entity") (UDTT.App (UDTT.Con "f") (UDTT.Var 0))
       -- typeA = DTS.Kind
       tcq = UDTT.TypeInferQuery signature context termA 
-      pss = QT.ProofSearchSetting Nothing Nothing (Just QT.Classical)
+      pss = QT.ProofSearchSetting Nothing Nothing (Just QT.Classical) False
   typeCheckResults <- toList $ typeInfer (nullProver pss) False tcq
   T.putStrLn $ T.toText $ head typeCheckResults
   --T.hPutStrLn S.stderr $ T.toText $ DTS.Judgment context (DTS.Var 0) DTS.Type
diff --git a/src/DTS/Prover/Wani/Prove.hs b/src/DTS/Prover/Wani/Prove.hs
index 89512131..efcf5dfd 100644
--- a/src/DTS/Prover/Wani/Prove.hs
+++ b/src/DTS/Prover/Wani/Prove.hs
@@ -17,6 +17,7 @@ import qualified DTS.QueryTypes as QT
 
 import qualified Data.Text.Lazy as T 
 import qualified Data.List as L 
+import qualified Data.Maybe as M
 import qualified Debug.Trace as D
 import qualified ListT as ListT
 
@@ -42,7 +43,7 @@ hojo varEnv sigEnv pre_type setting =
   let sigEnv' = map (Data.Bifunctor.second A.fromDT2A) sigEnv
       varEnv' = map A.fromDT2A varEnv
       arrowType = A.fromDT2A  pre_type
-      result = searchProof' sigEnv' varEnv' arrowType 1 setting
+      result = searchProofWithIncrementalDepth sigEnv' varEnv' arrowType 1 setting 1 (let num = WB.maxdepth setting in if num < 0 then M.Nothing else M.Just num)
   in WB.debugLog (sigEnv',varEnv') arrowType 0 setting "goal" result
 
 searchProof' :: WB.DeduceRule
@@ -50,6 +51,14 @@ searchProof' a b c d setting=
   let result =  B.deduce a b c d setting
   in result{WB.trees = L.nub (WB.trees result)}
 
+searchProofWithIncrementalDepth :: A.SAEnv -> A.AEnv -> WB.AType -> WB.Depth -> WB.Setting -> Int -> M.Maybe Int-> WB.Result
+searchProofWithIncrementalDepth a b c d setting currentDepth maybeLim =
+  let result = searchProof' a b c d setting{WB.maxdepth = currentDepth}
+  in D.trace ("d=" ++ (show currentDepth)) $ 
+       if (null (WB.trees result) && maybe True (currentDepth <) maybeLim)
+         then searchProofWithIncrementalDepth a b c d setting (currentDepth+1) maybeLim 
+         else result
+
 -- | Prover for lightblue:
 prove' :: QT.ProverBuilder
 prove' QT.ProofSearchSetting{..} (DdB.ProofSearchQuery sig ctx typ) =  -- LiftT IO (Tree (U.Judgment U.DTT) UDTTrule)
@@ -65,8 +74,8 @@ prove' QT.ProofSearchSetting{..} (DdB.ProofSearchQuery sig ctx typ) =  -- LiftT
         WB.maxtime = case maxTime of
                         Just t -> t
                         Nothing -> 100000,
-        WB.debug = False,
+        WB.debug = verbose,
         WB.sStatus = WB.statusDef
         };
-      result = hojo ctx sig typ setting
+      result =  hojo ctx sig typ setting
   in ListT.fromFoldable $ map A.aTreeTojTree' $ WB.trees result
diff --git a/src/DTS/QueryTypes.hs b/src/DTS/QueryTypes.hs
index c37c0e7f..b1f1a3a0 100644
--- a/src/DTS/QueryTypes.hs
+++ b/src/DTS/QueryTypes.hs
@@ -78,6 +78,7 @@ data ProofSearchSetting = ProofSearchSetting {
   maxDepth :: Maybe Int
   , maxTime :: Maybe Int
   , logicSystem :: Maybe LogicSystem
+  , verbose :: Bool
   } deriving (Eq, Show)
 
 type Prover = DTTdB.ProofSearchQuery -> ListT IO DTTProofDiagram