diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt
index 226af60..97edd8f 100644
--- a/src/interpreter/Preprocessor.kt
+++ b/src/interpreter/Preprocessor.kt
@@ -65,7 +65,6 @@ open class Preprocessor {
                     Functor.of("clause/2") -> ClauseOp(args[0] as Head, args[1] as Body)
                     Functor.of("atomic/1") -> AtomicOp(args[0])
                     Functor.of("compound/1") -> CompoundOp(args[0])
-                    Functor.of("=../2") -> Univ(args[0], args[1])
 
                     // Arithmetic
                     Functor.of("inf/0") -> Integer(Int.MAX_VALUE)
diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt
index 8db42e9..0473200 100644
--- a/src/parser/grammars/TermsGrammar.kt
+++ b/src/parser/grammars/TermsGrammar.kt
@@ -5,11 +5,8 @@ import com.github.h0tk3y.betterParse.grammar.parser
 import com.github.h0tk3y.betterParse.parser.Parser
 import prolog.ast.arithmetic.Float
 import prolog.ast.arithmetic.Integer
-import prolog.ast.lists.List
 import prolog.ast.terms.*
 import prolog.builtins.Dynamic
-import prolog.ast.lists.List.Empty
-import prolog.ast.lists.List.Cons
 
 /**
  * Precedence is based on the following table:
@@ -68,7 +65,6 @@ open class TermsGrammar : Tokens() {
     // Base terms (atoms, compounds, variables, numbers)
     protected val baseTerm: Parser<Term> by (dummy
             or (-leftParenthesis * parser(::term) * -rightParenthesis)
-            or parser(::list)
             or compound
             or atom
             or variable
@@ -91,7 +87,7 @@ open class TermsGrammar : Tokens() {
         t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
     }
 
-    protected val op700: Parser<String> by (univOp or equivalent or notEquivalent or equals or notEquals or isOp) use { text }
+    protected val op700: Parser<String> by (equivalent or notEquivalent or equals or notEquals or isOp) use { text }
     protected val term700: Parser<Term> by (term500 * optional(op700 * term500)) use {
         if (t2 == null) t1 else CompoundTerm(Atom(t2!!.t1), listOf(t1, t2!!.t2))
     }
@@ -116,20 +112,6 @@ open class TermsGrammar : Tokens() {
         t2.fold(t1) { acc, (op, term) -> CompoundTerm(Atom(op), listOf(acc, term)) }
     }
 
-    // Lists
-    protected val list: Parser<List> by (-leftBracket * separated(
-        parser(::termNoConjunction),
-        comma,
-        acceptZero = true
-    ) * -rightBracket) use {
-        var list: List = Empty
-        // Construct the list in reverse order
-        for (term in this.terms.reversed()) {
-            list = Cons(term, list)
-        }
-        list
-    }
-
     // Term - highest level expression
     protected val term: Parser<Term> by term1200
     protected val termNoConjunction: Parser<Term> by term700
diff --git a/src/parser/grammars/Tokens.kt b/src/parser/grammars/Tokens.kt
index b998fee..018417f 100644
--- a/src/parser/grammars/Tokens.kt
+++ b/src/parser/grammars/Tokens.kt
@@ -10,8 +10,6 @@ import com.github.h0tk3y.betterParse.lexer.token
 abstract class Tokens : Grammar<Any>() {
     protected val leftParenthesis: Token by literalToken("(")
     protected val rightParenthesis: Token by literalToken(")")
-    protected val leftBracket: Token by literalToken("[")
-    protected val rightBracket: Token by literalToken("]")
     protected val exclamation: Token by literalToken("!")
     // 1200
     protected val neck by literalToken(":-")
@@ -22,7 +20,6 @@ abstract class Tokens : Grammar<Any>() {
     // 1000
     protected val comma: Token by literalToken(",")
     // 700
-    protected val univOp: Token by literalToken("=..")
     protected val notEquivalent: Token by literalToken("\\==")
     protected val equivalent: Token by literalToken("==")
     protected val equals: Token by literalToken("=")
diff --git a/src/prolog/ast/lists/List.kt b/src/prolog/ast/lists/List.kt
deleted file mode 100644
index 494aa08..0000000
--- a/src/prolog/ast/lists/List.kt
+++ /dev/null
@@ -1,57 +0,0 @@
-package prolog.ast.lists
-
-import prolog.Substitutions
-import prolog.ast.terms.Term
-import prolog.ast.arithmetic.Integer
-
-sealed class List : Term {
-    abstract val head: Term
-    open val tail: List? = null
-    val size: Integer
-        get() = when (this) {
-            is Empty -> Integer(0)
-            is Cons -> Integer(1 + tail.size.value)
-        }
-
-    fun isEmpty(): Boolean = this is Empty
-
-    /**
-     * The empty list []
-     */
-    object Empty : List() {
-        override val head = this
-        override fun applySubstitution(subs: Substitutions): Empty = this
-        override fun toString(): String = "[]"
-    }
-
-    class Cons(override val head: Term, override var tail: List) : List() {
-        override fun applySubstitution(subs: Substitutions): List {
-            val newHead = head.applySubstitution(subs)
-            val newTail = tail.applySubstitution(subs) as List
-            return Cons(newHead, newTail)
-        }
-
-        override fun toString(): String {
-            val values = mutableListOf<Term>()
-            var current: List? = this
-            while (current != null && current !is Empty) {
-                values.add(current.head)
-                current = current.tail
-            }
-            return "[${values.joinToString(", ")}]"
-        }
-    }
-
-    override fun equals(other: Any?): Boolean {
-        if (this === other) return true
-        if (other == null) return false
-        if (other !is List) return false
-        if (this is Empty && other is Empty) return true
-        if (this is Cons && other is Cons) {
-            return this.head == other.head && this.tail == other.tail
-        }
-        return false
-    }
-
-    override fun hashCode(): Int = super.hashCode()
-}
diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt
index dc1c0c4..a2af1f3 100644
--- a/src/prolog/ast/logic/Clause.kt
+++ b/src/prolog/ast/logic/Clause.kt
@@ -39,26 +39,28 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
                 // Filter the substitutions to only include those that map from head to goal
                 val headToGoalSubs = headAndGoalSubs.filterKeys { it in headRenaming.values }
                 val goalToHeadSubs = headAndGoalSubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
-                val headResult = headToGoalSubs.filterKeys { key ->
-                    goalToHeadSubs.any { occurs(key as Variable, it.value) }
-                }
                 val newSubs = headRenaming + headToGoalSubs
                 body.satisfy(newSubs).forEach { bodyAnswer ->
                     bodyAnswer.fold(
                         onSuccess = { bodySubs ->
                             // If the body can be proven, yield the (combined) substitutions
-                            val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
-                            val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
-                            yield(Result.success(goalResult + headResult + bodyResult))
+                            val goalToHeadResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
+                            val headResult = headToGoalSubs.filterKeys { key ->
+                                goalToHeadSubs.any {
+                                    occurs(
+                                        key as Variable,
+                                        it.value
+                                    )
+                                }
+                            }
+                            yield(Result.success(goalToHeadResult + headResult))
                         },
                         onFailure = { error ->
                             if (error is AppliedCut) {
                                 // Find single solution and return immediately
                                 if (error.subs != null) {
-                                    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)))
+                                    var result = goalToHeadSubs.mapValues { applySubstitution(it.value, error.subs) }
+                                    yield(Result.failure(AppliedCut(result)))
                                 } else {
                                     yield(Result.failure(AppliedCut()))
                                 }
diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt
index 42c12c5..fccf9fc 100644
--- a/src/prolog/ast/terms/Atom.kt
+++ b/src/prolog/ast/terms/Atom.kt
@@ -11,7 +11,7 @@ open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
 
     override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)
 
-    override fun applySubstitution(subs: Substitutions): Atom = this
+    override fun applySubstitution(subs: Substitutions): Atom = Atom(name)
 
     override fun toString(): String {
         return name
diff --git a/src/prolog/builtins/analysisOperators.kt b/src/prolog/builtins/analysisOperators.kt
index f905696..4aff69e 100644
--- a/src/prolog/builtins/analysisOperators.kt
+++ b/src/prolog/builtins/analysisOperators.kt
@@ -7,9 +7,6 @@ import prolog.ast.arithmetic.Integer
 import prolog.ast.terms.*
 import prolog.ast.logic.Clause
 import prolog.logic.*
-import prolog.ast.lists.List
-import prolog.ast.lists.List.Empty
-import prolog.ast.lists.List.Cons
 
 /**
  * [True] when [Term] is a term with [Functor] Name/Arity.
@@ -35,11 +32,10 @@ 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(t to result)))
+                sequenceOf(Result.success(mapOf(term to result)))
             }
 
             else -> throw IllegalStateException()
@@ -70,13 +66,15 @@ class Arg(private val arg: Term, private val term: Term, private val value: Term
                 // Value will be unified with the successive arguments of term.
                 // On successful unification, arg is unified with the argument number.
                 // Backtracking yields alternative solutions.
-                for ((count, argument) in t.arguments.withIndex()) {
+                var count = 0
+                for (argument in t.arguments) {
                     unifyLazy(value, argument, subs).forEach { result ->
                         result.map {
                             val sub = arg to Integer(count + 1)
                             yield(Result.success(it + sub))
                         }
                     }
+                    count++
                 }
 
             }
@@ -96,12 +94,6 @@ class Arg(private val arg: Term, private val term: Term, private val value: Term
             }
         }
     }
-
-    override fun applySubstitution(subs: Substitutions): Arg = Arg(
-        arg.applySubstitution(subs),
-        term.applySubstitution(subs),
-        value.applySubstitution(subs)
-    )
 }
 
 /**
@@ -126,14 +118,11 @@ class ClauseOp(private val head: Head, private val body: Body) :
                 val clauseHead = clause.head
                 val clauseBody = clause.body
 
-                val appliedHead = applySubstitution(head, subs)
-                val appliedBody = applySubstitution(body, subs)
-
                 // Unify the head of the clause with the head of the goal
-                unifyLazy(clauseHead, appliedHead, subs).forEach { result ->
+                unifyLazy(clauseHead, head, subs).forEach { result ->
                     result.map { headSubs ->
                         // Unify the body of the clause with the body of the goal
-                        unifyLazy(clauseBody, appliedBody, headSubs).forEach { bodyResult ->
+                        unifyLazy(clauseBody, body, headSubs).forEach { bodyResult ->
                             bodyResult.map { bodySubs ->
                                 // Combine the substitutions from the head and body
                                 val combinedSubs = headSubs + bodySubs
@@ -147,11 +136,6 @@ class ClauseOp(private val head: Head, private val body: Body) :
             yield(Result.success(emptyMap()))
         }
     }
-
-    override fun applySubstitution(subs: Substitutions): ClauseOp = ClauseOp(
-        head.applySubstitution(subs) as Head,
-        body.applySubstitution(subs) as Body
-    )
 }
 
 class AtomicOp(private val term: Term) : Operator(Atom("atomic"), null, term) {
@@ -162,8 +146,6 @@ class AtomicOp(private val term: Term) : Operator(Atom("atomic"), null, term) {
             emptySequence()
         }
     }
-
-    override fun applySubstitution(subs: Substitutions): AtomicOp = AtomicOp(term.applySubstitution(subs))
 }
 
 class CompoundOp(private val term: Term) : Operator(Atom("compound"), null, term) {
@@ -174,75 +156,4 @@ class CompoundOp(private val term: Term) : Operator(Atom("compound"), null, term
             emptySequence()
         }
     }
-
-    override fun applySubstitution(subs: Substitutions): CompoundOp = CompoundOp(term.applySubstitution(subs))
-}
-
-open class Univ(private val term: Term, private val list: Term) : Operator(Atom("=.."), term, list) {
-    override fun satisfy(subs: Substitutions): Answers {
-        return when {
-            nonvariable(term, subs) && nonvariable(list, subs) -> {
-                val t = applySubstitution(term, subs)
-                val l = applySubstitution(list, subs) as List
-                unifyLazy(t, listToTerm(l), subs)
-            }
-
-            variable(term, subs) && nonvariable(list, subs) -> {
-                val l = applySubstitution(list, subs) as List
-                val t = listToTerm(l)
-                unifyLazy(term, t, subs)
-            }
-
-            nonvariable(term, subs) && variable(list, subs) -> {
-                val t = applySubstitution(term, subs)
-                val l = termToList(t)
-                unifyLazy(l, list, subs)
-            }
-
-            else -> throw Exception("Arguments are not sufficiently instantiated")
-        }
-    }
-
-    protected open fun listToTerm(list: List): Term {
-        return when {
-            list.size.value == 1 -> list.head
-
-            list.size.value > 1 -> {
-                val head = list.head
-                val arguments = mutableListOf<Term>()
-                var tail: List? = list.tail
-                while (tail != null && tail !is Empty) {
-                    arguments.add(tail.head)
-                    tail = tail.tail
-                }
-                Structure(head as Atom, arguments)
-            }
-
-            else -> throw IllegalStateException("List is empty")
-        }
-    }
-
-    protected open fun termToList(term: Term): List {
-        return when (term) {
-            is Atom -> Cons(term, Empty)
-
-            is Structure -> {
-                val head = term.functor.name
-                val arguments = term.arguments
-                // Construct the list by iterating over the arguments in reverse
-                var tail: List = Empty
-                for (i in arguments.size - 1 downTo 0) {
-                    tail = Cons(arguments[i], tail)
-                }
-                return Cons(head, tail)
-            }
-
-            else -> throw IllegalStateException("Term is not a valid structure")
-        }
-    }
-
-    override fun applySubstitution(subs: Substitutions): Univ = Univ(
-        term.applySubstitution(subs),
-        list.applySubstitution(subs)
-    )
 }
diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt
index 63908d1..41c8b6d 100644
--- a/src/prolog/builtins/controlOperators.kt
+++ b/src/prolog/builtins/controlOperators.kt
@@ -2,15 +2,14 @@ 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.
@@ -54,8 +53,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 { right ->
-                        right.fold(
+                    right.satisfy(subs + leftSubs).forEach {
+                        it.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/builtins/listOperators.kt b/src/prolog/builtins/listOperators.kt
deleted file mode 100644
index 4adbced..0000000
--- a/src/prolog/builtins/listOperators.kt
+++ /dev/null
@@ -1,27 +0,0 @@
-package prolog.builtins
-
-import prolog.Answers
-import prolog.Substitutions
-import prolog.ast.lists.List
-import prolog.ast.lists.List.Cons
-import prolog.ast.lists.List.Empty
-import prolog.ast.terms.Atom
-import prolog.ast.terms.Operator
-import prolog.ast.terms.Term
-
-class Member(private val element: Term, private val list: List) : Operator(Atom("member"), element, list) {
-    private var solution: Operator = if (list is Empty) {
-        Unify(element, list)
-    } else if (list is Cons) {
-        Disjunction(
-            Unify(element, list.head),
-            Member(element, list.tail)
-        )
-    } else {
-        throw IllegalArgumentException("Invalid list type: ${list::class.simpleName}")
-    }
-
-    override fun satisfy(subs: Substitutions): Answers = solution.satisfy(subs)
-
-    override fun toString(): String = "$element ∈ $list"
-}
diff --git a/src/prolog/builtins/unificationOperators.kt b/src/prolog/builtins/unificationOperators.kt
index 5ebeed3..ad55acf 100644
--- a/src/prolog/builtins/unificationOperators.kt
+++ b/src/prolog/builtins/unificationOperators.kt
@@ -22,7 +22,7 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
         val t1 = applySubstitution(term1, subs)
         val t2 = applySubstitution(term2, subs)
 
-        yieldAll(unifyLazy(t1, t2, emptyMap()))
+        yieldAll(unifyLazy(t1, t2, subs))
     }
 
     override fun applySubstitution(subs: Substitutions): Unify = Unify(
@@ -45,7 +45,7 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
         val t1 = applySubstitution(term1, subs)
         val t2 = applySubstitution(term2, subs)
 
-        if (equivalent(t1, t2, emptyMap())) {
+        if (equivalent(t1, t2, subs)) {
             yield(Result.success(emptyMap()))
         }
     }
diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt
index 8b9457a..50560e0 100644
--- a/src/prolog/logic/unification.kt
+++ b/src/prolog/logic/unification.kt
@@ -7,11 +7,10 @@ import prolog.ast.arithmetic.Expression
 import prolog.ast.arithmetic.Float
 import prolog.ast.arithmetic.Integer
 import prolog.ast.arithmetic.Number
-import prolog.ast.lists.List
-import prolog.ast.lists.List.Cons
-import prolog.ast.lists.List.Empty
+import prolog.ast.logic.Clause
 import prolog.ast.logic.Fact
 import prolog.ast.logic.LogicOperator
+import prolog.ast.logic.Rule
 import prolog.ast.terms.*
 
 // Apply substitutions to a term
@@ -59,10 +58,7 @@ 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,32 +81,18 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
                 val args1 = structure1.arguments
                 val args2 = structure2.arguments
                 if (args1.size == args2.size) {
-                    yieldAll(unifyArgs(args1, args2, subs))
-                }
-            }
-        }
-
-        t1 is List && t2 is List -> {
-            if (equivalent(t1, t2, subs)) {
-                yield(Result.success(emptyMap()))
-            } else if (t1.size == t2.size) {
-                val head1 = t1.head
-                val head2 = t2.head
-
-                unifyLazy(head1, head2, subs).forEach { headSubs ->
-                    headSubs.map { headResult ->
-                        if (t1 is Empty && t2 is Empty) {
-                            yield(Result.success(headResult))
-                        } else if (t1 is Cons && t2 is Cons) {
-                            val tail1 = t1.tail
-                            val tail2 = t2.tail
-                            unifyLazy(tail1, tail2, headResult).forEach { tailSubs ->
-                                tailSubs.map { tailResult ->
-                                    yield(Result.success(headResult + tailResult))
-                                }
-                            }
-                        }
+                    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)
                 }
             }
         }
@@ -119,32 +101,6 @@ 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()) {
@@ -160,32 +116,12 @@ fun unify(term1: Term, term2: Term): Answer {
 fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean {
     return when {
         term1 is Atom && term2 is Atom -> compare(term1, term2, subs) == 0
-        term1 is Structure && term2 is Structure -> {
-            term1.functor == term2.functor && term1.arguments.zip(term2.arguments).all { (arg1, arg2) ->
-                equivalent(arg1, arg2, subs)
-            }
-        }
-
+        term1 is Structure && term2 is Structure -> compare(term1, term2, subs) == 0
         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
         term1 is Variable -> term1 in subs && equivalent(subs[term1]!!, term2, subs)
         term2 is Variable -> term2 in subs && equivalent(subs[term2]!!, term1, subs)
-        term1 is List && term2 is List -> {
-            if (term1.isEmpty() && term2.isEmpty()) {
-                true
-            } else if (term1.isEmpty() || term2.isEmpty()) {
-                false
-            } else {
-                require(term1 is Cons && term2 is Cons)
-                val head1 = term1.head
-                val tail1 = term1.tail
-                val head2 = term2.head
-                val tail2 = term2.tail
-                equivalent(head1, head2, subs) && equivalent(tail1, tail2, subs)
-            }
-        }
-
         else -> false
     }
 }
diff --git a/tests/parser/grammars/TermsGrammarTests.kt b/tests/parser/grammars/TermsGrammarTests.kt
index b39a0d8..d3b45e2 100644
--- a/tests/parser/grammars/TermsGrammarTests.kt
+++ b/tests/parser/grammars/TermsGrammarTests.kt
@@ -19,8 +19,6 @@ import prolog.ast.terms.Term
 import prolog.ast.terms.Variable
 import prolog.builtins.Is
 import prolog.logic.equivalent
-import prolog.ast.lists.List.Empty
-import prolog.ast.lists.List.Cons
 
 class TermsGrammarTests {
     private lateinit var parser: Grammar<Term>
@@ -354,49 +352,4 @@ class TermsGrammarTests {
             )
         }
     }
-
-    @Nested
-    class Lists {
-        private lateinit var parser: Grammar<Term>
-
-        @BeforeEach
-        fun setup() {
-            parser = TermsGrammar() as Grammar<Term>
-        }
-
-        @Test
-        fun `parse empty list`() {
-            val input = "[]"
-
-            val result = parser.parseToEnd(input)
-
-            assertEquals(Empty, result, "Expected empty list")
-        }
-
-        @Test
-        fun `parse non-empty list`() {
-            val input = "[a, b, c]"
-
-            val result = parser.parseToEnd(input)
-
-            assertEquals(
-                Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Empty))),
-                result,
-                "Expected non-empty list"
-            )
-        }
-
-        @Test
-        fun `parse nested lists`() {
-            val input = "[a, [b, c], d]"
-
-            val result = parser.parseToEnd(input)
-
-            assertEquals(
-                Cons(Atom("a"), Cons(Cons(Atom("b"), Cons(Atom("c"), Empty)), Cons(Atom("d"), Empty))),
-                result,
-                "Expected nested lists"
-            )
-        }
-    }
 }
\ No newline at end of file
diff --git a/tests/prolog/EvaluationTests.kt b/tests/prolog/EvaluationTests.kt
index 8392eae..1a62390 100644
--- a/tests/prolog/EvaluationTests.kt
+++ b/tests/prolog/EvaluationTests.kt
@@ -15,10 +15,7 @@ import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
 import prolog.ast.Database.Program
 import prolog.ast.arithmetic.Integer
-import prolog.ast.lists.List.Empty
-import prolog.ast.lists.List.Cons
 import prolog.ast.terms.AnonymousVariable
-import prolog.builtins.Unify
 
 class EvaluationTests {
     @BeforeEach
@@ -482,20 +479,4 @@ class EvaluationTests {
         assertEquals(1, subs3c.size, "Expected 1 substitution")
         assertEquals(Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))), subs3c[Variable("X")], "Expected X to be s(s(0))")
     }
-
-    @Test
-    fun `foo(emptyList) = foo(X)`() {
-        val list = Empty
-        val left = Structure(Atom("foo"), listOf(list))
-        val right = Structure(Atom("foo"), listOf(Variable("X")))
-
-        val unific = Unify(left, right)
-        val result = unific.satisfy(emptyMap()).toList()
-
-        assertEquals(1, result.size, "Expected 1 result")
-        assertTrue(result[0].isSuccess, "Expected success")
-        val subs = result[0].getOrNull()!!
-        assertEquals(1, subs.size, "Expected 1 substitution")
-        assertEquals(list, subs[Variable("X")], "Expected X to be list(1, 2)")
-    }
 }
diff --git a/tests/prolog/builtins/AnalysisOperatorsTests.kt b/tests/prolog/builtins/AnalysisOperatorsTests.kt
index a6866c3..dbd3b03 100644
--- a/tests/prolog/builtins/AnalysisOperatorsTests.kt
+++ b/tests/prolog/builtins/AnalysisOperatorsTests.kt
@@ -7,13 +7,13 @@ import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.assertThrows
 import prolog.ast.Database.Program
 import prolog.ast.arithmetic.Integer
-import prolog.ast.lists.List
-import prolog.ast.lists.List.Cons
-import prolog.ast.lists.List.Empty
 import prolog.ast.logic.Fact
 import prolog.ast.logic.Rule
-import prolog.ast.terms.*
-import prolog.logic.equivalent
+import prolog.ast.terms.CompoundTerm
+import prolog.ast.terms.AnonymousVariable
+import prolog.ast.terms.Atom
+import prolog.ast.terms.Structure
+import prolog.ast.terms.Variable
 
 class AnalysisOperatorsTests {
     @Test
@@ -401,246 +401,4 @@ class AnalysisOperatorsTests {
             )
         }
     }
-
-    @Nested
-    class `Univ operator` {
-        @Test
-        fun `univ without variables`() {
-            val univ = Univ(Atom("foo"), Cons(Atom("foo"), Empty))
-
-            val result = univ.satisfy(emptyMap()).toList()
-
-            assertEquals(1, result.size, "Expected 1 result")
-            assertTrue(result[0].isSuccess, "Expected success")
-            val subs = result[0].getOrNull()!!
-            assertTrue(subs.isEmpty(), "Expected empty substitutions")
-        }
-
-        @Test
-        fun `univ with variable list`() {
-            val list = Variable("List")
-            val univ = Univ(
-                CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))),
-                list
-            )
-            val expected = Cons(Atom("foo"), Cons(Atom("a"), Cons(Atom("b"), Empty)))
-
-            val result = univ.satisfy(emptyMap()).toList()
-
-            assertEquals(1, result.size, "Expected 1 result")
-            assertTrue(result[0].isSuccess, "Expected success")
-            val subs = result[0].getOrNull()!!
-            assertEquals(1, subs.size, "Expected 1 substitution")
-            assertEquals(expected, subs[list], "Expected List to be $expected")
-        }
-
-        @Test
-        fun `univ with variable in compound`() {
-            val list = Variable("List")
-            val univ = Univ(
-                CompoundTerm(Atom("foo"), listOf(Variable("X"))),
-                list
-            )
-            val expected = Cons(Atom("foo"), Cons(Variable("X"), Empty))
-
-            val result = univ.satisfy(emptyMap()).toList()
-
-            assertEquals(1, result.size, "Expected 1 result")
-            assertTrue(result[0].isSuccess, "Expected success")
-            val subs = result[0].getOrNull()!!
-            assertEquals(1, subs.size, "Expected 1 substitution")
-            assertEquals(expected, subs[list], "Expected List to be $expected")
-        }
-
-        @Test
-        fun `univ with var foo`() {
-            val univ = Univ(
-                Variable("Term"),
-                Cons(Atom("foo"), Empty)
-            )
-
-            val result = univ.satisfy(emptyMap()).toList()
-
-            assertEquals(1, result.size, "Expected 1 result")
-            assertTrue(result[0].isSuccess, "Expected success")
-            val subs = result[0].getOrNull()!!
-            assertEquals(1, subs.size, "Expected 1 substitution")
-            assertEquals(Atom("foo"), subs[Variable("Term")], "Expected Term to be foo")
-        }
-
-        @Test
-        fun `univ with var foo(a)`() {
-            val univ = Univ(
-                Variable("Term"),
-                Cons(Atom("foo"), Cons(Atom("a"), Empty))
-            )
-
-            val result = univ.satisfy(emptyMap()).toList()
-
-            assertEquals(1, result.size, "Expected 1 result")
-            assertTrue(result[0].isSuccess, "Expected success")
-            val subs = result[0].getOrNull()!!
-            assertEquals(1, subs.size, "Expected 1 substitution")
-            assertEquals(
-                Structure(Atom("foo"), listOf(Atom("a"))),
-                subs[Variable("Term")],
-                "Expected Term to be foo(a)"
-            )
-        }
-
-        @Test
-        fun `univ with var foo(X)`() {
-            val univ = Univ(
-                Variable("Term"),
-                Cons(Atom("foo"), Cons(Variable("X"), Empty))
-            )
-
-            val result = univ.satisfy(emptyMap()).toList()
-
-            assertEquals(1, result.size, "Expected 1 result")
-            assertTrue(result[0].isSuccess, "Expected success")
-            val subs = result[0].getOrNull()!!
-            assertEquals(1, subs.size, "Expected 1 substitution")
-            assertEquals(
-                Structure(Atom("foo"), listOf(Variable("X"))),
-                subs[Variable("Term")],
-                "Expected Term to be foo(X)"
-            )
-        }
-
-        @Test
-        fun `univ with var foo(a, b(X), c)`() {
-            val univ = Univ(
-                Variable("Term"),
-                Cons(
-                    Atom("foo"),
-                    Cons(Atom("a"), Cons(CompoundTerm(Atom("b"), listOf(Variable("X"))), Cons(Atom("c"), Empty)))
-                )
-            )
-            val expected = CompoundTerm(
-                Atom("foo"),
-                listOf(Atom("a"), CompoundTerm(Atom("b"), listOf(Variable("X"))), Atom("c"))
-            )
-
-            val result = univ.satisfy(emptyMap()).toList()
-
-            assertEquals(1, result.size, "Expected 1 result")
-            assertTrue(result[0].isSuccess, "Expected success")
-            val subs = result[0].getOrNull()!!
-            assertEquals(1, subs.size, "Expected 1 substitution")
-            assertEquals(expected, subs[Variable("Term")], "Expected Term to be $expected")
-        }
-
-        @Test
-        fun `univ with unified var should return substitution`() {
-            val univ = Univ(
-                CompoundTerm(
-                    Atom("foo"), listOf(
-                        Atom("a"),
-                        CompoundTerm(Atom("bar"), listOf(Variable("X"))),
-                        Atom("c")
-                    )
-                ),
-                Cons(
-                    Atom("foo"),
-                    Cons(Atom("a"), Cons(CompoundTerm(Atom("bar"), listOf(Atom("b"))), Cons(Atom("c"), Empty)))
-                )
-            )
-
-            val result = univ.satisfy(emptyMap()).toList()
-
-            assertEquals(1, result.size, "Expected 1 result")
-            assertTrue(result[0].isSuccess, "Expected success")
-            val subs = result[0].getOrNull()!!
-            assertEquals(1, subs.size, "Expected 1 substitution")
-            assertEquals(Atom("b"), subs[Variable("X")], "Expected X to be b")
-        }
-
-        @Test
-        fun `univ of incompatible structures should fail`() {
-            val univ = Univ(
-                CompoundTerm(Atom("foo"), listOf(Atom("a"))),
-                Cons(Atom("bar"), Empty)
-            )
-
-            val result = univ.satisfy(emptyMap()).toList()
-
-            assertEquals(0, result.size, "Expected 0 results")
-        }
-
-        @Test
-        fun `univ with two vars should throw`() {
-            val univ = Univ(Variable("X"), Variable("Y"))
-
-            val exception = assertThrows<Exception> {
-                univ.satisfy(emptyMap()).toList()
-            }
-            assertEquals("Arguments are not sufficiently instantiated", exception.message)
-        }
-
-        class OpenUniv(term: Term, list: Term) : Univ(term, list) {
-            public override fun listToTerm(list: List): Term = super.listToTerm(list)
-            public override fun termToList(term: Term): List = super.termToList(term)
-        }
-
-        @Test
-        fun `a to term`() {
-            val univ = OpenUniv(Atom(""), Empty)
-
-            val originalList = Cons(Atom("a"), Empty)
-            val originalTerm = Atom("a")
-
-            val term = univ.listToTerm(originalList)
-            assertEquals(originalTerm, term, "Expected term to be a")
-
-            val list = univ.termToList(term)
-            assertEquals(originalList, list, "Expected list to be [a]")
-        }
-
-        @Test
-        fun `foo, bar to compound`() {
-            val univ = OpenUniv(Atom(""), Empty)
-
-            val originalList = Cons(Atom("foo"), Cons(Atom("bar"), Empty))
-            val originalTerm = CompoundTerm(Atom("foo"), listOf(Atom("bar")))
-
-            val term = univ.listToTerm(originalList)
-            assertEquals(originalTerm, term)
-
-            val list = univ.termToList(term)
-            assertEquals(originalList, list)
-        }
-
-        @Test
-        fun `foo, bar, baz to compound`() {
-            val univ = OpenUniv(Atom(""), Empty)
-
-            val originalList = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Atom("baz"), Empty)))
-            val originalTerm = CompoundTerm(Atom("foo"), listOf(Atom("bar"), Atom("baz")))
-
-            val term = univ.listToTerm(originalList)
-            assertEquals(originalTerm, term)
-
-            val list = univ.termToList(term)
-            assertEquals(originalList, list)
-        }
-
-        @Test
-        fun `foo, bar, (baz, bar) to compound with list`() {
-            val univ = OpenUniv(Atom(""), Empty)
-
-            val originalList =
-                Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
-            val originalTerm = CompoundTerm(
-                Atom("foo"),
-                listOf(Atom("bar"), Cons(Atom("baz"), Cons(Atom("bar"), Empty)))
-            )
-
-            val term = univ.listToTerm(originalList)
-            assertTrue(equivalent(originalTerm, term, emptyMap()), "Expected term to be foo(bar, [baz, bar]))")
-
-            val list = univ.termToList(term)
-            assertTrue(equivalent(originalList, list, emptyMap()), "Expected list to be [foo, bar, [baz, bar]]")
-        }
-    }
 }
diff --git a/tests/prolog/builtins/ListOperatorsTests.kt b/tests/prolog/builtins/ListOperatorsTests.kt
deleted file mode 100644
index d0c44c2..0000000
--- a/tests/prolog/builtins/ListOperatorsTests.kt
+++ /dev/null
@@ -1,73 +0,0 @@
-package prolog.builtins
-
-import org.junit.jupiter.api.Assertions.assertEquals
-import org.junit.jupiter.api.Assertions.assertTrue
-import org.junit.jupiter.api.Disabled
-import org.junit.jupiter.api.Test
-import prolog.ast.lists.List.Cons
-import prolog.ast.lists.List.Empty
-import prolog.ast.terms.Atom
-import prolog.ast.terms.Variable
-
-class ListOperatorsTests {
-    @Test
-    fun `size empty list is 0`() {
-        assertEquals(0, Empty.size.value, "Expected size of empty list to be 0")
-    }
-
-    @Test
-    fun `size of singleton is 1`() {
-        val list = Cons(Atom("a"), Empty)
-
-        assertEquals(1, list.size.value, "Expected size of singleton list to be 1")
-    }
-
-    @Test
-    fun `size of list with five elements is 5`() {
-        val list = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Cons(Atom("e"), Empty)))))
-
-        assertEquals(5, list.size.value, "Expected size of list with five elements to be 5")
-    }
-
-    @Test
-    fun `member(a, list of a)`() {
-        val atom = Atom("a")
-        val list = Cons(atom, Empty)
-
-        val member = Member(atom, list)
-
-        val result = member.satisfy(emptyMap()).toList()
-
-        assertEquals(1, result.size, "Expected one solution")
-        assertTrue(result[0].isSuccess, "Expected success")
-        assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map")
-    }
-
-    @Test
-    fun `member should only check shallow`() {
-        val list = Cons(Atom("a"), Cons(Cons(Atom("b"), Empty), Empty))
-
-        var result = Member(Atom("a"), list).satisfy(emptyMap()).toList()
-        assertEquals(1, result.size, "Expected one solution")
-        assertTrue(result[0].isSuccess, "Expected success")
-        assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map")
-
-        result = Member(Atom("b"), list).satisfy(emptyMap()).toList()
-        assertEquals(0, result.size, "Expected no solution")
-    }
-
-    @Test
-    fun `member with variable in list`() {
-        val atom = Atom("a")
-        val variable = Variable("X")
-        val list = Cons(variable, Empty)
-
-        val member = Member(atom, list)
-
-        val result = member.satisfy(emptyMap()).toList()
-
-        assertEquals(1, result.size, "Expected one solution")
-        assertTrue(result[0].isSuccess, "Expected success")
-        assertEquals(atom, result[0].getOrNull()!![variable], "Expected variable to be unified with atom")
-    }
-}
\ No newline at end of file
diff --git a/tests/prolog/logic/UnificationTests.kt b/tests/prolog/logic/UnificationTests.kt
index 1324a12..10a37e7 100644
--- a/tests/prolog/logic/UnificationTests.kt
+++ b/tests/prolog/logic/UnificationTests.kt
@@ -10,16 +10,13 @@ import prolog.ast.terms.Variable
 import prolog.builtins.Add
 import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Nested
-import prolog.ast.lists.List
-import prolog.ast.lists.List.Empty
-import prolog.ast.lists.List.Cons
 
 /*
  * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms
  */
 class UnificationTests {
     @Nested
-    class `unify logic` {
+    class `unify` {
         @Test
         fun identical_atoms_unify() {
             val atom1 = Atom("a")
@@ -333,7 +330,7 @@ class UnificationTests {
     }
 
     @Nested
-    class `applySubstitution logic` {
+    class `applySubstitution` {
         @Test
         fun `apply substitution without sub`() {
             val term = Variable("X")
@@ -370,120 +367,4 @@ class UnificationTests {
             assertEquals(Integer(35), result)
         }
     }
-
-    @Nested
-    class `equivalent logic` {
-        @Test
-        fun `empty lists are equivalent`() {
-            var eq = equivalent(Empty, Empty, emptyMap())
-            assertTrue(eq, "Empty lists should be equivalent")
-
-            val variable = Variable("X")
-
-            eq = equivalent(Empty, variable, mapOf(variable to Empty))
-            assertTrue(eq, "Empty list and variable should be equivalent")
-
-            eq = equivalent(variable, Empty, mapOf(variable to Empty))
-            assertTrue(eq, "Variable and empty list should be equivalent")
-        }
-
-        @Test
-        fun `singletons are equivalent`() {
-            val atom = Atom("a")
-            val list1 = Cons(atom, Empty)
-            val list2 = Cons(atom, Empty)
-
-            var eq = equivalent(list1, list2, emptyMap())
-            assertTrue(eq, "Singleton lists should be equivalent")
-
-            val variable = Variable("X")
-
-            eq = equivalent(list1, variable, mapOf(variable to list2))
-            assertTrue(eq, "Singleton list and variable should be equivalent")
-
-            eq = equivalent(variable, list1, mapOf(variable to list2))
-            assertTrue(eq, "Variable and singleton list should be equivalent")
-        }
-
-        @Test
-        fun `singleton and empty list are not equivalent`() {
-            val atom = Atom("a")
-            val list1 = Cons(atom, Empty)
-            val list2 = Empty
-
-            var eq = equivalent(list1, list2, emptyMap())
-            assertFalse(eq, "Singleton and empty lists should not be equivalent")
-
-            eq = equivalent(list2, list1, emptyMap())
-            assertFalse(eq, "Empty and singleton lists should not be equivalent")
-
-            val variable = Variable("X")
-
-            eq = equivalent(list1, variable, mapOf(variable to list2))
-            assertFalse(eq, "Singleton list and variable should not be equivalent")
-
-            eq = equivalent(variable, list1, mapOf(variable to list2))
-            assertFalse(eq, "Variable and singleton list should not be equivalent")
-        }
-
-        @Test
-        fun `identical lists are equivalent`() {
-            val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty))
-            val list2 = Cons(Atom("a"), Cons(Atom("b"), Empty))
-
-            var eq = equivalent(list1, list2, emptyMap())
-            assertTrue(eq, "Identical lists should be equivalent")
-
-            eq = equivalent(list2, list1, emptyMap())
-            assertTrue(eq, "Identical lists should be equivalent")
-
-            val variable = Variable("X")
-
-            eq = equivalent(list1, variable, mapOf(variable to list2))
-            assertTrue(eq, "Identical lists should be equivalent")
-
-            eq = equivalent(variable, list2, mapOf(variable to list1))
-            assertTrue(eq, "Identical lists should be equivalent")
-        }
-
-        @Test
-        fun `identical nested lists are equivalent`() {
-            val list1 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
-            val list2 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
-
-            var eq = equivalent(list1, list2, emptyMap())
-            assertTrue(eq, "Identical nested lists should be equivalent")
-
-            eq = equivalent(list2, list1, emptyMap())
-            assertTrue(eq, "Identical nested lists should be equivalent")
-
-            val variable = Variable("X")
-
-            eq = equivalent(list1, variable, mapOf(variable to list2))
-            assertTrue(eq, "Identical nested lists should be equivalent")
-
-            eq = equivalent(variable, list2, mapOf(variable to list1))
-            assertTrue(eq, "Identical nested lists should be equivalent")
-        }
-
-        @Test
-        fun `lists with different nests are not equivalent`() {
-            val list1 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("bar"), Cons(Atom("baz"), Empty)), Empty)))
-            val list2 = Cons(Atom("foo"), Cons(Atom("bar"), Cons(Cons(Atom("baz"), Cons(Atom("bar"), Empty)), Empty)))
-
-            var eq = equivalent(list1, list2, emptyMap())
-            assertFalse(eq, "Lists with different nests should not be equivalent")
-
-            eq = equivalent(list2, list1, emptyMap())
-            assertFalse(eq, "Lists with different nests should not be equivalent")
-
-            val variable = Variable("X")
-
-            eq = equivalent(list1, variable, mapOf(variable to list2))
-            assertFalse(eq, "Lists with different nests should not be equivalent")
-
-            eq = equivalent(variable, list2, mapOf(variable to list1))
-            assertFalse(eq, "Lists with different nests should not be equivalent")
-        }
-    }
 }
\ No newline at end of file