diff --git a/mc.cc b/mc.cc
index 1f443cf..c4a3173 100644
--- a/mc.cc
+++ b/mc.cc
@@ -359,6 +359,14 @@ BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form)
     auto proc_id = srs->rs->getProcessID(form->getSingleAgent());
     return *reach - (statesNK(*reach - getStatesRSCTLK(form->getLeftSF()), proc_id) * *reach);
   }
+  else if (oper == RSCTLK_NE) {
+    auto proc_set = form->getAgentsAsProcSet(srs->rs);
+    return statesNE(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_set) * *reach;
+  }
+  else if (oper == RSCTLK_UE) {
+    auto proc_set = form->getAgentsAsProcSet(srs->rs);
+    return *reach - (statesNE(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach);
+  }
   else if (oper == RSCTLK_NC)
   {
     auto proc_set = form->getAgentsAsProcSet(srs->rs);
@@ -463,6 +471,18 @@ BDD ModelChecker::statesNK(const BDD &states, Process proc_id)
   return x;
 }
 
+BDD ModelChecker::statesNE(const BDD &states, ProcSet processes)
+{
+  BDD x = BDD_FALSE;
+
+  for (auto const &proc_id : processes)
+  {
+    x += states.ExistAbstract(getIthOnly(proc_id));
+  }
+
+  return x;
+}
+
 BDD ModelChecker::statesNC(const BDD &states, ProcSet processes)
 {
   BDD x = BDD_FALSE;
diff --git a/mc.hh b/mc.hh
index 1274f61..a331bb0 100644
--- a/mc.hh
+++ b/mc.hh
@@ -61,6 +61,7 @@ class ModelChecker
     BDD statesEUctx(const BDD *contexts, const BDD &statesA, const BDD &statesB);
     BDD statesEFctx(const BDD *contexts, const BDD &states);
     BDD statesNK(const BDD &states, Process proc_id);
+    BDD statesNE(const BDD &states, ProcSet processes);
     BDD statesNC(const BDD &states, ProcSet processes);
 
     BDD getIthOnly(Process proc_id);
diff --git a/rsin_parser.yy b/rsin_parser.yy
index ebece8b..9cead08 100644
--- a/rsin_parser.yy
+++ b/rsin_parser.yy
@@ -409,6 +409,14 @@ rsctlk_form:
         $$ = new FormRSCTLK(RSCTLK_NE, *$3, $6);
         free($3);
     }
+    | UC LSB agents RSB LRB rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_UC, *$3, $6);
+        free($3);
+    }
+    | NC LSB agents RSB LRB rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_NC, *$3, $6);
+        free($3);
+    }
 
     // | E LSB actions RSB X rsctlk_form {
     //     $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);