diff --git a/reasoning/4color/4color_answer.n3 b/reasoning/4color/4color_answer.n3 index d2b87d0bf..1b95fe0fb 100644 --- a/reasoning/4color/4color_answer.n3 +++ b/reasoning/4color/4color_answer.n3 @@ -1,3 +1,3 @@ @prefix : . -:mapEU :color ((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)). +:mapEU :color ((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)). diff --git a/reasoning/4color/4color_data.n3 b/reasoning/4color/4color_data.n3 index 3a830f3b0..c58627294 100644 --- a/reasoning/4color/4color_data.n3 +++ b/reasoning/4color/4color_data.n3 @@ -1,30 +1,30 @@ @prefix : . +# mapEU +:Belgium :neighbours (:France :Netherlands :Luxemburg :Germany). +:Netherlands :neighbours (:Belgium :Germany). +:Luxemburg :neighbours (:Belgium :France :Germany). +:France :neighbours (:Spain :Belgium :Luxemburg :Germany :Italy). +:Germany :neighbours (:Netherlands :Belgium :Luxemburg :Denmark :France :Austria :Poland :Czech_Republic). +:Italy :neighbours (:France :Austria :Slovenia). +:Denmark :neighbours (:Germany :Sweden). +:Ireland :neighbours (). +:Greece :neighbours (:Bulgaria :Cyprus). +:Spain :neighbours (:France :Portugal). +:Portugal :neighbours (:Spain). :Austria :neighbours (:Czech_Republic :Germany :Hungary :Italy :Slovenia :Slovakia). -:Belgium :neighbours (:France :Netherlands :Luxemburg :Germany :United_Kingdom). -:Bulgaria :neighbours (:Romania :Greece). -:Croatia :neighbours (:Slovenia :Hungary). +:Sweden :neighbours (:Finland :Denmark). +:Finland :neighbours (:Estonia :Sweden). :Cyprus :neighbours (:Greece). +:Malta :neighbours (). +:Poland :neighbours (:Germany :Czech_Republic :Slovakia :Lithuania). +:Hungary :neighbours (:Austria :Slovakia :Romania :Croatia :Slovenia). :Czech_Republic :neighbours (:Germany :Poland :Slovakia :Austria). -:Denmark :neighbours (:Germany :Sweden). +:Slovakia :neighbours (:Czech_Republic :Poland :Hungary :Austria). +:Slovenia :neighbours (:Austria :Italy :Hungary :Croatia). :Estonia :neighbours (:Finland :Latvia :Lithuania). -:Finland :neighbours (:Estonia :Sweden). -:France :neighbours (:Spain :Belgium :Luxemburg :Germany :Italy :United_Kingdom). -:Germany :neighbours (:Netherlands :Belgium :Luxemburg :Denmark :France :Austria :Poland :Czech_Republic). -:Greece :neighbours (:Bulgaria :Cyprus). -:Hungary :neighbours (:Austria :Slovakia :Romania :Croatia :Slovenia). -:Ireland :neighbours (:United_Kingdom). -:Italy :neighbours (:France :Austria :Slovenia). :Latvia :neighbours (:Estonia :Lithuania). :Lithuania :neighbours (:Estonia :Latvia :Poland). -:Luxemburg :neighbours (:Belgium :France :Germany). -:Malta :neighbours (). -:Netherlands :neighbours (:Belgium :Germany :United_Kingdom). -:Poland :neighbours (:Germany :Czech_Republic :Slovakia :Lithuania). -:Portugal :neighbours (:Spain). +:Bulgaria :neighbours (:Romania :Greece). :Romania :neighbours (:Hungary :Bulgaria). -:Slovakia :neighbours (:Czech_Republic :Poland :Hungary :Austria). -:Slovenia :neighbours (:Austria :Italy :Hungary :Croatia). -:Spain :neighbours (:France :Portugal). -:Sweden :neighbours (:Finland :Denmark). -:United_Kingdom :neighbours (:Ireland :Netherlands :Belgium :France). +:Croatia :neighbours (:Slovenia :Hungary). diff --git a/reasoning/4color/4color_proof.n3 b/reasoning/4color/4color_proof.n3 index 6c2d5d687..d56dfd247 100644 --- a/reasoning/4color/4color_proof.n3 +++ b/reasoning/4color/4color_proof.n3 @@ -9,27 +9,27 @@ skolem:proof a r:Proof, r:Conjunction; r:component skolem:lemma1; r:gives { - :mapEU :color ((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)). + :mapEU :color ((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)). }. skolem:lemma1 a r:Inference; r:gives { - :mapEU :color ((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)). + :mapEU :color ((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)). }; r:evidence ( skolem:lemma2 ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; r:rule skolem:lemma3. skolem:lemma2 a r:Inference; r:gives { - :mapEU :color ((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)). + :mapEU :color ((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)). }; r:evidence ( [ a r:Fact; r:gives {((_:sk_0 _:sk_1) { _:sk_0 :neighbours _:sk_2. - } ((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))) log:collectAllIn (( ) 1)}] + } ((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))) log:collectAllIn (( ) 1)}] skolem:lemma4 [ a r:Fact; r:gives {true log:callWithCut true}] ); @@ -37,7 +37,7 @@ skolem:lemma2 a r:Inference; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_1"]]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_2"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#mapEU"]]; r:rule skolem:lemma5. @@ -53,23 +53,23 @@ skolem:lemma3 a r:Extraction; skolem:lemma4 a r:Inference; r:gives { - ((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Austria :green) ((:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Belgium :yellow) ((:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma6 skolem:lemma7 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :yellow}] [ a r:Fact; r:gives {(1 { - ((:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Czech_Republic :Germany :Hungary :Italy :Slovenia :Slovakia) list:member _:sk_0. + ((:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :yellow). + (:France :Netherlands :Luxemburg :Germany) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Austria :green) (:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Austria"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Czech_Republic :Germany :Hungary :Italy :Slovenia :Slovakia)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Belgium :yellow) (:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Belgium"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#yellow"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:France :Netherlands :Luxemburg :Germany)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. @@ -90,30 +90,30 @@ skolem:lemma5 a r:Extraction; skolem:lemma6 a r:Inference; r:gives { - ((:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Belgium :yellow) ((:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Netherlands :green) ((:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma9 skolem:lemma10 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :yellow}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] [ a r:Fact; r:gives {(1 { - ((:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :yellow). - (:France :Netherlands :Luxemburg :Germany :United_Kingdom) list:member _:sk_0. + ((:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :green). + (:Belgium :Germany) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Belgium :yellow) (:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Belgium"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#yellow"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:France :Netherlands :Luxemburg :Germany :United_Kingdom)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Netherlands :green) (:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Netherlands"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Belgium :Germany)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma7 a r:Extraction; r:gives { - :Austria :neighbours (:Czech_Republic :Germany :Hungary :Italy :Slovenia :Slovakia). + :Belgium :neighbours (:France :Netherlands :Luxemburg :Germany). }; r:because [ a r:Parsing; r:source ]. @@ -136,138 +136,138 @@ skolem:lemma8 a r:Extraction; skolem:lemma9 a r:Inference; r:gives { - ((:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Bulgaria :green) ((:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Luxemburg :green) ((:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma11 skolem:lemma12 [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] [ a r:Fact; r:gives {(1 { - ((:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Romania :Greece) list:member _:sk_0. + ((:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :green). + (:Belgium :France :Germany) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Bulgaria :green) (:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Bulgaria"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Luxemburg :green) (:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Luxemburg"]]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Romania :Greece)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Belgium :France :Germany)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma10 a r:Extraction; r:gives { - :Belgium :neighbours (:France :Netherlands :Luxemburg :Germany :United_Kingdom). + :Netherlands :neighbours (:Belgium :Germany). }; r:because [ a r:Parsing; r:source ]. skolem:lemma11 a r:Inference; r:gives { - ((:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Croatia :green) ((:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:France :blue) ((:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma13 skolem:lemma14 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] [ a r:Fact; r:gives {(1 { - ((:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Slovenia :Hungary) list:member _:sk_0. + ((:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :blue). + (:Spain :Belgium :Luxemburg :Germany :Italy) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Croatia :green) (:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Croatia"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Slovenia :Hungary)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:France :blue) (:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#France"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Spain :Belgium :Luxemburg :Germany :Italy)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma12 a r:Extraction; r:gives { - :Bulgaria :neighbours (:Romania :Greece). + :Luxemburg :neighbours (:Belgium :France :Germany). }; r:because [ a r:Parsing; r:source ]. skolem:lemma13 a r:Inference; r:gives { - ((:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Cyprus :green) ((:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Germany :red) ((:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma15 skolem:lemma16 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Greece) list:member _:sk_0. + ((:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :red). + (:Netherlands :Belgium :Luxemburg :Denmark :France :Austria :Poland :Czech_Republic) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Cyprus :green) (:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Cyprus"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Greece)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Germany :red) (:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Germany"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Netherlands :Belgium :Luxemburg :Denmark :France :Austria :Poland :Czech_Republic)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma14 a r:Extraction; r:gives { - :Croatia :neighbours (:Slovenia :Hungary). + :France :neighbours (:Spain :Belgium :Luxemburg :Germany :Italy). }; r:because [ a r:Parsing; r:source ]. skolem:lemma15 a r:Inference; r:gives { - ((:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Czech_Republic :yellow) ((:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Italy :red) ((:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma17 skolem:lemma18 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :yellow}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :yellow). - (:Germany :Poland :Slovakia :Austria) list:member _:sk_0. + ((:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :red). + (:France :Austria :Slovenia) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Czech_Republic :yellow) (:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Czech_Republic"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#yellow"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Germany :Poland :Slovakia :Austria)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Italy :red) (:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Italy"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:France :Austria :Slovenia)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma16 a r:Extraction; r:gives { - :Cyprus :neighbours (:Greece). + :Germany :neighbours (:Netherlands :Belgium :Luxemburg :Denmark :France :Austria :Poland :Czech_Republic). }; r:because [ a r:Parsing; r:source ]. skolem:lemma17 a r:Inference; r:gives { - ((:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Denmark :green) ((:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Denmark :blue) ((:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma19 skolem:lemma20 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] [ a r:Fact; r:gives {(1 { - ((:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). + ((:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :blue). (:Germany :Sweden) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Denmark :green) (:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Denmark :blue) (:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Denmark"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Germany :Sweden)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; @@ -275,29 +275,29 @@ skolem:lemma17 a r:Inference; skolem:lemma18 a r:Extraction; r:gives { - :Czech_Republic :neighbours (:Germany :Poland :Slovakia :Austria). + :Italy :neighbours (:France :Austria :Slovenia). }; r:because [ a r:Parsing; r:source ]. skolem:lemma19 a r:Inference; r:gives { - ((:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Estonia :blue) ((:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Ireland :red) ((:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma21 skolem:lemma22 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :blue). - (:Finland :Latvia :Lithuania) list:member _:sk_0. + ((:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :red). + () list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Estonia :blue) (:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Estonia"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Finland :Latvia :Lithuania)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Ireland :red) (:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Ireland"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. @@ -310,600 +310,571 @@ skolem:lemma20 a r:Extraction; skolem:lemma21 a r:Inference; r:gives { - ((:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Finland :green) ((:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Greece :blue) ((:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma23 skolem:lemma24 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] [ a r:Fact; r:gives {(1 { - ((:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Estonia :Sweden) list:member _:sk_0. + ((:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :blue). + (:Bulgaria :Cyprus) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Finland :green) (:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Finland"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Estonia :Sweden)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Greece :blue) (:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Greece"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Bulgaria :Cyprus)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma22 a r:Extraction; r:gives { - :Estonia :neighbours (:Finland :Latvia :Lithuania). + :Ireland :neighbours (). }; r:because [ a r:Parsing; r:source ]. skolem:lemma23 a r:Inference; r:gives { - ((:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:France :green) ((:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Spain :green) ((:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma25 skolem:lemma26 [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] [ a r:Fact; r:gives {(1 { - ((:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Spain :Belgium :Luxemburg :Germany :Italy :United_Kingdom) list:member _:sk_0. + ((:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :green). + (:France :Portugal) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:France :green) (:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#France"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Spain :green) (:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Spain"]]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Spain :Belgium :Luxemburg :Germany :Italy :United_Kingdom)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:France :Portugal)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma24 a r:Extraction; r:gives { - :Finland :neighbours (:Estonia :Sweden). + :Greece :neighbours (:Bulgaria :Cyprus). }; r:because [ a r:Parsing; r:source ]. skolem:lemma25 a r:Inference; r:gives { - ((:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Germany :blue) ((:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Portugal :red) ((:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma27 skolem:lemma28 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :blue). - (:Netherlands :Belgium :Luxemburg :Denmark :France :Austria :Poland :Czech_Republic) list:member _:sk_0. + ((:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :red). + (:Spain) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Germany :blue) (:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Germany"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Netherlands :Belgium :Luxemburg :Denmark :France :Austria :Poland :Czech_Republic)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Portugal :red) (:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Portugal"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Spain)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma26 a r:Extraction; r:gives { - :France :neighbours (:Spain :Belgium :Luxemburg :Germany :Italy :United_Kingdom). + :Spain :neighbours (:France :Portugal). }; r:because [ a r:Parsing; r:source ]. skolem:lemma27 a r:Inference; r:gives { - ((:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Greece :red) ((:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Austria :yellow) ((:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma29 skolem:lemma30 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :yellow}] [ a r:Fact; r:gives {(1 { - ((:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :red). - (:Bulgaria :Cyprus) list:member _:sk_0. + ((:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :yellow). + (:Czech_Republic :Germany :Hungary :Italy :Slovenia :Slovakia) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Greece :red) (:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Greece"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Bulgaria :Cyprus)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Austria :yellow) (:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Austria"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#yellow"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Czech_Republic :Germany :Hungary :Italy :Slovenia :Slovakia)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma28 a r:Extraction; r:gives { - :Germany :neighbours (:Netherlands :Belgium :Luxemburg :Denmark :France :Austria :Poland :Czech_Republic). + :Portugal :neighbours (:Spain). }; r:because [ a r:Parsing; r:source ]. skolem:lemma29 a r:Inference; r:gives { - ((:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Hungary :blue) ((:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Sweden :green) ((:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma31 skolem:lemma32 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] [ a r:Fact; r:gives {(1 { - ((:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :blue). - (:Austria :Slovakia :Romania :Croatia :Slovenia) list:member _:sk_0. + ((:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :green). + (:Finland :Denmark) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Hungary :blue) (:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Hungary"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Austria :Slovakia :Romania :Croatia :Slovenia)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Sweden :green) (:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Sweden"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Finland :Denmark)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma30 a r:Extraction; r:gives { - :Greece :neighbours (:Bulgaria :Cyprus). + :Austria :neighbours (:Czech_Republic :Germany :Hungary :Italy :Slovenia :Slovakia). }; r:because [ a r:Parsing; r:source ]. skolem:lemma31 a r:Inference; r:gives { - ((:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Ireland :green) ((:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Finland :red) ((:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma33 skolem:lemma34 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:United_Kingdom) list:member _:sk_0. + ((:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :red). + (:Estonia :Sweden) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Ireland :green) (:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Ireland"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:United_Kingdom)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Finland :red) (:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Finland"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Estonia :Sweden)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma32 a r:Extraction; r:gives { - :Hungary :neighbours (:Austria :Slovakia :Romania :Croatia :Slovenia). + :Sweden :neighbours (:Finland :Denmark). }; r:because [ a r:Parsing; r:source ]. skolem:lemma33 a r:Inference; r:gives { - ((:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Italy :blue) ((:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Cyprus :red) ((:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma35 skolem:lemma36 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :blue). - (:France :Austria :Slovenia) list:member _:sk_0. + ((:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :red). + (:Greece) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Italy :blue) (:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Italy"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:France :Austria :Slovenia)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Cyprus :red) (:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Cyprus"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Greece)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma34 a r:Extraction; r:gives { - :Ireland :neighbours (:United_Kingdom). + :Finland :neighbours (:Estonia :Sweden). }; r:because [ a r:Parsing; r:source ]. skolem:lemma35 a r:Inference; r:gives { - ((:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Latvia :green) ((:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Malta :red) ((:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma37 skolem:lemma38 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Estonia :Lithuania) list:member _:sk_0. + ((:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :red). + () list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Latvia :green) (:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Latvia"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Estonia :Lithuania)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Malta :red) (:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Malta"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma36 a r:Extraction; r:gives { - :Italy :neighbours (:France :Austria :Slovenia). + :Cyprus :neighbours (:Greece). }; r:because [ a r:Parsing; r:source ]. skolem:lemma37 a r:Inference; r:gives { - ((:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Lithuania :red) ((:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Poland :blue) ((:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma39 skolem:lemma40 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] [ a r:Fact; r:gives {(1 { - ((:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :red). - (:Estonia :Latvia :Poland) list:member _:sk_0. + ((:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :blue). + (:Germany :Czech_Republic :Slovakia :Lithuania) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Lithuania :red) (:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Lithuania"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Estonia :Latvia :Poland)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Poland :blue) (:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Poland"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Germany :Czech_Republic :Slovakia :Lithuania)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma38 a r:Extraction; r:gives { - :Latvia :neighbours (:Estonia :Lithuania). + :Malta :neighbours (). }; r:because [ a r:Parsing; r:source ]. skolem:lemma39 a r:Inference; r:gives { - ((:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Luxemburg :red) ((:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Hungary :blue) ((:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma41 skolem:lemma42 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] [ a r:Fact; r:gives {(1 { - ((:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :red). - (:Belgium :France :Germany) list:member _:sk_0. + ((:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :blue). + (:Austria :Slovakia :Romania :Croatia :Slovenia) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Luxemburg :red) (:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Luxemburg"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Belgium :France :Germany)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Hungary :blue) (:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Hungary"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Austria :Slovakia :Romania :Croatia :Slovenia)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma40 a r:Extraction; r:gives { - :Lithuania :neighbours (:Estonia :Latvia :Poland). + :Poland :neighbours (:Germany :Czech_Republic :Slovakia :Lithuania). }; r:because [ a r:Parsing; r:source ]. skolem:lemma41 a r:Inference; r:gives { - ((:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Malta :red) ((:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Czech_Republic :green) ((:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma43 skolem:lemma44 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] [ a r:Fact; r:gives {(1 { - ((:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :red). - () list:member _:sk_0. + ((:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :green). + (:Germany :Poland :Slovakia :Austria) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Malta :red) (:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Malta"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo ()]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Czech_Republic :green) (:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Czech_Republic"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Germany :Poland :Slovakia :Austria)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma42 a r:Extraction; r:gives { - :Luxemburg :neighbours (:Belgium :France :Germany). + :Hungary :neighbours (:Austria :Slovakia :Romania :Croatia :Slovenia). }; r:because [ a r:Parsing; r:source ]. skolem:lemma43 a r:Inference; r:gives { - ((:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Netherlands :green) ((:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Slovakia :red) ((:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma45 skolem:lemma46 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Belgium :Germany :United_Kingdom) list:member _:sk_0. + ((:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :red). + (:Czech_Republic :Poland :Hungary :Austria) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Netherlands :green) (:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Netherlands"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Belgium :Germany :United_Kingdom)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Slovakia :red) (:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Slovakia"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Czech_Republic :Poland :Hungary :Austria)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma44 a r:Extraction; r:gives { - :Malta :neighbours (). + :Czech_Republic :neighbours (:Germany :Poland :Slovakia :Austria). }; r:because [ a r:Parsing; r:source ]. skolem:lemma45 a r:Inference; r:gives { - ((:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Poland :green) ((:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Slovenia :green) ((:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma47 skolem:lemma48 [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] [ a r:Fact; r:gives {(1 { - ((:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Germany :Czech_Republic :Slovakia :Lithuania) list:member _:sk_0. + ((:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :green). + (:Austria :Italy :Hungary :Croatia) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Poland :green) (:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Poland"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Slovenia :green) (:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Slovenia"]]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Germany :Czech_Republic :Slovakia :Lithuania)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Austria :Italy :Hungary :Croatia)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma46 a r:Extraction; r:gives { - :Netherlands :neighbours (:Belgium :Germany :United_Kingdom). + :Slovakia :neighbours (:Czech_Republic :Poland :Hungary :Austria). }; r:because [ a r:Parsing; r:source ]. skolem:lemma47 a r:Inference; r:gives { - ((:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Portugal :green) ((:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Estonia :blue) ((:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma49 skolem:lemma50 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :blue}] [ a r:Fact; r:gives {(1 { - ((:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :green). - (:Spain) list:member _:sk_0. + ((:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :blue). + (:Finland :Latvia :Lithuania) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Portugal :green) (:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Portugal"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Spain)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Estonia :blue) (:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Estonia"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#blue"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Finland :Latvia :Lithuania)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma48 a r:Extraction; r:gives { - :Poland :neighbours (:Germany :Czech_Republic :Slovakia :Lithuania). + :Slovenia :neighbours (:Austria :Italy :Hungary :Croatia). }; r:because [ a r:Parsing; r:source ]. skolem:lemma49 a r:Inference; r:gives { - ((:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Romania :red) ((:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Latvia :green) ((:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma51 skolem:lemma52 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] [ a r:Fact; r:gives {(1 { - ((:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :red). - (:Hungary :Bulgaria) list:member _:sk_0. + ((:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :green). + (:Estonia :Lithuania) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Romania :red) (:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Romania"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Hungary :Bulgaria)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Latvia :green) (:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Latvia"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Estonia :Lithuania)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma50 a r:Extraction; r:gives { - :Portugal :neighbours (:Spain). + :Estonia :neighbours (:Finland :Latvia :Lithuania). }; r:because [ a r:Parsing; r:source ]. skolem:lemma51 a r:Inference; r:gives { - ((:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Slovakia :red) ((:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Lithuania :red) ((:Bulgaria :green) (:Romania :red) (:Croatia :red)))}] skolem:lemma53 skolem:lemma54 [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :red). - (:Czech_Republic :Poland :Hungary :Austria) list:member _:sk_0. + ((:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:member (_:sk_0 :red). + (:Estonia :Latvia :Poland) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Slovakia :red) (:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Slovakia"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Lithuania :red) (:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Lithuania"]]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Czech_Republic :Poland :Hungary :Austria)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Estonia :Latvia :Poland)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma52 a r:Extraction; r:gives { - :Romania :neighbours (:Hungary :Bulgaria). + :Latvia :neighbours (:Estonia :Lithuania). }; r:because [ a r:Parsing; r:source ]. skolem:lemma53 a r:Inference; r:gives { - ((:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Bulgaria :green) (:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Slovenia :red) ((:Spain :red) (:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Bulgaria :green) (:Romania :red) (:Croatia :red)) list:firstRest ((:Bulgaria :green) ((:Romania :red) (:Croatia :red)))}] skolem:lemma55 skolem:lemma56 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] + [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :green}] [ a r:Fact; r:gives {(1 { - ((:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :red). - (:Austria :Italy :Hungary :Croatia) list:member _:sk_0. + ((:Romania :red) (:Croatia :red)) list:member (_:sk_0 :green). + (:Romania :Greece) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Slovenia :red) (:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Slovenia"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Austria :Italy :Hungary :Croatia)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Bulgaria :green) (:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Bulgaria"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#green"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Romania :Greece)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma54 a r:Extraction; r:gives { - :Slovakia :neighbours (:Czech_Republic :Poland :Hungary :Austria). + :Lithuania :neighbours (:Estonia :Latvia :Poland). }; r:because [ a r:Parsing; r:source ]. skolem:lemma55 a r:Inference; r:gives { - ((:Spain :red) (:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Romania :red) (:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Spain :red) (:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Spain :red) ((:Sweden :red) (:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Romania :red) (:Croatia :red)) list:firstRest ((:Romania :red) ((:Croatia :red)))}] skolem:lemma57 skolem:lemma58 [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { - ((:Sweden :red) (:United_Kingdom :red)) list:member (_:sk_0 :red). - (:France :Portugal) list:member _:sk_0. + ((:Croatia :red)) list:member (_:sk_0 :red). + (:Hungary :Bulgaria) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Spain :red) (:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Spain"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Romania :red) (:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Romania"]]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:France :Portugal)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Hungary :Bulgaria)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. skolem:lemma56 a r:Extraction; r:gives { - :Slovenia :neighbours (:Austria :Italy :Hungary :Croatia). + :Bulgaria :neighbours (:Romania :Greece). }; r:because [ a r:Parsing; r:source ]. skolem:lemma57 a r:Inference; r:gives { - ((:Sweden :red) (:United_Kingdom :red)) :places true. + ((:Croatia :red)) :places true. }; r:evidence ( - [ a r:Fact; r:gives {((:Sweden :red) (:United_Kingdom :red)) list:firstRest ((:Sweden :red) ((:United_Kingdom :red)))}] + [ a r:Fact; r:gives {((:Croatia :red)) list:firstRest ((:Croatia :red) ())}] skolem:lemma59 skolem:lemma60 [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] - [ a r:Fact; r:gives {(1 { - ((:United_Kingdom :red)) list:member (_:sk_0 :red). - (:Finland :Denmark) list:member _:sk_0. - } ()) log:collectAllIn (( ) 1)}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Sweden :red) (:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Sweden"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo ((:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Finland :Denmark)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; - r:rule skolem:lemma8. - -skolem:lemma58 a r:Extraction; - r:gives { - :Spain :neighbours (:France :Portugal). - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma59 a r:Inference; - r:gives { - ((:United_Kingdom :red)) :places true. - }; - r:evidence ( - [ a r:Fact; r:gives {((:United_Kingdom :red)) list:firstRest ((:United_Kingdom :red) ())}] - skolem:lemma61 - skolem:lemma62 - [ a r:Fact; r:gives {(:red :green :blue :yellow) list:member :red}] [ a r:Fact; r:gives {(1 { () list:member (_:sk_0 :red). - (:Ireland :Netherlands :Belgium :France) list:member _:sk_0. + (:Slovenia :Hungary) list:member _:sk_0. } ()) log:collectAllIn (( ) 1)}] ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:United_Kingdom :red))]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#United_Kingdom"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:Croatia :red))]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#Croatia"]]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/4color#red"]]; 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_4"]; r:boundTo (:Ireland :Netherlands :Belgium :France)]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo (:Slovenia :Hungary)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo (( ) 1)]; r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ a r:Existential; n3:nodeId "_:sk_0"]]; r:rule skolem:lemma8. -skolem:lemma60 a r:Extraction; +skolem:lemma58 a r:Extraction; r:gives { - :Sweden :neighbours (:Finland :Denmark). + :Romania :neighbours (:Hungary :Bulgaria). }; r:because [ a r:Parsing; r:source ]. -skolem:lemma61 a r:Inference; +skolem:lemma59 a r:Inference; r:gives { () :places true. }; r:evidence ( [ a r:Fact; r:gives true] ); - r:rule skolem:lemma63. + r:rule skolem:lemma61. -skolem:lemma62 a r:Extraction; +skolem:lemma60 a r:Extraction; r:gives { - :United_Kingdom :neighbours (:Ireland :Netherlands :Belgium :France). + :Croatia :neighbours (:Slovenia :Hungary). }; r:because [ a r:Parsing; r:source ]. -skolem:lemma63 a r:Extraction; +skolem:lemma61 a r:Extraction; r:gives { { () :places true.