diff --git a/src/Main.java b/src/Main.java
index 6264b8d..7d0b393 100644
--- a/src/Main.java
+++ b/src/Main.java
@@ -67,6 +67,7 @@
 		
 		
 		sandbox1();
+		sandbox2();
 	}
 	
 	static void sandbox1() {
@@ -97,6 +98,21 @@
 		System.out.println(tmp4);
 	}
 	
+	static void sandbox2() {
+		System.out.println("----------------------------------------------------sandbox2");
+		ResourceVariable a = new ResourceVariable("a", INT, 1);
+		ResourceVariable b = new ResourceVariable("b", INT, 1);
+		ResourceVariable c = new ResourceVariable("c", INT, 1);
+		ResourceVariable d = new ResourceVariable("d", INT, 1);
+		EquationFormula ef1 = new EquationFormula(a, b);
+		EquationFormula ef2 = new EquationFormula(b, a);
+		EquationFormula ef3 = new EquationFormula(b, c);
+		EquationFormula ef4 = new EquationFormula(c, d);
+		EquationFormula ef5 = new EquationFormula(d, a);
+		System.out.println(ProofSystem.check(List.of(ef1), ef2));
+		System.out.println(ProofSystem.check(List.of(ef1, ef2, ef3, ef4), ef5));
+	}
+	
 	@SneakyThrows
 	static Expression parse(String expr) {
 		stream.addLine(expr);
diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index 18416fd..e652591 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -1,14 +1,23 @@
 package inference;
 
+import java.util.ArrayDeque;
+import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Deque;
+import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
+import java.util.Map;
+import java.util.Set;
 
 import models.algebra.Constant;
 import models.algebra.Variable;
+import models.formulas.EquationFormula;
 import models.formulas.Formula;
 import models.formulas.meta.MetaDependencyFormula;
 import models.formulas.meta.MetaEquationFormula;
 import models.formulas.meta.MetaInFormula;
+import models.terms.EvaluatableTerm;
 import models.terms.meta.MetaDependencyVariable;
 import models.terms.meta.MetaEvaluatableTermVariable;
 import models.terms.meta.MetaRDLTerm;
@@ -59,7 +68,7 @@
 			)
 	);
 	
-	public final static InferenceRule RIGHT_PROJECTION = new InferenceRule("left projection", 
+	public final static InferenceRule RIGHT_PROJECTION = new InferenceRule("right projection", 
 			List.of(new MetaDependencyFormula(
 								new MetaRDLTerm(
 										new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
@@ -136,7 +145,6 @@
 			)
 	);
 	
-	
 	public final static InferenceRule IDENTITY_LAW = new InferenceRule("identity law", 
 			List.of(new MetaInFormula(
 					new MetaEvaluatableTermVariable(new Variable("te")), 
@@ -274,19 +282,58 @@
 	);//準同型性??
 	
 	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
-		if (assumptionsContainConclusionCheck(assumptions, conclusion)) {
+		if (equationTransitionCheck(assumptions, conclusion)) {
 			return true;
 		}
 		return false;
 	}
 	
-	private static boolean assumptionsContainConclusionCheck(Collection<Formula> assumptions, Formula conclusion) {
-		for(var assumption : assumptions) {
-			if (assumption.equals(conclusion)) {
+	private static boolean equationTransitionCheck(Collection<Formula> assumptions, Formula conclusion) {
+		if (! (conclusion instanceof EquationFormula)) {
+			return false;
+		}
+		EquationFormula equationConclusion = (EquationFormula) conclusion;
+		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = constructEquationGraph(assumptions);
+		Deque<EvaluatableTerm> que = new ArrayDeque<>();
+		Set<EvaluatableTerm> visited = new HashSet<>();
+		que.add(equationConclusion.getLeftSideHand());
+		while (! que.isEmpty()) {
+			EvaluatableTerm curNode = que.pollFirst();
+			if (curNode.equals(equationConclusion.getRightSideHand())) {
 				return true;
 			}
+			for (EvaluatableTerm nextNode : graph.getOrDefault(curNode, new ArrayList<>())) {
+				if (visited.contains(nextNode)) {
+					continue;
+				}
+				visited.add(nextNode);
+				que.add(nextNode);
+			}
 		}
 		return false;
 	}
 	
+	private static Map<EvaluatableTerm, List<EvaluatableTerm>> constructEquationGraph(Collection<Formula> assumptions) {
+		List<EquationFormula> equations = new ArrayList<>();
+		for (Formula assumption : assumptions) {
+			if (assumption instanceof EquationFormula) {
+				equations.add((EquationFormula) assumption);
+			}
+		}
+		
+		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = new HashMap<>();
+		for (EquationFormula equation : equations) {
+			EvaluatableTerm lsh = equation.getLeftSideHand();
+			EvaluatableTerm rsh = equation.getRightSideHand();
+			if (! graph.containsKey(lsh)) {
+				graph.put(lsh, new ArrayList<>());
+			}
+			if (! graph.containsKey(rsh)) {
+				graph.put(rsh, new ArrayList<>());
+			}
+			graph.get(lsh).add(rsh);
+			graph.get(rsh).add(lsh);
+		}
+		return graph;
+	}
 }