diff --git a/src/Theory/Constraint/Solver/Contradictions.hs b/src/Theory/Constraint/Solver/Contradictions.hs
--- a/src/Theory/Constraint/Solver/Contradictions.hs
+++ b/src/Theory/Constraint/Solver/Contradictions.hs
@@ -187,7 +187,8 @@
         -- FIXME: There should be a weaker version of the rule that just
         -- introduces the constraint 'k < j || k == j' here.
         checkRule jRu    = any conflictingFact (L.get rPrems jRu) &&
-                           k `S.member` D.reachableSet [j] less
+                           (k `S.member` D.reachableSet [j] less
+                             || isLast se k)
 
     guard isCounterExample
     return (i, j, k) -- counter-example to unique fact instances
diff --git a/tamarin-prover-theory.cabal b/tamarin-prover-theory.cabal
--- a/tamarin-prover-theory.cabal
+++ b/tamarin-prover-theory.cabal
@@ -2,7 +2,7 @@
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            0.8.5.1
+version:            0.8.6.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers