doc-src/Sledgehammer/sledgehammer.tex

 Specifies the maximum number of facts that may be returned by the relevance
 filter. If the option is set to \textit{smart}, it is set to a value that was
 empirically found to be appropriate for the prover. A typical value would be
 250.
 
-\opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
+\opdefault{max\_new\_mono\_instances}{int}{\upshape 200}
 Specifies the maximum number of monomorphic instances to generate beyond
 \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
 are potentially generated. Whether monomorphization takes place depends on the
 type system used.