diff --git a/solve-classic/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestClassicNotProvable.kt b/solve-classic/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestClassicNotProvable.kt
new file mode 100644
index 000000000..95a5f5a0d
--- /dev/null
+++ b/solve-classic/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestClassicNotProvable.kt
@@ -0,0 +1,48 @@
+package it.unibo.tuprolog.solve.systemtest
+
+import it.unibo.tuprolog.solve.ClassicSolverFactory
+import it.unibo.tuprolog.solve.SolverFactory
+import it.unibo.tuprolog.solve.TestNotProvable
+import kotlin.test.Ignore
+import kotlin.test.Test
+
+class TestClassicNotProvable : TestNotProvable, SolverFactory by ClassicSolverFactory  {
+    private val prototype = TestNotProvable.prototype(this)
+
+    @Test
+    override fun testNPTrue() {
+        prototype.testNPTrue()
+    }
+
+    @Test
+    override fun testNPCut() {
+        prototype.testNPCut()
+    }
+
+    @Test
+    @Ignore //solver returns no
+    override fun testNPCutFail() {
+        prototype.testNPCutFail()
+    }
+
+    @Test
+    override fun testNPEquals() {
+        prototype.testNPEquals()
+    }
+
+    @Test
+    override fun testNPNum() {
+        prototype.testNPNum()
+    }
+
+    @Test
+    override fun testNPX() {
+        prototype.testNPX()
+    }
+
+    @Test
+    @Ignore //solver returns no
+    override fun testOrNotCutFail() {
+        prototype.testOrNotCutFail()
+    }
+}
\ No newline at end of file
diff --git a/solve-streams/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestStreamsNotProvable.kt b/solve-streams/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestStreamsNotProvable.kt
new file mode 100644
index 000000000..c7d12ae20
--- /dev/null
+++ b/solve-streams/src/commonTest/kotlin/it/unibo/tuprolog/solve/systemtest/TestStreamsNotProvable.kt
@@ -0,0 +1,48 @@
+package it.unibo.tuprolog.solve.systemtest
+
+import it.unibo.tuprolog.solve.SolverFactory
+import it.unibo.tuprolog.solve.StreamsSolverFactory
+import it.unibo.tuprolog.solve.TestNotProvable
+import kotlin.test.Ignore
+import kotlin.test.Test
+
+class TestStreamsNotProvable : TestNotProvable, SolverFactory by StreamsSolverFactory  {
+    private val prototype = TestNotProvable.prototype(this)
+
+    @Test
+    override fun testNPTrue() {
+        prototype.testNPTrue()
+    }
+
+    @Test
+    override fun testNPCut() {
+        prototype.testNPCut()
+    }
+
+    @Test
+    @Ignore //solver returns no
+    override fun testNPCutFail() {
+        prototype.testNPCutFail()
+    }
+
+    @Test
+    override fun testNPEquals() {
+        prototype.testNPEquals()
+    }
+
+    @Test
+    override fun testNPNum() {
+        prototype.testNPNum()
+    }
+
+    @Test
+    override fun testNPX() {
+        prototype.testNPX()
+    }
+
+    @Test
+    @Ignore //solver returns no
+    override fun testOrNotCutFail() {
+        prototype.testOrNotCutFail()
+    }
+}
\ No newline at end of file
diff --git a/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotProvable.kt b/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotProvable.kt
new file mode 100644
index 000000000..4ede4fa4b
--- /dev/null
+++ b/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotProvable.kt
@@ -0,0 +1,74 @@
+package it.unibo.tuprolog.solve
+
+interface TestNotProvable : SolverTest {
+    companion object {
+        fun prototype(solverFactory: SolverFactory): TestNotProvable =
+            TestNotProvableImpl(solverFactory)
+    }
+
+    /**
+     * Tests the queries
+     * ```prolog
+     * ?- \+(true).
+     * ```
+     * fails on a solver initialized with default built-ins and with and empty theory,
+     */
+    fun testNPTrue()
+
+    /**
+     * Tests the queries
+     * ```prolog
+     * ?- \+(!).
+     * ```
+     * fails on a solver initialized with default built-ins and with and empty theory,
+     */
+    fun testNPCut()
+
+    /**
+     * Tests the queries
+     * ```prolog
+     * ?- \+(!,fail).
+     * ```
+     * succeeds on a solver initialized with default built-ins and with and empty theory,
+     */
+    fun testNPCutFail()
+
+    /**
+     * Tests the queries
+     * ```prolog
+     * ?- ((X = 1;X = 2), \+((!,fail))).
+     * ```
+     * succeeds on a solver initialized with default built-ins and with and empty theory,
+     * producing 2 solutions which binds variable `X` to `1` and `X` to `2`.
+     */
+    fun testOrNotCutFail()
+
+    /**
+     * Tests the queries
+     * ```prolog
+     * ?- \+(4 = 5).
+     * ```
+     * succeeds on a solver initialized with default built-ins and with and empty theory,
+     */
+    fun testNPEquals()
+
+    /**
+     * Tests the queries
+     * ```prolog
+     * ?- \+(3).
+     * ```
+     * fails on a solver initialized with default built-ins and with and empty theory,
+     * producing exception `type_error(callable, 3)`.
+     */
+    fun testNPNum()
+
+    /**
+     * Tests the queries
+     * ```prolog
+     * ?- \+(X).
+     * ```
+     * fails on a solver initialized with default built-ins and with and empty theory,
+     * producing exception `instantiation_error`.
+     */
+    fun testNPX()
+}
\ No newline at end of file
diff --git a/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotProvableImpl.kt b/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotProvableImpl.kt
new file mode 100644
index 000000000..3424c4021
--- /dev/null
+++ b/test-solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/TestNotProvableImpl.kt
@@ -0,0 +1,133 @@
+package it.unibo.tuprolog.solve
+
+import it.unibo.tuprolog.dsl.theory.prolog
+import it.unibo.tuprolog.solve.exception.error.InstantiationError
+import it.unibo.tuprolog.solve.exception.error.TypeError
+
+class TestNotProvableImpl(private val solverFactory: SolverFactory) : TestNotProvable {
+    override fun testNPTrue() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query =  "not"(true)
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                kotlin.collections.listOf(
+                    query.no()),
+                solutions
+            )
+        }
+    }
+
+    override fun testNPCut() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query =  "not"("!")
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                kotlin.collections.listOf(
+                    query.no()),
+                solutions
+            )
+        }
+    }
+
+    override fun testNPCutFail() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query =  "not"(("!" and fail))
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                kotlin.collections.listOf(
+                    query.yes()),
+                solutions
+            )
+        }
+    }
+
+    override fun testOrNotCutFail() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = ((("X" `=` 1) or ("X" `=` 2)) and "not"(("!" and fail)))
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                with(query) {
+                    kotlin.collections.listOf(
+                        yes("X" to 1),
+                        yes("X" to 2)
+                    )
+                },
+                solutions
+            )
+        }
+    }
+
+    override fun testNPEquals() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = "not"(4 `=` 5)
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                kotlin.collections.listOf(
+                    query.yes()
+                ),
+                solutions
+            )
+        }
+    }
+
+    override fun testNPNum() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = "not"(3)
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                kotlin.collections.listOf(
+                    query.halt(
+                        TypeError.forGoal(
+                            DummyInstances.executionContext,
+                            Signature("not", 1),
+                            TypeError.Expected.CALLABLE,
+                            numOf(3)
+
+                        )
+                    )
+                ),
+                solutions
+            )
+        }
+    }
+
+    override fun testNPX() {
+        prolog {
+            val solver = solverFactory.solverWithDefaultBuiltins()
+
+            val query = "not"("X")
+            val solutions = solver.solve(query, mediumDuration).toList()
+
+            assertSolutionEquals(
+                kotlin.collections.listOf(
+                    query.halt(
+                        InstantiationError.forGoal(
+                            DummyInstances.executionContext,
+                            Signature("not", 1),
+                            varOf("X")
+                        )
+                    )
+                ),
+                solutions
+            )
+        }
+    }
+}
\ No newline at end of file