From ddfd17de01901609273b88eb6bb90b7da07b92ed Mon Sep 17 00:00:00 2001
From: josd <josderoo@gmail.com>
Date: Thu, 12 Dec 2024 21:19:41 +0100
Subject: [PATCH] refreshing

---
 .../proof-by-contrapositive/example2-proof.n3 | 33 +++++++++++++------
 reasoning/proof-by-contrapositive/example2.n3 |  2 +-
 2 files changed, 24 insertions(+), 11 deletions(-)

diff --git a/reasoning/proof-by-contrapositive/example2-proof.n3 b/reasoning/proof-by-contrapositive/example2-proof.n3
index 872093e46..33432a2ed 100644
--- a/reasoning/proof-by-contrapositive/example2-proof.n3
+++ b/reasoning/proof-by-contrapositive/example2-proof.n3
@@ -26,15 +26,8 @@ skolem:lemma2 a r:Inference;
         :ground :is :wet.
     };
     r:evidence (
-        [ a r:Fact; r:gives {{
-            {
-                :ground :is :wet.
-            } => false.
-        } => false}]
+        [ a r:Fact; r:gives true]
     );
-    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo {
-        :ground :is :wet.
-    }];
     r:rule skolem:lemma4.
 
 skolem:lemma3 a r:Extraction;
@@ -47,13 +40,33 @@ skolem:lemma3 a r:Extraction;
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example2-query.n3>].
 
-skolem:lemma4 a r:Extraction;
+skolem:lemma4 a r:Inference;
+    r:gives {
+        true => {
+            :ground :is :wet.
+        }.
+    };
+    r:evidence (
+        [ a r:Fact; r:gives {{
+            {
+                :ground :is :wet.
+            } => false.
+        } => false}]
+    );
+    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo {
+        :ground :is :wet.
+    }];
+    r:rule skolem:lemma5.
+
+skolem:lemma5 a r:Extraction;
     r:gives {
         @forAll var:x_0. {
             {
                 var:x_0 => false.
             } => false.
-        } => var:x_0.
+        } => {
+            true => var:x_0.
+        }.
     };
     r:because [ a r:Parsing; r:source <https://eyereasoner.github.io/eye/reasoning/proof-by-contrapositive/example2.n3>].
 
diff --git a/reasoning/proof-by-contrapositive/example2.n3 b/reasoning/proof-by-contrapositive/example2.n3
index 8508ff48d..828925517 100644
--- a/reasoning/proof-by-contrapositive/example2.n3
+++ b/reasoning/proof-by-contrapositive/example2.n3
@@ -5,4 +5,4 @@
 { { :ground :is :wet } => false } => false.
 
 # proof by contrapositive
-{ { ?P => false } => false } => ?P.
+{ { ?P => false } => false } => { true => ?P }.