diff --git a/src/Main.java b/src/Main.java
index be3a996..9290575 100644
--- a/src/Main.java
+++ b/src/Main.java
@@ -80,8 +80,8 @@
 		ResourceVariable b = new ResourceVariable("B", INT, 2);
 		ResourceVariable c = new ResourceVariable("C", INT, 2);
 		ResourceVariable ap = new ResourceVariable("A'", INT, 2);
-		ResourceVariable bp = new ResourceVariable("B''", INT, 2);
-		ResourceVariable cp = new ResourceVariable("C''", INT, 2);
+		ResourceVariable bp = new ResourceVariable("B'", INT, 2);
+		ResourceVariable cp = new ResourceVariable("C'", INT, 2);
 		
 		DependencyTerm d1 = new DependencyTerm(a, b, c);
 		DependencyTerm d11 = new DependencyTerm(a, b, c);
@@ -89,9 +89,19 @@
 		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, binding, orderConstraint);
-		boolean tmp2 = ProofSystem.RIGHT_REPLACEMENT.check(List.of(), conclu1, binding, orderConstraint);
-		System.out.println(tmp1);
+		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);
+		d11.setDependingTerm(a);
+		d11.setDependedVariable(bp);
+		boolean tmp3 = ProofSystem.CENTER_REPLACEMENT.check(List.of(new EquationFormula(b, bp)), conclu1);
+		d11.setDependedVariable(b);
+		d11.setArgumentTerm(cp);
+		boolean tmp4 = ProofSystem.RIGHT_REPLACEMENT.check(List.of(new EquationFormula(c, cp)), conclu1);
+		d11.setArgumentTerm(c);
+		System.out.println(tmp2);
+		System.out.println(tmp3);
+		System.out.println(tmp4);
 	}
 	
 	@SneakyThrows
diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java
index da86702..e99e7c4 100644
--- a/src/inference/InferenceRule.java
+++ b/src/inference/InferenceRule.java
@@ -52,36 +52,32 @@
 		this.defaultOrderConstraint = null;
 	}
 	
-	public boolean check(Collection<Formula> assumptions, Formula conclusion, 
-			Map<Variable, RDLTerm> binding, Map<Variable, OrderVariableConstraint> orderConstraints) {
+	public boolean check(Collection<Formula> assumptions, Formula conclusion) {
 		if (this.assumptions.size() > assumptions.size()) {
 			return false;
 		}
 		for(List<Formula> assumption : permutation(assumptions, this.assumptions.size())) {
-			if (check(assumption, conclusion, binding, orderConstraints)) {
+			if (check(assumption, conclusion)) {
 				return true;
 			}
 		}
 		return false;
 	}
 	
-	private boolean check(List<Formula> assumptions, Formula conclusion, 
-			Map<Variable, RDLTerm> binding, Map<Variable, OrderVariableConstraint> orderConstraints) {
-		Map<Variable, RDLTerm> tmpBinding = new HashMap<>(binding);
-		Map<Variable, OrderVariableConstraint> tmpOrderConstraints = new HashMap<>(orderConstraints);
+	private boolean check(List<Formula> assumptions, Formula conclusion) {
+		Map<Variable, RDLTerm> binding = new HashMap<>();
+		Map<Variable, OrderVariableConstraint> orderConstraints = new HashMap<>();
 		for (int i = 0; i < assumptions.size(); i++) {
-			if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), tmpBinding, tmpOrderConstraints)) {
+			if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraints)) {
 				return false;
 			}
 		}
-		if (! this.conclusion.isMatchedBy(conclusion, tmpBinding, tmpOrderConstraints)) {
+		if (! this.conclusion.isMatchedBy(conclusion, binding, orderConstraints)) {
 			return false;
 		}
 		if (this.defaultOrderConstraint != null) {
-			return defaultOrderConstraint.check(tmpOrderConstraints);
+			return defaultOrderConstraint.check(orderConstraints);
 		}
-		binding.putAll(tmpBinding);
-		orderConstraints.putAll(tmpOrderConstraints);
 		return true;
 	}
 	
diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index 5ce155e..5df8f9c 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -104,6 +104,39 @@
 			)
 	);
 	
+	public final static InferenceRule LEFT_REPLACEMENT = new InferenceRule("left replacement",
+			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("ue")))),
+			new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaResourceVariable(new Variable("v")),
+							new MetaEvaluatableTermVariable(new Variable("te"))
+					),
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("ue")),
+							new MetaResourceVariable(new Variable("v")),
+							new MetaEvaluatableTermVariable(new Variable("te"))
+					)
+			)
+	);
+	
+	public final static InferenceRule CENTER_REPLACEMENT = new InferenceRule("center replacement",
+			List.of(new MetaEquationFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))),
+			new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaResourceVariable(new Variable("v")),
+							new MetaEvaluatableTermVariable(new Variable("te"))
+					),
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaResourceVariable(new Variable("w")),
+							new MetaEvaluatableTermVariable(new Variable("te"))
+					)
+			)
+	);
+	
+	
 	public final static InferenceRule IDENTITY_LAW = new InferenceRule("identity law", 
 			List.of(new MetaInFormula(
 					new MetaEvaluatableTermVariable(new Variable("te")), 
diff --git a/src/tests/inferencerule/InferenceRuleTest.java b/src/tests/inferencerule/InferenceRuleTest.java
index 05f2b34..f1e89bb 100644
--- a/src/tests/inferencerule/InferenceRuleTest.java
+++ b/src/tests/inferencerule/InferenceRuleTest.java
@@ -5,7 +5,6 @@
 
 import org.junit.jupiter.api.Test;
 
-import java.util.HashMap;
 import java.util.List;
 
 import inference.InferenceRule;
@@ -45,7 +44,7 @@
 		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, new HashMap<>(), new HashMap<>()));
+		assertTrue(goseShazo.check(List.of(df1, df2), df3));
 		
 	}
 	
@@ -74,7 +73,7 @@
 		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, new HashMap<>(), new HashMap<>()));
+		assertTrue(rightReplacement.check(List.of(assump2), concl2));
 	}
 	
 }