diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt
index 3bd5fa9..6c17705 100644
--- a/src/interpreter/Preprocessor.kt
+++ b/src/interpreter/Preprocessor.kt
@@ -75,7 +75,6 @@ open class Preprocessor {
                     term.functor == ",/2" -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
                     term.functor == ";/2" -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
                     term.functor == "\\+/1" -> Not(args[0] as Goal)
-                    term.functor == "\\==/2" -> NotEquivalent(args[0], args[1])
                     term.functor == "==/2" -> Equivalent(args[0], args[1])
 
                     term.functor == "=\\=/2" && args.all { it is Expression } -> EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)
@@ -91,12 +90,10 @@ open class Preprocessor {
                     term.functor == "*/2" && args.all { it is Expression } -> Multiply(args[0] as Expression, args[1] as Expression)
                     term.functor == "//2" && args.all { it is Expression } -> Divide(args[0] as Expression, args[1] as Expression)
                     term.functor == "between/3" && args.all { it is Expression } -> Between(args[0] as Expression, args[1] as Expression, args[2] as Expression)
-                    term.functor == "succ/2" && args.all { it is Expression } -> Successor(args[0] as Expression, args[1] as Expression)
 
                     // Database
                     term.functor == "dynamic/1" -> Dynamic((args[0] as Atom).name)
                     term.functor == "retract/1" -> Retract(args[0])
-                    term.functor == "retractall/1" -> RetractAll(args[0])
                     term.functor == "assert/1" -> {
                         if (args[0] is Rule) {
                             Assert(args[0] as Rule)
@@ -141,4 +138,4 @@ open class Preprocessor {
 
         return prepped
     }
-}
+}
\ No newline at end of file
diff --git a/src/io/IoHandler.kt b/src/io/IoHandler.kt
index f12deb7..c5706a1 100644
--- a/src/io/IoHandler.kt
+++ b/src/io/IoHandler.kt
@@ -3,8 +3,7 @@ package io
 interface IoHandler {
     fun prompt(
         message: String,
-        hint: () -> String = { "Please enter a valid input." },
-        check: (String) -> Boolean = { true }
+        hint: () -> String = { "Please enter a valid input." }
     ): String
 
     fun say(message: String)
diff --git a/src/io/Terminal.kt b/src/io/Terminal.kt
index d20c8e8..1b9df94 100644
--- a/src/io/Terminal.kt
+++ b/src/io/Terminal.kt
@@ -20,16 +20,15 @@ class Terminal(
 
     override fun prompt(
         message: String,
-        hint: () -> String,
-        check: (String) -> Boolean,
+        hint: () -> String
     ): String {
         say("$message ")
-        var input: String = readLine().trim()
-        while (!check(input)) {
+        var input: String = readLine()
+        while (input.isBlank()) {
             say(hint(), error)
-            input += readLine().trim()
+            input = readLine()
         }
-        return input.trim()
+        return input
     }
 
     override fun say(message: String) {
diff --git a/src/parser/grammars/TermsGrammar.kt b/src/parser/grammars/TermsGrammar.kt
index 0473200..3fb9e48 100644
--- a/src/parser/grammars/TermsGrammar.kt
+++ b/src/parser/grammars/TermsGrammar.kt
@@ -87,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 (equivalent or notEquivalent or equals or notEquals or isOp) use { text }
+    protected val op700: Parser<String> by (equivalent 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))
     }
diff --git a/src/parser/grammars/Tokens.kt b/src/parser/grammars/Tokens.kt
index 018417f..ac8c36f 100644
--- a/src/parser/grammars/Tokens.kt
+++ b/src/parser/grammars/Tokens.kt
@@ -20,7 +20,6 @@ abstract class Tokens : Grammar<Any>() {
     // 1000
     protected val comma: Token by literalToken(",")
     // 700
-    protected val notEquivalent: Token by literalToken("\\==")
     protected val equivalent: Token by literalToken("==")
     protected val equals: Token by literalToken("=")
     protected val isOp: Token by literalToken("is")
diff --git a/src/prolog/ast/arithmetic/Float.kt b/src/prolog/ast/arithmetic/Float.kt
index a787cb2..da49530 100644
--- a/src/prolog/ast/arithmetic/Float.kt
+++ b/src/prolog/ast/arithmetic/Float.kt
@@ -32,8 +32,6 @@ class Float(override val value: kotlin.Float): Number {
         else -> throw IllegalArgumentException("Cannot multiply $this and $other")
     }
 
-    override fun applySubstitution(subs: Substitutions): Float = this
-
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
         if (other !is Float) return false
diff --git a/src/prolog/ast/arithmetic/Integer.kt b/src/prolog/ast/arithmetic/Integer.kt
index c12cfcd..dbf9c39 100644
--- a/src/prolog/ast/arithmetic/Integer.kt
+++ b/src/prolog/ast/arithmetic/Integer.kt
@@ -33,7 +33,6 @@ data class Integer(override val value: Int) : Number, LogicOperand() {
                 Float(value / other.value.toFloat())
             }
         }
-
         else -> throw IllegalArgumentException("Cannot divide $this and $other")
     }
 
@@ -42,6 +41,4 @@ 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 applySubstitution(subs: Substitutions): Integer = this
 }
diff --git a/src/prolog/ast/logic/Clause.kt b/src/prolog/ast/logic/Clause.kt
index 4e97a14..2abfa77 100644
--- a/src/prolog/ast/logic/Clause.kt
+++ b/src/prolog/ast/logic/Clause.kt
@@ -27,23 +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.
 
-        val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, subs)
-        Program.variableRenamingStart = headEnd
+        // 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 renamedHead = applySubstitution(head, subs + headRenaming)
-        val renamedBody = applySubstitution(body, subs + headRenaming) as Body
+        val reverse = renamed.entries.associate { (a, b) -> b to a }
+        Program.variableRenamingStart = end
 
-        unifyLazy(goal, renamedHead, subs).forEach { headAnswer ->
+        var newSubs: Substitutions = subs + renamed
+        unifyLazy(applySubstitution(goal, subs), head, newSubs).forEach { headAnswer ->
             headAnswer.map { headSubs ->
-                val subsNotInGoal = headSubs.filterNot { occurs(it.key as Variable, goal, emptyMap()) }
-                renamedBody.satisfy(subsNotInGoal).forEach { bodyAnswer ->
+                // If the body can be proven, yield the (combined) substitutions
+                newSubs = subs + renamed + headSubs
+                body.satisfy(newSubs).forEach { bodyAnswer ->
                     bodyAnswer.fold(
-                        // If the body can be proven, yield the (combined) substitutions
                         onSuccess = { bodySubs ->
-                            var result = headSubs + bodySubs
-                            result = result
-                                .mapValues { applySubstitution(it.value, result) }
-                                .filterKeys { it !is AnonymousVariable && occurs(it as Variable, goal, emptyMap()) }
+                            var result = (headSubs + bodySubs)
+                                .mapKeys { applySubstitution(it.key, reverse)}
+                                .mapValues { applySubstitution(it.value, reverse) }
+                            result = result.map { it.key to applySubstitution(it.value, result) }
+                                .toMap()
+                                .filterNot { it.key in renamed.keys && !occurs(it.key as Variable, goal, emptyMap())}
                             yield(Result.success(result))
                         },
                         onFailure = { error ->
@@ -77,5 +81,7 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
         return true
     }
 
-    override fun hashCode(): Int = super.hashCode()
+    override fun hashCode(): Int {
+        return super.hashCode()
+    }
 }
diff --git a/src/prolog/ast/logic/Fact.kt b/src/prolog/ast/logic/Fact.kt
index b6cc83d..a52990e 100644
--- a/src/prolog/ast/logic/Fact.kt
+++ b/src/prolog/ast/logic/Fact.kt
@@ -1,10 +1,6 @@
 package prolog.ast.logic
 
-import prolog.Substitutions
 import prolog.ast.terms.Head
 import prolog.builtins.True
-import prolog.logic.applySubstitution
 
-class Fact(head: Head) : Clause(head, True) {
-    override fun applySubstitution(subs: Substitutions): Fact = Fact(applySubstitution(head, subs) as Head)
-}
+class Fact(head: Head) : Clause(head, True)
\ No newline at end of file
diff --git a/src/prolog/ast/logic/Rule.kt b/src/prolog/ast/logic/Rule.kt
index 26148a3..9eba36e 100644
--- a/src/prolog/ast/logic/Rule.kt
+++ b/src/prolog/ast/logic/Rule.kt
@@ -1,13 +1,6 @@
 package prolog.ast.logic
 
-import prolog.Substitutions
 import prolog.ast.terms.Body
 import prolog.ast.terms.Head
-import prolog.logic.applySubstitution
 
-class Rule(head: Head, body: Body) : Clause(head, body) {
-    override fun applySubstitution(subs: Substitutions): Rule = Rule(
-        head = applySubstitution(head, subs) as Head,
-        body = applySubstitution(body, subs) as Body
-    )
-}
+class Rule(head: Head, body: Body) : Clause(head, body)
\ No newline at end of file
diff --git a/src/prolog/ast/terms/AnonymousVariable.kt b/src/prolog/ast/terms/AnonymousVariable.kt
index abb751c..1bc0633 100644
--- a/src/prolog/ast/terms/AnonymousVariable.kt
+++ b/src/prolog/ast/terms/AnonymousVariable.kt
@@ -1,9 +1,8 @@
 package prolog.ast.terms
 
 import io.Logger
-import prolog.Substitutions
 
-class AnonymousVariable(private val id: Int) : Variable("_$id") {
+class AnonymousVariable(id: Int) : Variable("_$id") {
     companion object {
         private var counter = 0
         fun create(): AnonymousVariable {
@@ -14,7 +13,5 @@ class AnonymousVariable(private val id: Int) : Variable("_$id") {
         }
     }
 
-    override fun applySubstitution(subs: Substitutions): AnonymousVariable = this
-
     override fun toString(): String = "_"
 }
\ No newline at end of file
diff --git a/src/prolog/ast/terms/Atom.kt b/src/prolog/ast/terms/Atom.kt
index 5bc2004..3a6afad 100644
--- a/src/prolog/ast/terms/Atom.kt
+++ b/src/prolog/ast/terms/Atom.kt
@@ -10,8 +10,6 @@ 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 = Atom(name)
-
     override fun toString(): String {
         return name
     }
diff --git a/src/prolog/ast/terms/Body.kt b/src/prolog/ast/terms/Body.kt
index 989c4d9..dc61c7d 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 : Term, Satisfiable
+interface Body : Satisfiable
\ No newline at end of file
diff --git a/src/prolog/ast/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt
index afed37c..385da2c 100644
--- a/src/prolog/ast/terms/Structure.kt
+++ b/src/prolog/ast/terms/Structure.kt
@@ -3,7 +3,6 @@ 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
@@ -24,11 +23,6 @@ open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), He
         }
     }
 
-    override fun applySubstitution(subs: Substitutions): Structure = Structure(
-        name,
-        arguments.map { applySubstitution(it, subs) }
-    )
-
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
         if (other !is Structure) return false
diff --git a/src/prolog/ast/terms/Term.kt b/src/prolog/ast/terms/Term.kt
index 8e46626..0fdad49 100644
--- a/src/prolog/ast/terms/Term.kt
+++ b/src/prolog/ast/terms/Term.kt
@@ -1,18 +1,14 @@
 package prolog.ast.terms
 
-import prolog.Substitutions
-import prolog.ast.arithmetic.Float
-import prolog.ast.arithmetic.Integer
 import prolog.logic.compare
 
 /**
  * Value in Prolog.
  *
- * A [Term] is either a [Variable], [Atom], [Integer],
- * [Float] or [CompoundTerm].
+ * A [Term] is either a [Variable], [Atom], [Integer][prolog.ast.arithmetic.Integer],
+ * [Float][prolog.ast.arithmetic.Float] or [CompoundTerm].
  * In addition, SWI-Prolog also defines the type TODO string.
  */
 interface Term : Comparable<Term> {
     override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
-    fun applySubstitution(subs: Substitutions): Term
 }
diff --git a/src/prolog/ast/terms/Variable.kt b/src/prolog/ast/terms/Variable.kt
index bcfee5c..2d23170 100644
--- a/src/prolog/ast/terms/Variable.kt
+++ b/src/prolog/ast/terms/Variable.kt
@@ -34,8 +34,6 @@ open class Variable(val name: String) : Term, Body, Expression, LogicOperand() {
         return name == other.name
     }
 
-    override fun applySubstitution(subs: Substitutions): Variable = this
-
     override fun hashCode(): Int {
         return name.hashCode()
     }
diff --git a/src/prolog/builtins/arithmeticOperators.kt b/src/prolog/builtins/arithmeticOperators.kt
index 963a2ca..306337e 100644
--- a/src/prolog/builtins/arithmeticOperators.kt
+++ b/src/prolog/builtins/arithmeticOperators.kt
@@ -39,10 +39,6 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr
         }
     }
 
-    override fun applySubstitution(subs: Substitutions): EvaluatesToDifferent = EvaluatesToDifferent(
-        left.applySubstitution(subs) as Expression,
-        right.applySubstitution(subs) as Expression
-    )
 }
 
 /**
@@ -61,11 +57,6 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) :
 
         return if (equivalent(t1.to, t2.to, subs)) sequenceOf(Result.success(emptyMap())) else emptySequence()
     }
-
-    override fun applySubstitution(subs: Substitutions): EvaluatesTo = EvaluatesTo(
-        left.applySubstitution(subs) as Expression,
-        right.applySubstitution(subs) as Expression
-    )
 }
 
 /**
@@ -87,11 +78,6 @@ class Is(val number: Expression, val expr: Expression) :
 
         return unifyLazy(t1.to, t2.to, subs)
     }
-
-    override fun applySubstitution(subs: Substitutions): Is = Is(
-        number.applySubstitution(subs) as Expression,
-        expr.applySubstitution(subs) as Expression
-    )
 }
 
 /**
@@ -115,11 +101,6 @@ open class Add(private val expr1: Expression, private val expr2: Expression) :
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
-
-    override fun applySubstitution(subs: Substitutions): Add = Add(
-        expr1.applySubstitution(subs) as Expression,
-        expr2.applySubstitution(subs) as Expression
-    )
 }
 
 /**
@@ -133,11 +114,6 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
-
-    override fun applySubstitution(subs: Substitutions): Subtract = Subtract(
-        expr1.applySubstitution(subs) as Expression,
-        expr2.applySubstitution(subs) as Expression
-    )
 }
 
 /**
@@ -151,11 +127,6 @@ class Multiply(val expr1: Expression, val expr2: Expression) :
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
-
-    override fun applySubstitution(subs: Substitutions): Multiply = Multiply(
-        expr1.applySubstitution(subs) as Expression,
-        expr2.applySubstitution(subs) as Expression
-    )
 }
 
 class Divide(private val expr1: Expression, private val expr2: Expression) :
@@ -166,11 +137,6 @@ class Divide(private val expr1: Expression, private val expr2: Expression) :
         val simplification = result.simplify(map.first().getOrThrow())
         return Simplification(this, simplification.to)
     }
-
-    override fun applySubstitution(subs: Substitutions): Divide = Divide(
-        expr1.applySubstitution(subs) as Expression,
-        expr2.applySubstitution(subs) as Expression
-    )
 }
 
 // TODO Expr mod Expr
@@ -200,16 +166,5 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
         }
     }
 
-    override fun applySubstitution(subs: Substitutions): Between = Between(
-        expr1.applySubstitution(subs) as Expression,
-        expr2.applySubstitution(subs) as Expression,
-        expr3.applySubstitution(subs) as Expression
-    )
-
     override fun toString(): String = "$expr1..$expr3..$expr2"
 }
-
-class Successor(private val expr1: Expression, private val expr2: Expression) :
-    CompoundTerm(Atom("succ"), listOf(expr1, expr2)), Satisfiable {
-    override fun satisfy(subs: Substitutions): Answers = succ(expr1, expr2, subs)
-}
diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt
index 41c8b6d..613c915 100644
--- a/src/prolog/builtins/controlOperators.kt
+++ b/src/prolog/builtins/controlOperators.kt
@@ -7,16 +7,13 @@ 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
 
 /**
  * Always fail.
  */
 object Fail : Atom("fail"), Body {
     override fun satisfy(subs: Substitutions): Answers = emptySequence()
-    override fun applySubstitution(subs: Substitutions): Fail = Fail
 }
 
 /**
@@ -29,7 +26,6 @@ typealias False = Fail
  */
 object True : Atom("true"), Body {
     override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap()))
-    override fun applySubstitution(subs: Substitutions): True = True
 }
 
 // TODO Repeat/0
@@ -38,8 +34,6 @@ class Cut() : Atom("!") {
     override fun satisfy(subs: Substitutions): Answers {
         return sequenceOf(Result.failure(AppliedCut(emptyMap())))
     }
-
-    override fun applySubstitution(subs: Substitutions): Cut = Cut()
 }
 
 /**
@@ -100,11 +94,6 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
             )
         }
     }
-
-    override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction(
-        applySubstitution(left, subs) as LogicOperand,
-        applySubstitution(right, subs) as LogicOperand
-    )
 }
 
 /**
@@ -116,11 +105,6 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO
         yieldAll(left.satisfy(subs))
         yieldAll(right.satisfy(subs))
     }
-
-    override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction(
-        applySubstitution(left, subs) as LogicOperand,
-        applySubstitution(right, subs) as LogicOperand
-    )
 }
 
 @Deprecated("Use Disjunction instead")
@@ -143,6 +127,4 @@ class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = go
         // If the goal cannot be proven, return a sequence with an empty map
         return sequenceOf(Result.success(emptyMap()))
     }
-
-    override fun applySubstitution(subs: Substitutions): Not = Not(applySubstitution(goal, subs) as Goal)
 }
diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt
index ea36376..eaf67b8 100644
--- a/src/prolog/builtins/databaseOperators.kt
+++ b/src/prolog/builtins/databaseOperators.kt
@@ -1,6 +1,5 @@
 package prolog.builtins
 
-import io.Logger
 import prolog.Answers
 import prolog.Substitutions
 import prolog.ast.logic.Clause
@@ -43,8 +42,6 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
     }
 
     override fun hashCode(): Int = super.hashCode()
-
-    override fun applySubstitution(subs: Substitutions): Dynamic = Dynamic(dynamicFunctor)
 }
 
 class Assert(clause: Clause) : AssertZ(clause) {
@@ -62,8 +59,6 @@ class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) {
 
         return sequenceOf(Result.success(emptyMap()))
     }
-
-    override fun applySubstitution(subs: Substitutions): AssertA = AssertA(applySubstitution(clause, subs) as Clause)
 }
 
 /**
@@ -77,8 +72,6 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause)
 
         return sequenceOf(Result.success(emptyMap()))
     }
-
-    override fun applySubstitution(subs: Substitutions): AssertZ = AssertZ(applySubstitution(clause, subs) as Clause)
 }
 
 /**
@@ -87,7 +80,7 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause)
  *
  * @see [SWI-Prolog Predicate retract/1](https://www.swi-prolog.org/pldoc/doc_for?object=retract/1)
  */
-open class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
+class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
     override fun satisfy(subs: Substitutions): Answers = sequence {
         // Check that term is a structure or atom
         if (term !is Structure && term !is Atom) {
@@ -102,12 +95,6 @@ open class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
             return@sequence
         }
 
-        // Check if the predicate is dynamic
-        if (!predicate.dynamic) {
-            yield(Result.failure(Exception("No permission to modify static procedure '$functorName'")))
-            return@sequence
-        }
-
         predicate.clauses.toList().forEach { clause ->
             unifyLazy(term, clause.head, subs).forEach { unifyResult ->
                 unifyResult.fold(
@@ -123,32 +110,4 @@ open class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
             }
         }
     }
-
-    override fun applySubstitution(subs: Substitutions): Retract = Retract(applySubstitution(term, subs))
-}
-
-class RetractAll(term: Term) : Retract(term) {
-    override fun satisfy(subs: Substitutions): Answers {
-        // Check that term is a structure or atom
-        if (term !is Structure && term !is Atom) {
-            return sequenceOf(Result.failure(Exception("Cannot retract a non-structure or non-atom")))
-        }
-
-        // If the predicate does not exist, implicitly create it
-        val functor = term.functor
-        val predicate = Program.db.predicates[functor]
-        if (predicate == null) {
-            Logger.debug("Predicate $functor not found, creating it")
-            Program.db.predicates += functor to Predicate(functor, dynamic = true)
-        }
-
-        // Propagate errors from the super class
-        super.satisfy(subs).forEach {
-            if (it.isFailure) {
-                return sequenceOf(it)
-            }
-        }
-
-        return sequenceOf(Result.success(emptyMap()))
-    }
 }
diff --git a/src/prolog/builtins/ioOperators.kt b/src/prolog/builtins/ioOperators.kt
index 4c80d61..1271296 100644
--- a/src/prolog/builtins/ioOperators.kt
+++ b/src/prolog/builtins/ioOperators.kt
@@ -27,8 +27,6 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis
         return sequenceOf(Result.success(emptyMap()))
     }
 
-    override fun applySubstitution(subs: Substitutions): Write = Write(applySubstitution(term, subs))
-
     override fun toString(): String = "write($term)"
 }
 
@@ -41,8 +39,6 @@ object Nl : Atom("nl"), Satisfiable {
         Program.storeNewLine = false
         return sequenceOf(Result.success(emptyMap()))
     }
-
-    override fun applySubstitution(subs: Substitutions): Nl = this
 }
 
 /**
@@ -76,6 +72,4 @@ class Read(private val term: Term) : Operator(Atom("read"), null, term), Satisfi
 
         yieldAll(unifyLazy(t1, t2, subs))
     }
-
-    override fun applySubstitution(subs: Substitutions): Read = Read(applySubstitution(term, subs))
 }
diff --git a/src/prolog/builtins/unificationOperators.kt b/src/prolog/builtins/unificationOperators.kt
index ad55acf..892c616 100644
--- a/src/prolog/builtins/unificationOperators.kt
+++ b/src/prolog/builtins/unificationOperators.kt
@@ -24,20 +24,11 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
 
         yieldAll(unifyLazy(t1, t2, subs))
     }
-
-    override fun applySubstitution(subs: Substitutions): Unify = Unify(
-        applySubstitution(term1, subs),
-        applySubstitution(term2, subs)
-    )
 }
 
-class NotUnify(private val term1: Term, private val term2: Term) : Operator(Atom("\\="), term1, term2) {
+class NotUnify(term1: Term, term2: Term) : Operator(Atom("\\="), term1, term2) {
     private val not = Not(Unify(term1, term2))
     override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
-    override fun applySubstitution(subs: Substitutions): NotUnify = NotUnify(
-        applySubstitution(term1, subs),
-        applySubstitution(term2, subs)
-    )
 }
 
 class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) {
@@ -49,18 +40,4 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
             yield(Result.success(emptyMap()))
         }
     }
-
-    override fun applySubstitution(subs: Substitutions): Equivalent = Equivalent(
-        applySubstitution(term1, subs),
-        applySubstitution(term2, subs)
-    )
-}
-
-class NotEquivalent(private val term1: Term, private val term2: Term) : Operator(Atom("\\=="), term1, term2) {
-    private val not = Not(Equivalent(term1, term2))
-    override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
-    override fun applySubstitution(subs: Substitutions): NotEquivalent = NotEquivalent(
-        applySubstitution(term1, subs),
-        applySubstitution(term2, subs)
-    )
 }
diff --git a/src/prolog/logic/unification.kt b/src/prolog/logic/unification.kt
index 6dd033f..1e7b57f 100644
--- a/src/prolog/logic/unification.kt
+++ b/src/prolog/logic/unification.kt
@@ -15,15 +15,19 @@ import prolog.ast.terms.*
 
 // Apply substitutions to a term
 fun applySubstitution(term: Term, subs: Substitutions): Term = when {
-    term is Fact -> term.applySubstitution(subs)
+    term is Fact -> {
+        Fact(applySubstitution(term.head, subs) as Head)
+    }
 
     variable(term, emptyMap()) -> {
         val variable = term as Variable
         subs[variable]?.let { applySubstitution(term = it, subs = subs) } ?: term
     }
-
     atomic(term, subs) -> term
-    compound(term, subs) -> term.applySubstitution(subs)
+    compound(term, subs) -> {
+        val structure = term as Structure
+        Structure(structure.name, structure.arguments.map { applySubstitution(it, subs) })
+    }
 
     else -> term
 }
diff --git a/src/repl/Repl.kt b/src/repl/Repl.kt
index 4db4fbc..5e8b0d4 100644
--- a/src/repl/Repl.kt
+++ b/src/repl/Repl.kt
@@ -29,45 +29,40 @@ class Repl {
     }
 
     private fun query(): Answers {
-        val queryString = io.prompt("?-", { "|  " }, { it.endsWith(".") })
+        val queryString = io.prompt("?-", { "|  " })
         val simpleQuery = parser.parse(queryString)
         val query = preprocessor.preprocess(simpleQuery)
         return query.satisfy(emptyMap())
     }
 
     private fun printAnswers(answers: Answers) {
+        val knownCommands = setOf(";", "a", ".", "h")
+
         val iterator = answers.iterator()
 
         if (!iterator.hasNext()) {
             io.say("false.\n")
-            return
-        }
+        } else {
+            io.say(prettyPrint(iterator.next()))
 
-        io.say(prettyPrint(iterator.next()))
+            while (iterator.hasNext()) {
+                var command = io.prompt("")
 
-        while (true) {
-            when (io.prompt("")) {
-                ";" -> {
-                    try {
+                while (command !in knownCommands) {
+                    io.say("Unknown action: $command (h for help)\n")
+                    command = io.prompt("Action?")
+                }
+
+                when (command) {
+                    ";" -> {
                         io.say(prettyPrint(iterator.next()))
-                    } catch (_: NoSuchElementException) {
-                        break
                     }
-                }
-
-                "a" -> return
-                "." -> {
-                    io.checkNewLine()
-                    return
-                }
-                "h" -> {
-                    help()
-                    io.say("Action?")
-                }
-
-                else -> {
-                    io.say("Unknown action: (h for help)\n")
-                    io.say("Action?")
+                    "a" -> return
+                    "." -> return
+                    "h" -> {
+                        help()
+                        io.say("Action?")
+                    }
                 }
             }
         }
@@ -95,7 +90,9 @@ class Repl {
                 return subs.entries.joinToString(",\n") { "${it.key} = ${it.value}" }
             },
             onFailure = {
-                return "ERROR: ${it.message}"
+                val text = "Failure: ${it.message}"
+                Logger.warn(text)
+                return text
             }
         )
     }
diff --git a/tests/prolog/EvaluationTests.kt b/tests/prolog/EvaluationTests.kt
index 1a62390..ac3df3f 100644
--- a/tests/prolog/EvaluationTests.kt
+++ b/tests/prolog/EvaluationTests.kt
@@ -14,8 +14,6 @@ import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
 import prolog.ast.Database.Program
-import prolog.ast.arithmetic.Integer
-import prolog.ast.terms.AnonymousVariable
 
 class EvaluationTests {
     @BeforeEach
@@ -110,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))
@@ -120,14 +118,10 @@ class EvaluationTests {
 
         Program.load(listOf(father, mother, parent))
 
-        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 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 result3 = Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jane"))))
         assertFalse(result3.any())
@@ -420,63 +414,4 @@ class EvaluationTests {
             assertEquals(Atom("bob"), subs5[Variable("Person")], "Expected bob")
         }
     }
-
-    @Test
-    fun `leq Peano`() {
-        val fact = Fact(Structure(Atom("leq"), listOf(Integer(0), AnonymousVariable.create())))
-        val rule = Rule(
-            Structure(
-                Atom("leq"),
-                listOf(Structure(Atom("s"), listOf(Variable("X"))), Structure(Atom("s"), listOf(Variable("Y"))))
-            ),
-            Structure(Atom("leq"), listOf(Variable("X"), Variable("Y"))),
-        )
-
-        Program.db.load(listOf(fact, rule))
-
-        val result1 = Program.query(Structure(Atom("leq"), listOf(Variable("X"), Integer(0)))).toList()
-
-        assertEquals(1, result1.size, "Expected 1 result")
-        assertTrue(result1[0].isSuccess, "Expected success")
-        val subs = result1[0].getOrNull()!!
-        assertEquals(1, subs.size, "Expected 1 substitution")
-        assertEquals(Integer(0), subs[Variable("X")], "Expected X to be 0")
-
-        val result2 =
-            Program.query(Structure(Atom("leq"), listOf(Variable("X"), Structure(Atom("s"), listOf(Integer(0))))))
-                .toList()
-
-        assertEquals(2, result2.size, "Expected 2 results")
-
-        assertTrue(result2[0].isSuccess, "Expected success")
-        val subs2a = result2[0].getOrNull()!!
-        assertEquals(1, subs2a.size, "Expected 1 substitution")
-        assertEquals(Integer(0), subs2a[Variable("X")], "Expected X to be 0")
-
-        assertTrue(result2[1].isSuccess, "Expected success")
-        val subs2b = result2[1].getOrNull()!!
-        assertEquals(1, subs2b.size, "Expected 1 substitution")
-        assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs2b[Variable("X")], "Expected X to be s(0)")
-
-        val result3 = Program.query(
-            Structure(
-                Atom("leq"),
-                listOf(Variable("X"), Structure(Atom("s"), listOf(Structure(Atom("s"), listOf(Integer(0))))))
-            )
-        ).toList()
-
-        assertEquals(3, result3.size, "Expected 3 results")
-        assertTrue(result3[0].isSuccess, "Expected success")
-        val subs3a = result3[0].getOrNull()!!
-        assertEquals(1, subs3a.size, "Expected 1 substitution")
-        assertEquals(Integer(0), subs3a[Variable("X")], "Expected X to be 0")
-        assertTrue(result3[1].isSuccess, "Expected success")
-        val subs3b = result3[1].getOrNull()!!
-        assertEquals(1, subs3b.size, "Expected 1 substitution")
-        assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs3b[Variable("X")], "Expected X to be s(0)")
-        assertTrue(result3[2].isSuccess, "Expected success")
-        val subs3c = result3[2].getOrNull()!!
-        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))")
-    }
 }
diff --git a/tests/prolog/builtins/DatabaseOperatorsTests.kt b/tests/prolog/builtins/DatabaseOperatorsTests.kt
index 73cfef0..8e96085 100644
--- a/tests/prolog/builtins/DatabaseOperatorsTests.kt
+++ b/tests/prolog/builtins/DatabaseOperatorsTests.kt
@@ -15,7 +15,6 @@ import prolog.ast.logic.Fact
 import prolog.ast.logic.Predicate
 import prolog.ast.logic.Rule
 import prolog.ast.terms.Atom
-import prolog.ast.terms.Functor
 import prolog.ast.terms.Structure
 import prolog.ast.terms.Variable
 
@@ -132,7 +131,7 @@ class DatabaseOperatorsTests {
 
     @Test
     fun `simple retract`() {
-        val predicate = Predicate(listOf(Fact(Atom("a"))), dynamic = true)
+        val predicate = Predicate(listOf(Fact(Atom("a"))))
         Program.db.load(predicate)
 
         assertEquals(1, Program.query(Atom("a")).count())
@@ -147,13 +146,11 @@ class DatabaseOperatorsTests {
 
     @Test
     fun `retract atom`() {
-        val predicate = Predicate(
-            listOf(
-                Fact(Atom("a")),
-                Fact(Atom("a")),
-                Fact(Atom("a"))
-            ), dynamic = true
-        )
+        val predicate = Predicate(listOf(
+            Fact(Atom("a")),
+            Fact(Atom("a")),
+            Fact(Atom("a"))
+        ))
         Program.db.load(predicate)
 
         val control = Program.query(Atom("a")).toList()
@@ -173,9 +170,11 @@ class DatabaseOperatorsTests {
         assertTrue(answer.isSuccess, "Expected success")
         assertTrue(answer.getOrNull()!!.isEmpty(), "Expected no substitutions")
 
+        assertTrue(result.hasNext(), "Expected more results")
         assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
 
         assertTrue(result.next().isSuccess)
+        assertTrue(result.hasNext(), "Expected more results")
         assertTrue(result.next().isSuccess)
 
         assertFalse(result.hasNext(), "Expected more results")
@@ -184,13 +183,11 @@ class DatabaseOperatorsTests {
 
     @Test
     fun `retract compound with variable`() {
-        val predicate = Predicate(
-            listOf(
-                Fact(Structure(Atom("a"), listOf(Atom("b")))),
-                Fact(Structure(Atom("a"), listOf(Atom("c")))),
-                Fact(Structure(Atom("a"), listOf(Atom("d"))))
-            ), dynamic = true
-        )
+        val predicate = Predicate(listOf(
+            Fact(Structure(Atom("a"), listOf(Atom("b")))),
+            Fact(Structure(Atom("a"), listOf(Atom("c")))),
+            Fact(Structure(Atom("a"), listOf(Atom("d"))))
+        ))
         Program.db.load(predicate)
 
         val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList()
@@ -211,6 +208,7 @@ class DatabaseOperatorsTests {
         assertTrue(subs.isNotEmpty(), "Expected substitutions")
         assertTrue(Variable("X") in subs, "Expected variable X")
         assertEquals(Atom("b"), subs[Variable("X")], "Expected b")
+        assertTrue(result.hasNext(), "Expected more results")
         assertEquals(2, predicate.clauses.size, "Expected 2 clauses")
 
         answer = result.next()
@@ -220,6 +218,7 @@ class DatabaseOperatorsTests {
         assertTrue(subs.isNotEmpty(), "Expected substitutions")
         assertTrue(Variable("X") in subs, "Expected variable X")
         assertEquals(Atom("c"), subs[Variable("X")], "Expected c")
+        assertTrue(result.hasNext(), "Expected more results")
         assertEquals(1, predicate.clauses.size, "Expected 1 clause")
 
         answer = result.next()
@@ -229,9 +228,8 @@ class DatabaseOperatorsTests {
         assertTrue(subs.isNotEmpty(), "Expected substitutions")
         assertTrue(Variable("X") in subs, "Expected variable X")
         assertEquals(Atom("d"), subs[Variable("X")], "Expected d")
-        assertEquals(0, predicate.clauses.size, "Expected no clauses")
-
         assertFalse(result.hasNext(), "Expected no more results")
+        assertEquals(0, predicate.clauses.size, "Expected no clauses")
     }
 
     @Test
@@ -294,45 +292,4 @@ class DatabaseOperatorsTests {
         assertEquals(Atom("bob"), result2[Variable("X")], "Expected bob")
         assertEquals(Atom("sushi"), result2[Variable("Y")], "Expected sushi")
     }
-
-    @Test
-    fun `retract all`() {
-        val predicate = Predicate(
-            listOf(
-                Fact(Structure(Atom("a"), listOf(Atom("b")))),
-                Fact(Structure(Atom("a"), listOf(Atom("c")))),
-                Fact(Structure(Atom("a"), listOf(Atom("d"))))
-            ), dynamic = true
-        )
-
-        Program.db.load(predicate)
-
-        val control = Program.query(Structure(Atom("a"), listOf(Variable("X")))).toList()
-        assertEquals(3, control.size, "Expected 3 results")
-        assertEquals(3, Program.db.predicates["a/1"]!!.clauses.size, "Expected 3 clauses")
-
-        val retract = RetractAll(Structure(Atom("a"), listOf(Variable("X"))))
-        val result = retract.satisfy(emptyMap()).toList()
-
-        assertEquals(1, result.size, "Expected 1 result")
-        assertTrue(result[0].isSuccess, "Expected success")
-        assertEquals(0, Program.db.predicates["a/1"]!!.clauses.size, "Expected 0 clauses")
-    }
-
-    @Test
-    fun `If Head refers to a predicate that is not defined, it is implicitly created as a dynamic predicate`() {
-        val predicateName = "idonotyetexist"
-        val predicateFunctor = "$predicateName/1"
-
-        assertFalse(predicateFunctor in Program.db.predicates, "Expected predicate to not exist before")
-
-        val retractAll = RetractAll(Structure(Atom(predicateName), listOf(Variable("X"))))
-        val result = retractAll.satisfy(emptyMap()).toList()
-
-        assertEquals(1, result.size, "Expected 1 result")
-        assertTrue(result[0].isSuccess, "Expected success")
-
-        assertTrue(predicateFunctor in Program.db.predicates, "Expected predicate to exist after")
-        assertTrue(Program.db.predicates[predicateFunctor]!!.dynamic, "Expected predicate to be dynamic")
-    }
 }
\ No newline at end of file