diff --git a/src/Main.java b/src/Main.java
index 9290575..6264b8d 100644
--- a/src/Main.java
+++ b/src/Main.java
@@ -1,13 +1,10 @@
 import java.util.ArrayList;
-import java.util.HashMap;
 import java.util.List;
-import java.util.Map;
 
 import inference.ProofSystem;
 import lombok.SneakyThrows;
 import models.algebra.Expression;
 import models.algebra.Type;
-import models.algebra.Variable;
 import models.dataConstraintModel.DataConstraintModel;
 import models.dataFlowModel.DataTransferModel;
 import models.formulas.DependencyFormula;
@@ -16,9 +13,7 @@
 import models.terms.Dependency;
 import models.terms.DependencyTerm;
 import models.terms.EvaluatableTerm;
-import models.terms.RDLTerm;
 import models.terms.ResourceVariable;
-import models.terms.meta.OrderVariableConstraint;
 import parser.Parser;
 import parser.Parser.TokenStream;
 
@@ -87,8 +82,6 @@
 		DependencyTerm d11 = new DependencyTerm(a, b, c);
 		DependencyTerm d2 = new DependencyTerm(ap, bp, cp);
 		EquationFormula conclu1 = new EquationFormula(d1, d11);
-		Map<Variable, RDLTerm> binding = new HashMap<>();
-		Map<Variable, OrderVariableConstraint> orderConstraint = new HashMap<>();
 		boolean tmp1 = ProofSystem.REFLEXIVE_LAW.check(List.of(), conclu1);
 		d11.setDependingTerm(ap);
 		boolean tmp2 = ProofSystem.LEFT_REPLACEMENT.check(List.of(new EquationFormula(a, ap)), conclu1);
diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index 5df8f9c..18416fd 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -274,6 +274,18 @@
 	);//準同型性??
 	
 	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
+		if (assumptionsContainConclusionCheck(assumptions, conclusion)) {
+			return true;
+		}
+		return false;
+	}
+	
+	private static boolean assumptionsContainConclusionCheck(Collection<Formula> assumptions, Formula conclusion) {
+		for(var assumption : assumptions) {
+			if (assumption.equals(conclusion)) {
+				return true;
+			}
+		}
 		return false;
 	}