diff --git a/src/Main.java b/src/Main.java
index 725541c..d337f41 100644
--- a/src/Main.java
+++ b/src/Main.java
@@ -1,19 +1,18 @@
+import java.util.ArrayList;
 import java.util.List;
 
-import inference.InferenceRule;
+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;
 import models.formulas.EquationFormula;
-import models.formulas.meta.MetaEquationFormula;
+import models.formulas.Formula;
+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;
 import parser.Parser;
 import parser.Parser.TokenStream;
 
@@ -26,32 +25,34 @@
 	static Type INT = DataConstraintModel.typeInt;
 
 	public static void main(String[] args) {
-
-		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 b = new ResourceVariable("b", 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]]
 		
-		System.out.println(rightReplacement.check(List.of(assump2), concl2));
+		List<Formula> initialConditions = new ArrayList<>();
+		ResourceVariable A = new ResourceVariable("A", INT, 2);
+		ResourceVariable B = new ResourceVariable("B", INT, 2);
+		ResourceVariable C = new ResourceVariable("C", INT, 2);
+		ResourceVariable D = new ResourceVariable("D", INT, 2);
+		ResourceVariable E = new ResourceVariable("E", INT, 1);
+		ResourceVariable F = new ResourceVariable("F", INT, 1);
+		ResourceVariable G = new ResourceVariable("G", INT, 0);
+		
+		ResourceVariable Ap = new ResourceVariable("A'", INT, 2);
+		ResourceVariable Bp = new ResourceVariable("B'", INT, 2);
+		ResourceVariable Cp = new ResourceVariable("C'", INT, 2);
+		ResourceVariable Dp = new ResourceVariable("D'", INT, 2);
+		ResourceVariable Fp = new ResourceVariable("F'", INT, 1);
+		
+		initialConditions.add(new DependencyFormula(new Dependency(new Dependency(A, B), D), F));
+		initialConditions.add(new DependencyFormula(new Dependency(new Dependency(Ap, Bp), Dp), Fp));
+		initialConditions.add(new EquationFormula(new DependencyTerm(A, B, C), new DependencyTerm(Ap, Bp, Cp)));
+		Formula conclusion = new EquationFormula(
+			new DependencyTerm(new DependencyTerm(new DependencyTerm(A, B, C), D, E), F, G),
+			new DependencyTerm(new DependencyTerm(new DependencyTerm(Ap, Bp, Cp), D, E), F, G)
+		);
+		for(var cond : initialConditions) {
+			System.out.println(cond.toString());
+		}
+		System.out.println(conclusion.toString());
+		ProofSystem.check(initialConditions, conclusion);
 	}
 	
 	@SneakyThrows
diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index 859e976..a34bce9 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -4,9 +4,9 @@
 import java.util.List;
 
 import models.algebra.Variable;
+import models.formulas.Formula;
 import models.formulas.meta.MetaDependencyFormula;
 import models.formulas.meta.MetaEquationFormula;
-import models.terms.RDLTerm;
 import models.terms.meta.MetaEvaluatableTermVariable;
 import models.terms.meta.MetaRDLTerm;
 import models.terms.meta.MetaResourceVariable;
@@ -90,7 +90,7 @@
 	private final static InferenceRule SET_EQUIVALENCE = null;//集合同値性??
 	private final static InferenceRule HOMOMORPHISM = null;//準同型性??
 	
-	public static boolean check(Collection<RDLTerm> assumptions, RDLTerm conclusion) {
+	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
 		return false;
 	}