diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index c7f4a376ed0cdaf01b58ecd44f4124dd3328321f..58b3492a76c2214111297eb69cb8e6cef111aa97 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -209,18 +209,32 @@ let mkRule_CL sort bs sl : stateExpander =
   let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
   let disjoints = maxDisjoints sort boxes in
   (*print_endline ("disjoints: "^(string_of_coalition_list sort disjoints)); *)
+  let nCandsEmpty = ref (true) in
   let nCands = bsetMakeRealEmpty () in (* all N-diamonds *)
+  let dCandsEmpty = ref (true) in
   let hasFullAgentList formula =
     let aglist = lfGetDestAg sort formula in
     let value = TArray.all (fun x -> TArray.elem x aglist) (cl_get_agents ()) in
-    if (value) then bsetAdd nCands formula else () ;
+    if (value) then
+    begin
+        bsetAdd nCands formula;
+        nCandsEmpty := false
+    end
+    else dCandsEmpty := false;
     value
   in
   (* Candidates for D in Rule 2 *)
+  (* implicitly fill nCands *)
   let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
+  (*
+  print_endline ("For set " ^(CoAlgMisc.bsetToString sort bs));
+  print_endline ("N-Cands: " ^(CoAlgMisc.bsetToString sort nCands));
+  print_endline ("D-Cands: " ^(CoAlgMisc.bsetToString sort dCands));
+  *)
   let c_j : localFormula list =
     bsetFold (fun f a -> (lfGetDest1 sort f)::a) nCands []
   in
+  (* rule 2 for diamaonds where D is a proper subset of the agent set N *)
   let getRule2 diamDb acc = (* diamDb = <D> b *)
     (* print_endline "Rule2" ; *)
     let d = lfGetDestAg sort diamDb in (* the agent list *)
@@ -247,6 +261,31 @@ let mkRule_CL sort bs sl : stateExpander =
     List.fold_left createSingleRule acc maxdisj
   in
   let rules = bsetFold getRule2 dCands [] in
+  let getRule2ForFullAgents acc =
+    (* if there are N-diamonds but no diamonds with a proper subset of the agents,
+       then we need an explicit rule 2
+    *)
+    if not !nCandsEmpty && !dCandsEmpty then begin
+        (* create rule 2 once for all the diamonds with a full agent set *)
+        let maxdisj = maxDisjoints sort boxes in
+        let createSingleRule acc coalitions =
+            let a_i : localFormula list =
+                bsetFold (fun f a -> (lfGetDest1 sort f)::a) coalitions []
+            in
+            (* now do rule 2:
+                coalitions  /\ nCands
+               ———————————————————————
+                  a_i       /\ c_j
+            *)
+            let children = bsetMakeRealEmpty () in
+            List.iter (bsetAdd children) (c_j) ;
+            List.iter (bsetAdd children) (a_i) ;
+            ((fun bs1 -> bs), lazylistFromList [(s1, children)])::acc
+        in
+        List.fold_left createSingleRule acc maxdisj
+    end else acc
+  in
+  let rules = getRule2ForFullAgents rules in
   let getRule1 acc coalitions =
     (* print_endline "Rule1" ; *)
     (* do rule 1:
diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index 63fb1fded518fa1efd43a78f8472d17e33e11034..9074919d974d244fd6c50e0532113f03bc05f878 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -62,7 +62,7 @@ let runSatCheckVerbose (sc:satCheck) =
     let res = runSatCheck sc in
     (if (res = expectation)
     then PF.printf "%s\n" (cs "1;32" "Yes")
-    else PF.printf "%s, it is %s\n"
+    else PF.printf "%s, cool claims it is %s\n"
                     (cs "1;31" "No")
                     (sotr res));
     flush stdout;
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 3e94b7592cbd35b8647ac9146b2b1dbc57851c07..6bab2be75f26785eef719cd0f938e50b8ebf71d3 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -74,6 +74,7 @@ let cl_testcases : testcase_section =
     ; unsat "[{1}] C & <{ 1 2 }> ~C"
     ; sat   "<{ 1 2 }> C & <{ 1 2 }> ~C"
     ; unsat "<{ 1 2 }> C & [{ 1 2 }] ~C"
+    ; unsat "<{ 1 2 3 4 5 }> C & <{ 1 2 3 4 5 }> ~C"
     ; sat   "([{1 3}] C) & ([{ 2 3 }] ~C )"
     ]