diff --git a/src/Main.java b/src/Main.java
index 9f8cae4..36f4d00 100644
--- a/src/Main.java
+++ b/src/Main.java
@@ -31,8 +31,7 @@
 	public static void main(String[] args) {
 //		sandbox1();
 //		sandbox2();
-//		sandbox3();
-		sandbox4();
+		sandbox3();
 //		ProofSystem.debug();
 	}
 	
@@ -101,16 +100,6 @@
 		System.out.println(result);
 	}
 	
-	static void sandbox4() {
-		ResourceVariable followee = new ResourceVariable("followee", INT, 2);
-		ResourceVariable fno = new ResourceVariable("fno", INT, 2);
-		ResourceVariable follower = new ResourceVariable("follower", INT, 1);
-		DependencyFormula f1 = new DependencyFormula(new Dependency(followee, fno), follower);
-		DependencyFormula f2 = new DependencyFormula(new Dependency(new Dependency(new SetEvaluatableTerm(followee), follower)));
-		boolean result = ProofSystem.check(List.of(f1), f2);
-		System.out.println(result);
-	}
-	
 	
 	
 	@SneakyThrows
diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index 4b119c2..643b605 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -31,9 +31,6 @@
 
 public class ProofSystem {
 
-	//MetaExistFormulaのような存在が必要ということを示すFormulaを作ってもいいかも
-	//あるいはチェックの時にconclusionのほうから必要なものをあらかじめ抽出しておく
-	
 	//======================Equality Axioms=============================
 	
 	private static final InferenceRule reflexivity = new InferenceRule(
diff --git a/src/models/terms/Dependency.java b/src/models/terms/Dependency.java
index d59de46..e334f94 100644
--- a/src/models/terms/Dependency.java
+++ b/src/models/terms/Dependency.java
@@ -12,7 +12,7 @@
 	private boolean isListType;
 	
 	public Dependency(RDLTerm dependingTerm, ResourceVariable dependedVariable) {
-		super(new Symbol(":", 2), dependedVariable.getOrder());
+		super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize());
 		this.dependingTerm = dependingTerm;
 		this.dependedVariable = dependedVariable;
 		this.dependency = null;
@@ -22,7 +22,7 @@
 	}
 	
 	public Dependency(Dependency dependency) {
-		super(new Symbol(":", 1), dependency.getOrder() - 1);
+		super(new Symbol(":", 1), dependency.getOrder() - 1, dependency.getSize());
 		this.dependency = dependency;
 		this.dependingTerm = null;
 		this.dependedVariable = null;
@@ -31,7 +31,7 @@
 	}
 	
 	public Dependency(RDLTerm dependingTerm, ResourceVariable dependedVariable, int order) {
-		super(new Symbol(":", order == dependedVariable.order ? 2 : 1), order);
+		super(new Symbol(":", order == dependedVariable.order ? 2 : 1), order, dependingTerm.getSize() + dependedVariable.getSize());
 		if(order == dependedVariable.order) {
 			this.dependingTerm = dependingTerm;
 			this.dependedVariable = dependedVariable;
diff --git a/src/models/terms/DependencyTerm.java b/src/models/terms/DependencyTerm.java
index bef9d63..0995cf7 100644
--- a/src/models/terms/DependencyTerm.java
+++ b/src/models/terms/DependencyTerm.java
@@ -10,12 +10,16 @@
 	private ResourceVariable dependedVariable;
 	private EvaluatableTerm argumentTerm;
 	
-	public DependencyTerm(int order) {
-		super(new Symbol(":", 3), order);
-	}
+//	public DependencyTerm(int order) {
+//		super(new Symbol(":", 3), order);
+//	}
 	
 	public DependencyTerm(EvaluatableTerm dependingTerm, ResourceVariable dependedVariable, EvaluatableTerm argumentTerm) {
-		super(new Symbol(":", 3), dependedVariable.getOrder() == argumentTerm.getOrder() ? dependedVariable.getOrder() : dependedVariable.getOrder() - 1);
+		super(
+				new Symbol(":", 3), 
+				dependedVariable.getOrder() == argumentTerm.getOrder() ? dependedVariable.getOrder() : dependedVariable.getOrder() - 1,
+				dependedVariable.getSize() + argumentTerm.getSize() + dependedVariable.getSize()
+		);
 		this.dependingTerm = dependingTerm;
 		this.dependedVariable = dependedVariable;
 		this.argumentTerm = argumentTerm;
diff --git a/src/models/terms/EvaluatableTerm.java b/src/models/terms/EvaluatableTerm.java
index d75d77b..59641a9 100644
--- a/src/models/terms/EvaluatableTerm.java
+++ b/src/models/terms/EvaluatableTerm.java
@@ -6,8 +6,8 @@
 
 public abstract class EvaluatableTerm extends RDLTerm{
 
-	public EvaluatableTerm(Symbol symbol, int order) {
-		super(symbol, order);
+	protected EvaluatableTerm(Symbol symbol, int order, int size) {
+		super(symbol, order, size);
 	}
 	
 	public abstract boolean isLinearRightNormalized();
diff --git a/src/models/terms/RDLTerm.java b/src/models/terms/RDLTerm.java
index 0ec2003..9b8a038 100644
--- a/src/models/terms/RDLTerm.java
+++ b/src/models/terms/RDLTerm.java
@@ -5,13 +5,15 @@
 import models.algebra.Term;
 
 @Getter
-public abstract class RDLTerm extends Term{
+public abstract class RDLTerm extends Term {
 
 	protected int order;
+	protected int size;
 	
-	public RDLTerm(Symbol symbol, int order) {
+	protected RDLTerm(Symbol symbol, int order, int size) {
 		super(symbol);
 		this.order = order;
+		this.size = size;
 	}
 	
 	public int getTermOrder() {
diff --git a/src/models/terms/ResourceConstant.java b/src/models/terms/ResourceConstant.java
index a7c2d1b..1158b84 100644
--- a/src/models/terms/ResourceConstant.java
+++ b/src/models/terms/ResourceConstant.java
@@ -11,13 +11,13 @@
 	private Type type;
 	
 	public ResourceConstant(String name) {
-		super(new Symbol("", 0), 0);
+		super(new Symbol("", 0), 0, 1);
 		this.name = name;
 		this.type = null;
 	}
 	
 	public ResourceConstant(String name, Type type) {
-		super(new Symbol("", 0), 0);
+		super(new Symbol("", 0), 0, 1);
 		this.name = name;
 		this.type = type;
 	}
diff --git a/src/models/terms/ResourceVariable.java b/src/models/terms/ResourceVariable.java
index 819f362..57b0a9b 100644
--- a/src/models/terms/ResourceVariable.java
+++ b/src/models/terms/ResourceVariable.java
@@ -11,7 +11,7 @@
 	private Type type;
 	
 	public ResourceVariable(String name, Type type, int order) {
-		super(new Symbol("", 0), order);
+		super(new Symbol("", 0), order, 1);
 		this.name = name;
 		this.type = type;
 	}
diff --git a/src/models/terms/SetEvaluatableTerm.java b/src/models/terms/SetEvaluatableTerm.java
index 5a9c1c9..05fc8e2 100644
--- a/src/models/terms/SetEvaluatableTerm.java
+++ b/src/models/terms/SetEvaluatableTerm.java
@@ -9,13 +9,13 @@
 	private EvaluatableTerm term;
 	
 	public SetEvaluatableTerm(EvaluatableTerm term) {
-		super(new Symbol("", 1), term.getOrder() - 1);
+		super(new Symbol("", 1), term.getOrder() - 1, term.getSize());
 		this.term = term;
 		this.addChild(term);
 	}
 	
 	public SetEvaluatableTerm(EvaluatableTerm term, int order) {
-		super(new Symbol("", 1), order);
+		super(new Symbol("", 1), order, term.getSize());
 		if(term.getOrder() > order + 1) {
 			var childTerm = new SetEvaluatableTerm(term, order+1); 
 			this.term = childTerm;
diff --git a/src/models/terms/meta/MetaRDLTerm.java b/src/models/terms/meta/MetaRDLTerm.java
index 17ae060..93600c5 100644
--- a/src/models/terms/meta/MetaRDLTerm.java
+++ b/src/models/terms/meta/MetaRDLTerm.java
@@ -23,8 +23,8 @@
 	protected TermType termType;
 	protected LinearRightNormalizedType linearRightNormalizedType = LinearRightNormalizedType.UNDEFINED;
 	
-	protected MetaRDLTerm(Symbol symbol, TermType termType) {
-		super(symbol, -1);
+	protected MetaRDLTerm(Symbol symbol, TermType termType, int size) {
+		super(symbol, -1, size);
 		this.termType = termType;
 		if (isResourceVariable()) {
 			linearRightNormalizedType = LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED;
@@ -33,21 +33,21 @@
 	
 	//dependency
 	public MetaRDLTerm(RDLTerm dependingTerm, MetaResourceVariable dependedVariable) {
-		super(new Symbol(":", 2), dependedVariable.getOrder());
+		super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize());
 		addChild(dependingTerm);
 		addChild(dependedVariable);
 		this.termType = TermType.META_DEPENDENCY;
 	}
 	
 	public MetaRDLTerm(MetaRDLTerm dependingTerm, ResourceVariable dependedVariable) {
-		super(new Symbol(":", 2), dependedVariable.getOrder());
+		super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize());
 		addChild(dependingTerm);
 		addChild(dependedVariable);
 		this.termType = TermType.META_DEPENDENCY;
 	}
 	
 	public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaResourceVariable dependedVariable) {
-		super(new Symbol(":", 2), dependedVariable.getOrder());
+		super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize());
 		addChild(dependingTerm);
 		addChild(dependedVariable);
 		this.termType = TermType.META_DEPENDENCY;
@@ -55,7 +55,7 @@
 	
 	//list type dependency or set term
 	public MetaRDLTerm(MetaRDLTerm term) {
-		super(new Symbol(":", 1), term.getOrder() - 1);
+		super(new Symbol(":", 1), term.getOrder() - 1, term.getSize());
 		if (term.isDependency()) {
 			this.termType = TermType.META_DEPENDENCY_LIST;
 		} else if (term.isEvaluatableTerm()) {
@@ -66,7 +66,7 @@
 	
 	//dependency term
 	public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaResourceVariable dependedVariable, MetaRDLTerm argumentTerm) {
-		super(new Symbol(":", 3), -1);
+		super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize());
 		if (! EvaluatableTerm.class.isAssignableFrom(dependingTerm.getTermType().getBaseTermClass())) {
 			throw new IllegalTypeException();
 		}
@@ -80,7 +80,7 @@
 	}
 	
 	public MetaRDLTerm(EvaluatableTerm dependingTerm, MetaRDLTerm dependedVariable, MetaRDLTerm argumentTerm) {
-		super(new Symbol(":", 3), -1);
+		super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize());
 		if(! EvaluatableTerm.class.isAssignableFrom(argumentTerm.getTermType().getBaseTermClass())) {
 			throw new IllegalTypeException();
 		}
@@ -91,7 +91,7 @@
 	}
 	
 	public MetaRDLTerm(MetaRDLTerm dependingTerm, ResourceVariable dependedVariable, MetaRDLTerm argumentTerm) {
-		super(new Symbol(":", 3), -1);
+		super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize());
 		if (! EvaluatableTerm.class.isAssignableFrom(dependingTerm.getTermType().getBaseTermClass())) {
 			throw new IllegalTypeException();
 		}
@@ -105,7 +105,7 @@
 	}
 	
 	public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm dependedVariable, EvaluatableTerm argumentTerm) {
-		super(new Symbol(":", 3), -1);
+		super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize());
 		if (! EvaluatableTerm.class.isAssignableFrom(dependingTerm.getTermType().getBaseTermClass())) {
 			throw new IllegalTypeException();
 		}
@@ -116,7 +116,7 @@
 	}
 	
 	public MetaRDLTerm(MetaRDLTerm dependingTerm, ResourceVariable dependedVariable, EvaluatableTerm argumentTerm) {
-		super(new Symbol(":", 3), -1);
+		super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize());
 		if (! EvaluatableTerm.class.isAssignableFrom(dependingTerm.getTermType().getBaseTermClass())) {
 			throw new IllegalTypeException();
 		}
@@ -127,7 +127,7 @@
 	}
 	
 	public MetaRDLTerm(EvaluatableTerm dependingTerm, MetaResourceVariable dependedVariable, EvaluatableTerm argumentTerm) {
-		super(new Symbol(":", 3), -1);
+		super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize());
 		addChild(dependingTerm);
 		addChild(dependedVariable);
 		addChild(argumentTerm);
@@ -135,7 +135,7 @@
 	}
 	
 	public MetaRDLTerm(EvaluatableTerm dependingTerm, ResourceVariable dependedVariable, MetaRDLTerm argumentTerm) {
-		super(new Symbol(":", 3), -1);
+		super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize());
 		if(! EvaluatableTerm.class.isAssignableFrom(argumentTerm.getTermType().getBaseTermClass())) {
 			throw new IllegalTypeException();
 		}
@@ -155,7 +155,9 @@
 			if (dependedVariable instanceof MetaRDLTerm) {
 				dependedVariable = ((MetaRDLTerm) dependedVariable).substitute(binding);
 			}
-			return new Dependency(dependingTerm, (ResourceVariable) dependedVariable);
+			if (dependedVariable instanceof ResourceVariable) {
+				return new Dependency(dependingTerm, (ResourceVariable) dependedVariable);
+			}
 		}
 		else if (isDependencyTerm()) {
 			RDLTerm dependingTerm = (RDLTerm) getChild(0);
diff --git a/src/models/terms/meta/MetaVariable.java b/src/models/terms/meta/MetaVariable.java
index 27e13db..804f1c2 100644
--- a/src/models/terms/meta/MetaVariable.java
+++ b/src/models/terms/meta/MetaVariable.java
@@ -24,7 +24,7 @@
 	protected Expression orderExpression;
  	
 	protected MetaVariable(Symbol symbol, TermType termType, Variable name, OrderConstraint constraint, Expression order) {
-		super(symbol, termType);
+		super(symbol, termType, 1);
 		this.variableName = name;
 		this.constraint = constraint;
 		this.orderExpression = order;
@@ -46,7 +46,7 @@
 	}
 	
 	protected MetaVariable(Symbol symbol, TermType termType, Variable name, OrderConstraint constraint, Expression order, LinearRightNormalizedType linearRIghtNormalizedType) {
-		super(symbol, termType);
+		super(symbol, termType, 1);
 		this.variableName = name;
 		this.constraint = constraint;
 		this.orderExpression = order;