diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java
new file mode 100644
index 0000000..29a216b
--- /dev/null
+++ b/src/main/java/inference/EquationAxiom.java
@@ -0,0 +1,95 @@
+package inference;
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
+import exceptions.SubstituteFailedException;
+import models.formulas.DependencyFormula;
+import models.formulas.EquationFormula;
+import models.formulas.Formula;
+import models.formulas.meta.MetaEquationFormula;
+import models.formulas.meta.MetaFormula;
+import models.terms.DependencyTerm;
+import models.terms.EvaluatableTerm;
+import models.terms.RDLTerm;
+import models.terms.Resource;
+import models.terms.meta.MatchConstraint;
+import models.terms.meta.MetaRDLTerm;
+
+public class EquationAxiom extends InferenceRule {
+
+	public EquationAxiom(String name, List<MetaFormula> assumptions, MetaEquationFormula conclusion, InferenceOrderConstraint constraint) {
+		super(name, assumptions, conclusion, constraint);
+	}
+	
+	public EquationAxiom(String name, List<MetaFormula> assumptions, MetaEquationFormula conclusion) {
+		super(name, assumptions, conclusion);
+	}
+	
+	public Set<EquationFormula> apply(List<Formula>assumptions,  EvaluatableTerm leftSideHand) {
+		Set<EquationFormula> result = new HashSet<>();
+		if (assumptions.size() < this.assumptions.size()) {
+			return new HashSet<>();
+		}
+		MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion;
+		Set<MatchConstraint> matchResult = ((MetaRDLTerm) metaConclusion.getLeftSideHand()).isMatchedBy(leftSideHand);
+		if (result.isEmpty()) {
+			return new HashSet<>();
+		}
+		for (int i = 0; i < assumptions.size(); i++) {
+			Formula assumption = assumptions.get(i);
+			MetaFormula metaAssumption = this.assumptions.get(i);
+			matchResult = metaAssumption.isMatchedBy(assumption, matchResult);
+			if (result.isEmpty()) {
+				return new HashSet<>();
+			}
+		}
+		for (MatchConstraint matchRes: matchResult) {
+			try {
+				result.add(metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext()));
+			} catch (SubstituteFailedException e) {
+				continue;
+			}
+		}
+		return result;
+	}
+	
+	
+	
+	private static Set<DependencyFormula> requiredAssumptions(EvaluatableTerm term) {
+		if (term instanceof Resource) {
+			return new HashSet<>();
+		}
+		DependencyTerm depTerm = (DependencyTerm) term;
+		Set<DependencyFormula> result = new HashSet<>();
+		EvaluatableTerm dependingTerm = depTerm.getDependingTerm();
+		List<EvaluatableTerm> dependedTerms = depTerm.getDependedTerms();
+		List<EvaluatableTerm> argumentTerms = depTerm.getArgumentTerms();
+		if (dependingTerm instanceof Resource) {
+			result.add(new DependencyFormula(dependingTerm, dependedTerms));
+		} else if (dependingTerm instanceof DependencyTerm depending) {
+			for (Formula formula : requiredAssumptions(depending)) {
+				if (formula instanceof DependencyFormula dependency) {
+					DependencyTerm newDependingTerm = new DependencyTerm((EvaluatableTerm) dependency.getDependency().getDependingTerm(), dependedTerms, argumentTerms);
+					List<EvaluatableTerm> newDependedTerms = new ArrayList<>();
+					for (RDLTerm dependedTerm : dependency.getDependency().getDependedTerms()) {
+						newDependedTerms.add(new DependencyTerm((EvaluatableTerm) dependedTerm, dependedTerms, argumentTerms));
+					}
+					result.add(new DependencyFormula(newDependingTerm, newDependedTerms));
+				} 
+			}
+		}
+		return result;
+	}
+	
+	private static boolean conclusionCheck(EvaluatableTerm leftSideHand, Set<Formula> formulas) {
+		for (Formula formula: requiredAssumptions(leftSideHand)) {
+			if (! formulas.contains(formula)) { 
+				return false;
+			}
+		}
+		return true;
+	}
+	
+}
diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java
index c8c1ffc..ffe0934 100644
--- a/src/main/java/inference/InferenceRule.java
+++ b/src/main/java/inference/InferenceRule.java
@@ -1,24 +1,12 @@
 package inference;
 
 import java.util.ArrayList;
-import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
 
-import exceptions.SubstituteFailedException;
 import lombok.Getter;
-import models.formulas.DependencyFormula;
-import models.formulas.EquationFormula;
-import models.formulas.Formula;
-import models.formulas.meta.MetaEquationFormula;
 import models.formulas.meta.MetaFormula;
-import models.terms.DependencyTerm;
-import models.terms.EvaluatableTerm;
-import models.terms.RDLTerm;
-import models.terms.Resource;
-import models.terms.meta.MatchConstraint;
 import models.terms.meta.MetaVariable;
-import utils.Product;
 
 public class InferenceRule {
 
@@ -53,158 +41,96 @@
 		this(name, assumptions, conclusion, null);
 	}
 	
-	public Set<Formula> apply(Set<Formula> formulas, Set<RDLTerm> existTerms) {
-		List<List<Formula>> matchFormulas = new ArrayList<>();
-		List<List<RDLTerm>> matchTerms = new ArrayList<>();
-		Set<Formula> result = new HashSet<>();
-		for (int i = 0; i < assumptions.size(); i++) {
-			matchFormulas.add(new ArrayList<>());
-			for (Formula formula: formulas) {
-				if (! assumptions.get(i).isMatchedBy(formula).isEmpty()) {
-					matchFormulas.get(i).add(formula);
-				}
-			}
-			if (matchFormulas.get(i).isEmpty()) { 
-				return new HashSet<>();
-			}
-		}
-		for (int i = 0; i < missingVariables.size(); i++) {
-			matchTerms.add(new ArrayList<>());
-			for (RDLTerm term : existTerms) {
-				if (! missingVariables.get(i).isMatchedBy(term).isEmpty()) {
-					matchTerms.get(i).add(term);
-				}
-			}
-			if (matchTerms.get(i).isEmpty()) {
-				return new HashSet<>();
-			}
-		}
-		if (matchFormulas.size() == 0) {
-			for (List<RDLTerm> terms : Product.product(matchTerms)) {
-				MatchConstraint constraint = MatchConstraint.createDefault();
-				for (int i = 0; i < terms.size(); i++) {
-					MetaVariable variable = missingVariables.get(i);
-					RDLTerm term = terms.get(i);
-					constraint.setBinding(variable.getVariableName(), term);
-					Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
-					if (conclusionCheck(conclusion, constraint, formulas)) {
-						result.add(conclusion);
-					}
-				}
-			}
-		}
-		for (List<Formula> assumptions: Product.product(matchFormulas)) {
-			Set<MatchConstraint> matchResult = matchCheck(assumptions);
-			if (matchResult.isEmpty()) {
-				continue;
-			}
-			for (MatchConstraint constraint: matchResult) {
-				if (missingVariables.size() == 0) {
-					try {
-						Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
-						if (conclusionCheck(conclusion, constraint, formulas)) {
-							result.add(conclusion);
-						}
-					} catch (SubstituteFailedException e) {
-						continue;
-					}
-				}
-				for (List<RDLTerm> terms : Product.product(matchTerms)) {
-					for (int i = 0; i < terms.size(); i++) {
-						MetaVariable variable = missingVariables.get(i);
-						RDLTerm term = terms.get(i);
-						constraint.setBinding(variable.getVariableName(), term);
-						try {
-							Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
-							if (conclusionCheck(conclusion, constraint, formulas)) {
-								result.add(conclusion);
-							}
-						} catch (SubstituteFailedException e) {
-							continue;
-						}
-						
-					}
-				}
-			}
-		}
-		return result;
-	}
-	
-	protected Set<MatchConstraint> matchCheck(List<Formula> assumptions) {
-		Set<MatchConstraint> matchResult = new HashSet<>();
-		matchResult.add(MatchConstraint.createDefault());
-		for (int i = 0; i < assumptions.size(); i++) {
-			Formula assumption = assumptions.get(i);
-			MetaFormula metaAssumption = this.assumptions.get(i);
-			matchResult = metaAssumption.isMatchedBy(assumption, matchResult);
-			if (matchResult.isEmpty()) {
-				return new HashSet<>();
-			}
-		}
-		return matchResult;
-	}
-	
-	private static Set<Formula> requiredAssumptions(EvaluatableTerm term) {
-		if (term instanceof Resource) {
-			return new HashSet<>();
-		}
-		DependencyTerm depTerm = (DependencyTerm) term;
-		Set<Formula> result = new HashSet<>();
-		EvaluatableTerm dependingTerm = depTerm.getDependingTerm();
-		List<EvaluatableTerm> dependedTerms = depTerm.getDependedTerms();
-		List<EvaluatableTerm> argumentTerms = depTerm.getArgumentTerms();
-		for (int i = 0; i < dependedTerms.size(); i++) {
-			EvaluatableTerm dependedTerm = dependedTerms.get(i);
-			EvaluatableTerm argTerm = argumentTerms.get(i);
-			In in = new In(argTerm, dependedTerm);
-			result.add(in);
-		}
-		if (dependingTerm instanceof Resource) {
-			result.add(new DependencyFormula(dependingTerm, dependedTerms));
-		} else if (dependingTerm instanceof DependencyTerm depending) {
-			for (Formula formula : requiredAssumptions(depending)) {
-				if (formula instanceof DependencyFormula dependency) {
-					DependencyTerm newDependingTerm = new DependencyTerm((EvaluatableTerm) dependency.getDependency().getDependingTerm(), dependedTerms, argumentTerms);
-					List<EvaluatableTerm> newDependedTerms = new ArrayList<>();
-					for (RDLTerm dependedTerm : dependency.getDependency().getDependedTerms()) {
-						newDependedTerms.add(new DependencyTerm((EvaluatableTerm) dependedTerm, dependedTerms, argumentTerms));
-					}
-					result.add(new DependencyFormula(newDependingTerm, newDependedTerms));
-				} else if(formula instanceof In in) {
-					result.add(new In(new DependencyTerm(in.getLeftSideHand(), dependedTerms, argumentTerms), new DependencyTerm(in.getRightSideHand(), dependedTerms, argumentTerms)));
-				}
-			}
-		}
-		return result;
-	}
-	
-	private static boolean conclusionCheck(Formula conclusion, MatchConstraint constraint, Set<Formula> formulas) {
-		if (conclusion instanceof DependencyFormula) return true;
-		EquationFormula eq = (EquationFormula) conclusion;
-		EvaluatableTerm leftSideHand = eq.getLeftSideHand();
-		for (Formula formula: requiredAssumptions(leftSideHand)) {
-			if (formula instanceof DependencyFormula dep) {
-				if (! formulas.contains(dep)) { 
-					return false;
-				}
-			} else if (formula instanceof In in) {
-				boolean flg = false;
-				for (MetaEquationFormula metaFormula: in.deriveRule()) {
-					for (Formula existFormula: formulas) {
-						if (! metaFormula.isMatchedBy(existFormula, constraint).isEmpty()) {
-							flg = true;
-							break;
-						}
-					}
-					if (flg) break;
-				}
-				if (!flg) {
-					return false;
-				}
-			}
-		}
-		return true;
-	}
+//	public Set<Formula> apply(Set<Formula> formulas, Set<RDLTerm> existTerms) {
+//		List<List<Formula>> matchFormulas = new ArrayList<>();
+//		List<List<RDLTerm>> matchTerms = new ArrayList<>();
+//		Set<Formula> result = new HashSet<>();
+//		for (int i = 0; i < assumptions.size(); i++) {
+//			matchFormulas.add(new ArrayList<>());
+//			for (Formula formula: formulas) {
+//				if (! assumptions.get(i).isMatchedBy(formula).isEmpty()) {
+//					matchFormulas.get(i).add(formula);
+//				}
+//			}
+//			if (matchFormulas.get(i).isEmpty()) { 
+//				return new HashSet<>();
+//			}
+//		}
+//		for (int i = 0; i < missingVariables.size(); i++) {
+//			matchTerms.add(new ArrayList<>());
+//			for (RDLTerm term : existTerms) {
+//				if (! missingVariables.get(i).isMatchedBy(term).isEmpty()) {
+//					matchTerms.get(i).add(term);
+//				}
+//			}
+//			if (matchTerms.get(i).isEmpty()) {
+//				return new HashSet<>();
+//			}
+//		}
+//		if (matchFormulas.size() == 0) {
+//			for (List<RDLTerm> terms : Product.product(matchTerms)) {
+//				MatchConstraint constraint = MatchConstraint.createDefault();
+//				for (int i = 0; i < terms.size(); i++) {
+//					MetaVariable variable = missingVariables.get(i);
+//					RDLTerm term = terms.get(i);
+//					constraint.setBinding(variable.getVariableName(), term);
+//					Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
+//					if (conclusionCheck(conclusion, constraint, formulas)) {
+//						result.add(conclusion);
+//					}
+//				}
+//			}
+//		}
+//		for (List<Formula> assumptions: Product.product(matchFormulas)) {
+//			Set<MatchConstraint> matchResult = matchCheck(assumptions);
+//			if (matchResult.isEmpty()) {
+//				continue;
+//			}
+//			for (MatchConstraint constraint: matchResult) {
+//				if (missingVariables.size() == 0) {
+//					try {
+//						Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
+//						if (conclusionCheck(conclusion, constraint, formulas)) {
+//							result.add(conclusion);
+//						}
+//					} catch (SubstituteFailedException e) {
+//						continue;
+//					}
+//				}
+//				for (List<RDLTerm> terms : Product.product(matchTerms)) {
+//					for (int i = 0; i < terms.size(); i++) {
+//						MetaVariable variable = missingVariables.get(i);
+//						RDLTerm term = terms.get(i);
+//						constraint.setBinding(variable.getVariableName(), term);
+//						try {
+//							Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext());
+//							if (conclusionCheck(conclusion, constraint, formulas)) {
+//								result.add(conclusion);
+//							}
+//						} catch (SubstituteFailedException e) {
+//							continue;
+//						}
+//						
+//					}
+//				}
+//			}
+//		}
+//		return result;
+//	}
+//	
+//	protected Set<MatchConstraint> matchCheck(List<Formula> assumptions) {
+//		Set<MatchConstraint> matchResult = new HashSet<>();
+//		matchResult.add(MatchConstraint.createDefault());
+//		for (int i = 0; i < assumptions.size(); i++) {
+//			Formula assumption = assumptions.get(i);
+//			MetaFormula metaAssumption = this.assumptions.get(i);
+//			matchResult = metaAssumption.isMatchedBy(assumption, matchResult);
+//			if (matchResult.isEmpty()) {
+//				return new HashSet<>();
+//			}
+//		}
+//		return matchResult;
+//	}
 	
 	public int getAssumptionSize() {
 		return this.assumptions.size();
diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java
index 99f8f3e..a1fea57 100644
--- a/src/main/java/inference/ProofSystem.java
+++ b/src/main/java/inference/ProofSystem.java
@@ -1,22 +1,16 @@
 package inference;
 
-import java.util.ArrayList;
-import java.util.HashMap;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
 
-import com.google.common.collect.BoundType;
-
 import models.algebra.Variable;
 import models.formulas.DependencyFormula;
 import models.formulas.EquationFormula;
 import models.formulas.Formula;
 import models.formulas.meta.MetaDependencyFormula;
 import models.formulas.meta.MetaEquationFormula;
-import models.terms.Dependency;
-import models.terms.EvaluatableTerm;
 import models.terms.RDLTerm;
 import models.terms.meta.MetaDynamicDependency;
 import models.terms.meta.MetaDynamicDependencyTerm;
@@ -124,99 +118,66 @@
 					)
 			)
 	);
-//	
-//	public static final InferenceRule leftSubstitution = new EquationAxiom(
-//			"Left Substitution",
-//			List.of(
-//					new MetaEquationFormula(
-//							new MetaEvaluatableTermVariable(new Variable("se")),
-//							new MetaEvaluatableTermVariable(new Variable("te"))
-//					)
-//			),
-//			List.of(
-//					new MetaDependencyFormula(
-//							new MetaEvaluatableTermVariable(new Variable("se")), 
-//							new MetaEvaluatableTermVariable(new Variable("re")) 
-//					),
-//					new MetaEquationFormula(
-//							new MetaDependencyTerm(
-//									new MetaEvaluatableTermVariable(new Variable("re")),
-//									new MetaEvaluatableTermVariable(new Variable("x")),
-//									new MetaEvaluatableTermVariable(new Variable("y"))
-//							),
-//							new MetaEvaluatableTermVariable(new Variable("ue"))
-//					)
-//			),
-//			new MetaEquationFormula(
-//					new MetaDynamicDependencyTerm(
-//							new MetaTermGenerator() {
-//								@Override
-//								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
-//									curIndex -= 1;
-//									if (curIndex % 2 == 0) {
-//										return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2));
-//									}
-//									return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
-//								}
-//							},
-//							new MetaEvaluatableTermVariable(new Variable("se"))
-//					),
-//					new MetaDynamicDependencyTerm(
-//							new MetaTermGenerator() {
-//								@Override
-//								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
-//									curIndex -= 1;
-//									if (curIndex % 2 == 0) {
-//										return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2));
-//									}
-//									return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
-//								}
-//							},
-//							new MetaEvaluatableTermVariable(new Variable("te"))
-//					)
-//			),
-//			null,
-//			(assumptions) -> (assumptions.size() - 1) / 2 * 2 + 1,
-//			(assumptions) -> 1,
-//			(conclusion) -> (conclusion.getMaxIndex() - 1) / 2
-//	);
-//	
+	
+	
+	public static final InferenceRule leftSubstitution = new InferenceRule(
+			"Left Substitution",
+			List.of(
+					new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te")))
+			),
+			new MetaEquationFormula(
+					new MetaDynamicDependencyTerm(
+							new MetaTermGenerator() {
+								@Override
+								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+									curIndex -= 1;
+									if (curIndex % 2 == 0) {
+										return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
+									}
+									return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
+								}
+							},
+							new MetaEvaluatableTermVariable(new Variable("se"))
+					),
+					new MetaDynamicDependencyTerm(
+							new MetaTermGenerator() {
+								@Override
+								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+									curIndex -= 1;
+									if (curIndex % 2 == 0) {
+										return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
+									}
+									return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
+								}
+							},
+							new MetaEvaluatableTermVariable(new Variable("te"))
+					)
+			)
+	);
 
-//	public static final InferenceRule identity = new EquationAxiom(
-//			"Identity",
-//			List.of(),
-//			List.of(
-//				new MetaEquationFormula(
-//							new MetaDependencyTerm(
-//									new MetaEvaluatableTermVariable(new Variable("se")),
-//									new MetaEvaluatableTermVariable(new Variable("x")),
-//									new MetaEvaluatableTermVariable(new Variable("y"))
-//							),
-//							new MetaEvaluatableTermVariable(new Variable("te"))
-//					)
-//			),
-//			new MetaEquationFormula(
-//					new MetaDynamicDependencyTerm(
-//							new MetaTermGenerator() {
-//								@Override
-//								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
-//									curIndex -= 1;
-//									if (curIndex % 2 == 0) {
-//										return new MetaEvaluatableTermVariable(new Variable("se" + curIndex / 2));
-//									}
-//									return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
-//								}
-//								
-//							},
-//							new MetaEvaluatableTermVariable(new Variable("se0"))
-//					),
-//					new MetaEvaluatableTermVariable(new Variable("te0"))
-//			),
-//			null,
-//			(assumptions) -> assumptions.size() * 2 + 1,
-//			(assumptions) -> 1,
-//			(conclusion) -> (conclusion.getMaxIndex() - 1) / 2
-//	);
+	
+	public static final InferenceRule identity = new InferenceRule(
+			"Identity",
+			List.of(),
+			new MetaEquationFormula(
+					new MetaDynamicDependencyTerm(
+							new MetaTermGenerator() {
+								@Override
+								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+									curIndex -= 1;
+									if (curIndex % 2 == 0) {
+										return new MetaEvaluatableTermVariable(new Variable("ue"));
+									}
+									return new MetaEvaluatableTermVariable(new Variable("ve"));
+								}
+							},
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaEvaluatableTermVariable(new Variable("te"))
+					),
+					new MetaEvaluatableTermVariable(new Variable("te"))
+			)
+	);
 //	
 //	public static final InferenceRule mapComposition = new MapComposition();
 //	
@@ -353,49 +314,18 @@
 
 	private Set<DependencyFormula> dependencyFormulas = new HashSet<>();
 	private Set<EquationFormula> equationFormulas = new HashSet<>();
-	private Map<DependencyFormula, List<Set<In>>> dependencyInMap = new HashMap<>();
-	private Map<EvaluatableTerm, Set<In>> ins = new HashMap<>();
 	private Set<RDLTerm> terms = new HashSet<>();
 	
-	public void addDependency(Dependency dependency) {
-		addDependency(new DependencyFormula(dependency));
-	}
-	
-	public void addDependency(DependencyFormula dependency) {
-		dependencyFormulas.add(dependency);
-		addExistTerms(dependency);
-		Dependency dep = dependency.getDependency();
-		dependencyInMap.put(dependency, new ArrayList<>());
-		for (EvaluatableTerm dependedTerm : dep.getDependedTerms()) {
-			if (ins.containsKey(dependedTerm)) {
-				dependencyInMap.get(dependency).add(new HashSet<>(ins.get(dependedTerm)));
-			} else {
-				dependencyInMap.get(dependency).add(new HashSet<>());
-			}
-		}
+	public void addDependencyFormula(DependencyFormula dep) {
+		dependencyFormulas.add(dep);
+		addExistTerms(dep);
 	}
 	
 	public void addEquationFormula(EquationFormula eq) {
-		addExistTerms(eq);
 		equationFormulas.add(eq);
-		Set<In> ins = In.deriveIn(eq);
-		for (In in : ins) {
-			this.ins.computeIfAbsent(in.getRightSideHand(), t -> new HashSet<>()).add(in);
-			for (DependencyFormula depFormula : dependencyInMap.keySet()) {
-				int startIndex = depFormula.getDependency().getDependedTerms().headMultiset(in.getRightSideHand(), BoundType.OPEN).size();
-				int count = depFormula.getDependency().getDependedTerms().count(in.getRightSideHand());
-				for (int i = 0; i < count; i++) {
-					dependencyInMap.get(depFormula).get(startIndex + i).add(in);
-				}
-			}
-		}
+		addExistTerms(eq);
 	}
 	
-	private void dependencyInMap(DependencyFormula key, int index, In in) {
-		
-	}
-	
-	
 	private void addExistTerms(Formula formula) {
 		if (formula instanceof EquationFormula) {
 			RDLTerm leftSideHand = ((EquationFormula) formula).getLeftSideHand();