diff --git a/solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/stdlib/primitive/Retract.kt b/solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/stdlib/primitive/Retract.kt
index fcbe49f97..9435423e6 100644
--- a/solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/stdlib/primitive/Retract.kt
+++ b/solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/stdlib/primitive/Retract.kt
@@ -6,32 +6,19 @@ import it.unibo.tuprolog.solve.ExecutionContext
 import it.unibo.tuprolog.solve.SideEffect
 import it.unibo.tuprolog.solve.Solve
 import it.unibo.tuprolog.solve.primitive.UnaryPredicate
-import it.unibo.tuprolog.theory.RetractResult
 import it.unibo.tuprolog.unify.Unificator.Companion.mguWith
+import it.unibo.tuprolog.utils.buffered
 
-// TODO reimplement
 object Retract : UnaryPredicate<ExecutionContext>("retract") {
     override fun Solve.Request<ExecutionContext>.computeAll(first: Term): Sequence<Solve.Response> {
         ensuringArgumentIsStruct(0)
         val clause = if (first is Clause) first else Rule.of(first as Struct, Var.anonymous())
-        return sequence {
-            var dynamicKb = context.dynamicKb
-            while (true) {
-                val result = dynamicKb.retract(clause)
-                if (result is RetractResult.Success) {
-                    dynamicKb = result.theory
-                    val substitution = when (first) {
-                        is Clause -> (first mguWith result.firstClause) as Substitution.Unifier
-                        else -> (first mguWith result.firstClause.head!!) as Substitution.Unifier
-                    }
-                    yield(
-                        replySuccess(substitution, null, SideEffect.RemoveDynamicClauses(result.firstClause))
-                    )
-                } else {
-                    break
-                }
+        return context.dynamicKb[clause].buffered().map {
+            val substitution = when (first) {
+                is Clause -> (first mguWith it) as Substitution.Unifier
+                else -> (first mguWith it.head!!) as Substitution.Unifier
             }
-            yield(replyFail())
+            replySuccess(substitution, null, SideEffect.RemoveDynamicClauses(it))
         }
     }
 }
\ No newline at end of file
diff --git a/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/SolverTestImpl.kt b/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/SolverTestImpl.kt
index 0dd40f105..4c4a64bc7 100644
--- a/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/SolverTestImpl.kt
+++ b/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/SolverTestImpl.kt
@@ -300,7 +300,7 @@ internal class SolverTestImpl(private val solverFactory: SolverFactory) : Solver
             assertSolutionEquals(
                 ktListOf(
                     query.yes("X" to listOf(2, 3), "Y" to listOf(1)),
-                    query.yes("X" to listOf(2), "Y" to listOf(1, 2)),
+                    query.yes("X" to listOf(3), "Y" to listOf(1, 2)),
                     query.yes("X" to emptyList(), "Y" to listOf(1, 2, 3))
                 ),
                 solutions
@@ -942,8 +942,7 @@ internal class SolverTestImpl(private val solverFactory: SolverFactory) : Solver
             assertSolutionEquals(
                 ktListOf(
                     query.yes("X" to 1),
-                    query.yes("X" to 2),
-                    query.no()
+                    query.yes("X" to 2)
 
                 ),
                 solutions