diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index e652591..f3c89d2 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -10,277 +10,12 @@
 import java.util.Map;
 import java.util.Set;
 
-import models.algebra.Constant;
-import models.algebra.Variable;
 import models.formulas.EquationFormula;
 import models.formulas.Formula;
-import models.formulas.meta.MetaDependencyFormula;
-import models.formulas.meta.MetaEquationFormula;
-import models.formulas.meta.MetaInFormula;
 import models.terms.EvaluatableTerm;
-import models.terms.meta.MetaDependencyVariable;
-import models.terms.meta.MetaEvaluatableTermVariable;
-import models.terms.meta.MetaRDLTerm;
-import models.terms.meta.MetaResourceVariable;
-import models.terms.meta.OrderConstraint;
 
 public class ProofSystem {
 
-	public final static InferenceRule REFLEXIVE_LAW = new InferenceRule("relfexive law", List.of(), 
-			new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("te"))));
-	
-	public final static InferenceRule SYMMETRIC_LAW = new InferenceRule("symmetric law", 
-		List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("se")))),
-		new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te"))));
-	
-	public final static InferenceRule TRANSITIVE_LAW = new InferenceRule("transitive law", 
-			List.of(
-					new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te"))),
-					new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue")))
-			),
-			new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("ue")))
-	);
-	
-	public final static InferenceRule IDENTITY_MAPPING = new InferenceRule("identity mapping", 
-			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v")))),
-			new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v")))
-	);
-	
-	public final static InferenceRule COMPOSITE_MAPPING = new InferenceRule("composite mapping", 
-			List.of(
-					new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v"))),
-					new MetaDependencyFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))
-			),
-			new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("w")))
-	);
-	
-	public final static InferenceRule LEFT_PROJECTION = new InferenceRule("left projection", 
-			List.of(new MetaDependencyFormula(
-								new MetaRDLTerm(
-										new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
-										new MetaResourceVariable(new Variable("v"), new Variable("m"))
-								),
-								new MetaResourceVariable(new Variable("w"), new Variable("l"))
-			)),
-			new MetaDependencyFormula(
-					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))),
-					new MetaResourceVariable(new Variable("w"), new Variable("l"))
-			)
-	);
-	
-	public final static InferenceRule RIGHT_PROJECTION = new InferenceRule("right projection", 
-			List.of(new MetaDependencyFormula(
-								new MetaRDLTerm(
-										new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
-										new MetaResourceVariable(new Variable("v"), new Variable("m"))
-								),
-								new MetaResourceVariable(new Variable("w"), new Variable("l"))
-			)),
-			new MetaDependencyFormula(
-					new MetaRDLTerm(new MetaResourceVariable(new Variable("v"), new Variable("m"))),
-					new MetaResourceVariable(new Variable("w"), new Variable("l"))
-			)
-	);
-	
-	public final static InferenceRule CONSTANT_MAPPING = new InferenceRule("constant mapping", 
-			List.of(),
-			new MetaDependencyFormula(
-					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
-					new MetaResourceVariable(new Variable("v"), new Variable("m"))
-			),
-			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
-	); // 定値写像??
-	
-	public final static InferenceRule ORDER_DESCENTING = new InferenceRule("order descenting", 
-			List.of(new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")))),
-			new MetaDependencyFormula(new MetaRDLTerm(new MetaDependencyVariable(new Variable("d"), new Variable("n")))),
-			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
-	); // 階数降下??
-		
-	public final static InferenceRule RIGHT_REPLACEMENT = new InferenceRule("right replacement",
-			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), 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("se")),
-							new MetaResourceVariable(new Variable("v")),
-							new MetaEvaluatableTermVariable(new Variable("ue"))
-					)
-			)
-	);
-	
-	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")), 
-					new MetaRDLTerm(new MetaResourceVariable(new Variable("v"))))
-			),
-			new MetaEquationFormula(
-					new MetaRDLTerm(
-							new MetaResourceVariable(new Variable("v")),
-							new MetaResourceVariable(new Variable("v")),
-							new MetaEvaluatableTermVariable(new Variable("te"))
-					),
-					new MetaEvaluatableTermVariable(new Variable("te"))
-			)
-	);
-	
-	public final static InferenceRule JOIN = new InferenceRule("join",
-			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 MetaRDLTerm(
-									new MetaResourceVariable(new Variable("w")),
-									new MetaResourceVariable(new Variable("x")),
-									new MetaEvaluatableTermVariable(new Variable("te"))
-							)
-					),
-					new MetaRDLTerm(
-							new MetaEvaluatableTermVariable(new Variable("se")),
-							new MetaResourceVariable(new Variable("x")),
-							new MetaEvaluatableTermVariable(new Variable("te"))
-					)
-			)
-	);
-	
-	public final static InferenceRule CONSTANT_VALUE_LAW = new InferenceRule("constant value law", 
-			List.of(new MetaInFormula(
-					new MetaEvaluatableTermVariable(new Variable("t")), 
-					new MetaRDLTerm(new MetaResourceVariable(new Variable("v"), new Variable("m"))))
-			),
-			new MetaEquationFormula(
-					new MetaRDLTerm(
-							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
-							new MetaResourceVariable(new Variable("v"), new Variable("m")),
-							new MetaEvaluatableTermVariable(new Variable("t"))
-					),
-					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
-			),
-			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
-	);//定値性??
-	
-	public final static InferenceRule RIGHT_NORMALIZE = new InferenceRule("right normalize", 
-			List.of(
-					new MetaDependencyFormula(
-							new MetaEvaluatableTermVariable(new Variable("te")),
-							new MetaResourceVariable(new Variable("v"), new Variable("n"))
-					),
-					new MetaDependencyFormula(
-							new MetaEvaluatableTermVariable(new Variable("se")),
-							new MetaResourceVariable(new Variable("w"), new Variable("n"))
-					)
-			),
-			new MetaEquationFormula(
-					new MetaRDLTerm(
-							new MetaRDLTerm(
-									new MetaEvaluatableTermVariable(new Variable("te")),
-									new MetaResourceVariable(new Variable("v"), new Variable("n")),
-									new MetaEvaluatableTermVariable(new Variable("se"))
-							),
-							new MetaResourceVariable(new Variable("w"), new Variable("n")),
-							new MetaEvaluatableTermVariable(new Variable("ue"))
-					),
-					new MetaRDLTerm(
-							new MetaEvaluatableTermVariable(new Variable("te")),
-							new MetaResourceVariable(new Variable("v"), new Variable("n")),
-							new MetaRDLTerm(
-									new MetaEvaluatableTermVariable(new Variable("se")),
-									new MetaResourceVariable(new Variable("w"), new Variable("n")),
-									new MetaEvaluatableTermVariable(new Variable("ue"))
-							)
-					)
-			),
-			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
-	);
-	
-	public final static InferenceRule PSEUDO_IDENTITY_LAW = new InferenceRule("pseudo identity law",
-			List.of(
-					new MetaDependencyFormula(
-							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
-							new MetaResourceVariable(new Variable("v"), new Variable("n"))
-					)
-			),
-			new MetaEquationFormula(
-					new MetaRDLTerm(
-							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
-							new MetaResourceVariable(new Variable("v"), new Variable("n")),
-							new MetaResourceVariable(new Variable("v"), new Variable("n"))
-					),
-					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
-			),
-			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
-	);//疑似恒等性??
-	
-	public final static InferenceRule SET_EQUIVALENCE = new InferenceRule("set equivalence",
-			List.of(new MetaEquationFormula(
-					new MetaEvaluatableTermVariable(new  Variable("se"), new Variable("n")),
-					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
-			)),
-			new MetaEquationFormula(
-					new MetaRDLTerm(new MetaEvaluatableTermVariable(new  Variable("se"), new Variable("n"))),
-					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")))
-			),
-			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
-	);//集合同値性??
-	
-	public final static InferenceRule HOMOMORPHISM = new InferenceRule("homomorphism",
-			List.of(new MetaDependencyFormula(
-					new MetaEvaluatableTermVariable(new Variable("se")),
-					new MetaResourceVariable(new Variable("v"))
-			)),
-			new MetaEquationFormula(
-					new MetaRDLTerm(
-							new MetaEvaluatableTermVariable(new Variable("se")),
-							new MetaResourceVariable(new Variable("v")),
-							new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te")))
-					),
-					new MetaRDLTerm(
-							new MetaRDLTerm(
-									new MetaEvaluatableTermVariable(new Variable("se")),
-									new MetaResourceVariable(new Variable("v")),
-									new MetaEvaluatableTermVariable(new Variable("te"))
-							)
-					)
-			)
-	);//準同型性??
-	
 	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
 		if (equationTransitionCheck(assumptions, conclusion)) {
 			return true;