diff --git a/GMLMIP-0.1/formulas/formula.cpp b/GMLMIP-0.1/formulas/formula.cpp
index 09a9e6ab22fb25e1e894799104bdf0fa8266f7bf..ec2beb4ed7e7bb1beea1af13d99d75b8ed26576e 100644
--- a/GMLMIP-0.1/formulas/formula.cpp
+++ b/GMLMIP-0.1/formulas/formula.cpp
@@ -109,7 +109,7 @@ 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(underlying_formulae, i));
+				result.insert(concs.get_jth_conclusion((IFormula*)this, underlying_formulae, i));
 			}
 		} else {
 			result = enumerate_rules(premise, underlying_formulae);
@@ -221,7 +221,7 @@ 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(underlying_formulae, 0));
+						result.insert(temp.get_jth_conclusion(this, underlying_formulae, 0));
 					} 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 6226bbf1804d684a6f32f02626afbf37c48c8384..e263210c523b08b3434aa8cf438d1cf0e18f7fd0 100644
--- a/GMLMIP-0.1/formulas/formula.h
+++ b/GMLMIP-0.1/formulas/formula.h
@@ -46,6 +46,7 @@ class IFormula {
 		virtual bool satisfiability(int option)=0;
 		virtual void clear_maps()=0;
 		virtual RuleCollection onestep() = 0;
+		virtual int get_variables_back(int bddvar) = 0;
 };
 
 template<class ModalValueType>
@@ -151,6 +152,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]; }
 		
 		bool satisfiability(int option){ assert(0=="patched GMLMIP\n"); return true;};
 		RuleCollection onestep() { return check_satisfiability(bdd_rep); };
diff --git a/GMLMIP-0.1/onestep.cpp b/GMLMIP-0.1/onestep.cpp
index 99bf6b77a320385f3f37930beffb8a45d1a7d608..94182a0b342526db643d7ac75b25df244ebf9931 100644
--- a/GMLMIP-0.1/onestep.cpp
+++ b/GMLMIP-0.1/onestep.cpp
@@ -9,6 +9,7 @@
 #include "./formulas/PML_formula.h"
 #include "./formulas/rational.h"
 #include "./formulas/satisfyingassignment.h"
+#include "./rules/setofconclusions.h"
 #include "satisfyingstack.h"
 
 using namespace std;
diff --git a/GMLMIP-0.1/rules/setofconclusions.cpp b/GMLMIP-0.1/rules/setofconclusions.cpp
index 98b25f15725366e6948162ba3b1919d193a38da3..8af62ccac61fdd3edc3f9e6011def9b3a8320a59 100644
--- a/GMLMIP-0.1/rules/setofconclusions.cpp
+++ b/GMLMIP-0.1/rules/setofconclusions.cpp
@@ -1,5 +1,6 @@
 #include "setofconclusions.h"
 #include <set>
+#include "../formulas/formula.h"
 
 SetOfConclusions::SetOfConclusions(int n, const vector<vector<bool> >& set){
 	no_of_literals=n;
@@ -18,18 +19,17 @@ SetOfConclusions::SetOfConclusions(int n, const vector<vector<bool> >& set){
 	}
 }
 
-set<set<int> > SetOfConclusions::get_jth_conclusion(bdd** underlying, int j){
+set<set<int> > SetOfConclusions::get_jth_conclusion(IFormula* f, bdd** underlying, int j){
 	set< set<int> > disj;
 	for(unsigned int i=0; i < rules[j].size(); i++){
 		set<int> conj;
 		for(int k=0; k < no_of_literals; k++){
 			if(rules[j][i].get_p_i(k)==1)
-				conj.insert(bdd_var(*(underlying[k])));
+				conj.insert(f->get_variables_back(bdd_var(*(underlying[k]))));
 			if(rules[j][i].get_p_i(k)==0)
-				conj.insert(-bdd_var(bdd_not(*(underlying[k]))));
+				conj.insert(-f->get_variables_back(bdd_var(bdd_not(*(underlying[k])))));
 		}
 		disj.insert(conj);
 	}
 	return disj;
 }
-
diff --git a/GMLMIP-0.1/rules/setofconclusions.h b/GMLMIP-0.1/rules/setofconclusions.h
index c0e11425e54e6ecac7dd5cc5de390b2efca8e4cb..54e1451919663cf02e68b3cc840cf2db4f8a529e 100644
--- a/GMLMIP-0.1/rules/setofconclusions.h
+++ b/GMLMIP-0.1/rules/setofconclusions.h
@@ -19,6 +19,8 @@ using namespace std;
 
 typedef vector<TruthAssignment> Conclusion;
 
+class IFormula;
+
 class SetOfConclusions{
 	private:
 		int no_of_literals;
@@ -29,10 +31,7 @@ class SetOfConclusions{
 		SetOfConclusions(int n, const vector<vector<bool> >& set);
 		
 		int number_of_conclusions(){return rules.size();};		
-		set<set<int> > get_jth_conclusion(bdd** underlying, int j);
-		
-		
-		
+		set<set<int> > get_jth_conclusion(IFormula* f, bdd** underlying, int j);
 		
 		//bdd get_ith_conclusion(int i, bdd* bddarray);
 };