From 65ae8981e982900a0a799b52fd9f3d9a66441ac3 Mon Sep 17 00:00:00 2001
From: josd <josderoo@gmail.com>
Date: Fri, 13 Dec 2024 20:44:38 +0100
Subject: [PATCH] refreshing

---
 reasoning/nand/nand.n3        |  4 +-
 reasoning/nand/test1-proof.n3 | 43 ++++++----------
 reasoning/nand/test2-proof.n3 | 43 ++++++----------
 reasoning/nand/test3-proof.n3 | 97 +++++++++++++----------------------
 reasoning/nand/test4-proof.n3 | 93 +++++++++++----------------------
 reasoning/nand/test5-proof.n3 | 70 +++++++++----------------
 reasoning/nand/test6-proof.n3 | 45 ++++++----------
 7 files changed, 140 insertions(+), 255 deletions(-)

diff --git a/reasoning/nand/nand.n3 b/reasoning/nand/nand.n3
index ad0db6f62..05e1ea7ac 100644
--- a/reasoning/nand/nand.n3
+++ b/reasoning/nand/nand.n3
@@ -12,9 +12,9 @@
     ?P => false.
     ?P graph:list ?L.
     ?L list:select (?A ?B).
-    (   { ?A log:notIsomorphic { ?X => false } }
+    (   { ?A log:equalTo { ?C => false } }
+        true
         { ?C log:equalTo { ?A => false } }
-        { ?A log:equalTo { ?C => false } }
     ) log:ifThenElseIn ?SCOPE.
     ?R graph:list ?B.
 } => {
diff --git a/reasoning/nand/test1-proof.n3 b/reasoning/nand/test1-proof.n3
index bf3018db7..bc9cf5483 100644
--- a/reasoning/nand/test1-proof.n3
+++ b/reasoning/nand/test1-proof.n3
@@ -96,10 +96,12 @@ skolem:lemma6 a r:Inference;
                 {
                     :P a :Test.
                 } => false.
-            } log:notIsomorphic {
-                _:sk_0 => false.
+            } log:equalTo {
+                {
+                    :P a :Test.
+                } => false.
             }.
-        } {
+        } true {
             {
                 :P a :Test.
             } log:equalTo {
@@ -109,16 +111,6 @@ skolem:lemma6 a r:Inference;
                     } => false.
                 } => false.
             }.
-        } {
-            {
-                {
-                    :P a :Test.
-                } => false.
-            } log:equalTo {
-                {
-                    :P a :Test.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test1.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {true graph:list ()}]
     );
@@ -138,37 +130,32 @@ skolem:lemma6 a r:Inference;
         } => false.
     }];
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ()];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test1.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test1.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         :P a :Test.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo true];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true];
     r:rule skolem:lemma7.
 
 skolem:lemma7 a r:Extraction;
     r:gives {
-        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6, var:x_7. {
+        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. {
             <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>.
             var:x_0 => false.
             var:x_0 graph:list var:x_1.
             var:x_1 list:select (var:x_2 var:x_3).
             ({
-                var:x_2 log:notIsomorphic {
+                var:x_2 log:equalTo {
                     var:x_4 => false.
                 }.
-            } {
-                var:x_5 log:equalTo {
+            } true {
+                var:x_4 log:equalTo {
                     var:x_2 => false.
                 }.
-            } {
-                var:x_2 log:equalTo {
-                    var:x_5 => false.
-                }.
-            }) log:ifThenElseIn var:x_6.
-            var:x_7 graph:list var:x_3.
+            }) log:ifThenElseIn var:x_5.
+            var:x_6 graph:list var:x_3.
         } => {
-            var:x_7 => var:x_5.
+            var:x_6 => var:x_4.
         }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
diff --git a/reasoning/nand/test2-proof.n3 b/reasoning/nand/test2-proof.n3
index 48b71d206..4d8a4d7dd 100644
--- a/reasoning/nand/test2-proof.n3
+++ b/reasoning/nand/test2-proof.n3
@@ -128,10 +128,12 @@ skolem:lemma8 a r:Inference;
                 {
                     :R a :Test.
                 } => false.
-            } log:notIsomorphic {
-                _:sk_2 => false.
+            } log:equalTo {
+                {
+                    :R a :Test.
+                } => false.
             }.
-        } {
+        } true {
             {
                 :R a :Test.
             } log:equalTo {
@@ -141,16 +143,6 @@ skolem:lemma8 a r:Inference;
                     } => false.
                 } => false.
             }.
-        } {
-            {
-                {
-                    :R a :Test.
-                } => false.
-            } log:equalTo {
-                {
-                    :R a :Test.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test2.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {{
             :P a :Test.
@@ -187,12 +179,11 @@ skolem:lemma8 a r:Inference;
     } {
         :Q a :Test.
     })];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test2.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_2"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test2.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         :R a :Test.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo {
         :P a :Test.
         :Q a :Test.
     }];
@@ -200,27 +191,23 @@ skolem:lemma8 a r:Inference;
 
 skolem:lemma9 a r:Extraction;
     r:gives {
-        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6, var:x_7. {
+        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. {
             <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>.
             var:x_0 => false.
             var:x_0 graph:list var:x_1.
             var:x_1 list:select (var:x_2 var:x_3).
             ({
-                var:x_2 log:notIsomorphic {
+                var:x_2 log:equalTo {
                     var:x_4 => false.
                 }.
-            } {
-                var:x_5 log:equalTo {
+            } true {
+                var:x_4 log:equalTo {
                     var:x_2 => false.
                 }.
-            } {
-                var:x_2 log:equalTo {
-                    var:x_5 => false.
-                }.
-            }) log:ifThenElseIn var:x_6.
-            var:x_7 graph:list var:x_3.
+            }) log:ifThenElseIn var:x_5.
+            var:x_6 graph:list var:x_3.
         } => {
-            var:x_7 => var:x_5.
+            var:x_6 => var:x_4.
         }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
diff --git a/reasoning/nand/test3-proof.n3 b/reasoning/nand/test3-proof.n3
index 63d29ca39..1d7c86165 100644
--- a/reasoning/nand/test3-proof.n3
+++ b/reasoning/nand/test3-proof.n3
@@ -162,10 +162,12 @@ skolem:lemma8 a r:Inference;
                 {
                     :Q a :Test.
                 } => false.
-            } log:notIsomorphic {
-                _:sk_1 => false.
+            } log:equalTo {
+                {
+                    :Q a :Test.
+                } => false.
             }.
-        } {
+        } true {
             {
                 :Q a :Test.
             } log:equalTo {
@@ -175,16 +177,6 @@ skolem:lemma8 a r:Inference;
                     } => false.
                 } => false.
             }.
-        } {
-            {
-                {
-                    :Q a :Test.
-                } => false.
-            } log:equalTo {
-                {
-                    :Q a :Test.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {{
             {
@@ -241,12 +233,11 @@ skolem:lemma8 a r:Inference;
             :R a :Test.
         } => false.
     })];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_1"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         :Q a :Test.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo {
         {
             :P a :Test.
         } => false.
@@ -280,10 +271,14 @@ skolem:lemma9 a r:Inference;
         [ a r:Fact; r:gives {({
             {
                 :P a :Test.
-            } log:notIsomorphic {
-                _:sk_3 => false.
+            } log:equalTo {
+                {
+                    {
+                        :P a :Test.
+                    } => false.
+                } => false.
             }.
-        } {
+        } true {
             {
                 {
                     :P a :Test.
@@ -293,16 +288,6 @@ skolem:lemma9 a r:Inference;
                     :P a :Test.
                 } => false.
             }.
-        } {
-            {
-                :P a :Test.
-            } log:equalTo {
-                {
-                    {
-                        :P a :Test.
-                    } => false.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {true graph:list ()}]
     );
@@ -316,14 +301,13 @@ skolem:lemma9 a r:Inference;
         :P a :Test.
     }];
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ()];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_3"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         {
             :P a :Test.
         } => false.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo true];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true];
     r:rule skolem:lemma11.
 
 skolem:lemma10 a r:Inference;
@@ -350,10 +334,14 @@ skolem:lemma10 a r:Inference;
         [ a r:Fact; r:gives {({
             {
                 :R a :Test.
-            } log:notIsomorphic {
-                _:sk_4 => false.
+            } log:equalTo {
+                {
+                    {
+                        :R a :Test.
+                    } => false.
+                } => false.
             }.
-        } {
+        } true {
             {
                 {
                     :R a :Test.
@@ -363,16 +351,6 @@ skolem:lemma10 a r:Inference;
                     :R a :Test.
                 } => false.
             }.
-        } {
-            {
-                :R a :Test.
-            } log:equalTo {
-                {
-                    {
-                        :R a :Test.
-                    } => false.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {true graph:list ()}]
     );
@@ -386,39 +364,34 @@ skolem:lemma10 a r:Inference;
         :R a :Test.
     }];
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ()];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_4"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test3.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         {
             :R a :Test.
         } => false.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo true];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true];
     r:rule skolem:lemma11.
 
 skolem:lemma11 a r:Extraction;
     r:gives {
-        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6, var:x_7. {
+        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. {
             <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>.
             var:x_0 => false.
             var:x_0 graph:list var:x_1.
             var:x_1 list:select (var:x_2 var:x_3).
             ({
-                var:x_2 log:notIsomorphic {
+                var:x_2 log:equalTo {
                     var:x_4 => false.
                 }.
-            } {
-                var:x_5 log:equalTo {
+            } true {
+                var:x_4 log:equalTo {
                     var:x_2 => false.
                 }.
-            } {
-                var:x_2 log:equalTo {
-                    var:x_5 => false.
-                }.
-            }) log:ifThenElseIn var:x_6.
-            var:x_7 graph:list var:x_3.
+            }) log:ifThenElseIn var:x_5.
+            var:x_6 graph:list var:x_3.
         } => {
-            var:x_7 => var:x_5.
+            var:x_6 => var:x_4.
         }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
diff --git a/reasoning/nand/test4-proof.n3 b/reasoning/nand/test4-proof.n3
index a67d8587e..e4b809720 100644
--- a/reasoning/nand/test4-proof.n3
+++ b/reasoning/nand/test4-proof.n3
@@ -92,10 +92,12 @@ skolem:lemma6 a r:Inference;
                 {
                     :Q a :Test.
                 } => false.
-            } log:notIsomorphic {
-                _:sk_12 => false.
+            } log:equalTo {
+                {
+                    :Q a :Test.
+                } => false.
             }.
-        } {
+        } true {
             {
                 :Q a :Test.
             } log:equalTo {
@@ -105,16 +107,6 @@ skolem:lemma6 a r:Inference;
                     } => false.
                 } => false.
             }.
-        } {
-            {
-                {
-                    :Q a :Test.
-                } => false.
-            } log:equalTo {
-                {
-                    :Q a :Test.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test4.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {true graph:list ()}]
     );
@@ -134,12 +126,11 @@ skolem:lemma6 a r:Inference;
         } => false.
     }];
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ()];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test4.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_12"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test4.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         :Q a :Test.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo true];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true];
     r:rule skolem:lemma8.
 
 skolem:lemma7 a r:Inference;
@@ -287,27 +278,23 @@ skolem:lemma7 a r:Inference;
 
 skolem:lemma8 a r:Extraction;
     r:gives {
-        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6, var:x_7. {
+        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. {
             <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>.
             var:x_0 => false.
             var:x_0 graph:list var:x_1.
             var:x_1 list:select (var:x_2 var:x_3).
             ({
-                var:x_2 log:notIsomorphic {
+                var:x_2 log:equalTo {
                     var:x_4 => false.
                 }.
-            } {
-                var:x_5 log:equalTo {
+            } true {
+                var:x_4 log:equalTo {
                     var:x_2 => false.
                 }.
-            } {
-                var:x_2 log:equalTo {
-                    var:x_5 => false.
-                }.
-            }) log:ifThenElseIn var:x_6.
-            var:x_7 graph:list var:x_3.
+            }) log:ifThenElseIn var:x_5.
+            var:x_6 graph:list var:x_3.
         } => {
-            var:x_7 => var:x_5.
+            var:x_6 => var:x_4.
         }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
@@ -533,10 +520,12 @@ skolem:lemma10 a r:Inference;
                 {
                     :Q a :Test.
                 } => false.
-            } log:notIsomorphic {
-                _:sk_3 => false.
+            } log:equalTo {
+                {
+                    :Q a :Test.
+                } => false.
             }.
-        } {
+        } true {
             {
                 :Q a :Test.
             } log:equalTo {
@@ -546,16 +535,6 @@ skolem:lemma10 a r:Inference;
                     } => false.
                 } => false.
             }.
-        } {
-            {
-                {
-                    :Q a :Test.
-                } => false.
-            } log:equalTo {
-                {
-                    :Q a :Test.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test4.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {{
             :R a :Test.
@@ -584,12 +563,11 @@ skolem:lemma10 a r:Inference;
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({
         :R a :Test.
     })];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test4.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_3"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test4.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         :Q a :Test.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo {
         :R a :Test.
     }];
     r:rule skolem:lemma8.
@@ -671,10 +649,12 @@ skolem:lemma12 a r:Inference;
                 {
                     :Q a :Test.
                 } => false.
-            } log:notIsomorphic {
-                _:sk_1 => false.
+            } log:equalTo {
+                {
+                    :Q a :Test.
+                } => false.
             }.
-        } {
+        } true {
             {
                 :Q a :Test.
             } log:equalTo {
@@ -684,16 +664,6 @@ skolem:lemma12 a r:Inference;
                     } => false.
                 } => false.
             }.
-        } {
-            {
-                {
-                    :Q a :Test.
-                } => false.
-            } log:equalTo {
-                {
-                    :Q a :Test.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test4.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {{
             :P a :Test.
@@ -722,12 +692,11 @@ skolem:lemma12 a r:Inference;
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ({
         :P a :Test.
     })];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test4.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_1"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test4.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         :Q a :Test.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo {
         :P a :Test.
     }];
     r:rule skolem:lemma8.
diff --git a/reasoning/nand/test5-proof.n3 b/reasoning/nand/test5-proof.n3
index 3a3283578..cc3a320f7 100644
--- a/reasoning/nand/test5-proof.n3
+++ b/reasoning/nand/test5-proof.n3
@@ -196,10 +196,14 @@ skolem:lemma6 a r:Inference;
         [ a r:Fact; r:gives {({
             {
                 :R a :Test.
-            } log:notIsomorphic {
-                _:sk_3 => false.
+            } log:equalTo {
+                {
+                    {
+                        :R a :Test.
+                    } => false.
+                } => false.
             }.
-        } {
+        } true {
             {
                 {
                     :R a :Test.
@@ -209,16 +213,6 @@ skolem:lemma6 a r:Inference;
                     :R a :Test.
                 } => false.
             }.
-        } {
-            {
-                :R a :Test.
-            } log:equalTo {
-                {
-                    {
-                        :R a :Test.
-                    } => false.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test5.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {true graph:list ()}]
     );
@@ -232,14 +226,13 @@ skolem:lemma6 a r:Inference;
         :R a :Test.
     }];
     r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ()];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test5.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_3"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test5.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         {
             :R a :Test.
         } => false.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo true];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo true];
     r:rule skolem:lemma9.
 
 skolem:lemma7 a r:Inference;
@@ -297,10 +290,12 @@ skolem:lemma7 a r:Inference;
                 {
                     :R a :Test.
                 } => false.
-            } log:notIsomorphic {
-                _:sk_2 => false.
+            } log:equalTo {
+                {
+                    :R a :Test.
+                } => false.
             }.
-        } {
+        } true {
             {
                 :R a :Test.
             } log:equalTo {
@@ -310,16 +305,6 @@ skolem:lemma7 a r:Inference;
                     } => false.
                 } => false.
             }.
-        } {
-            {
-                {
-                    :R a :Test.
-                } => false.
-            } log:equalTo {
-                {
-                    :R a :Test.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test5.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {{
             :P a :Test.
@@ -356,12 +341,11 @@ skolem:lemma7 a r:Inference;
     } {
         :Q a :Test.
     })];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test5.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_2"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test5.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         :R a :Test.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo {
         :P a :Test.
         :Q a :Test.
     }];
@@ -400,27 +384,23 @@ skolem:lemma8 a r:Extraction;
 
 skolem:lemma9 a r:Extraction;
     r:gives {
-        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6, var:x_7. {
+        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. {
             <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>.
             var:x_0 => false.
             var:x_0 graph:list var:x_1.
             var:x_1 list:select (var:x_2 var:x_3).
             ({
-                var:x_2 log:notIsomorphic {
+                var:x_2 log:equalTo {
                     var:x_4 => false.
                 }.
-            } {
-                var:x_5 log:equalTo {
+            } true {
+                var:x_4 log:equalTo {
                     var:x_2 => false.
                 }.
-            } {
-                var:x_2 log:equalTo {
-                    var:x_5 => false.
-                }.
-            }) log:ifThenElseIn var:x_6.
-            var:x_7 graph:list var:x_3.
+            }) log:ifThenElseIn var:x_5.
+            var:x_6 graph:list var:x_3.
         } => {
-            var:x_7 => var:x_5.
+            var:x_6 => var:x_4.
         }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].
diff --git a/reasoning/nand/test6-proof.n3 b/reasoning/nand/test6-proof.n3
index 264de9168..b85a9d158 100644
--- a/reasoning/nand/test6-proof.n3
+++ b/reasoning/nand/test6-proof.n3
@@ -122,10 +122,14 @@ skolem:lemma8 a r:Inference;
         [ a r:Fact; r:gives {({
             {
                 :P a :Test.
-            } log:notIsomorphic {
-                _:sk_0 => false.
+            } log:equalTo {
+                {
+                    {
+                        :P a :Test.
+                    } => false.
+                } => false.
             }.
-        } {
+        } true {
             {
                 {
                     :P a :Test.
@@ -135,16 +139,6 @@ skolem:lemma8 a r:Inference;
                     :P a :Test.
                 } => false.
             }.
-        } {
-            {
-                :P a :Test.
-            } log:equalTo {
-                {
-                    {
-                        :P a :Test.
-                    } => false.
-                } => false.
-            }.
         }) log:ifThenElseIn ((<https://eyereasoner.github.io/eye/reasoning/nand/test6.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)}]
         [ a r:Fact; r:gives {{
             :Q a :Test.
@@ -175,14 +169,13 @@ skolem:lemma8 a r:Inference;
     } {
         :R a :Test.
     })];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test6.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo ((<https://eyereasoner.github.io/eye/reasoning/nand/test6.n3> <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>) 1)];
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo {
         {
             :P a :Test.
         } => false.
     }];
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo {
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo {
         :Q a :Test.
         :R a :Test.
     }];
@@ -190,27 +183,23 @@ skolem:lemma8 a r:Inference;
 
 skolem:lemma9 a r:Extraction;
     r:gives {
-        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6, var:x_7. {
+        @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6. {
             <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand> log:equalTo <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3#nand>.
             var:x_0 => false.
             var:x_0 graph:list var:x_1.
             var:x_1 list:select (var:x_2 var:x_3).
             ({
-                var:x_2 log:notIsomorphic {
+                var:x_2 log:equalTo {
                     var:x_4 => false.
                 }.
-            } {
-                var:x_5 log:equalTo {
+            } true {
+                var:x_4 log:equalTo {
                     var:x_2 => false.
                 }.
-            } {
-                var:x_2 log:equalTo {
-                    var:x_5 => false.
-                }.
-            }) log:ifThenElseIn var:x_6.
-            var:x_7 graph:list var:x_3.
+            }) log:ifThenElseIn var:x_5.
+            var:x_6 graph:list var:x_3.
         } => {
-            var:x_7 => var:x_5.
+            var:x_6 => var:x_4.
         }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/nand/nand.n3>].