diff --git a/src/Main.java b/src/Main.java
index 36f4d00..c342afb 100644
--- a/src/Main.java
+++ b/src/Main.java
@@ -31,7 +31,8 @@
 	public static void main(String[] args) {
 //		sandbox1();
 //		sandbox2();
-		sandbox3();
+//		sandbox3();
+		sandbox4();
 //		ProofSystem.debug();
 	}
 	
@@ -100,7 +101,30 @@
 		System.out.println(result);
 	}
 	
-	
+	static void sandbox4() {
+		ResourceVariable X = new ResourceVariable("X", INT, 1);
+		ResourceVariable Y= new ResourceVariable("Y", INT, 1);
+		ResourceVariable U = new ResourceVariable("U", INT, 1);
+		ResourceVariable W = new ResourceVariable("W", INT, 1);
+		
+		EquationFormula f1 = new EquationFormula(X, Y);
+		DependencyFormula f2 = new DependencyFormula(X, U);
+		DependencyFormula f3 = new DependencyFormula(U, W);
+		DependencyTerm t1 = new DependencyTerm(X, U, U);
+		DependencyTerm t2 = new DependencyTerm(t1, W, W);
+		DependencyTerm t3 = new DependencyTerm(Y, U, U);
+		DependencyTerm t4 = new DependencyTerm(t3, W, W);
+//		EquationFormula f4 = new EquationFormula(t1, X);
+//		EquationFormula f4 = new EquationFormula(X, t1);
+//		EquationFormula f4 = new EquationFormula(t2, X);
+//		EquationFormula f4 = new EquationFormula(t3, Y);
+//		EquationFormula f4 = new EquationFormula(t4, Y);
+		EquationFormula f4 = new EquationFormula(t2, t4);
+//		DependencyFormula f4 = new DependencyFormula(Y, U);
+		System.out.println(f1 + ", " + f2 + ", " + f3);
+		boolean result = ProofSystem.check(List.of(f1, f2, f3), f4);
+		System.out.println(result);
+	}
 	
 	@SneakyThrows
 	static Expression parse(String expr) {
diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index 643b605..6736e74 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -566,7 +566,7 @@
 	);
 
 	private static final List<InferenceRule> axioms = List.of(
-			reflexivity, 
+//			reflexivity, 
 			symmetry, 
 			transitivity,
 			rightSubstitution, 
@@ -640,7 +640,7 @@
 		
 		formulaQueue.add(conclusion);
 		depthQueue.add(0);
-		
+
 		while (formulaQueue.size() != 0) {
 			Formula currentFormula = formulaQueue.poll();
 			if (used.contains(currentFormula)) {
@@ -664,7 +664,7 @@
 			}
 		}
 		int prevDepth = depthResult.get(depthResult.size() - 1);
-		List<Formula> sameDepthFormulas = new ArrayList<>();
+		Set<Formula> sameDepthFormulas = new HashSet<>();
 		for (int i = formulaResult.size() - 1; i >= 0; i--) {
 			int currentDepth = depthResult.get(i);
 			Formula currentFormula = formulaResult.get(i);
@@ -700,8 +700,10 @@
 			Set<Formula> applied = axiom.apply(applyFormulas, existTerms);
 			if (applied != null) {
 				for (Formula formula : applied) {
-					addExistTerms(formula, existTerms);
-					proofGraph.put(formula, new AxiomResult(axiom, applyFormulas));
+					if (! formulas.contains(formula)) {
+						addExistTerms(formula, existTerms);
+						proofGraph.put(formula, new AxiomResult(axiom, applyFormulas));
+					}
 				}
 				result.addAll(applied);
 				appliedFormulas.add(applyFormulas);