#Processed by $Id: euler.yap 2905 2009-06-12 19:09:32Z josd $

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
@prefix : <http://eulersharp.sourceforge.net/2007/07test/socrates#>.
@prefix var: <http://localhost/var#>.
@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
@prefix n3: <http://www.w3.org/2004/06/rei#>.

[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :Human}; r:evidence (
  [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
  r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Human"]];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1. {var:x0 a var:x1} => {var:x0 a var:x1}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:component [ a r:Inference; r:gives {:socrates a :NonFemale}; r:evidence (
  [ a r:Extraction; r:gives {:socrates a :NonFemale}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
  r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#NonFemale"]];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1. {var:x0 a var:x1} => {var:x0 a var:x1}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:component [ a r:Inference; r:gives {:socrates a :MaleOrFemale}; r:evidence (
  [ a r:Inference; r:gives {:socrates a :MaleOrFemale}; r:evidence (
   [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]
   [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]);
   r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Human"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#MaleOrFemale"]];
   r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a var:x1. var:x1 rdfs:subClassOf var:x2} => {var:x0 a var:x2}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
  r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#MaleOrFemale"]];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1. {var:x0 a var:x1} => {var:x0 a var:x1}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:gives {
  :socrates a :Human.
  :socrates a :NonFemale.
  :socrates a :MaleOrFemale.
 }].

[ e:falseModel {:socrates a :Female}
; e:because [ e:integrityConstraint {{:socrates a :NonFemale. :NonFemale owl:disjointWith :Female. :socrates a :Female} => false}
  ; e:selected [ e:triple {:socrates a :NonFemale}
    ; e:falseAncestors true
    ; e:falseDescendents true
    ]
  ; e:selected [ e:triple {:NonFemale owl:disjointWith :Female}
    ; e:falseAncestors true
    ; e:falseDescendents true
    ]
  ; e:selected [ e:triple {:socrates a :Female}
    ; e:falseAncestors true
    ; e:falseDescendents true
    ]
  ]
; r:gives {
[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :Female}; r:evidence (
  [ a r:Inference; r:gives {:socrates a :Female}; r:evidence (
   [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]
   [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]
   [ a r:Extraction; r:gives {:MaleOrFemale owl:unionOf (:Female :Male)}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]);
   r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Human"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#MaleOrFemale"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Female"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Male"]];
   r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 a var:x1. var:x1 rdfs:subClassOf var:x2. var:x2 owl:unionOf (var:x3 var:x4)} => ({var:x0 a var:x3} {var:x0 a var:x4})!e:disjunction}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
  r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Female"]];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1. {var:x0 a var:x1} => {var:x0 a var:x1}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:component [ a r:Inference; r:gives {:socrates a :Mortal}; r:evidence (
  [ a r:Inference; r:gives {:socrates a :Mortal}; r:evidence (
   [ a r:Inference; r:gives {:socrates a :Female}; r:evidence (
    [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]
    [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]
    [ a r:Extraction; r:gives {:MaleOrFemale owl:unionOf (:Female :Male)}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]);
    r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
    r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Human"]];
    r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#MaleOrFemale"]];
    r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Female"]];
    r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Male"]];
    r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 a var:x1. var:x1 rdfs:subClassOf var:x2. var:x2 owl:unionOf (var:x3 var:x4)} => ({var:x0 a var:x3} {var:x0 a var:x4})!e:disjunction}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]]
   [ a r:Extraction; r:gives {:Female rdfs:subClassOf :Mortal}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]);
   r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Female"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Mortal"]];
   r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a var:x1. var:x1 rdfs:subClassOf var:x2} => {var:x0 a var:x2}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
  r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Mortal"]];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1. {var:x0 a var:x1} => {var:x0 a var:x1}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:component [ a r:Inference; r:gives {{:socrates a :Mortal} e:allAncestors {:socrates a :Female. :socrates a :Human. :Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf (:Female :Male). :Female rdfs:subClassOf :Mortal}}; r:evidence (
  [ a r:Fact; r:gives {{:socrates a :Mortal} e:allAncestors {:socrates a :Female. :socrates a :Human. :Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf (:Female :Male). :Female rdfs:subClassOf :Mortal}}]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo {:socrates a :Female. :socrates a :Human. :Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf (:Female :Male). :Female rdfs:subClassOf :Mortal}];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0. {{:socrates a :Mortal} e:allAncestors var:x0} => {{:socrates a :Mortal} e:allAncestors var:x0}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:component [ a r:Inference; r:gives {{:socrates a :Mortal} e:allDescendents true}; r:evidence (
  [ a r:Fact; r:gives {{:socrates a :Mortal} e:allDescendents true}]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo true];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0. {{:socrates a :Mortal} e:allDescendents var:x0} => {{:socrates a :Mortal} e:allDescendents var:x0}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:gives {
  :socrates a :Female.
  :socrates a :Mortal.
  {:socrates a :Mortal} e:allAncestors {:socrates a :Female. :socrates a :Human. :Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf (:Female :Male). :Female rdfs:subClassOf :Mortal}.
  {:socrates a :Mortal} e:allDescendents true.
 }].

}].

[ e:possibleModel {:socrates a :Male}
; r:gives {
[ a r:Proof, r:Conjunction;
 r:component [ a r:Inference; r:gives {:socrates a :Male}; r:evidence (
  [ a r:Inference; r:gives {:socrates a :Male}; r:evidence (
   [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]
   [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]
   [ a r:Extraction; r:gives {:MaleOrFemale owl:unionOf (:Female :Male)}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]);
   r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Human"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#MaleOrFemale"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Female"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Male"]];
   r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 a var:x1. var:x1 rdfs:subClassOf var:x2. var:x2 owl:unionOf (var:x3 var:x4)} => ({var:x0 a var:x3} {var:x0 a var:x4})!e:disjunction}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
  r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Male"]];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1. {var:x0 a var:x1} => {var:x0 a var:x1}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:component [ a r:Inference; r:gives {:socrates a :Mortal}; r:evidence (
  [ a r:Inference; r:gives {:socrates a :Mortal}; r:evidence (
   [ a r:Inference; r:gives {:socrates a :Male}; r:evidence (
    [ a r:Extraction; r:gives {:socrates a :Human}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]
    [ a r:Extraction; r:gives {:Human rdfs:subClassOf :MaleOrFemale}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]
    [ a r:Extraction; r:gives {:MaleOrFemale owl:unionOf (:Female :Male)}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]);
    r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
    r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Human"]];
    r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#MaleOrFemale"]];
    r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Female"]];
    r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Male"]];
    r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 a var:x1. var:x1 rdfs:subClassOf var:x2. var:x2 owl:unionOf (var:x3 var:x4)} => ({var:x0 a var:x3} {var:x0 a var:x4})!e:disjunction}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]]
   [ a r:Extraction; r:gives {:Male rdfs:subClassOf :Mortal}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]);
   r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Male"]];
   r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Mortal"]];
   r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a var:x1. var:x1 rdfs:subClassOf var:x2} => {var:x0 a var:x2}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socrates.n3>]]]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#socrates"]];
  r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/socrates#Mortal"]];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1. {var:x0 a var:x1} => {var:x0 a var:x1}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:component [ a r:Inference; r:gives {{:socrates a :Mortal} e:allAncestors {:socrates a :Male. :socrates a :Human. :Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf (:Female :Male). :Male rdfs:subClassOf :Mortal}}; r:evidence (
  [ a r:Fact; r:gives {{:socrates a :Mortal} e:allAncestors {:socrates a :Male. :socrates a :Human. :Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf (:Female :Male). :Male rdfs:subClassOf :Mortal}}]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo {:socrates a :Male. :socrates a :Human. :Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf (:Female :Male). :Male rdfs:subClassOf :Mortal}];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0. {{:socrates a :Mortal} e:allAncestors var:x0} => {{:socrates a :Mortal} e:allAncestors var:x0}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:component [ a r:Inference; r:gives {{:socrates a :Mortal} e:allDescendents true}; r:evidence (
  [ a r:Fact; r:gives {{:socrates a :Mortal} e:allDescendents true}]);
  r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo true];
  r:rule [ a r:Extraction; r:gives {@forAll var:x0. {{:socrates a :Mortal} e:allDescendents var:x0} => {{:socrates a :Mortal} e:allDescendents var:x0}}; r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2007/07test/socratesQ.n3>]]];

 r:gives {
  :socrates a :Male.
  :socrates a :Mortal.
  {:socrates a :Mortal} e:allAncestors {:socrates a :Male. :socrates a :Human. :Human rdfs:subClassOf :MaleOrFemale. :MaleOrFemale owl:unionOf (:Female :Male). :Male rdfs:subClassOf :Mortal}.
  {:socrates a :Mortal} e:allDescendents true.
 }].

}].

#ENDS 48 msec
#Trunk : 16/24 = 66.6666666666667 %
#Branch: 19/104 = 18.2692307692308 %