diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java
index eed767d..6abbded 100644
--- a/src/main/java/inference/InferenceRule.java
+++ b/src/main/java/inference/InferenceRule.java
@@ -12,6 +12,7 @@
 import lombok.Getter;
 import models.algebra.Variable;
 import models.formulas.Formula;
+import models.formulas.meta.MetaEquationFormula;
 import models.formulas.meta.MetaFormula;
 import models.terms.RDLTerm;
 import models.terms.meta.MatchConstraint;
@@ -59,6 +60,10 @@
 		this(name, assumptions, conclusion, null);
 	}
 	
+	public InferenceRule(String name, List<MetaFormula> assumptions, AssumptionGenerator generator, MetaFormula conclusion) {
+		this(name, assumptions, generator, conclusion, null);
+	}
+	
 	public InferenceRule(List<MetaFormula> assumptions, MetaFormula conclusion) {
 		this("undefined", assumptions, conclusion, null);
 	}
@@ -148,7 +153,7 @@
 	}
 	
 	public Formula apply(Collection<Formula> assumptions) {
-		if (assumptions.size() != getAssumptionSize()) {
+		if (assumptions.size() < getAssumptionSize()) {
 			return null;
 		}
 		for (List<Formula> assumptionList : Permutation.permutation(assumptions, assumptions.size())) {
@@ -178,7 +183,7 @@
 			}
 		}
 		if (hasDynamicAssumption) {
-			for (int i = 0; i < assumptions.size(); i++) {
+			for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) {
 				int j = getAssumptionSize() + i;
 				result = this.generator.generate(i).isMatchedBy(assumptions.get(j), result);
 				if (result.isEmpty()) {
@@ -197,6 +202,33 @@
 		return subRes;
 	}
 	
+	
+	public RDLTerm generateRightSideHand(List<Formula> assumptions, RDLTerm leftSideHand) {
+		if (! (this.conclusion instanceof MetaEquationFormula)) return null;
+		if (this.assumptions.size()  > assumptions.size()) return null;
+		MetaEquationFormula metaFormula = (MetaEquationFormula) this.conclusion;
+		Set<MatchConstraint> constraints = metaFormula.getLeftSideHand().isMatchedBy(leftSideHand);
+		for (List<Formula> assumptionList: Permutation.permutation(assumptions, assumptions.size())) {
+			for (int i = 0; i < getAssumptionSize(); i++) {
+				constraints = this.assumptions.get(i).isMatchedBy(assumptionList.get(i), constraints);
+			}
+			if (hasDynamicAssumption) {
+				for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) {
+					int j = getAssumptionSize() + i;
+					constraints = this.generator.generate(i).isMatchedBy(assumptions.get(j), constraints);
+				}
+			}
+			for (MatchConstraint constraint: constraints) {
+				try {
+					return metaFormula.getRightSideHand().substitute(constraint.getBinding());
+				} catch (SubstituteFailedException e) {
+					continue;
+				}
+			}
+		}
+		return null;
+	}
+	
 	public int getAssumptionSize() {
 		return this.assumptions.size();
 	}
diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java
index 76ca42f..03eaacc 100644
--- a/src/main/java/inference/ProofSystem.java
+++ b/src/main/java/inference/ProofSystem.java
@@ -89,16 +89,16 @@
 									new MetaEvaluatableTermVariable(new Variable("se")),
 									(MetaTermGenerator) (index, depth, isLast) -> new MetaEvaluatableTermVariable(new Variable("re" + index))
 							)
-					),
-					new MetaEquationFormula(
-							new MetaRDLTerm(
-									new MetaEvaluatableTermVariable(new Variable("re0")), 
-									new MetaEvaluatableTermVariable(new Variable("x")), 
-									new MetaEvaluatableTermVariable(new Variable("y"))
-							),
-							new MetaEvaluatableTermVariable(new Variable("te0"))
 					)
 			),
+			(i) -> new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("re" + i)), 
+							new MetaEvaluatableTermVariable(new Variable("x" + i)), 
+							new MetaEvaluatableTermVariable(new Variable("y" + i))
+					),
+					new MetaEvaluatableTermVariable(new Variable("te" + i))
+			),
 			new MetaEquationFormula(
 					new MetaDynamicTerm(
 							new MetaEvaluatableTermVariable(new Variable("se")),
@@ -125,28 +125,34 @@
 							new MetaEvaluatableTermVariable(new Variable("te"))
 					),
 					new MetaDependencyFormula(
-							new MetaEvaluatableTermVariable(new Variable("se")),
-							new MetaEvaluatableTermVariable(new Variable("re"))
-					),
-					new MetaEquationFormula(
-							new MetaRDLTerm(
-									new MetaEvaluatableTermVariable(new Variable("re")), 
-									new MetaEvaluatableTermVariable(new Variable("x")), 
-									new MetaEvaluatableTermVariable(new Variable("y"))
-							),
-							new MetaEvaluatableTermVariable(new Variable("ue"))
+							new MetaDynamicTerm(
+									new MetaEvaluatableTermVariable(new Variable("se")),
+									(MetaTermGenerator) (index, depth, isLast) -> new MetaEvaluatableTermVariable(new Variable("re" + index))
+							)
 					)
 			),
-			new MetaEquationFormula(
+			(i) -> new MetaEquationFormula(
 					new MetaRDLTerm(
-							new MetaEvaluatableTermVariable(new Variable("se")),
-							new MetaEvaluatableTermVariable(new Variable("re")),
-							new MetaEvaluatableTermVariable(new Variable("ue"))
+							new MetaEvaluatableTermVariable(new Variable("re" + i)), 
+							new MetaEvaluatableTermVariable(new Variable("x" + i)), 
+							new MetaEvaluatableTermVariable(new Variable("y" + i))
 					),
-					new MetaRDLTerm(
+					new MetaEvaluatableTermVariable(new Variable("ue" + i))
+			),
+			new MetaEquationFormula(
+					new MetaDynamicTerm(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							(MetaTermPairGenerator) (index, depth, isLast) -> new TermPair(
+									new MetaEvaluatableTermVariable(new Variable("re" + index)),
+									new MetaEvaluatableTermVariable(new Variable("ue" + index))
+							)
+					),
+					new MetaDynamicTerm(
 							new MetaEvaluatableTermVariable(new Variable("te")),
-							new MetaEvaluatableTermVariable(new Variable("re")),
-							new MetaEvaluatableTermVariable(new Variable("ue"))
+							(MetaTermPairGenerator) (index, depth, isLast) -> new TermPair(
+									new MetaEvaluatableTermVariable(new Variable("re" + index)),
+									new MetaEvaluatableTermVariable(new Variable("ue" + index))
+							)
 					)
 			)
 	);
diff --git a/src/main/java/models/formulas/meta/MetaFormula.java b/src/main/java/models/formulas/meta/MetaFormula.java
index 4087d45..bb54cc0 100644
--- a/src/main/java/models/formulas/meta/MetaFormula.java
+++ b/src/main/java/models/formulas/meta/MetaFormula.java
@@ -26,7 +26,6 @@
 		return result;
 	}
 	
-	
 	public abstract Formula substitution(Map<Variable, RDLTerm> binding);
 	
     public abstract <T extends RDLTerm> Set<T> getSubTerms(Class<T> clazz);
diff --git a/src/main/java/models/terms/meta/MetaDynamicTerm.java b/src/main/java/models/terms/meta/MetaDynamicTerm.java
index a50ab8b..2bfa5f1 100644
--- a/src/main/java/models/terms/meta/MetaDynamicTerm.java
+++ b/src/main/java/models/terms/meta/MetaDynamicTerm.java
@@ -215,8 +215,8 @@
 		TermPair termPair = termPairGenerator.generate(0, depth, depth == maxRecursion - 1);
 		termPairs.add(termPair.dependedTerm());
 		termPairs.add(termPair.argTerm());
-		for (int i = 0; i < searchMaxTermPairIndex(binding, depth, depth == maxRecursion - 1); i++) {
-			TermPair pair = termPairGenerator.generate(0, depth, depth == maxRecursion - 1);
+		for (int i = 1; i <= searchMaxTermPairIndex(binding, depth, depth == maxRecursion - 1); i++) {
+			TermPair pair = termPairGenerator.generate(i, depth, depth == maxRecursion - 1);
 			termPairs.add(pair.dependedTerm());
 			termPairs.add(pair.argTerm());
 		}
@@ -295,7 +295,7 @@
 	}
 	
 	public MetaRDLTerm dependencyTermGenerate(Map<Variable, RDLTerm> binding) {
-		int ok = -1;
+		int ok = 0;
 		int ng = 100;
 		while (Math.abs(ok - ng) > 1) {
 			int mid = (ok + ng) / 2;
diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java
index 3b2ca78..d92d06e 100644
--- a/src/test/java/inferencerule/EqualityAxiomTest.java
+++ b/src/test/java/inferencerule/EqualityAxiomTest.java
@@ -12,6 +12,7 @@
 import models.formulas.Formula;
 import models.terms.Dependency;
 import models.terms.DependencyTerm;
+import models.terms.RDLTerm;
 import models.terms.Resource;
 import utils.Utils;
 
@@ -80,11 +81,13 @@
 		EquationFormula eq1 = new EquationFormula(te0, ue);
 		DependencyFormula df1 = new DependencyFormula(se, re0, re1, re2);
 		EquationFormula eq2 = new EquationFormula(new DependencyTerm(re0, a, b), te0);
+		EquationFormula eq21 = new EquationFormula(new DependencyTerm(re1, c, d), te1);
+		EquationFormula eq22 = new EquationFormula(new DependencyTerm(re2, e, f), te2);
 		DependencyTerm dt1 = new DependencyTerm(se, re0, te0, re1, te1, re2, te2);
 		DependencyTerm dt2 = new DependencyTerm(se, re0, ue, re1, te1, re2, te2);
 		EquationFormula eq3 = new EquationFormula(dt1, dt2);
-		Set<Formula> result2 = ProofSystem.rightSubstitution.apply(List.of(eq1, df1, eq2), Set.of(te1, te2));
-		assertTrue(result2.contains(eq3));
+		RDLTerm result2 = ProofSystem.rightSubstitution.generateRightSideHand(List.of(eq1, df1, eq2, eq21, eq22), eq3.getLeftSideHand());
+		assertEquals(result2, eq3.getRightSideHand());
 		
 	}