diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java
index aec04d1..76ca42f 100644
--- a/src/main/java/inference/ProofSystem.java
+++ b/src/main/java/inference/ProofSystem.java
@@ -21,10 +21,13 @@
 import models.formulas.meta.MetaEquationFormula;
 import models.terms.EvaluatableTerm;
 import models.terms.RDLTerm;
+import models.terms.meta.MetaDynamicTerm;
 import models.terms.meta.MetaEvaluatableTermVariable;
 import models.terms.meta.MetaRDLTerm;
 import models.terms.meta.MetaResource;
 import models.terms.meta.MetaTermGenerator;
+import models.terms.meta.MetaTermPairGenerator;
+import models.terms.meta.MetaTermPairGenerator.TermPair;
 import models.terms.meta.OrderConstraint;
 import utils.ExpressionUitls;
 import utils.Product;
@@ -78,32 +81,38 @@
 			"Right Substitution",
 			List.of(
 					new MetaEquationFormula(
-							new MetaEvaluatableTermVariable(new Variable("te")),
+							new MetaEvaluatableTermVariable(new Variable("te0")),
 							new MetaEvaluatableTermVariable(new Variable("ue"))
 					),
 					new MetaDependencyFormula(
-							new MetaEvaluatableTermVariable(new Variable("se")),
-							new MetaEvaluatableTermVariable(new Variable("re"))
+							new MetaDynamicTerm(
+									new MetaEvaluatableTermVariable(new Variable("se")),
+									(MetaTermGenerator) (index, depth, isLast) -> new MetaEvaluatableTermVariable(new Variable("re" + index))
+							)
 					),
 					new MetaEquationFormula(
 							new MetaRDLTerm(
-									new MetaEvaluatableTermVariable(new Variable("re")), 
+									new MetaEvaluatableTermVariable(new Variable("re0")), 
 									new MetaEvaluatableTermVariable(new Variable("x")), 
 									new MetaEvaluatableTermVariable(new Variable("y"))
 							),
-							new MetaEvaluatableTermVariable(new Variable("te"))
+							new MetaEvaluatableTermVariable(new Variable("te0"))
 					)
 			),
 			new MetaEquationFormula(
-					new MetaRDLTerm(
+					new MetaDynamicTerm(
 							new MetaEvaluatableTermVariable(new Variable("se")),
-							new MetaEvaluatableTermVariable(new Variable("re")),
-							new MetaEvaluatableTermVariable(new Variable("te"))
+							(MetaTermPairGenerator) (index, depth, isLast) -> new TermPair(
+									new MetaEvaluatableTermVariable(new Variable("re" + index)),
+									new MetaEvaluatableTermVariable(new Variable("te" + index))
+							)
 					),
-					new MetaRDLTerm(
+					new MetaDynamicTerm(
 							new MetaEvaluatableTermVariable(new Variable("se")),
-							new MetaEvaluatableTermVariable(new Variable("re")),
-							new MetaEvaluatableTermVariable(new Variable("ue"))
+							(MetaTermPairGenerator) (index, depth, isLast) -> new TermPair(
+									new MetaEvaluatableTermVariable(new Variable("re" + index)),
+									index == 0 ? new MetaEvaluatableTermVariable(new Variable("ue")) : new MetaEvaluatableTermVariable(new Variable("te" + index))
+							)
 					)
 			)
 	);
diff --git a/src/main/java/models/terms/meta/MetaDynamicTerm.java b/src/main/java/models/terms/meta/MetaDynamicTerm.java
index e3e78a4..a50ab8b 100644
--- a/src/main/java/models/terms/meta/MetaDynamicTerm.java
+++ b/src/main/java/models/terms/meta/MetaDynamicTerm.java
@@ -300,6 +300,10 @@
 		while (Math.abs(ok - ng) > 1) {
 			int mid = (ok + ng) / 2;
 			MetaRDLTerm generatedTerm = dependencyTermRecursionGenerate(mid, 0);
+			if (generatedTerm == null) {
+				ng = mid;
+				continue;
+			}
 			Set<Variable> variables = new HashSet<>(generatedTerm.getAllVariables().stream().map(v -> v.getVariableName()).toList());
 			variables.removeAll(binding.keySet());
 			if (variables.isEmpty()) {
diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java
index 9bd49d2..3b2ca78 100644
--- a/src/test/java/inferencerule/EqualityAxiomTest.java
+++ b/src/test/java/inferencerule/EqualityAxiomTest.java
@@ -68,6 +68,24 @@
 		EquationFormula f3 = new EquationFormula(t2, t3);
 		Formula result = ProofSystem.rightSubstitution.apply(List.of(f1, d1, f2));
 		assertEquals(result, f3);
+		
+		Resource te0 = new Resource("te0", Utils.INT, 1);
+		Resource te1 = new Resource("te1", Utils.INT, 1);
+		Resource te2 = new Resource("te2", Utils.INT, 1);
+		Resource ue = new Resource("ue", Utils.INT, 1);
+		Resource se = new Resource("se", Utils.INT, 1);
+		Resource re0 = new Resource("re0", Utils.INT, 1);
+		Resource re1 = new Resource("r1", Utils.INT, 1);
+		Resource re2 = new Resource("r2", Utils.INT, 1);
+		EquationFormula eq1 = new EquationFormula(te0, ue);
+		DependencyFormula df1 = new DependencyFormula(se, re0, re1, re2);
+		EquationFormula eq2 = new EquationFormula(new DependencyTerm(re0, a, b), te0);
+		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));
+		
 	}
 	
 	@Test