diff --git a/src/prolog/ast/arithmetic/Float.kt b/src/prolog/ast/arithmetic/Float.kt
index da49530..80d0bde 100644
--- a/src/prolog/ast/arithmetic/Float.kt
+++ b/src/prolog/ast/arithmetic/Float.kt
@@ -1,6 +1,7 @@
 package prolog.ast.arithmetic
 
 import prolog.Substitutions
+import prolog.ast.terms.Term
 
 class Float(override val value: kotlin.Float): Number {
     // Floats are already evaluated
@@ -42,4 +43,7 @@ class Float(override val value: kotlin.Float): Number {
     override fun hashCode(): Int {
         return super.hashCode()
     }
+
+    override fun clone(): Float = Float(value)
+    override fun applySubstitution(subs: Substitutions): Float = this
 }
\ No newline at end of file
diff --git a/src/prolog/ast/arithmetic/Integer.kt b/src/prolog/ast/arithmetic/Integer.kt
index dbf9c39..d0a48cb 100644
--- a/src/prolog/ast/arithmetic/Integer.kt
+++ b/src/prolog/ast/arithmetic/Integer.kt
@@ -3,6 +3,7 @@ package prolog.ast.arithmetic
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.logic.LogicOperand
+import prolog.ast.terms.Term
 
 data class Integer(override val value: Int) : Number, LogicOperand() {
     // Integers are already evaluated
@@ -41,4 +42,7 @@ data class Integer(override val value: Int) : Number, LogicOperand() {
         is Integer -> Integer(value * other.value)
         else -> throw IllegalArgumentException("Cannot multiply $this and $other")
     }
+
+    override fun clone(): Integer = Integer(value)
+    override fun applySubstitution(subs: Substitutions): Integer = this
 }
diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt
index 2abfa77..ed8690f 100644
--- a/src/prolog/ast/logic/Clause.kt
+++ b/src/prolog/ast/logic/Clause.kt
@@ -27,27 +27,27 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
         // Only if the body can be proven, the substitutions should be returned.
         // Do this in a lazy way.
 
-        // Since we are only interested in substitutions in the goal (as opposed to the head of this clause),
-        //  we can use variable renaming and filter out the substitutions that are not in the goal.
-        val (end, renamed: Substitutions) = numbervars(head, Program.variableRenamingStart, subs)
+        val preHead = applySubstitution(head, subs)
+        val preGoal = applySubstitution(goal, subs)
 
-        val reverse = renamed.entries.associate { (a, b) -> b to a }
-        Program.variableRenamingStart = end
+        val (headEnd, headRenaming) = numbervars(preHead, Program.variableRenamingStart, subs)
+        val headReverse = headRenaming.entries.associate { (a, b) -> b to a }
+        Program.variableRenamingStart = headEnd
 
-        var newSubs: Substitutions = subs + renamed
-        unifyLazy(applySubstitution(goal, subs), head, newSubs).forEach { headAnswer ->
+        val renamedHead = applySubstitution(head, headRenaming)
+        unifyLazy(preGoal, renamedHead, subs).forEach { headAnswer ->
             headAnswer.map { headSubs ->
                 // If the body can be proven, yield the (combined) substitutions
-                newSubs = subs + renamed + headSubs
-                body.satisfy(newSubs).forEach { bodyAnswer ->
+                val preBody = applySubstitution(body, headRenaming + headSubs) as Body
+                preBody.satisfy(subs).forEach { bodyAnswer ->
                     bodyAnswer.fold(
                         onSuccess = { bodySubs ->
                             var result = (headSubs + bodySubs)
-                                .mapKeys { applySubstitution(it.key, reverse)}
-                                .mapValues { applySubstitution(it.value, reverse) }
+                                .mapKeys { applySubstitution(it.key, headReverse) }
+                                .mapValues { applySubstitution(it.value, headReverse) }
                             result = result.map { it.key to applySubstitution(it.value, result) }
                                 .toMap()
-                                .filterNot { it.key in renamed.keys && !occurs(it.key as Variable, goal, emptyMap())}
+                                .filterNot { it.key in headRenaming.keys && !occurs(it.key as Variable, goal, emptyMap())}
                             yield(Result.success(result))
                         },
                         onFailure = { error ->
diff --git a/src/prolog/ast/logic/Fact.kt b/src/prolog/ast/logic/Fact.kt
index a52990e..f0cae19 100644
--- a/src/prolog/ast/logic/Fact.kt
+++ b/src/prolog/ast/logic/Fact.kt
@@ -1,6 +1,12 @@
 package prolog.ast.logic
 
+import prolog.Substitutions
 import prolog.ast.terms.Head
+import prolog.ast.terms.Term
 import prolog.builtins.True
+import prolog.logic.applySubstitution
 
-class Fact(head: Head) : Clause(head, True)
\ No newline at end of file
+class Fact(head: Head) : Clause(head, True) {
+    override fun clone(): Fact = Fact(head)
+    override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head as Term, subs) as Head)
+}
\ No newline at end of file
diff --git a/src/prolog/ast/logic/Rule.kt b/src/prolog/ast/logic/Rule.kt
index 9eba36e..add106d 100644
--- a/src/prolog/ast/logic/Rule.kt
+++ b/src/prolog/ast/logic/Rule.kt
@@ -1,6 +1,15 @@
 package prolog.ast.logic
 
+import prolog.Substitutions
 import prolog.ast.terms.Body
 import prolog.ast.terms.Head
+import prolog.ast.terms.Term
+import prolog.logic.applySubstitution
 
-class Rule(head: Head, body: Body) : Clause(head, body)
\ No newline at end of file
+class Rule(head: Head, body: Body) : Clause(head, body) {
+    override fun clone(): Rule = Rule(head, body)
+    override fun applySubstitution(subs: Substitutions): Rule = Rule(
+        head = applySubstitution(head as Term, subs) as Head,
+        body = applySubstitution(body, subs) as Body
+    )
+}
diff --git a/src/prolog/ast/terms/AnonymousVariable.kt b/src/prolog/ast/terms/AnonymousVariable.kt
index 1bc0633..8211292 100644
--- a/src/prolog/ast/terms/AnonymousVariable.kt
+++ b/src/prolog/ast/terms/AnonymousVariable.kt
@@ -1,8 +1,9 @@
 package prolog.ast.terms
 
 import io.Logger
+import prolog.Substitutions
 
-class AnonymousVariable(id: Int) : Variable("_$id") {
+class AnonymousVariable(private val id: Int) : Variable("_$id") {
     companion object {
         private var counter = 0
         fun create(): AnonymousVariable {
@@ -14,4 +15,7 @@ class AnonymousVariable(id: Int) : Variable("_$id") {
     }
 
     override fun toString(): String = "_"
+
+    override fun clone(): AnonymousVariable = AnonymousVariable(id)
+    override fun applySubstitution(subs: Substitutions): AnonymousVariable = this
 }
\ No newline at end of file
diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt
index 3a6afad..dcd0a7d 100644
--- a/src/prolog/ast/terms/Atom.kt
+++ b/src/prolog/ast/terms/Atom.kt
@@ -21,4 +21,7 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
     override fun hashCode(): Int {
         return javaClass.hashCode()
     }
+
+    override fun clone(): Atom = Atom(name)
+    override fun applySubstitution(subs: Substitutions): Atom = Atom(name)
 }
\ No newline at end of file
diff --git a/src/prolog/ast/terms/Body.kt b/src/prolog/ast/terms/Body.kt
index dc61c7d..4918d1e 100644
--- a/src/prolog/ast/terms/Body.kt
+++ b/src/prolog/ast/terms/Body.kt
@@ -2,4 +2,4 @@ package prolog.ast.terms
 
 import prolog.ast.logic.Satisfiable
 
-interface Body : Satisfiable
\ No newline at end of file
+interface Body : Term, Satisfiable
\ No newline at end of file
diff --git a/src/prolog/ast/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt
index 385da2c..bcd5e71 100644
--- a/src/prolog/ast/terms/Structure.kt
+++ b/src/prolog/ast/terms/Structure.kt
@@ -3,6 +3,7 @@ package prolog.ast.terms
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.logic.Resolvent
+import prolog.logic.applySubstitution
 import prolog.logic.unifyLazy
 
 typealias Argument = Term
@@ -33,4 +34,10 @@ open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), He
     override fun hashCode(): Int {
         return javaClass.hashCode()
     }
+
+    override fun clone(): Structure = Structure(name, arguments)
+    override fun applySubstitution(subs: Substitutions): Structure = Structure(
+        name,
+        arguments.map { applySubstitution(it, subs) }
+    )
 }
diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt
index 0fdad49..8174310 100644
--- a/src/prolog/ast/terms/Term.kt
+++ b/src/prolog/ast/terms/Term.kt
@@ -1,14 +1,19 @@
 package prolog.ast.terms
 
+import prolog.Substitutions
 import prolog.logic.compare
+import prolog.ast.arithmetic.Integer
+import prolog.ast.arithmetic.Float
 
 /**
  * Value in Prolog.
  *
- * A [Term] is either a [Variable], [Atom], [Integer][prolog.ast.arithmetic.Integer],
- * [Float][prolog.ast.arithmetic.Float] or [CompoundTerm].
+ * A [Term] is either a [Variable], [Atom], [Integer],
+ * [Float] or [CompoundTerm].
  * In addition, SWI-Prolog also defines the type TODO string.
  */
-interface Term : Comparable<Term> {
+interface Term : Comparable<Term>, Cloneable {
     override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
+    fun applySubstitution(subs: Substitutions): Term
+    public override fun clone(): Term
 }
diff --git a/src/prolog/ast/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt
index 2d23170..8068864 100644
--- a/src/prolog/ast/terms/Variable.kt
+++ b/src/prolog/ast/terms/Variable.kt
@@ -39,4 +39,7 @@ open class Variable(val name: String) : Term, Body, Expression, LogicOperand() {
     }
 
     override fun toString(): String = name
+
+    override fun clone(): Variable = Variable(name)
+    override fun applySubstitution(subs: Substitutions): Variable = this
 }
\ No newline at end of file
diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt
index 613c915..b9eeef4 100644
--- a/src/prolog/builtins/controlOperators.kt
+++ b/src/prolog/builtins/controlOperators.kt
@@ -7,6 +7,7 @@ import prolog.ast.logic.LogicOperator
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Body
 import prolog.ast.terms.Goal
+import prolog.ast.terms.Structure
 import prolog.flags.AppliedCut
 
 /**
@@ -34,6 +35,8 @@ class Cut() : Atom("!") {
     override fun satisfy(subs: Substitutions): Answers {
         return sequenceOf(Result.failure(AppliedCut(emptyMap())))
     }
+
+    override fun applySubstitution(subs: Substitutions): Cut = Cut()
 }
 
 /**
@@ -94,6 +97,11 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
             )
         }
     }
+
+    override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction(
+        left.applySubstitution(subs) as LogicOperand,
+        right.applySubstitution(subs) as LogicOperand
+    )
 }
 
 /**
@@ -105,6 +113,12 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO
         yieldAll(left.satisfy(subs))
         yieldAll(right.satisfy(subs))
     }
+
+    override fun clone(): Disjunction = Disjunction(left.clone() as LogicOperand, right.clone() as LogicOperand)
+    override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction(
+        left.applySubstitution(subs) as LogicOperand,
+        right.applySubstitution(subs) as LogicOperand
+    )
 }
 
 @Deprecated("Use Disjunction instead")
diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt
index eaf67b8..54ebeb3 100644
--- a/src/prolog/builtins/databaseOperators.kt
+++ b/src/prolog/builtins/databaseOperators.kt
@@ -42,6 +42,9 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
     }
 
     override fun hashCode(): Int = super.hashCode()
+
+    override fun clone(): Dynamic = Dynamic(dynamicFunctor)
+    override fun applySubstitution(subs: Substitutions): Dynamic = Dynamic(dynamicFunctor)
 }
 
 class Assert(clause: Clause) : AssertZ(clause) {
diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt
index 1e7b57f..5b5d21e 100644
--- a/src/prolog/logic/unification.kt
+++ b/src/prolog/logic/unification.kt
@@ -15,9 +15,7 @@ import prolog.ast.terms.*
 
 // Apply substitutions to a term
 fun applySubstitution(term: Term, subs: Substitutions): Term = when {
-    term is Fact -> {
-        Fact(applySubstitution(term.head, subs) as Head)
-    }
+    term is Fact -> term.applySubstitution(subs)
 
     variable(term, emptyMap()) -> {
         val variable = term as Variable
@@ -25,8 +23,7 @@ fun applySubstitution(term: Term, subs: Substitutions): Term = when {
     }
     atomic(term, subs) -> term
     compound(term, subs) -> {
-        val structure = term as Structure
-        Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) })
+        term.applySubstitution(subs)
     }
 
     else -> term
diff --git a/tests/prolog/EvaluationTests.kt b/tests/prolog/EvaluationTests.kt
index ac3df3f..a1cbbfc 100644
--- a/tests/prolog/EvaluationTests.kt
+++ b/tests/prolog/EvaluationTests.kt
@@ -108,8 +108,8 @@ class EvaluationTests {
         val variable2 = Variable("Y")
 
         val parent = Rule(
-            Structure(Atom("parent"), listOf(variable1, variable2)),
-            /* :- */ Disjunction(
+            Structure(Atom("parent"), listOf(variable1, variable2)), /* :- */
+            Disjunction(
                 Structure(Atom("father"), listOf(variable1, variable2)),
                 /* ; */
                 Structure(Atom("mother"), listOf(variable1, variable2))
@@ -118,10 +118,14 @@ class EvaluationTests {
 
         Program.load(listOf(father, mother, parent))
 
-        val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy"))))
-        assertTrue(result1.toList().isNotEmpty())
-        val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy"))))
-        assertTrue(result2.toList().isNotEmpty())
+        val result1 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))).toList()
+        assertEquals(1, result1.size, "Expected 1 result")
+        assertTrue(result1[0].isSuccess, "Expected success")
+        assertTrue(result1[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
+        val result2 = Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))).toList()
+        assertEquals(1, result2.size, "Expected 1 result")
+        assertTrue(result2[0].isSuccess, "Expected success")
+        assertTrue(result2[0].getOrNull()!!.isEmpty(), "Expected no substitutions")
 
         val result3 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jane"))))
         assertFalse(result3.any())