diff --git a/plceopen.mlw b/plceopen.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..e1b6cd0f3115967534d4975afa78151dfd26cd8d
--- /dev/null
+++ b/plceopen.mlw
@@ -0,0 +1,14 @@
+module PLCopen
+
+  predicate s8000
+  predicate a
+  predicate b
+  
+  axiom a: s8000 -> a /\ b 
+  
+  lemma la: not a -> not s8000
+  lemma lb: not b -> not s8000
+  
+  lemma lab: not a \/ not b -> not s8000
+  
+end
\ No newline at end of file