diff --git a/CoAlgLogicUtils.ml b/CoAlgLogicUtils.ml
index c26417815e4001b0216718f96e7c9245737794b4..bea0a5166968a1a65cd65c983c17f42a8325942d 100644
--- a/CoAlgLogicUtils.ml
+++ b/CoAlgLogicUtils.ml
@@ -4,11 +4,17 @@ open Graph
 
 open CoAlgMisc
 
-let elemArray (x: 'a) (arr: 'a array) =
-    let res = ref (false) in
-    let f y = if (x == y) then res := true else () in
-    Array.iter f arr;
-    !res
+module TArray = struct
+    let any f arr =
+        let rec g idx =
+            if idx >= Array.length arr then false
+            else if f arr.(idx) then true
+            else g (idx + 1)
+        in g 0
+    let all f = any (fun x -> not (f x))
+    let elem (x: 'a) (arr: 'a array) =
+        any (fun y -> x == y) arr
+end
 
 let disjointAgents sort a b =
     assert (lfGetType sort a = EnforcesF || lfGetType sort a = AllowsF);
@@ -17,7 +23,7 @@ let disjointAgents sort a b =
     let lb = lfGetDestAg sort b in
     let res = ref (true) in
     let f idx =
-        if (elemArray idx lb) then res := false
+        if (TArray.elem idx lb) then res := false
         else ()
     in
     Array.iter f la;
diff --git a/CoAlgLogicUtils.mli b/CoAlgLogicUtils.mli
index 747b5ef1155626e72f482b970e99d791fdb0d2a2..24982aefe0ae6656dcf819865f5b3bf095e51016 100644
--- a/CoAlgLogicUtils.mli
+++ b/CoAlgLogicUtils.mli
@@ -6,10 +6,15 @@
 
 open CoAlgMisc
 
+module TArray : sig
+    val all : ('a -> bool) -> 'a array -> bool
+    val any : ('a -> bool) -> 'a array -> bool
+    val elem : 'a -> 'a array -> bool
+end
+
 val disjointAgents : sort -> localFormula -> localFormula -> bool
 
 val maxDisjoints : sort -> bset -> bset list
 
 
 
-
diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index fffff305e85695933c7402caa40bdca662cf3d3c..1c12404511e7f640d65b7c978cd51f9386f9225a 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -193,6 +193,7 @@ let compatible sort (a: bset) formula1 =
      /\ n                         /\ m              all C_i ⊆ D
     /  \i=1 a_i        /\    b   /  \j=1 c_j
 *)
+let agents = [|1;2;3;4;5;6;7;8;9;10|]
 
 let mkRule_CL sort bs sl =
   assert (List.length sl = 1); (* TODO: Why? *)
@@ -200,14 +201,18 @@ let mkRule_CL sort bs sl =
   let boxes = bsetFilter bs (fun f -> lfGetType sort f = EnforcesF) in
   let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
   let disjoints = maxDisjoints sort boxes in
+  let nCands = bsetMake () in (* all N-diamonds *)
+  let hasFullAgentList formula =
+    let aglist = lfGetDestAg sort formula in
+    let value = TArray.all (fun x -> TArray.elem x aglist) agents in
+    if (value) then bsetAdd nCands formula else () ;
+    value
+  in
+  (* Candidates for D in Rule 2 *)
+  let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
   (*
     mkRule_CL sort bs [s1]
-    = { (λ[bs1]. { ∀R.D
-      | <D> b ∈ bs
-      }
-      ∪ { (λ[bs1].{ [C_i]a_i ∈ bs | a_i ∈ bs1}
-          , [(s1, { a_i | i∈I })]
-          )
+    = { (λ[bs1]. bs, [(s1, { a_i | i∈I })])
         | {[C_i]a_i | i∈I} ⊆ bs,
           C_i pairwise disjoint and I maximal
         }
diff --git a/CoAlgLogics.mli b/CoAlgLogics.mli
index 48d0958b68bceec89898bf9788866dea0e7084bc..7416575b0cad34ec15c94bb7d9cce0bfd0d1b6ae 100644
--- a/CoAlgLogics.mli
+++ b/CoAlgLogics.mli
@@ -6,4 +6,5 @@
 open CoAlgMisc
 
 
+val agents : int array
 val getExpandingFunctionProducer : functors -> sort -> bset -> sort list -> stateExpander