diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs
index 1781e1ebecbe47caf19646a2ee466913f6fc174e..ce9c9632172bdd81796f4d32a567aa207464d3bf 100644
--- a/examples/eq_paper.rs
+++ b/examples/eq_paper.rs
@@ -71,12 +71,6 @@ fn main() {
       kassert!(DATA[i].a & DATA[i].b);
     }
 
-    // S8001 -> !a & !b
-    // we can only stay or enter the Init state unless either (or both) inputs are false
-    if STATE == S8001 {
-      kassert!(!DATA[i].a | !DATA[i].b);
-    }
-
     // transition invariants
     if i > 0 {
       match STATE_H[i - 1] {