diff --git a/src/inference/InferenceOrderConstraint.java b/src/inference/InferenceOrderConstraint.java
new file mode 100644
index 0000000..6c789e9
--- /dev/null
+++ b/src/inference/InferenceOrderConstraint.java
@@ -0,0 +1,83 @@
+package inference;
+import java.util.Map;
+
+import exceptions.IllegalTypeException;
+import lombok.Getter;
+import models.algebra.Constant;
+import models.algebra.Expression;
+import models.algebra.Variable;
+import models.terms.meta.OrderConstraint;
+import models.terms.meta.OrderVariableConstraint;
+
+@Getter
+public class InferenceOrderConstraint {
+	
+	private final Variable leftSideHandVariable;
+	private final int leftSideHandConstant;
+	private final OrderConstraint operator;
+	private final Variable rightSideHandVariable;
+	private final int rightSideHandConstant;
+	
+	public InferenceOrderConstraint(Expression left, OrderConstraint operator, Expression right) {
+		if ((left instanceof Constant) && (right instanceof Constant)) {
+			throw new IllegalTypeException("Both left and right can't be Constant");
+		}
+		if (left instanceof Constant) {
+			leftSideHandConstant = Integer.parseInt(((Constant) left).toString());
+			leftSideHandVariable = null;
+		} else if (left instanceof Variable) {
+			leftSideHandConstant = -1;
+			leftSideHandVariable = (Variable) left;
+		} else {
+			throw new IllegalTypeException("Left must be Constant or Variable");
+		}
+		
+		this.operator = operator;
+		
+		if (right instanceof Constant) {
+			rightSideHandConstant = Integer.parseInt(((Constant) right).toString());
+			rightSideHandVariable = null;
+		} else if (right instanceof Variable) {
+			rightSideHandConstant = -1;
+			rightSideHandVariable = (Variable) right;
+		} else {
+			throw new IllegalTypeException("Right must be Constant or Variable");
+		}
+	}
+	
+	public boolean check(Map<Variable, OrderVariableConstraint> orderConstraints) {
+		switch(this.operator) {
+		case EQ:
+			return getLeftValue(orderConstraints) == getRightValue(orderConstraints);
+		case GE:
+			return getLeftValue(orderConstraints) >= getRightValue(orderConstraints);
+		case GT:
+			return getLeftValue(orderConstraints) > getRightValue(orderConstraints);
+		case LE:
+			return getLeftValue(orderConstraints) <= getRightValue(orderConstraints);
+		case LT:
+			return getLeftValue(orderConstraints) < getRightValue(orderConstraints);
+		default:
+			return false;
+		}
+	}
+	
+	private int getLeftValue(Map<Variable, OrderVariableConstraint> orderConstraints) {
+		if (this.leftSideHandVariable != null) {
+			OrderVariableConstraint constraint = orderConstraints.get(this.leftSideHandVariable);
+			return constraint.getLower();
+		} else {
+			return this.leftSideHandConstant;
+		}
+	}
+	
+	private int getRightValue(Map<Variable, OrderVariableConstraint> orderConstraints) {
+		if (this.rightSideHandVariable != null) {
+			OrderVariableConstraint constraint = orderConstraints.get(this.rightSideHandVariable);
+			return constraint.getLower();
+		} else {
+			return this.rightSideHandConstant;
+		}
+	}
+	
+}
diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java
index 7f5798b..d1cc53a 100644
--- a/src/inference/InferenceRule.java
+++ b/src/inference/InferenceRule.java
@@ -8,18 +8,29 @@
 import java.util.Map;
 import java.util.Set;
 
-import lombok.RequiredArgsConstructor;
 import models.algebra.Variable;
 import models.formulas.Formula;
 import models.formulas.meta.MetaFormula;
 import models.terms.RDLTerm;
 import models.terms.meta.OrderVariableConstraint;
 
-@RequiredArgsConstructor
 public class InferenceRule {
 
 	private final List<MetaFormula> assumptions;
 	private final MetaFormula conclusion;
+	private final InferenceOrderConstraint defaultOrderConstraint;
+	
+	public InferenceRule(List<MetaFormula> assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) {
+		this.assumptions = assumptions;
+		this.conclusion = conclusion;
+		this.defaultOrderConstraint = constraint;
+	}
+	
+	public InferenceRule(List<MetaFormula> assumptions, MetaFormula conclusion) {
+		this.assumptions = assumptions;
+		this.conclusion = conclusion;
+		this.defaultOrderConstraint = null;
+	}
 	
 	public boolean check(Collection<Formula> assumptions, Formula conclusion) {
 		if (this.assumptions.size() > assumptions.size()) {
@@ -41,7 +52,13 @@
 				return false;
 			}
 		}
-		return this.conclusion.isMatchedBy(conclusion, binding, orderConstraints);
+		if (! this.conclusion.isMatchedBy(conclusion, binding, orderConstraints)) {
+			return false;
+		}
+		if (this.defaultOrderConstraint != null) {
+			return defaultOrderConstraint.check(orderConstraints);
+		}
+		return true;
 	}
 	
 	private <T> List<List<T>> permutation(Collection<T> list, int n) {
diff --git a/src/models/terms/meta/OrderVariableConstraint.java b/src/models/terms/meta/OrderVariableConstraint.java
index 41c7bd3..d997e0d 100644
--- a/src/models/terms/meta/OrderVariableConstraint.java
+++ b/src/models/terms/meta/OrderVariableConstraint.java
@@ -1,8 +1,10 @@
 package models.terms.meta;
 
+import lombok.Getter;
 import lombok.NoArgsConstructor;
 
 @NoArgsConstructor
+@Getter
 public class OrderVariableConstraint {
 
 	// lower <= x <= upper
@@ -28,10 +30,6 @@
 		return false;
 	}
 	
-	public boolean isOk() {
-		return isOk;
-	}
-	
 	
 	private boolean setEq(int eq) {
 		return setUpper(eq) && setLower(eq);