diff --git a/Example/Abduction_Example/TIP_prop_06.thy b/Example/Abduction_Example/TIP_prop_06.thy
index 6aa2f37b..bd5a8d30 100644
--- a/Example/Abduction_Example/TIP_prop_06.thy
+++ b/Example/Abduction_Example/TIP_prop_06.thy
@@ -30,6 +30,7 @@ fun t2 :: "Nat => Nat => Nat" where
   "t2 (Z) z = z"
 | "t2 (S z2) z = S (t2 z2 z)"
 
+(*On a MacBook Pro 2021 or later, this takes about 30 minutes.*)
 prove  property0: "((length (rev (x y z))) = (t2 (length y) (length z)))"
 
 end
diff --git a/Example/Abduction_Example/TIP_prop_11.thy b/Example/Abduction_Example/TIP_prop_11.thy
index e0f76c34..751cf7d7 100644
--- a/Example/Abduction_Example/TIP_prop_11.thy
+++ b/Example/Abduction_Example/TIP_prop_11.thy
@@ -20,6 +20,7 @@ fun rev :: "'a list => 'a list" where
   "rev (nil2) = nil2"
 | "rev (cons2 z xs) = x (rev xs) (cons2 z (nil2))"
 
+(*On a MacBook Pro 2021 or later, this takes about 10 minutes.*)
 prove property0 :
   "((rev (x (rev y) (rev z))) = (x z y))"