diff --git a/src/Main.java b/src/Main.java
index 5e92af1..9f8cae4 100644
--- a/src/Main.java
+++ b/src/Main.java
@@ -32,7 +32,8 @@
 //		sandbox1();
 //		sandbox2();
 //		sandbox3();
-		ProofSystem.debug();
+		sandbox4();
+//		ProofSystem.debug();
 	}
 	
 	static void sandbox1() {
@@ -100,6 +101,16 @@
 		System.out.println(result);
 	}
 	
+	static void sandbox4() {
+		ResourceVariable followee = new ResourceVariable("followee", INT, 2);
+		ResourceVariable fno = new ResourceVariable("fno", INT, 2);
+		ResourceVariable follower = new ResourceVariable("follower", INT, 1);
+		DependencyFormula f1 = new DependencyFormula(new Dependency(followee, fno), follower);
+		DependencyFormula f2 = new DependencyFormula(new Dependency(new Dependency(new SetEvaluatableTerm(followee), follower)));
+		boolean result = ProofSystem.check(List.of(f1), f2);
+		System.out.println(result);
+	}
+	
 	
 	
 	@SneakyThrows
diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java
index fb29d37..1a3243b 100644
--- a/src/inference/InferenceRule.java
+++ b/src/inference/InferenceRule.java
@@ -7,9 +7,12 @@
 import java.util.Map;
 import java.util.Set;
 
+import exceptions.SubstituteFailedException;
 import lombok.Getter;
 import models.algebra.Variable;
 import models.formulas.Formula;
+import models.formulas.meta.MetaDependencyFormula;
+import models.formulas.meta.MetaEquationFormula;
 import models.formulas.meta.MetaFormula;
 import models.terms.RDLTerm;
 import models.terms.meta.OrderVariableConstraint;
@@ -129,6 +132,53 @@
 		return conclusion.substitution(binding);
 	}
 	
+	public Set<Formula> apply(List<Formula> assumptions, Set<RDLTerm> existTerms) {
+		Set<Formula> result = new HashSet<>();
+		if (assumptions.size() != getAssumptionSize()) {
+			return null;
+		}
+		Map<Variable, RDLTerm> binding = new HashMap<>();
+		Map<Variable, OrderVariableConstraint> orderConstraint = new HashMap<>();
+		for (int i = 0; i < getAssumptionSize(); i++) {
+			if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraint)) {
+				return result;
+			}
+		}
+		try {
+			result.add(conclusion.substitution(binding));
+		} catch (SubstituteFailedException e) {
+			
+		}
+		for (RDLTerm term : existTerms) {
+			Map<Variable, RDLTerm> localBinding = new HashMap<>(binding);
+			Map<Variable, OrderVariableConstraint> localOrderConstraint = new HashMap<>(orderConstraint);
+			if (conclusion instanceof MetaEquationFormula) {
+				MetaEquationFormula equation = (MetaEquationFormula) conclusion;
+				if (equation.getLeftSideHand().isMatchedBy(term, localBinding, localOrderConstraint)) {
+					result.add(conclusion.substitution(localBinding));
+				}
+			}
+			else if (conclusion instanceof MetaDependencyFormula) {
+				MetaDependencyFormula dependency = (MetaDependencyFormula) conclusion;
+				if (dependency.getDependency().isMatchedBy(term, localBinding, localOrderConstraint)) {
+					result.add(conclusion.substitution(localBinding));
+				}
+			} 
+		}
+		
+		for (RDLTerm term : existTerms) {
+			Map<Variable, RDLTerm> localBinding = new HashMap<>(binding);
+			Map<Variable, OrderVariableConstraint> localOrderConstraint = new HashMap<>(orderConstraint);
+			if (conclusion instanceof MetaEquationFormula) {
+				MetaEquationFormula equation = (MetaEquationFormula) conclusion;
+				if (equation.getRightSideHand().isMatchedBy(term, localBinding, localOrderConstraint)) {
+					result.add(conclusion.substitution(localBinding));
+				}
+			}
+		}
+		return result; 
+	}
+	
 	public Formula apply(Collection<Formula> assumptions) {
 		if (assumptions.size() != getAssumptionSize()) {
 			return null;
diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index 8d57806..4b119c2 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -14,12 +14,15 @@
 
 import models.algebra.Constant;
 import models.algebra.Variable;
+import models.formulas.DependencyFormula;
 import models.formulas.EquationFormula;
 import models.formulas.Formula;
+import models.formulas.InFormula;
 import models.formulas.meta.MetaDependencyFormula;
 import models.formulas.meta.MetaEquationFormula;
 import models.formulas.meta.MetaInFormula;
 import models.terms.EvaluatableTerm;
+import models.terms.RDLTerm;
 import models.terms.meta.MetaEvaluatableTermVariable;
 import models.terms.meta.MetaRDLTerm;
 import models.terms.meta.MetaResourceVariable;
@@ -567,7 +570,7 @@
 
 	private static final List<InferenceRule> axioms = List.of(
 			reflexivity, 
-//			symmetry, 
+			symmetry, 
 			transitivity,
 			rightSubstitution, 
 			leftSubstitution, 
@@ -605,16 +608,21 @@
 		
 		Map<Formula, AxiomResult> proofGraph = new HashMap<>();
 		Map<InferenceRule, Set<List<Formula>>> appliedFormulas = new HashMap<>(); 
+		
 		for (InferenceRule axiom : axioms) {
 			appliedFormulas.put(axiom, new HashSet<>());
 		}
 		
 		Set<Formula> appearFormulas = new HashSet<>(assumptions);
+		Set<RDLTerm> existTerms = new HashSet<>();
+		for (Formula assumption : assumptions) {
+			addExistTerms(assumption, existTerms);
+		}
 		int prevAppearFormulasSize = appearFormulas.size();
 		while (! appearFormulas.contains(conclusion)) {
 			Set<Formula> derivedFormulas = new HashSet<>();
 			for(InferenceRule axiom : axioms) {
-				derivedFormulas.addAll(applyAxiom(axiom, appearFormulas, appliedFormulas.get(axiom), proofGraph));
+				derivedFormulas.addAll(applyAxiom(axiom, appearFormulas, appliedFormulas.get(axiom), existTerms, proofGraph));
 			}
 			if (derivedFormulas.size() == 0) {
 				return false;
@@ -630,6 +638,7 @@
 		Queue<Integer> depthQueue = new ArrayDeque<>();
 		List<Formula> formulaResult = new ArrayList<>();
 		List<Integer> depthResult = new ArrayList<>();
+		Set<Formula> used = new HashSet<>();
 		Map<Integer, Set<InferenceRule>> usedAxioms = new HashMap<>();
 		
 		formulaQueue.add(conclusion);
@@ -637,11 +646,18 @@
 		
 		while (formulaQueue.size() != 0) {
 			Formula currentFormula = formulaQueue.poll();
+			if (used.contains(currentFormula)) {
+				continue;
+			}
+			used.add(currentFormula);
 			int currentDepth = depthQueue.poll();
 			formulaResult.add(currentFormula);
 			depthResult.add(currentDepth);
 			if (! proofGraph.containsKey(currentFormula)) continue;
 			for (Formula nextFormula : proofGraph.get(currentFormula).formulas) {
+				if (used.contains(nextFormula)) {
+					continue;
+				}
 				formulaQueue.add(nextFormula);
 				depthQueue.add(currentDepth + 1);
 				if (! usedAxioms.containsKey(currentDepth + 1)) {
@@ -671,7 +687,7 @@
 		return true;
 	}
 	
-	private static Set<Formula> applyAxiom(InferenceRule axiom, Set<Formula> formulas, Set<List<Formula>> appliedFormulas,  Map<Formula, AxiomResult> proofGraph) {
+	private static Set<Formula> applyAxiom(InferenceRule axiom, Set<Formula> formulas, Set<List<Formula>> appliedFormulas,  Set<RDLTerm> existTerms, Map<Formula, AxiomResult> proofGraph) {
 		Set<Formula> result = new HashSet<>();
 		List<List<Formula>> matchedFormulas = new ArrayList<>();
 		for (int i = 0; i < axiom.getAssumptionSize(); i++) {
@@ -684,16 +700,36 @@
 		}
 		for(List<Formula> applyFormulas : Product.product(matchedFormulas)) {
 			if (appliedFormulas.contains(applyFormulas)) continue;
-			Formula applied = axiom.apply(applyFormulas);
+			Set<Formula> applied = axiom.apply(applyFormulas, existTerms);
 			if (applied != null) {
-				result.add(axiom.apply(applyFormulas));
+				for (Formula formula : applied) {
+					addExistTerms(formula, existTerms);
+					proofGraph.put(formula, new AxiomResult(axiom, applyFormulas));
+				}
+				result.addAll(applied);
 				appliedFormulas.add(applyFormulas);
-				proofGraph.put(applied, new AxiomResult(axiom, applyFormulas));
 			}
 		}
 		return result;
 	}
 	
+	private static void addExistTerms(Formula formula, Set<RDLTerm> existTerms) {
+		if (formula instanceof EquationFormula) {
+			RDLTerm leftSideHand = ((EquationFormula) formula).getLeftSideHand();
+			RDLTerm rightSideHand = ((EquationFormula) formula).getRightSideHand();
+			existTerms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values());
+			existTerms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values());
+		} else if (formula instanceof DependencyFormula) {
+			RDLTerm dependency = ((DependencyFormula) formula).getDependency();
+			existTerms.addAll(dependency.getSubTerms(RDLTerm.class).values());
+		} else if (formula instanceof InFormula){
+			RDLTerm leftSideHand = ((InFormula) formula).getLeftSideHand();
+			RDLTerm rightSideHand = ((InFormula) formula).getRightSideHand();
+			existTerms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values());
+			existTerms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values());
+		}
+	}
+	
 	private static boolean equationTransitionCheck(Collection<Formula> assumptions, Formula conclusion) {
 		if (! (conclusion instanceof EquationFormula)) {
 			return false;