diff --git a/src/command_line/arguments.rs b/src/command_line/arguments.rs
index 6a39f919..674470fa 100644
--- a/src/command_line/arguments.rs
+++ b/src/command_line/arguments.rs
@@ -73,6 +73,10 @@ pub enum Command {
         ///   - additional knowledge used to construct the claim (e.g., user guide, proof outline).
         #[arg(verbatim_doc_comment)]
         files: Vec<PathBuf>,
+
+        /// The time limit in seconds to prove each conjecture passed to Vampire
+        #[arg(long, short, default_value_t = 30)]
+        time_limit: u16,
     },
 }
 
diff --git a/src/command_line/procedures.rs b/src/command_line/procedures.rs
index 815535f1..96db84c0 100644
--- a/src/command_line/procedures.rs
+++ b/src/command_line/procedures.rs
@@ -73,6 +73,7 @@ pub fn main() -> Result<()> {
             no_proof_search,
             save_problems: out_dir,
             files,
+            time_limit,
         } => {
             let files =
                 Files::sort(files).context("unable to sort the given files by their function")?;
@@ -140,7 +141,7 @@ pub fn main() -> Result<()> {
                 let mut success = true;
                 for problem in problems {
                     // TODO: Handle the error cases properly
-                    let report = Vampire.prove(problem)?;
+                    let report = Vampire.prove(problem, time_limit)?;
                     if !matches!(report.status()?, Status::Success(Success::Theorem)) {
                         success = false;
                     }
diff --git a/src/verifying/prover/mod.rs b/src/verifying/prover/mod.rs
index 93cf123d..144f2991 100644
--- a/src/verifying/prover/mod.rs
+++ b/src/verifying/prover/mod.rs
@@ -95,5 +95,5 @@ pub trait Prover {
     type Report: Report;
     type Error;
 
-    fn prove(&self, problem: Problem) -> Result<Self::Report, Self::Error>;
+    fn prove(&self, problem: Problem, time_limit: u16) -> Result<Self::Report, Self::Error>;
 }
diff --git a/src/verifying/prover/vampire.rs b/src/verifying/prover/vampire.rs
index ad98a691..bf3866a6 100644
--- a/src/verifying/prover/vampire.rs
+++ b/src/verifying/prover/vampire.rs
@@ -83,9 +83,9 @@ impl Prover for Vampire {
     type Error = VampireError;
     type Report = VampireReport;
 
-    fn prove(&self, problem: Problem) -> Result<Self::Report, Self::Error> {
+    fn prove(&self, problem: Problem, time_limit: u16) -> Result<Self::Report, Self::Error> {
         let mut child = Command::new("vampire")
-            .args(["--mode", "casc"])
+            .args(["--mode", "casc", "--time_limit", &time_limit.to_string()])
             .stdin(Stdio::piped())
             .stdout(Stdio::piped())
             .stderr(Stdio::piped())