diff --git a/src/Main.java b/src/Main.java
index 8e03d99..725541c 100644
--- a/src/Main.java
+++ b/src/Main.java
@@ -23,10 +23,10 @@
 	static Parser parser = new Parser(stream);
 	static DataTransferModel model = new DataTransferModel();
 	
+	static Type INT = DataConstraintModel.typeInt;
+
 	public static void main(String[] args) {
 
-		Type INT = DataConstraintModel.typeInt;
-		
 		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te"));
 		MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue"));
 		MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"));
@@ -53,7 +53,7 @@
 		
 		System.out.println(rightReplacement.check(List.of(assump2), concl2));
 	}
-
+	
 	@SneakyThrows
 	static Expression parse(String expr) {
 		stream.addLine(expr);
diff --git a/src/tests/inferencerule/InferenceRuleTest.java b/src/tests/inferencerule/InferenceRuleTest.java
new file mode 100644
index 0000000..f1e89bb
--- /dev/null
+++ b/src/tests/inferencerule/InferenceRuleTest.java
@@ -0,0 +1,79 @@
+package tests.inferencerule;
+
+import static org.junit.jupiter.api.Assertions.*;
+import static tests.Utils.*;
+
+import org.junit.jupiter.api.Test;
+
+import java.util.List;
+
+import inference.InferenceRule;
+import models.algebra.Variable;
+import models.formulas.DependencyFormula;
+import models.formulas.EquationFormula;
+import models.formulas.meta.MetaDependencyFormula;
+import models.formulas.meta.MetaEquationFormula;
+import models.terms.Dependency;
+import models.terms.DependencyTerm;
+import models.terms.ResourceVariable;
+import models.terms.meta.MetaEvaluatableTermVariable;
+import models.terms.meta.MetaRDLTerm;
+import models.terms.meta.MetaResourceVariable;
+
+public class InferenceRuleTest {
+
+	@Test
+	void InferenceRuleTerst1() {
+		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new  Variable("te"));
+		MetaResourceVariable v = new MetaResourceVariable(new Variable("v"));
+		MetaResourceVariable w = new MetaResourceVariable(new Variable("w"));
+		MetaRDLTerm metaD1 = new MetaRDLTerm(te, v);
+		MetaRDLTerm metaD2 = new MetaRDLTerm(v, w);
+		MetaRDLTerm metaD3 = new MetaRDLTerm(te, w);
+		MetaDependencyFormula metaDf1 = new MetaDependencyFormula(metaD1);
+		MetaDependencyFormula metaDf2 = new MetaDependencyFormula(metaD2);
+		MetaDependencyFormula metaDf3 = new MetaDependencyFormula(metaD3);
+		InferenceRule goseShazo = new InferenceRule(List.of(metaDf1, metaDf2), metaDf3);
+		
+		ResourceVariable a = new ResourceVariable("a", INT, 0);
+		ResourceVariable b = new ResourceVariable("b", INT, 0);
+		ResourceVariable c = new ResourceVariable("c", INT, 0);
+		Dependency d1 = new Dependency(a, b);
+		Dependency d2 = new Dependency(b, c);
+		Dependency d3 = new Dependency(a, c);
+		DependencyFormula df1 = new DependencyFormula(d1); // a : b
+		DependencyFormula df2 = new DependencyFormula(d2); // b : c
+		DependencyFormula df3 = new DependencyFormula(d3); // a : c
+		assertTrue(goseShazo.check(List.of(df1, df2), df3));
+		
+	}
+	
+	@Test
+	void InferencuRuleTest2() {
+		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te"));
+		MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue"));
+		MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"));
+		MetaResourceVariable v = new MetaResourceVariable(new Variable("v"));
+		MetaEquationFormula assump1 = new MetaEquationFormula(te, ue);
+		MetaEquationFormula concl1 = new MetaEquationFormula(new MetaRDLTerm(se, v, te), new MetaRDLTerm(se, v, ue));
+		/*
+		 *                 te = ue
+		 *  ----------------------------------------
+		 *   [se : v -> te] = [se : v -> ue]
+		 */
+		InferenceRule rightReplacement = new InferenceRule(List.of(assump1), concl1);
+
+		ResourceVariable a = new ResourceVariable("a", INT, 0);
+		ResourceVariable c = new ResourceVariable("c", INT, 0);
+		ResourceVariable d = new ResourceVariable("d", INT, 0);
+		ResourceVariable x = new ResourceVariable("x", INT, 0);
+		ResourceVariable y = new ResourceVariable("y", INT, 0);
+		ResourceVariable z = new ResourceVariable("z", INT, 0);
+		DependencyTerm xyz = new DependencyTerm(x, y, z);
+		EquationFormula assump2 = new EquationFormula(a, xyz); // a = [x : y -> z]
+		EquationFormula concl2 = new EquationFormula(new DependencyTerm(c, d, a), new DependencyTerm(c, d, xyz)); // [c : d -> a] = [c : d -> [x : y -> z]]
+		
+		assertTrue(rightReplacement.check(List.of(assump2), concl2));
+	}
+	
+}