diff --git a/src/main/asp/unifyPaper.pl b/src/main/asp/unifyPaper.pl
new file mode 100644
index 0000000..1754fbc
--- /dev/null
+++ b/src/main/asp/unifyPaper.pl
@@ -0,0 +1,30 @@
+
+type("Name", paramList).
+type("Name", params()).
+params(paramList, tph(a), 1).
+
+% subst:
+subst(tph(A), type(N,P)) :- equalcons(tph(A), type(N, P)).
+
+% subst-L:
+substcons(B,C) :- subst(A, B), substcons(A, C).
+%subst-R:
+substcons(B,C) :- subst(A, B), substcons(C, A).
+%subst-Equal:
+equalcons(B,C) :- subst(A, B), substcons(A, C).
+
+%swap:
+equalcons(A,B) :- equalcons(B,A).
+
+%unfold:
+equalcons(T, T) :- equalcons(tph(_), type(_, params(T, _, _))).
+equalcons(T, T) :- equalcons(tph(_), type(_, params(_, T, _))).
+equalcons(T, T) :- equalcons(tph(_), type(_, params(_, _, T))).
+
+% here we check if there is a constraint a <. C, where there is no other Constraint. This is the solution-Gen rule
+%Solution-Subst:
+hasNoSupertype(tph(A), type(D,P2)) :- substcons(tph(A), type(C,P)), substcons(tph(A), type(D,P2)), not super(D, C).
+equalcons(tph(A), type(C,P)) :- substcons(tph(A), type(C,P)), hasNoSupertype(tph(A), type(C,P)).
+
+%Solution:
+sigma(tph(A), tpye(C,P)) :- equalcons(tph(A), type(C, P)), not tphs(_, P).
\ No newline at end of file