diff --git a/src/terms.c b/src/terms.c
index 35c931b..aeca1eb 100644
--- a/src/terms.c
+++ b/src/terms.c
@@ -1,10 +1,15 @@
-/**
- * @file terms.c 
- * \brief Term related base functions.
+/** @file terms.c \brief Term related base functions.
  *
- * Intended to be a standalone file, however during development it turned out that a termlist structure was needed
- * to define term types, so there is now a dependency loop with termlists.c.
+ * Intended to be a standalone file, however during development it turned out
+ * that a termlist structure was needed to define term types, so there is now a
+ * dependency loop with termlists.c.
+ *
+ * Until now, symbols were unique and never deleted.  The same holds for basic
+ * terms; leaves are equal when their pointers are equal.  We are looking to
+ * extend this to whole terms. At that point, term equality is be reduced to
+ * pointer comparison, which is what we want. However, for comparison of terms
  */
+
 #include <strings.h>
 #include <stdlib.h>
 #include <stdio.h>
@@ -161,6 +166,28 @@ hasTermVariable (Term term)
     }
 }
 
+#ifdef DEBUG
+int isTermEqualDebug (Term t1, Term t2)
+{
+  int test1, test2;
+
+  t1 = deVar (t1);
+  t2 = deVar (t2);
+
+  test1 = isTermEqualFn (t1,t2);
+  if (!(realTermLeaf (t1) && realTermLeaf (t2)))
+    {
+      return test1;
+    }
+
+  test2 = (t1 == t2);
+  if (test1 != test2)
+    {
+      error ("Pointer equality hypothesis for leaves does not hold!");
+    }
+  return test1;
+}
+#endif
 
 //!Tests whether two terms are completely identical.
 /**
@@ -189,7 +216,18 @@ isTermEqualFn (Term term1, Term term2)
     }
   if (realTermLeaf (term1))
     {
-      return (term1->left.symb == term2->left.symb && term1->right.runid == term2->right.runid);
+#ifdef DEBUG
+      int test;
+
+      test = (term1->left.symb == term2->left.symb && term1->right.runid == term2->right.runid);
+      if (test)
+	{
+	  error ("Strange node equality detected, should not occur.");
+	}
+      return test;
+#else
+      return 0;
+#endif
     }
   else
     {
diff --git a/src/terms.h b/src/terms.h
index bfdada4..b571c3c 100644
--- a/src/terms.h
+++ b/src/terms.h
@@ -74,7 +74,11 @@ Term deVarScan (Term t);
 #define isTermTuple(t)		realTermTuple(deVar(t))
 #define isTermEncrypt(t)	realTermEncrypt(deVar(t))
 #define isTermVariable(t)	realTermVariable(deVar(t))
-#define isTermEqual(t1,t2)	((substVar(t1) || substVar(t2)) \
+#ifdef DEBUG
+#define isTermEqual(t1,t2)      isTermEqualDebug(t1,t2)
+int isTermEqualDebug (Term t1, Term t2);
+#else
+#define isTermEqual1(t1,t2)	((substVar(t1) || substVar(t2)) \
 				?	isTermEqualFn(t1,t2) \
 				:	( \
 					(t1 == t2) \
@@ -84,7 +88,7 @@ Term deVarScan (Term t);
 						?	0 \
 						:	( \
 							realTermLeaf(t1) \
-							?	(t1->left.symb == t2->left.symb && t1->right.runid == t2->right.runid) \
+							?	0 \
 							:	( \
 								realTermEncrypt(t2) \
 								?	(isTermEqualFn(t1->right.key, t2->right.key) && \
@@ -97,6 +101,55 @@ Term deVarScan (Term t);
 					) \
 				)
 
+#define isTermEqual2(t1,t2)	((substVar(t1) || substVar(t2)) \
+				?	isTermEqual1(t1,t2) \
+				:	( \
+					(t1 == t2) \
+					?	1 \
+					:	( \
+						(t1 == NULL || t2 == NULL || t1->type != t2->type) \
+						?	0 \
+						:	( \
+							realTermLeaf(t1) \
+							?	0 \
+							:	( \
+								realTermEncrypt(t2) \
+								?	(isTermEqual1(t1->right.key, t2->right.key) && \
+									 isTermEqual1(t1->left.op,  t2->left.op)) \
+								:	(isTermEqual1(t1->left.op1, t2->left.op1) && \
+									 isTermEqual1(t1->right.op2, t2->right.op2)) \
+								) \
+							) \
+						 )  \
+					) \
+				)
+
+#define isTermEqual3(t1,t2)	((substVar(t1) || substVar(t2)) \
+				?	isTermEqual2(t1,t2) \
+				:	( \
+					(t1 == t2) \
+					?	1 \
+					:	( \
+						(t1 == NULL || t2 == NULL || t1->type != t2->type) \
+						?	0 \
+						:	( \
+							realTermLeaf(t1) \
+							?	0 \
+							:	( \
+								realTermEncrypt(t2) \
+								?	(isTermEqual2(t1->right.key, t2->right.key) && \
+									 isTermEqual2(t1->left.op,  t2->left.op)) \
+								:	(isTermEqual2(t1->left.op1, t2->left.op1) && \
+									 isTermEqual2(t1->right.op2, t2->right.op2)) \
+								) \
+							) \
+						 )  \
+					) \
+				)
+
+#define isTermEqual(t1,t2) isTermEqual2(t1,t2)
+#endif
+
 int hasTermVariable (Term term);
 int isTermEqualFn (Term term1, Term term2);
 int termOccurs (Term t, Term tsub);