diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index ec2beb4ed7e7bb1beea1af13d99d75b8ed26576e..6e909c60bf3b4ae8576a3ef2feefdd1c9db89d0a 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -1,6 +1,7 @@
 #include "formula.h"
 
 #include <set>
+#include <cassert>
 
 IFormula::~IFormula() {
 }
@@ -48,6 +49,34 @@ void Formula<ModalValueType>::print_back_vars(){
 	cout << endl;
 }
 
+vector<SatisfyingAssignment> gatherer_stack;
+
+void sat_handler_gatherer(char *varset, int size){
+	SatisfyingAssignment s(size, varset);
+	gatherer_stack.push_back(s);
+}
+
+template<class ModalValueType>
+set<set<int> > Formula<ModalValueType>::gatherRules(bdd b) {
+	bdd_allsat(b, sat_handler_gatherer);
+	vector<SatisfyingAssignment> sat_ass = gatherer_stack;
+	gatherer_stack.clear();
+	set<set<int> > disj;
+	for (vector<SatisfyingAssignment>::iterator it = sat_ass.begin();
+		it != sat_ass.end(); ++it)
+	{
+		set<int> conj;
+		SatisfyingAssignment& sat = *it;
+		for (int v = 0; v < sat.get_size(); v++) {
+			if (!variables_back.count(v)) continue;
+			int sgn = ((sat.get_array_i(v)==1) ? 1 : (-1));
+			conj.insert(variables_back[v] * sgn);
+		}
+		disj.insert(conj);
+	}
+	return disj;
+}
+
 void sat_handler(char *varset, int size){
 	SatisfyingAssignment s(size, varset);
 	sat_ass_stack.push_back(s);
@@ -59,8 +88,15 @@ RuleCollection Formula<ModalValueType>::check_satisfiability(bdd b){
 	bdd_allsat(b, sat_handler); // pushes satisfying assignment onto stack
 	vector<SatisfyingAssignment> sat_ass = sat_ass_stack; 
 	sat_ass_stack.clear();	
-	assert(sat_ass.size() == 1);
-	return apply_rules(sat_ass[0]);
+	// it might be zero if already on the syntactic level there is something like A /\ ~A
+	assert(sat_ass.size() <= 1);
+	if (sat_ass.size() == 1) {
+		return apply_rules(sat_ass[0]);
+	} else {
+		// TODO: return {} or { {} }?
+		// the secound one would mean { False }
+		return set<set<set<int> > >();
+	}
 }
 
 template<class ModalValueType>
@@ -109,7 +145,8 @@ RuleCollection Formula<ModalValueType>::apply_rules(SatisfyingAssignment& sat){
 		if(rule_cache.count(premise)){ // if in cache
 			SetOfConclusions concs = rule_cache[premise];
 			for(int i = 0; i < concs.number_of_conclusions(); i++){
-				result.insert(concs.get_jth_conclusion((IFormula*)this, underlying_formulae, i));
+				bdd b = concs.get_jth_conclusion(underlying_formulae, i);
+				result.insert(gatherRules(b));
 			}
 		} else {
 			result = enumerate_rules(premise, underlying_formulae);
@@ -221,7 +258,8 @@ RuleCollection Formula<ModalValueType>::enum_rules_intern(glp_prob* problem, glp
 						vector<vector<bool> > singleton;
 						singleton.push_back(new_node);
 						SetOfConclusions temp = SetOfConclusions(prem.get_n() + prem.get_m(), singleton);
-						result.insert(temp.get_jth_conclusion(this, underlying_formulae, 0));
+						bdd b = temp.get_jth_conclusion(underlying_formulae, 0);
+						result.insert(gatherRules(b));
 					} else {
 						new_node_queue.push_back(new_node);
 					}
diff --git a/GMLMIP-0.1/formulas/formula.h b/GMLMIP-0.1/formulas/formula.h
index e263210c523b08b3434aa8cf438d1cf0e18f7fd0..e7a50c40173a128afda7a8b55f9399a84d888c2b 100644
--- a/GMLMIP-0.1/formulas/formula.h
+++ b/GMLMIP-0.1/formulas/formula.h
@@ -153,6 +153,7 @@ class Formula : public IFormula{
 		void print_back_vars();
 		//virtual void print_back_modal()=0;
 		int get_variables_back(int bddvar) { return variables_back[bddvar]; }
+		set<set<int> > gatherRules(bdd b);
 		
 		bool satisfiability(int option){ assert(0=="patched GMLMIP\n"); return true;};
 		RuleCollection onestep() { return check_satisfiability(bdd_rep); };