diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt
index d2aa5c9..dc1c0c4 100644
--- a/src/prolog/ast/logic/Clause.kt
+++ b/src/prolog/ast/logic/Clause.kt
@@ -48,16 +48,17 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
                         onSuccess = { bodySubs ->
                             // If the body can be proven, yield the (combined) substitutions
                             val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
-                            yield(Result.success(goalResult + headResult))
+                            val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
+                            yield(Result.success(goalResult + headResult + bodyResult))
                         },
                         onFailure = { error ->
                             if (error is AppliedCut) {
                                 // Find single solution and return immediately
                                 if (error.subs != null) {
-                                    val goalResult = goalToHeadSubs.mapValues {
-                                        applySubstitution(it.value, error.subs)
-                                    }
-                                    yield(Result.failure(AppliedCut(goalResult + headResult)))
+                                    val bodySubs = error.subs
+                                    val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
+                                    val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
+                                    yield(Result.failure(AppliedCut(goalResult + headResult + bodyResult)))
                                 } else {
                                     yield(Result.failure(AppliedCut()))
                                 }
diff --git a/src/prolog/builtins/analysisOperators.kt b/src/prolog/builtins/analysisOperators.kt
index 2eb81a6..f905696 100644
--- a/src/prolog/builtins/analysisOperators.kt
+++ b/src/prolog/builtins/analysisOperators.kt
@@ -35,10 +35,11 @@ class FunctorOp(private val term: Term, private val functorName: Term, private v
                     "Arguments are not sufficiently instantiated"
                 }
 
+                val t = applySubstitution(term, subs)
                 val name = applySubstitution(functorName, subs) as Atom
                 val arity = applySubstitution(functorArity, subs) as Integer
                 val result = Structure(name, List(arity.value) { AnonymousVariable.create() })
-                sequenceOf(Result.success(mapOf(term to result)))
+                sequenceOf(Result.success(mapOf(t to result)))
             }
 
             else -> throw IllegalStateException()
diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt
index 41c8b6d..63908d1 100644
--- a/src/prolog/builtins/controlOperators.kt
+++ b/src/prolog/builtins/controlOperators.kt
@@ -2,14 +2,15 @@ package prolog.builtins
 
 import prolog.Answers
 import prolog.Substitutions
+import prolog.ast.Database.Program
 import prolog.ast.logic.LogicOperand
 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
 import prolog.logic.applySubstitution
+import prolog.logic.numbervars
 
 /**
  * Always fail.
@@ -53,8 +54,8 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
             left.fold(
                 // If it succeeds, satisfy the right part with the updated substitutions and return all results
                 onSuccess = { leftSubs ->
-                    right.satisfy(subs + leftSubs).forEach {
-                        it.fold(
+                    right.satisfy(subs + leftSubs).forEach { right ->
+                        right.fold(
                             // If the right part succeeds, yield the result with the left substitutions
                             onSuccess = { rightSubs ->
                                 yield(Result.success(leftSubs + rightSubs))
diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt
index 2fa6e23..8b9457a 100644
--- a/src/prolog/logic/unification.kt
+++ b/src/prolog/logic/unification.kt
@@ -12,10 +12,7 @@ import prolog.ast.lists.List.Cons
 import prolog.ast.lists.List.Empty
 import prolog.ast.logic.Fact
 import prolog.ast.logic.LogicOperator
-import prolog.ast.terms.Atom
-import prolog.ast.terms.Structure
-import prolog.ast.terms.Term
-import prolog.ast.terms.Variable
+import prolog.ast.terms.*
 
 // Apply substitutions to a term
 fun applySubstitution(term: Term, subs: Substitutions): Term = when {
@@ -62,7 +59,10 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
     val t2 = applySubstitution(term2, subs)
 
     when {
-        equivalent(t1, t2, subs) -> yield(Result.success(emptyMap()))
+        equivalent(t1, t2, subs) -> {
+            yield(Result.success(emptyMap()))
+        }
+
         variable(t1, subs) -> {
             val variable = t1 as Variable
             if (!occurs(variable, t2, subs)) {
@@ -85,19 +85,7 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
                 val args1 = structure1.arguments
                 val args2 = structure2.arguments
                 if (args1.size == args2.size) {
-                    // Keep track of the substitutions so far
-                    val results = args1.zip(args2).map { (arg1, arg2) ->
-                        unifyLazy(arg1, arg2, subs)
-                    }
-                    // Combine the results of all unifications
-                    val combinedResults = results.reduce { acc, result ->
-                        acc.flatMap { a ->
-                            result.map { b ->
-                                if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap()
-                            }
-                        }.map { Result.success(it) }
-                    }
-                    yieldAll(combinedResults)
+                    yieldAll(unifyArgs(args1, args2, subs))
                 }
             }
         }
@@ -131,6 +119,32 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
     }
 }
 
+private fun unifyArgs(
+    args1: kotlin.collections.List<Argument>,
+    args2: kotlin.collections.List<Argument>,
+    subs: Substitutions
+): Answers = sequence {
+    // Using the current subs, unify the first argument of each list
+    val arg1 = applySubstitution(args1[0], subs)
+    val arg2 = applySubstitution(args2[0], subs)
+    unifyLazy(arg1, arg2, subs).forEach { headResult ->
+        // Use the resulting substitutions to unify the rest of the arguments
+        headResult.map { headSubs ->
+            val rest1 = args1.drop(1).map { applySubstitution(it, headSubs) }
+            val rest2 = args2.drop(1).map { applySubstitution(it, headSubs) }
+            if (rest1.isEmpty() && rest2.isEmpty()) {
+                yield(Result.success(headSubs))
+            } else if (rest1.isNotEmpty() && rest2.isNotEmpty()) {
+                unifyArgs(rest1, rest2, subs).forEach { tailResult ->
+                    tailResult.map { tailSubs ->
+                        yield(Result.success(headSubs + tailSubs))
+                    }
+                }
+            }
+        }
+    }
+}
+
 fun unify(term1: Term, term2: Term): Answer {
     val substitutions = unifyLazy(term1, term2, emptyMap()).iterator()
     return if (substitutions.hasNext()) {
@@ -151,6 +165,7 @@ fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean {
                 equivalent(arg1, arg2, subs)
             }
         }
+
         term1 is Integer && term2 is Integer -> compare(term1, term2, subs) == 0
         term1 is Number && term2 is Number -> compare(term1, term2, subs) == 0
         term1 is Variable && term2 is Variable -> term1 == term2