diff --git a/prism-examples/phil_lss/phil_lss3.nm b/prism-examples/phil_lss/phil_lss3.nm
index c5e818fa..8365c802 100644
--- a/prism-examples/phil_lss/phil_lss3.nm
+++ b/prism-examples/phil_lss/phil_lss3.nm
@@ -56,8 +56,8 @@ endmodule
 // PHILOSOPHER 1
 // atomic formule 
 // left fork and right fork free resp.
-formula lfree = (p2=0..4,6,11,13);
-formula rfree = (p3=0..3,5,7,12,13);
+formula lfree = p2>=0&p2<=4|p2=6|p2=11|p2=13;
+formula rfree = p2>=0&p2<=3|p2=5|p2=7|p2=12|p2=13;
 
 module phil1
 
diff --git a/prism-examples/phil_lss/phil_lss4.nm b/prism-examples/phil_lss/phil_lss4.nm
index 0ef63eb3..cc0e4fcd 100644
--- a/prism-examples/phil_lss/phil_lss4.nm
+++ b/prism-examples/phil_lss/phil_lss4.nm
@@ -83,8 +83,8 @@ endmodule
 // PHILOSOPHER 1
 // atomic formule 
 // left fork and right fork free resp.
-formula lfree = (p2=0..4,6,11,13);
-formula rfree = (p4=0..3,5,7,12,13);
+formula lfree = p2>=0&p2<=4|p2=6|p2=11|p2=13;
+formula rfree = p2>=0&p2<=3|p2=5|p2=7|p2=12|p2=13;
 
 module phil1