#Processed by $Id: euler.yap 3213 2009-12-18 14:30:25Z josd $ @prefix ht: . @prefix dc: . @prefix cyc: . @prefix xsd: . @prefix log: . @prefix hs: . @prefix c: . @prefix rdf: . @prefix rdfs: . @prefix owl: . @prefix list: . @prefix str: . @prefix : . @prefix ns1: . @prefix var: . @prefix e: . @prefix r: . @prefix n3: . [ a r:Proof, r:Conjunction; r:component [ a r:Inference; r:gives { owl:differentFrom }; r:evidence ( [ a r:Inference; r:gives { owl:differentFrom }; r:evidence ( [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives {@forSome var:e5. var:e5}; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e5. var:e5}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e5"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e5. var:e5 xsd:date "2006-01-23"}; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives {@forSome var:e4. var:e4}; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e4. var:e4}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e4"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e4. var:e4 xsd:date "2008-05-16"}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {"2006-01-23" str:lessThan "2008-05-16"}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e5"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo "2006-01-23"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e4"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo "2008-05-16"]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5. {var:x0 var:x1. var:x1 xsd:date var:x2. var:x3 var:x4. var:x4 xsd:date var:x5. var:x2 str:lessThan var:x5} => {var:x0 var:x3}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { owl:propertyDisjointWith }; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives { c:says { . }}; r:evidence ( [ a r:Inference; r:gives { c:speaks_for }; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e3. var:e3 a }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives {@forSome var:e3. var:e3 }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives {@forSome var:e3. var:e3 }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e3"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a . var:x0 var:x1. var:x0 var:x2} => {var:x2 c:speaks_for var:x1}}; r:because [ a r:Parsing; r:source ]]] [ a r:Inference; r:gives { c:says { . }}; r:evidence ( [ a r:Inference; r:gives {@forSome var:e11. { . } var:e11 }; r:evidence ( [ a r:Inference; r:gives {{ . } hs:corresponds_to }; r:evidence ( [ a r:Inference; r:gives { c:controls_spo ({ . } hs:corresponds_to )}; r:evidence ( [ a r:Inference; r:gives { c:says {{ . } hs:corresponds_to }}; r:evidence ( [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Extraction; r:gives { ht:requests ()}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {() list:member }] [ a r:Extraction; r:gives { ht:methodName "GET"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:absoluteURI "http://example.org/1995/manifesto"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:resp }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:statusCodeNumber "200"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { hs:asEntity { . }}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo "http://example.org/1995/manifesto"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Q1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#A1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x6"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5, var:x6. {var:x0 log:uri var:x1. var:x2 ht:requests var:x3. var:x3 list:member var:x4. var:x4 ht:methodName "GET". var:x4 ht:absoluteURI var:x1. var:x4 ht:resp var:x5. var:x5 ht:statusCodeNumber "200". var:x5 hs:asEntity var:x6} => {var:x2 c:says {var:x6 hs:corresponds_to var:x0}}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { ht:connectionAuthority "example.org"}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Fact; r:gives {("http://example.org/1995/manifesto" "http://([^/]+)/") str:search ("example.org")}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo "example.org"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo "http://example.org/1995/manifesto"]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 c:says {var:x1 hs:corresponds_to var:x2}. var:x0 ht:connectionAuthority var:x3. var:x2 log:uri var:x4. (var:x4 "http://([^/]+)/") str:search (var:x3)} => {var:x0 c:controls_spo (var:x1 hs:corresponds_to var:x2)}}; r:because [ a r:Parsing; r:source ]]] [ a r:Inference; r:gives { c:says {{ . } hs:corresponds_to }}; r:evidence ( [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Extraction; r:gives { ht:requests ()}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {() list:member }] [ a r:Extraction; r:gives { ht:methodName "GET"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:absoluteURI "http://example.org/1995/manifesto"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:resp }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:statusCodeNumber "200"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { hs:asEntity { . }}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo "http://example.org/1995/manifesto"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Q1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#A1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x6"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5, var:x6. {var:x0 log:uri var:x1. var:x2 ht:requests var:x3. var:x3 list:member var:x4. var:x4 ht:methodName "GET". var:x4 ht:absoluteURI var:x1. var:x4 ht:resp var:x5. var:x5 ht:statusCodeNumber "200". var:x5 hs:asEntity var:x6} => {var:x2 c:says {var:x6 hs:corresponds_to var:x0}}}; r:because [ a r:Parsing; r:source ]]] [ a r:Fact; r:gives {{{ . } hs:corresponds_to } log:includes {{ . } hs:corresponds_to }}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/httpspeech#corresponds_to"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo {{ . } hs:corresponds_to }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 c:controls_spo (var:x1 var:x2 var:x3). var:x0 c:says var:x4. var:x4 log:includes {var:x1 var:x2 var:x3}} => {var:x1 var:x2 var:x3}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e11. hs:corresponds_to rdfs:subPropertyOf var:e11}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/httpspeech#corresponds_to"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e11"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e11. var:e11 owl:inverseOf c:says}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e11"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/speech#says"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 owl:inverseOf var:x3} => {var:x2 var:x3 var:x0}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 c:speaks_for var:x1. var:x0 c:says var:x2} => {var:x1 c:says var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Fact; r:gives {{ . } log:includes { }}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 c:says var:x1. var:x1 log:includes {var:x2 var:x3}} => {var:x0 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/perceives"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 var:x1 var:x2. var:x1 owl:propertyDisjointWith var:x3. var:x0 var:x3 var:x4} => {var:x2 owl:differentFrom var:x4}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0. {var:x0 owl:differentFrom var:x0} => {var:x0 owl:differentFrom var:x0}}; r:because [ a r:Parsing; r:source ]]]; r:component [ a r:Inference; r:gives { owl:differentFrom }; r:evidence ( [ a r:Inference; r:gives { owl:differentFrom }; r:evidence ( [ a r:Inference; r:gives { }; r:evidence ( [ a r:Extraction; r:gives { a owl:SymmetricProperty}; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives {@forSome var:e5. var:e5}; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e5. var:e5}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e5"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e5. var:e5 xsd:date "2006-01-23"}; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives {@forSome var:e4. var:e4}; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e4. var:e4}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e4"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e4. var:e4 xsd:date "2008-05-16"}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {"2006-01-23" str:lessThan "2008-05-16"}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e5"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo "2006-01-23"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e4"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo "2008-05-16"]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5. {var:x0 var:x1. var:x1 xsd:date var:x2. var:x3 var:x4. var:x4 xsd:date var:x5. var:x2 str:lessThan var:x5} => {var:x0 var:x3}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a owl:SymmetricProperty. var:x1 var:x0 var:x2} => {var:x2 var:x0 var:x1}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { owl:propertyDisjointWith }; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives { }; r:evidence ( [ a r:Extraction; r:gives { a owl:SymmetricProperty}; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives { c:says { . }}; r:evidence ( [ a r:Inference; r:gives { c:speaks_for }; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e3. var:e3 a }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives {@forSome var:e3. var:e3 }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives {@forSome var:e3. var:e3 }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e3"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a . var:x0 var:x1. var:x0 var:x2} => {var:x2 c:speaks_for var:x1}}; r:because [ a r:Parsing; r:source ]]] [ a r:Inference; r:gives { c:says { . }}; r:evidence ( [ a r:Inference; r:gives {@forSome var:e11. { . } var:e11 }; r:evidence ( [ a r:Inference; r:gives {{ . } hs:corresponds_to }; r:evidence ( [ a r:Inference; r:gives { c:controls_spo ({ . } hs:corresponds_to )}; r:evidence ( [ a r:Inference; r:gives { c:says {{ . } hs:corresponds_to }}; r:evidence ( [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Extraction; r:gives { ht:requests ()}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {() list:member }] [ a r:Extraction; r:gives { ht:methodName "GET"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:absoluteURI "http://example.org/1995/manifesto"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:resp }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:statusCodeNumber "200"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { hs:asEntity { . }}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo "http://example.org/1995/manifesto"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Q1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#A1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x6"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5, var:x6. {var:x0 log:uri var:x1. var:x2 ht:requests var:x3. var:x3 list:member var:x4. var:x4 ht:methodName "GET". var:x4 ht:absoluteURI var:x1. var:x4 ht:resp var:x5. var:x5 ht:statusCodeNumber "200". var:x5 hs:asEntity var:x6} => {var:x2 c:says {var:x6 hs:corresponds_to var:x0}}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { ht:connectionAuthority "example.org"}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Fact; r:gives {("http://example.org/1995/manifesto" "http://([^/]+)/") str:search ("example.org")}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo "example.org"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo "http://example.org/1995/manifesto"]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 c:says {var:x1 hs:corresponds_to var:x2}. var:x0 ht:connectionAuthority var:x3. var:x2 log:uri var:x4. (var:x4 "http://([^/]+)/") str:search (var:x3)} => {var:x0 c:controls_spo (var:x1 hs:corresponds_to var:x2)}}; r:because [ a r:Parsing; r:source ]]] [ a r:Inference; r:gives { c:says {{ . } hs:corresponds_to }}; r:evidence ( [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Extraction; r:gives { ht:requests ()}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {() list:member }] [ a r:Extraction; r:gives { ht:methodName "GET"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:absoluteURI "http://example.org/1995/manifesto"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:resp }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:statusCodeNumber "200"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { hs:asEntity { . }}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo "http://example.org/1995/manifesto"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Q1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#A1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x6"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5, var:x6. {var:x0 log:uri var:x1. var:x2 ht:requests var:x3. var:x3 list:member var:x4. var:x4 ht:methodName "GET". var:x4 ht:absoluteURI var:x1. var:x4 ht:resp var:x5. var:x5 ht:statusCodeNumber "200". var:x5 hs:asEntity var:x6} => {var:x2 c:says {var:x6 hs:corresponds_to var:x0}}}; r:because [ a r:Parsing; r:source ]]] [ a r:Fact; r:gives {{{ . } hs:corresponds_to } log:includes {{ . } hs:corresponds_to }}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/httpspeech#corresponds_to"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo {{ . } hs:corresponds_to }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 c:controls_spo (var:x1 var:x2 var:x3). var:x0 c:says var:x4. var:x4 log:includes {var:x1 var:x2 var:x3}} => {var:x1 var:x2 var:x3}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e11. hs:corresponds_to rdfs:subPropertyOf var:e11}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/httpspeech#corresponds_to"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e11"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e11. var:e11 owl:inverseOf c:says}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e11"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/speech#says"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 owl:inverseOf var:x3} => {var:x2 var:x3 var:x0}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 c:speaks_for var:x1. var:x0 c:says var:x2} => {var:x1 c:says var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Fact; r:gives {{ . } log:includes { }}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 c:says var:x1. var:x1 log:includes {var:x2 var:x3}} => {var:x0 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/perceives"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a owl:SymmetricProperty. var:x1 var:x0 var:x2} => {var:x2 var:x0 var:x1}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 var:x1 var:x2. var:x1 owl:propertyDisjointWith var:x3. var:x0 var:x3 var:x4} => {var:x2 owl:differentFrom var:x4}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/badmeta.n3#Bob"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0. {var:x0 owl:differentFrom var:x0} => {var:x0 owl:differentFrom var:x0}}; r:because [ a r:Parsing; r:source ]]]; r:gives { owl:differentFrom . owl:differentFrom . }]. #ENDS 76 msec #Trunk : 170/2940 = 5.78231292517007 % #Branch: 21/4197 = 0.50035739814153 % --=_mixed 00536508C1257690_Content-Type: text/plain; name="att2.txt" Content-Disposition: attachment; filename="att2.txt" Content-Transfer-Encoding: quoted-printable .. list-table:: Proof :widths: 2 70 20 20 :header-rows: 1 * - Step - Formula - Justification - Bindings * - 1 - ... - parsing - * - 2 - @forSome :e5 . :e5 . - erasure from step 1 - * - 3 - ... - parsing - * - 4 - :subPropertyOf . - erasure from step 3 - * - 5 - ... - parsing - * - 6 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 5 - * - 7 - @forSome :e5 . :e5 . - rule from step 6 applied to steps (2, 4) - {'x2': '[...]', 'x3': u'', 'x0': u'', 'x1': u''} * - 8 - ... - parsing - * - 9 - @forSome :e5 . :e5 xsd:date "2006-01-23" . - erasure from step 8 - * - 10 - ... - parsing - * - 11 - @forSome :e4 . :e4 . - erasure from step 10 - * - 12 - ... - parsing - * - 13 - :subPropertyOf . - erasure from step 12 - * - 14 - ... - parsing - * - 15 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 14 - * - 16 - @forSome :e4 . :e4 . - rule from step 15 applied to steps (11, 13) - {'x2': '[...]', 'x3': u'', 'x0': u'', 'x1': u''} * - 17 - ... - parsing - * - 18 - @forSome :e4 . :e4 xsd:date "2008-05-16" . - erasure from step 17 - * - 19 - "2006-01-23" :lessThan "2008-05-16" . - built-in Axiom str:lessThan - * - 20 - ... - parsing - * - 21 - @forAll :x0, :x1, :x2, :x3, :x4, :x5 . { :x0 :x1 . :x1 xsd:date :x2 . :x2 str:lessThan :x5 . :x3 :x4 . :x4 xsd:date :x5 . } log:implies {:x0 :x3 . } . - erasure from step 20 - * - 22 - :Bob . - rule from step 21 applied to steps (7, 9, 16, 18, 19) - {'x2': '"2006...1-23"', 'x3': u'', 'x0': u'', 'x1': '[...]', 'x4': '[...]', 'x5': '"2008...5-16"'} * - 23 - ... - parsing - * - 24 - :propertyDisjointWith . - erasure from step 23 - * - 25 - ... - parsing - * - 26 - @forSome :e3 . :e3 a . - erasure from step 25 - * - 27 - ... - parsing - * - 28 - @forSome :e3 . :e3 . - erasure from step 27 - * - 29 - ... - parsing - * - 30 - @forSome :e3 . :e3 . - erasure from step 29 - * - 31 - ... - parsing - * - 32 - @forAll :x0, :x1, :x2 . { :x0 a ; :x2; :x1 . } log:implies {:x2 c:speaks_for :x1 . } . - erasure from step 31 - * - 33 - c:speaks_for :Bob . - rule from step 32 applied to steps (26, 28, 30) - {'x2': u'', 'x0': '[...]', 'x1': u''} * - 34 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 35 - ... - parsing - * - 36 - :C1 ht:requests ( :Q1 ) . - erasure from step 35 - * - 37 - ( :Q1 ) list:member :Q1 . - built-in Axiom list:member - * - 38 - ... - parsing - * - 39 - :Q1 ht:methodName "GET" . - erasure from step 38 - * - 40 - ... - parsing - * - 41 - :Q1 ht:absoluteURI "http://example.org/1995/manifesto" . - erasure from step 40 - * - 42 - ... - parsing - * - 43 - :Q1 ht:resp :A1 . - erasure from step 42 - * - 44 - ... - parsing - * - 45 - :A1 ht:statusCodeNumber "200" . - erasure from step 44 - * - 46 - ... - parsing - * - 47 - :A1 hs:asEntity { :Bob . . } . - erasure from step 46 - * - 48 - ... - parsing - * - 49 - @forAll :x0, :x1, :x2, :x3, :x4, :x5, :x6 . { :x0 log:uri :x1 . :x2 ht:requests :x3 . :x3 list:member :x4 . :x4 ht:absoluteURI :x1; ht:methodName "GET"; ht:resp :x5 . :x5 hs:asEntity :x6; ht:statusCodeNumber "200" . } log:implies {:x2 c:says {:x6 hs:corresponds_to :x0 . } . } . - erasure from step 48 - * - 50 - :C1 c:says {{ :Bob . . } hs:corresponds_to . } . - rule from step 49 applied to steps (34, 36, 37, 39, 41, 43, 45, 47) - {'x2': u'', 'x3': '?', 'x0': u'', 'x1': '"http...esto"', 'x6': '{2}', 'x4': u'', 'x5': u''} * - 51 - ... - parsing - * - 52 - :C1 ht:connectionAuthority "example.org" . - erasure from step 51 - * - 53 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 54 - ( "http://example.org/1995/manifesto" "http://([^/]+)/" ) :search ( "example.org" ) . - built-in Axiom str:search - * - 55 - ... - parsing - * - 56 - @forAll :x0, :x1, :x2, :x3, :x4 . { ( :x4 "http://([^/]+)/" ) str:search ( :x3 ) . :x0 c:says {:x1 hs:corresponds_to :x2 . }; ht:connectionAuthority :x3 . :x2 log:uri :x4 . } log:implies {:x0 c:controls_spo ( :x1 hs:corresponds_to :x2 ) . } . - erasure from step 55 - * - 57 - :C1 c:controls_spo ( { :Bob . . } hs:corresponds_to ) . - rule from step 56 applied to steps (50, 52, 53, 54) - {'x2': u'', 'x3': '"exam....org"', 'x0': u'', 'x1': '{2}', 'x4': '"http...esto"'} * - 58 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 59 - ... - parsing - * - 60 - :C1 ht:requests ( :Q1 ) . - erasure from step 59 - * - 61 - ( :Q1 ) list:member :Q1 . - built-in Axiom list:member - * - 62 - ... - parsing - * - 63 - :Q1 ht:methodName "GET" . - erasure from step 62 - * - 64 - ... - parsing - * - 65 - :Q1 ht:absoluteURI "http://example.org/1995/manifesto" . - erasure from step 64 - * - 66 - ... - parsing - * - 67 - :Q1 ht:resp :A1 . - erasure from step 66 - * - 68 - ... - parsing - * - 69 - :A1 ht:statusCodeNumber "200" . - erasure from step 68 - * - 70 - ... - parsing - * - 71 - :A1 hs:asEntity { :Bob . . } . - erasure from step 70 - * - 72 - ... - parsing - * - 73 - @forAll :x0, :x1, :x2, :x3, :x4, :x5, :x6 . { :x0 log:uri :x1 . :x2 ht:requests :x3 . :x3 list:member :x4 . :x4 ht:absoluteURI :x1; ht:methodName "GET"; ht:resp :x5 . :x5 hs:asEntity :x6; ht:statusCodeNumber "200" . } log:implies {:x2 c:says {:x6 hs:corresponds_to :x0 . } . } . - erasure from step 72 - * - 74 - :C1 c:says {{ :Bob . . } hs:corresponds_to . } . - rule from step 73 applied to steps (58, 60, 61, 63, 65, 67, 69, 71) - {'x2': u'', 'x3': '?', 'x0': u'', 'x1': '"http...esto"', 'x6': '{2}', 'x4': u'', 'x5': u''} * - 75 - { { :Bob . . } hs:corresponds_to . } log:includes {{ :Bob . . } hs:corresponds_to . } . - built-in Axiom log:includes - * - 76 - ... - parsing - * - 77 - @forAll :x0, :x1, :x2, :x3, :x4 . { :x0 c:controls_spo ( :x1 :x2 :x3 ); c:says :x4 . :x4 log:includes {:x1 :x2 :x3 . } . } log:implies {:x1 :x2 :x3 . } . - erasure from step 76 - * - 78 - { :Bob . . } hs:corresponds_to . - rule from step 77 applied to steps (57, 74, 75) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': '{2}', 'x4': '{{2} hs:corresponds_to manifesto}'} * - 79 - ... - parsing - * - 80 - @forSome :e11 . hs:corresponds_to rdfs:subPropertyOf :e11 . - erasure from step 79 - * - 81 - ... - parsing - * - 82 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 81 - * - 83 - @forSome :e11 . { . . } :e11 . - rule from step 82 applied to steps (78, 80) - {'x2': u'', 'x3': '[...]', 'x0': '{2}', 'x1': u''} * - 84 - ... - parsing - * - 85 - @forSome :e11 . :e11 owl:inverseOf c:says . - erasure from step 84 - * - 86 - ... - parsing - * - 87 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 owl:inverseOf :x3 . } log:implies {:x2 :x3 :x0 . } . - erasure from step 86 - * - 88 - c:says { :Bob . . } . - rule from step 87 applied to steps (83, 85) - {'x2': u'', 'x3': u'', 'x0': '{2}', 'x1': '[...]'} * - 89 - ... - parsing - * - 90 - @forAll :x0, :x1, :x2 . { :x0 c:says :x2; c:speaks_for :x1 . } log:implies {:x1 c:says :x2 . } . - erasure from step 89 - * - 91 - :Bob c:says { :Bob . . } . - rule from step 90 applied to steps (33, 88) - {'x2': '{2}', 'x0': u'', 'x1': u''} * - 92 - { . . } :includes { . } . - built-in Axiom log:includes - * - 93 - ... - parsing - * - 94 - @forAll :x0, :x1, :x2, :x3 . { :x0 c:says :x1 . :x1 log:includes {:x2 :x3 . } . } log:implies {:x0 :x2 . } . - erasure from step 93 - * - 95 - :Bob . - rule from step 94 applied to steps (91, 92) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': '{2}'} * - 96 - ... - parsing - * - 97 - :subPropertyOf . - erasure from step 96 - * - 98 - ... - parsing - * - 99 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 98 - * - 100 - :Bob . - rule from step 99 applied to steps (95, 97) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': u''} * - 101 - ... - parsing - * - 102 - @forAll :x0, :x1, :x2, :x3, :x4 . { :x0 :x1 :x2; :x3 :x4 . :x1 owl:propertyDisjointWith :x3 . } log:implies {:x2 owl:differentFrom :x4 . } . - erasure from step 101 - * - 103 - :differentFrom . - rule from step 102 applied to steps (22, 24, 100) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': u'', 'x4': u''} * - 104 - ... - parsing - * - 105 - @forAll :x0 . { :x0 owl:differentFrom :x0 . } log:implies {:x0 owl:differentFrom :x0 . } . - erasure from step 104 - * - 106 - :differentFrom . - rule from step 105 applied to steps (103,) - {'x0': u''} * - 107 - ... - parsing - * - 108 - a :SymmetricProperty . - erasure from step 107 - * - 109 - ... - parsing - * - 110 - @forSome :e5 . :e5 . - erasure from step 109 - * - 111 - ... - parsing - * - 112 - :subPropertyOf . - erasure from step 111 - * - 113 - ... - parsing - * - 114 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 113 - * - 115 - @forSome :e5 . :e5 . - rule from step 114 applied to steps (110, 112) - {'x2': '[...]', 'x3': u'', 'x0': u'', 'x1': u''} * - 116 - ... - parsing - * - 117 - @forSome :e5 . :e5 xsd:date "2006-01-23" . - erasure from step 116 - * - 118 - ... - parsing - * - 119 - @forSome :e4 . :e4 . - erasure from step 118 - * - 120 - ... - parsing - * - 121 - :subPropertyOf . - erasure from step 120 - * - 122 - ... - parsing - * - 123 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 122 - * - 124 - @forSome :e4 . :e4 . - rule from step 123 applied to steps (119, 121) - {'x2': '[...]', 'x3': u'', 'x0': u'', 'x1': u''} * - 125 - ... - parsing - * - 126 - @forSome :e4 . :e4 xsd:date "2008-05-16" . - erasure from step 125 - * - 127 - "2006-01-23" :lessThan "2008-05-16" . - built-in Axiom str:lessThan - * - 128 - ... - parsing - * - 129 - @forAll :x0, :x1, :x2, :x3, :x4, :x5 . { :x0 :x1 . :x1 xsd:date :x2 . :x2 str:lessThan :x5 . :x3 :x4 . :x4 xsd:date :x5 . } log:implies {:x0 :x3 . } . - erasure from step 128 - * - 130 - :Bob . - rule from step 129 applied to steps (115, 117, 124, 126, 127) - {'x2': '"2006...1-23"', 'x3': u'', 'x0': u'', 'x1': '[...]', 'x4': '[...]', 'x5': '"2008...5-16"'} * - 131 - ... - parsing - * - 132 - @forAll :x0, :x1, :x2 . { :x0 a owl:SymmetricProperty . :x1 :x0 :x2 . } log:implies {:x2 :x0 :x1 . } . - erasure from step 131 - * - 133 - :Bob . - rule from step 132 applied to steps (108, 130) - {'x2': u'', 'x0': u'', 'x1': u''} * - 134 - ... - parsing - * - 135 - :propertyDisjointWith . - erasure from step 134 - * - 136 - ... - parsing - * - 137 - a :SymmetricProperty . - erasure from step 136 - * - 138 - ... - parsing - * - 139 - @forSome :e3 . :e3 a . - erasure from step 138 - * - 140 - ... - parsing - * - 141 - @forSome :e3 . :e3 . - erasure from step 140 - * - 142 - ... - parsing - * - 143 - @forSome :e3 . :e3 . - erasure from step 142 - * - 144 - ... - parsing - * - 145 - @forAll :x0, :x1, :x2 . { :x0 a ; :x2; :x1 . } log:implies {:x2 c:speaks_for :x1 . } . - erasure from step 144 - * - 146 - c:speaks_for :Bob . - rule from step 145 applied to steps (139, 141, 143) - {'x2': u'', 'x0': '[...]', 'x1': u''} * - 147 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 148 - ... - parsing - * - 149 - :C1 ht:requests ( :Q1 ) . - erasure from step 148 - * - 150 - ( :Q1 ) list:member :Q1 . - built-in Axiom list:member - * - 151 - ... - parsing - * - 152 - :Q1 ht:methodName "GET" . - erasure from step 151 - * - 153 - ... - parsing - * - 154 - :Q1 ht:absoluteURI "http://example.org/1995/manifesto" . - erasure from step 153 - * - 155 - ... - parsing - * - 156 - :Q1 ht:resp :A1 . - erasure from step 155 - * - 157 - ... - parsing - * - 158 - :A1 ht:statusCodeNumber "200" . - erasure from step 157 - * - 159 - ... - parsing - * - 160 - :A1 hs:asEntity { :Bob . . } . - erasure from step 159 - * - 161 - ... - parsing - * - 162 - @forAll :x0, :x1, :x2, :x3, :x4, :x5, :x6 . { :x0 log:uri :x1 . :x2 ht:requests :x3 . :x3 list:member :x4 . :x4 ht:absoluteURI :x1; ht:methodName "GET"; ht:resp :x5 . :x5 hs:asEntity :x6; ht:statusCodeNumber "200" . } log:implies {:x2 c:says {:x6 hs:corresponds_to :x0 . } . } . - erasure from step 161 - * - 163 - :C1 c:says {{ :Bob . . } hs:corresponds_to . } . - rule from step 162 applied to steps (147, 149, 150, 152, 154, 156, 158, 160) - {'x2': u'', 'x3': '?', 'x0': u'', 'x1': '"http...esto"', 'x6': '{2}', 'x4': u'', 'x5': u''} * - 164 - ... - parsing - * - 165 - :C1 ht:connectionAuthority "example.org" . - erasure from step 164 - * - 166 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 167 - ( "http://example.org/1995/manifesto" "http://([^/]+)/" ) :search ( "example.org" ) . - built-in Axiom str:search - * - 168 - ... - parsing - * - 169 - @forAll :x0, :x1, :x2, :x3, :x4 . { ( :x4 "http://([^/]+)/" ) str:search ( :x3 ) . :x0 c:says {:x1 hs:corresponds_to :x2 . }; ht:connectionAuthority :x3 . :x2 log:uri :x4 . } log:implies {:x0 c:controls_spo ( :x1 hs:corresponds_to :x2 ) . } . - erasure from step 168 - * - 170 - :C1 c:controls_spo ( { :Bob . . } hs:corresponds_to ) . - rule from step 169 applied to steps (163, 165, 166, 167) - {'x2': u'', 'x3': '"exam....org"', 'x0': u'', 'x1': '{2}', 'x4': '"http...esto"'} * - 171 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 172 - ... - parsing - * - 173 - :C1 ht:requests ( :Q1 ) . - erasure from step 172 - * - 174 - ( :Q1 ) list:member :Q1 . - built-in Axiom list:member - * - 175 - ... - parsing - * - 176 - :Q1 ht:methodName "GET" . - erasure from step 175 - * - 177 - ... - parsing - * - 178 - :Q1 ht:absoluteURI "http://example.org/1995/manifesto" . - erasure from step 177 - * - 179 - ... - parsing - * - 180 - :Q1 ht:resp :A1 . - erasure from step 179 - * - 181 - ... - parsing - * - 182 - :A1 ht:statusCodeNumber "200" . - erasure from step 181 - * - 183 - ... - parsing - * - 184 - :A1 hs:asEntity { :Bob . . } . - erasure from step 183 - * - 185 - ... - parsing - * - 186 - @forAll :x0, :x1, :x2, :x3, :x4, :x5, :x6 . { :x0 log:uri :x1 . :x2 ht:requests :x3 . :x3 list:member :x4 . :x4 ht:absoluteURI :x1; ht:methodName "GET"; ht:resp :x5 . :x5 hs:asEntity :x6; ht:statusCodeNumber "200" . } log:implies {:x2 c:says {:x6 hs:corresponds_to :x0 . } . } . - erasure from step 185 - * - 187 - :C1 c:says {{ :Bob . . } hs:corresponds_to . } . - rule from step 186 applied to steps (171, 173, 174, 176, 178, 180, 182, 184) - {'x2': u'', 'x3': '?', 'x0': u'', 'x1': '"http...esto"', 'x6': '{2}', 'x4': u'', 'x5': u''} * - 188 - { { :Bob . . } hs:corresponds_to . } log:includes {{ :Bob . . } hs:corresponds_to . } . - built-in Axiom log:includes - * - 189 - ... - parsing - * - 190 - @forAll :x0, :x1, :x2, :x3, :x4 . { :x0 c:controls_spo ( :x1 :x2 :x3 ); c:says :x4 . :x4 log:includes {:x1 :x2 :x3 . } . } log:implies {:x1 :x2 :x3 . } . - erasure from step 189 - * - 191 - { :Bob . . } hs:corresponds_to . - rule from step 190 applied to steps (170, 187, 188) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': '{2}', 'x4': '{{2} hs:corresponds_to manifesto}'} * - 192 - ... - parsing - * - 193 - @forSome :e11 . hs:corresponds_to rdfs:subPropertyOf :e11 . - erasure from step 192 - * - 194 - ... - parsing - * - 195 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 194 - * - 196 - @forSome :e11 . { . . } :e11 . - rule from step 195 applied to steps (191, 193) - {'x2': u'', 'x3': '[...]', 'x0': '{2}', 'x1': u''} * - 197 - ... - parsing - * - 198 - @forSome :e11 . :e11 owl:inverseOf c:says . - erasure from step 197 - * - 199 - ... - parsing - * - 200 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 owl:inverseOf :x3 . } log:implies {:x2 :x3 :x0 . } . - erasure from step 199 - * - 201 - c:says { :Bob . . } . - rule from step 200 applied to steps (196, 198) - {'x2': u'', 'x3': u'', 'x0': '{2}', 'x1': '[...]'} * - 202 - ... - parsing - * - 203 - @forAll :x0, :x1, :x2 . { :x0 c:says :x2; c:speaks_for :x1 . } log:implies {:x1 c:says :x2 . } . - erasure from step 202 - * - 204 - :Bob c:says { :Bob . . } . - rule from step 203 applied to steps (146, 201) - {'x2': '{2}', 'x0': u'', 'x1': u''} * - 205 - { . . } :includes { . } . - built-in Axiom log:includes - * - 206 - ... - parsing - * - 207 - @forAll :x0, :x1, :x2, :x3 . { :x0 c:says :x1 . :x1 log:includes {:x2 :x3 . } . } log:implies {:x0 :x2 . } . - erasure from step 206 - * - 208 - :Bob . - rule from step 207 applied to steps (204, 205) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': '{2}'} * - 209 - ... - parsing - * - 210 - :subPropertyOf . - erasure from step 209 - * - 211 - ... - parsing - * - 212 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 211 - * - 213 - :Bob . - rule from step 212 applied to steps (208, 210) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': u''} * - 214 - ... - parsing - * - 215 - @forAll :x0, :x1, :x2 . { :x0 a owl:SymmetricProperty . :x1 :x0 :x2 . } log:implies {:x2 :x0 :x1 . } . - erasure from step 214 - * - 216 - :Bob . - rule from step 215 applied to steps (137, 213) - {'x2': u'', 'x0': u'', 'x1': u''} * - 217 - ... - parsing - * - 218 - @forAll :x0, :x1, :x2, :x3, :x4 . { :x0 :x1 :x2; :x3 :x4 . :x1 owl:propertyDisjointWith :x3 . } log:implies {:x2 owl:differentFrom :x4 . } . - erasure from step 217 - * - 219 - :Bob owl:differentFrom :Bob . - rule from step 218 applied to steps (133, 135, 216) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': u'', 'x4': u''} * - 220 - ... - parsing - * - 221 - @forAll :x0 . { :x0 owl:differentFrom :x0 . } log:implies {:x0 owl:differentFrom :x0 . } . - erasure from step 220 - * - 222 - :Bob owl:differentFrom :Bob . - rule from step 221 applied to steps (219,) - {'x0': u''} * - 223 - owl:differentFrom . :Bob owl:differentFrom :Bob . - conjoining steps (106, 222) - Conclusion:: --=_mixed 00536508C1257690_Content-Type: text/plain; name="att3.txt" Content-Disposition: attachment; filename="att3.txt" Content-Transfer-Encoding: quoted-printable #Processed by $Id: euler.yap 3213 2009-12-18 14:30:25Z josd $ @prefix rdfs: . @prefix ht: . @prefix foaf: . @prefix dc: . @prefix cyc: . @prefix xsd: . @prefix log: . @prefix hs: . @prefix c: . @prefix rdf: . @prefix owl: . @prefix list: . @prefix str: . @prefix : . @prefix ns1: . @prefix var: . @prefix e: . @prefix r: . @prefix n3: . [ a r:Proof, r:Conjunction; r:component [ a r:Inference; r:gives { owl:differentFrom }; r:evidence ( [ a r:Inference; r:gives { owl:differentFrom }; r:evidence ( [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives {@forSome var:e3. var:e3}; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e3. var:e3}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e3"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e3. var:e3 xsd:date "2006-01-23"}; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives {@forSome var:e2. var:e2}; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e2. var:e2}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e2. var:e2 xsd:date "2008-05-16"}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {"2006-01-23" str:lessThan "2008-05-16"}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e3"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo "2006-01-23"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo "2008-05-16"]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5. {var:x0 var:x1. var:x1 xsd:date var:x2. var:x3 var:x4. var:x4 xsd:date var:x5. var:x2 str:lessThan var:x5} => {var:x0 var:x3}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { owl:propertyDisjointWith }; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives { c:says { . }}; r:evidence ( [ a r:Inference; r:gives { c:speaks_for }; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e1. var:e1 a }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives {@forSome var:e1. var:e1 }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives {@forSome var:e1. var:e1 }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a . var:x0 var:x1. var:x0 var:x2} => {var:x2 c:speaks_for var:x1}}; r:because [ a r:Parsing; r:source ]]] [ a r:Inference; r:gives { c:says { . }}; r:evidence ( [ a r:Inference; r:gives {@forSome var:e4. { . } var:e4 }; r:evidence ( [ a r:Inference; r:gives {{ . } hs:corresponds_to }; r:evidence ( [ a r:Inference; r:gives { c:controls_spo ({ . } hs:corresponds_to )}; r:evidence ( [ a r:Inference; r:gives { c:says {{ . } hs:corresponds_to }}; r:evidence ( [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Extraction; r:gives { ht:requests ()}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {() list:member }] [ a r:Extraction; r:gives { ht:methodName "GET"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:absoluteURI "http://example.org/1995/manifesto"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:resp }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:statusCodeNumber "200"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { hs:asEntity { . }}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo "http://example.org/1995/manifesto"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Q1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#A1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x6"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5, var:x6. {var:x0 log:uri var:x1. var:x2 ht:requests var:x3. var:x3 list:member var:x4. var:x4 ht:methodName "GET". var:x4 ht:absoluteURI var:x1. var:x4 ht:resp var:x5. var:x5 ht:statusCodeNumber "200". var:x5 hs:asEntity var:x6} => {var:x2 c:says {var:x6 hs:corresponds_to var:x0}}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { ht:connectionAuthority "example.org"}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Fact; r:gives {("http://example.org/1995/manifesto" "http://([^/]+)/") str:search ("example.org")}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo "example.org"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo "http://example.org/1995/manifesto"]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 c:says {var:x1 hs:corresponds_to var:x2}. var:x0 ht:connectionAuthority var:x3. var:x2 log:uri var:x4. (var:x4 "http://([^/]+)/") str:search (var:x3)} => {var:x0 c:controls_spo (var:x1 hs:corresponds_to var:x2)}}; r:because [ a r:Parsing; r:source ]]] [ a r:Inference; r:gives { c:says {{ . } hs:corresponds_to }}; r:evidence ( [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Extraction; r:gives { ht:requests ()}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {() list:member }] [ a r:Extraction; r:gives { ht:methodName "GET"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:absoluteURI "http://example.org/1995/manifesto"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:resp }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:statusCodeNumber "200"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { hs:asEntity { . }}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo "http://example.org/1995/manifesto"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Q1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#A1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x6"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5, var:x6. {var:x0 log:uri var:x1. var:x2 ht:requests var:x3. var:x3 list:member var:x4. var:x4 ht:methodName "GET". var:x4 ht:absoluteURI var:x1. var:x4 ht:resp var:x5. var:x5 ht:statusCodeNumber "200". var:x5 hs:asEntity var:x6} => {var:x2 c:says {var:x6 hs:corresponds_to var:x0}}}; r:because [ a r:Parsing; r:source ]]] [ a r:Fact; r:gives {{{ . } hs:corresponds_to } log:includes {{ . } hs:corresponds_to }}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/httpspeech#corresponds_to"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo {{ . } hs:corresponds_to }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 c:controls_spo (var:x1 var:x2 var:x3). var:x0 c:says var:x4. var:x4 log:includes {var:x1 var:x2 var:x3}} => {var:x1 var:x2 var:x3}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e4. hs:corresponds_to rdfs:subPropertyOf var:e4}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/httpspeech#corresponds_to"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e4"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e4. var:e4 owl:inverseOf c:says}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e4"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/speech#says"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 owl:inverseOf var:x3} => {var:x2 var:x3 var:x0}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 c:speaks_for var:x1. var:x0 c:says var:x2} => {var:x1 c:says var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Fact; r:gives {{ . } log:includes { }}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 c:says var:x1. var:x1 log:includes {var:x2 var:x3}} => {var:x0 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/perceives"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 var:x1 var:x2. var:x1 owl:propertyDisjointWith var:x3. var:x0 var:x3 var:x4} => {var:x2 owl:differentFrom var:x4}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0. {var:x0 owl:differentFrom var:x0} => {var:x0 owl:differentFrom var:x0}}; r:because [ a r:Parsing; r:source ]]]; r:component [ a r:Inference; r:gives { owl:differentFrom }; r:evidence ( [ a r:Inference; r:gives { owl:differentFrom }; r:evidence ( [ a r:Inference; r:gives { }; r:evidence ( [ a r:Extraction; r:gives { a owl:SymmetricProperty}; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives {@forSome var:e3. var:e3}; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e3. var:e3}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e3"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e3. var:e3 xsd:date "2006-01-23"}; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives {@forSome var:e2. var:e2}; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e2. var:e2}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e2. var:e2 xsd:date "2008-05-16"}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {"2006-01-23" str:lessThan "2008-05-16"}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e3"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo "2006-01-23"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo "2008-05-16"]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5. {var:x0 var:x1. var:x1 xsd:date var:x2. var:x3 var:x4. var:x4 xsd:date var:x5. var:x2 str:lessThan var:x5} => {var:x0 var:x3}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a owl:SymmetricProperty. var:x1 var:x0 var:x2} => {var:x2 var:x0 var:x1}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { owl:propertyDisjointWith }; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives { }; r:evidence ( [ a r:Extraction; r:gives { a owl:SymmetricProperty}; r:because [ a r:Parsing; r:source ]] [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives { }; r:evidence ( [ a r:Inference; r:gives { c:says { . }}; r:evidence ( [ a r:Inference; r:gives { c:speaks_for }; r:evidence ( [ a r:Extraction; r:gives {@forSome var:e1. var:e1 a }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives {@forSome var:e1. var:e1 }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives {@forSome var:e1. var:e1 }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a . var:x0 var:x1. var:x0 var:x2} => {var:x2 c:speaks_for var:x1}}; r:because [ a r:Parsing; r:source ]]] [ a r:Inference; r:gives { c:says { . }}; r:evidence ( [ a r:Inference; r:gives {@forSome var:e4. { . } var:e4 }; r:evidence ( [ a r:Inference; r:gives {{ . } hs:corresponds_to }; r:evidence ( [ a r:Inference; r:gives { c:controls_spo ({ . } hs:corresponds_to )}; r:evidence ( [ a r:Inference; r:gives { c:says {{ . } hs:corresponds_to }}; r:evidence ( [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Extraction; r:gives { ht:requests ()}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {() list:member }] [ a r:Extraction; r:gives { ht:methodName "GET"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:absoluteURI "http://example.org/1995/manifesto"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:resp }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:statusCodeNumber "200"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { hs:asEntity { . }}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo "http://example.org/1995/manifesto"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Q1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#A1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x6"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5, var:x6. {var:x0 log:uri var:x1. var:x2 ht:requests var:x3. var:x3 list:member var:x4. var:x4 ht:methodName "GET". var:x4 ht:absoluteURI var:x1. var:x4 ht:resp var:x5. var:x5 ht:statusCodeNumber "200". var:x5 hs:asEntity var:x6} => {var:x2 c:says {var:x6 hs:corresponds_to var:x0}}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { ht:connectionAuthority "example.org"}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Fact; r:gives {("http://example.org/1995/manifesto" "http://([^/]+)/") str:search ("example.org")}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo "example.org"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo "http://example.org/1995/manifesto"]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 c:says {var:x1 hs:corresponds_to var:x2}. var:x0 ht:connectionAuthority var:x3. var:x2 log:uri var:x4. (var:x4 "http://([^/]+)/") str:search (var:x3)} => {var:x0 c:controls_spo (var:x1 hs:corresponds_to var:x2)}}; r:because [ a r:Parsing; r:source ]]] [ a r:Inference; r:gives { c:says {{ . } hs:corresponds_to }}; r:evidence ( [ a r:Fact; r:gives { log:uri "http://example.org/1995/manifesto"}] [ a r:Extraction; r:gives { ht:requests ()}; r:because [ a r:Parsing; r:source ]] [ a r:Fact; r:gives {() list:member }] [ a r:Extraction; r:gives { ht:methodName "GET"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:absoluteURI "http://example.org/1995/manifesto"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:resp }; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { ht:statusCodeNumber "200"}; r:because [ a r:Parsing; r:source ]] [ a r:Extraction; r:gives { hs:asEntity { . }}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo "http://example.org/1995/manifesto"]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo ()]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Q1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x5"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#A1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x6"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4, var:x5, var:x6. {var:x0 log:uri var:x1. var:x2 ht:requests var:x3. var:x3 list:member var:x4. var:x4 ht:methodName "GET". var:x4 ht:absoluteURI var:x1. var:x4 ht:resp var:x5. var:x5 ht:statusCodeNumber "200". var:x5 hs:asEntity var:x6} => {var:x2 c:says {var:x6 hs:corresponds_to var:x0}}}; r:because [ a r:Parsing; r:source ]]] [ a r:Fact; r:gives {{{ . } hs:corresponds_to } log:includes {{ . } hs:corresponds_to }}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#C1"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/httpspeech#corresponds_to"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo {{ . } hs:corresponds_to }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 c:controls_spo (var:x1 var:x2 var:x3). var:x0 c:says var:x4. var:x4 log:includes {var:x1 var:x2 var:x3}} => {var:x1 var:x2 var:x3}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e4. hs:corresponds_to rdfs:subPropertyOf var:e4}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/httpspeech#corresponds_to"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e4"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives {@forSome var:e4. var:e4 owl:inverseOf c:says}; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ a r:Existential; n3:nodeId "http://localhost/var#e4"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://www.w3.org/2001/tag/dj9/speech#says"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 owl:inverseOf var:x3} => {var:x2 var:x3 var:x0}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo { . }]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 c:speaks_for var:x1. var:x0 c:says var:x2} => {var:x1 c:says var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Fact; r:gives {{ . } log:includes { }}]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo { . }]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://example.org/1995/manifesto"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 c:says var:x1. var:x1 log:includes {var:x2 var:x3}} => {var:x0 var:x2}}; r:because [ a r:Parsing; r:source ]]] [ a r:Extraction; r:gives { rdfs:subPropertyOf }; r:because [ a r:Parsing; r:source ]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/perceives"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3. {var:x0 var:x1 var:x2. var:x1 rdfs:subPropertyOf var:x3} => {var:x0 var:x3 var:x2}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2. {var:x0 a owl:SymmetricProperty. var:x1 var:x0 var:x2} => {var:x2 var:x0 var:x1}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://penguin-house.example/2008/article2"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x1"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x3"]; r:boundTo [ n3:uri "http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects"]]; r:binding [ r:variable [ n3:uri "http://localhost/var#x4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0, var:x1, var:x2, var:x3, var:x4. {var:x0 var:x1 var:x2. var:x1 owl:propertyDisjointWith var:x3. var:x0 var:x3 var:x4} => {var:x2 owl:differentFrom var:x4}}; r:because [ a r:Parsing; r:source ]]]); r:binding [ r:variable [ n3:uri "http://localhost/var#x0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2007/07test/badmeta.n3#Bob"]]; r:rule [ a r:Extraction; r:gives {@forAll var:x0. {var:x0 owl:differentFrom var:x0} => {var:x0 owl:differentFrom var:x0}}; r:because [ a r:Parsing; r:source ]]]; r:gives { owl:differentFrom . owl:differentFrom . }]. #ENDS 96 msec #Trunk : 170/2940 = 5.78231292517007 % #Branch: 21/4197 = 0.50035739814153 % --=_mixed 00536508C1257690_Content-Type: text/plain; name="att4.txt" Content-Disposition: attachment; filename="att4.txt" Content-Transfer-Encoding: quoted-printable .. list-table:: Proof :widths: 2 70 20 20 :header-rows: 1 * - Step - Formula - Justification - Bindings * - 1 - ... - parsing - * - 2 - @forSome :e3 . :e3 . - erasure from step 1 - * - 3 - ... - parsing - * - 4 - :subPropertyOf . - erasure from step 3 - * - 5 - ... - parsing - * - 6 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 5 - * - 7 - @forSome :e3 . :e3 . - rule from step 6 applied to steps (2, 4) - {'x2': '[...]', 'x3': u'', 'x0': u'', 'x1': u''} * - 8 - ... - parsing - * - 9 - @forSome :e3 . :e3 xsd:date "2006-01-23" . - erasure from step 8 - * - 10 - ... - parsing - * - 11 - @forSome :e2 . :e2 . - erasure from step 10 - * - 12 - ... - parsing - * - 13 - :subPropertyOf . - erasure from step 12 - * - 14 - ... - parsing - * - 15 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 14 - * - 16 - @forSome :e2 . :e2 . - rule from step 15 applied to steps (11, 13) - {'x2': '[...]', 'x3': u'', 'x0': u'', 'x1': u''} * - 17 - ... - parsing - * - 18 - @forSome :e2 . :e2 xsd:date "2008-05-16" . - erasure from step 17 - * - 19 - "2006-01-23" :lessThan "2008-05-16" . - built-in Axiom str:lessThan - * - 20 - ... - parsing - * - 21 - @forAll :x0, :x1, :x2, :x3, :x4, :x5 . { :x0 :x1 . :x1 xsd:date :x2 . :x2 str:lessThan :x5 . :x3 :x4 . :x4 xsd:date :x5 . } log:implies {:x0 :x3 . } . - erasure from step 20 - * - 22 - :Bob . - rule from step 21 applied to steps (7, 9, 16, 18, 19) - {'x2': '"2006...1-23"', 'x3': u'', 'x0': u'', 'x1': '[...]', 'x4': '[...]', 'x5': '"2008...5-16"'} * - 23 - ... - parsing - * - 24 - :propertyDisjointWith . - erasure from step 23 - * - 25 - ... - parsing - * - 26 - @forSome :e1 . :e1 a . - erasure from step 25 - * - 27 - ... - parsing - * - 28 - @forSome :e1 . :e1 . - erasure from step 27 - * - 29 - ... - parsing - * - 30 - @forSome :e1 . :e1 . - erasure from step 29 - * - 31 - ... - parsing - * - 32 - @forAll :x0, :x1, :x2 . { :x0 a ; :x2; :x1 . } log:implies {:x2 c:speaks_for :x1 . } . - erasure from step 31 - * - 33 - c:speaks_for :Bob . - rule from step 32 applied to steps (26, 28, 30) - {'x2': u'', 'x0': '[...]', 'x1': u''} * - 34 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 35 - ... - parsing - * - 36 - :C1 ht:requests ( :Q1 ) . - erasure from step 35 - * - 37 - ( :Q1 ) list:member :Q1 . - built-in Axiom list:member - * - 38 - ... - parsing - * - 39 - :Q1 ht:methodName "GET" . - erasure from step 38 - * - 40 - ... - parsing - * - 41 - :Q1 ht:absoluteURI "http://example.org/1995/manifesto" . - erasure from step 40 - * - 42 - ... - parsing - * - 43 - :Q1 ht:resp :A1 . - erasure from step 42 - * - 44 - ... - parsing - * - 45 - :A1 ht:statusCodeNumber "200" . - erasure from step 44 - * - 46 - ... - parsing - * - 47 - :A1 hs:asEntity { :Bob . . } . - erasure from step 46 - * - 48 - ... - parsing - * - 49 - @forAll :x0, :x1, :x2, :x3, :x4, :x5, :x6 . { :x0 log:uri :x1 . :x2 ht:requests :x3 . :x3 list:member :x4 . :x4 ht:absoluteURI :x1; ht:methodName "GET"; ht:resp :x5 . :x5 hs:asEntity :x6; ht:statusCodeNumber "200" . } log:implies {:x2 c:says {:x6 hs:corresponds_to :x0 . } . } . - erasure from step 48 - * - 50 - :C1 c:says {{ :Bob . . } hs:corresponds_to . } . - rule from step 49 applied to steps (34, 36, 37, 39, 41, 43, 45, 47) - {'x2': u'', 'x3': '?', 'x0': u'', 'x1': '"http...esto"', 'x6': '{2}', 'x4': u'', 'x5': u''} * - 51 - ... - parsing - * - 52 - :C1 ht:connectionAuthority "example.org" . - erasure from step 51 - * - 53 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 54 - ( "http://example.org/1995/manifesto" "http://([^/]+)/" ) :search ( "example.org" ) . - built-in Axiom str:search - * - 55 - ... - parsing - * - 56 - @forAll :x0, :x1, :x2, :x3, :x4 . { ( :x4 "http://([^/]+)/" ) str:search ( :x3 ) . :x0 c:says {:x1 hs:corresponds_to :x2 . }; ht:connectionAuthority :x3 . :x2 log:uri :x4 . } log:implies {:x0 c:controls_spo ( :x1 hs:corresponds_to :x2 ) . } . - erasure from step 55 - * - 57 - :C1 c:controls_spo ( { :Bob . . } hs:corresponds_to ) . - rule from step 56 applied to steps (50, 52, 53, 54) - {'x2': u'', 'x3': '"exam....org"', 'x0': u'', 'x1': '{2}', 'x4': '"http...esto"'} * - 58 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 59 - ... - parsing - * - 60 - :C1 ht:requests ( :Q1 ) . - erasure from step 59 - * - 61 - ( :Q1 ) list:member :Q1 . - built-in Axiom list:member - * - 62 - ... - parsing - * - 63 - :Q1 ht:methodName "GET" . - erasure from step 62 - * - 64 - ... - parsing - * - 65 - :Q1 ht:absoluteURI "http://example.org/1995/manifesto" . - erasure from step 64 - * - 66 - ... - parsing - * - 67 - :Q1 ht:resp :A1 . - erasure from step 66 - * - 68 - ... - parsing - * - 69 - :A1 ht:statusCodeNumber "200" . - erasure from step 68 - * - 70 - ... - parsing - * - 71 - :A1 hs:asEntity { :Bob . . } . - erasure from step 70 - * - 72 - ... - parsing - * - 73 - @forAll :x0, :x1, :x2, :x3, :x4, :x5, :x6 . { :x0 log:uri :x1 . :x2 ht:requests :x3 . :x3 list:member :x4 . :x4 ht:absoluteURI :x1; ht:methodName "GET"; ht:resp :x5 . :x5 hs:asEntity :x6; ht:statusCodeNumber "200" . } log:implies {:x2 c:says {:x6 hs:corresponds_to :x0 . } . } . - erasure from step 72 - * - 74 - :C1 c:says {{ :Bob . . } hs:corresponds_to . } . - rule from step 73 applied to steps (58, 60, 61, 63, 65, 67, 69, 71) - {'x2': u'', 'x3': '?', 'x0': u'', 'x1': '"http...esto"', 'x6': '{2}', 'x4': u'', 'x5': u''} * - 75 - { { :Bob . . } hs:corresponds_to . } log:includes {{ :Bob . . } hs:corresponds_to . } . - built-in Axiom log:includes - * - 76 - ... - parsing - * - 77 - @forAll :x0, :x1, :x2, :x3, :x4 . { :x0 c:controls_spo ( :x1 :x2 :x3 ); c:says :x4 . :x4 log:includes {:x1 :x2 :x3 . } . } log:implies {:x1 :x2 :x3 . } . - erasure from step 76 - * - 78 - { :Bob . . } hs:corresponds_to . - rule from step 77 applied to steps (57, 74, 75) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': '{2}', 'x4': '{{2} hs:corresponds_to manifesto}'} * - 79 - ... - parsing - * - 80 - @forSome :e4 . hs:corresponds_to rdfs:subPropertyOf :e4 . - erasure from step 79 - * - 81 - ... - parsing - * - 82 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 81 - * - 83 - @forSome :e4 . { . . } :e4 . - rule from step 82 applied to steps (78, 80) - {'x2': u'', 'x3': '[...]', 'x0': '{2}', 'x1': u''} * - 84 - ... - parsing - * - 85 - @forSome :e4 . :e4 owl:inverseOf c:says . - erasure from step 84 - * - 86 - ... - parsing - * - 87 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 owl:inverseOf :x3 . } log:implies {:x2 :x3 :x0 . } . - erasure from step 86 - * - 88 - c:says { :Bob . . } . - rule from step 87 applied to steps (83, 85) - {'x2': u'', 'x3': u'', 'x0': '{2}', 'x1': '[...]'} * - 89 - ... - parsing - * - 90 - @forAll :x0, :x1, :x2 . { :x0 c:says :x2; c:speaks_for :x1 . } log:implies {:x1 c:says :x2 . } . - erasure from step 89 - * - 91 - :Bob c:says { :Bob . . } . - rule from step 90 applied to steps (33, 88) - {'x2': '{2}', 'x0': u'', 'x1': u''} * - 92 - { :Bob . . } log:includes { . } . - built-in Axiom log:includes - * - 93 - ... - parsing - * - 94 - @forAll :x0, :x1, :x2, :x3 . { :x0 c:says :x1 . :x1 log:includes {:x2 :x3 . } . } log:implies {:x0 :x2 . } . - erasure from step 93 - * - 95 - :Bob . - rule from step 94 applied to steps (91, 92) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': '{2}'} * - 96 - ... - parsing - * - 97 - :subPropertyOf . - erasure from step 96 - * - 98 - ... - parsing - * - 99 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 98 - * - 100 - :Bob . - rule from step 99 applied to steps (95, 97) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': u''} * - 101 - ... - parsing - * - 102 - @forAll :x0, :x1, :x2, :x3, :x4 . { :x0 :x1 :x2; :x3 :x4 . :x1 owl:propertyDisjointWith :x3 . } log:implies {:x2 owl:differentFrom :x4 . } . - erasure from step 101 - * - 103 - :differentFrom . - rule from step 102 applied to steps (22, 24, 100) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': u'', 'x4': u''} * - 104 - ... - parsing - * - 105 - @forAll :x0 . { :x0 owl:differentFrom :x0 . } log:implies {:x0 owl:differentFrom :x0 . } . - erasure from step 104 - * - 106 - :differentFrom . - rule from step 105 applied to steps (103,) - {'x0': u''} * - 107 - ... - parsing - * - 108 - a :SymmetricProperty . - erasure from step 107 - * - 109 - ... - parsing - * - 110 - @forSome :e3 . :e3 . - erasure from step 109 - * - 111 - ... - parsing - * - 112 - :subPropertyOf . - erasure from step 111 - * - 113 - ... - parsing - * - 114 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 113 - * - 115 - @forSome :e3 . :e3 . - rule from step 114 applied to steps (110, 112) - {'x2': '[...]', 'x3': u'', 'x0': u'', 'x1': u''} * - 116 - ... - parsing - * - 117 - @forSome :e3 . :e3 xsd:date "2006-01-23" . - erasure from step 116 - * - 118 - ... - parsing - * - 119 - @forSome :e2 . :e2 . - erasure from step 118 - * - 120 - ... - parsing - * - 121 - :subPropertyOf . - erasure from step 120 - * - 122 - ... - parsing - * - 123 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 122 - * - 124 - @forSome :e2 . :e2 . - rule from step 123 applied to steps (119, 121) - {'x2': '[...]', 'x3': u'', 'x0': u'', 'x1': u''} * - 125 - ... - parsing - * - 126 - @forSome :e2 . :e2 xsd:date "2008-05-16" . - erasure from step 125 - * - 127 - "2006-01-23" :lessThan "2008-05-16" . - built-in Axiom str:lessThan - * - 128 - ... - parsing - * - 129 - @forAll :x0, :x1, :x2, :x3, :x4, :x5 . { :x0 :x1 . :x1 xsd:date :x2 . :x2 str:lessThan :x5 . :x3 :x4 . :x4 xsd:date :x5 . } log:implies {:x0 :x3 . } . - erasure from step 128 - * - 130 - :Bob . - rule from step 129 applied to steps (115, 117, 124, 126, 127) - {'x2': '"2006...1-23"', 'x3': u'', 'x0': u'', 'x1': '[...]', 'x4': '[...]', 'x5': '"2008...5-16"'} * - 131 - ... - parsing - * - 132 - @forAll :x0, :x1, :x2 . { :x0 a owl:SymmetricProperty . :x1 :x0 :x2 . } log:implies {:x2 :x0 :x1 . } . - erasure from step 131 - * - 133 - :Bob . - rule from step 132 applied to steps (108, 130) - {'x2': u'', 'x0': u'', 'x1': u''} * - 134 - ... - parsing - * - 135 - :propertyDisjointWith . - erasure from step 134 - * - 136 - ... - parsing - * - 137 - a :SymmetricProperty . - erasure from step 136 - * - 138 - ... - parsing - * - 139 - @forSome :e1 . :e1 a . - erasure from step 138 - * - 140 - ... - parsing - * - 141 - @forSome :e1 . :e1 . - erasure from step 140 - * - 142 - ... - parsing - * - 143 - @forSome :e1 . :e1 . - erasure from step 142 - * - 144 - ... - parsing - * - 145 - @forAll :x0, :x1, :x2 . { :x0 a ; :x2; :x1 . } log:implies {:x2 c:speaks_for :x1 . } . - erasure from step 144 - * - 146 - c:speaks_for :Bob . - rule from step 145 applied to steps (139, 141, 143) - {'x2': u'', 'x0': '[...]', 'x1': u''} * - 147 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 148 - ... - parsing - * - 149 - :C1 ht:requests ( :Q1 ) . - erasure from step 148 - * - 150 - ( :Q1 ) list:member :Q1 . - built-in Axiom list:member - * - 151 - ... - parsing - * - 152 - :Q1 ht:methodName "GET" . - erasure from step 151 - * - 153 - ... - parsing - * - 154 - :Q1 ht:absoluteURI "http://example.org/1995/manifesto" . - erasure from step 153 - * - 155 - ... - parsing - * - 156 - :Q1 ht:resp :A1 . - erasure from step 155 - * - 157 - ... - parsing - * - 158 - :A1 ht:statusCodeNumber "200" . - erasure from step 157 - * - 159 - ... - parsing - * - 160 - :A1 hs:asEntity { :Bob . . } . - erasure from step 159 - * - 161 - ... - parsing - * - 162 - @forAll :x0, :x1, :x2, :x3, :x4, :x5, :x6 . { :x0 log:uri :x1 . :x2 ht:requests :x3 . :x3 list:member :x4 . :x4 ht:absoluteURI :x1; ht:methodName "GET"; ht:resp :x5 . :x5 hs:asEntity :x6; ht:statusCodeNumber "200" . } log:implies {:x2 c:says {:x6 hs:corresponds_to :x0 . } . } . - erasure from step 161 - * - 163 - :C1 c:says {{ :Bob . . } hs:corresponds_to . } . - rule from step 162 applied to steps (147, 149, 150, 152, 154, 156, 158, 160) - {'x2': u'', 'x3': '?', 'x0': u'', 'x1': '"http...esto"', 'x6': '{2}', 'x4': u'', 'x5': u''} * - 164 - ... - parsing - * - 165 - :C1 ht:connectionAuthority "example.org" . - erasure from step 164 - * - 166 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 167 - ( "http://example.org/1995/manifesto" "http://([^/]+)/" ) :search ( "example.org" ) . - built-in Axiom str:search - * - 168 - ... - parsing - * - 169 - @forAll :x0, :x1, :x2, :x3, :x4 . { ( :x4 "http://([^/]+)/" ) str:search ( :x3 ) . :x0 c:says {:x1 hs:corresponds_to :x2 . }; ht:connectionAuthority :x3 . :x2 log:uri :x4 . } log:implies {:x0 c:controls_spo ( :x1 hs:corresponds_to :x2 ) . } . - erasure from step 168 - * - 170 - :C1 c:controls_spo ( { :Bob . . } hs:corresponds_to ) . - rule from step 169 applied to steps (163, 165, 166, 167) - {'x2': u'', 'x3': '"exam....org"', 'x0': u'', 'x1': '{2}', 'x4': '"http...esto"'} * - 171 - :uri "http://example.org/1995/manifesto" . - built-in Axiom log:uri - * - 172 - ... - parsing - * - 173 - :C1 ht:requests ( :Q1 ) . - erasure from step 172 - * - 174 - ( :Q1 ) list:member :Q1 . - built-in Axiom list:member - * - 175 - ... - parsing - * - 176 - :Q1 ht:methodName "GET" . - erasure from step 175 - * - 177 - ... - parsing - * - 178 - :Q1 ht:absoluteURI "http://example.org/1995/manifesto" . - erasure from step 177 - * - 179 - ... - parsing - * - 180 - :Q1 ht:resp :A1 . - erasure from step 179 - * - 181 - ... - parsing - * - 182 - :A1 ht:statusCodeNumber "200" . - erasure from step 181 - * - 183 - ... - parsing - * - 184 - :A1 hs:asEntity { :Bob . . } . - erasure from step 183 - * - 185 - ... - parsing - * - 186 - @forAll :x0, :x1, :x2, :x3, :x4, :x5, :x6 . { :x0 log:uri :x1 . :x2 ht:requests :x3 . :x3 list:member :x4 . :x4 ht:absoluteURI :x1; ht:methodName "GET"; ht:resp :x5 . :x5 hs:asEntity :x6; ht:statusCodeNumber "200" . } log:implies {:x2 c:says {:x6 hs:corresponds_to :x0 . } . } . - erasure from step 185 - * - 187 - :C1 c:says {{ :Bob . . } hs:corresponds_to . } . - rule from step 186 applied to steps (171, 173, 174, 176, 178, 180, 182, 184) - {'x2': u'', 'x3': '?', 'x0': u'', 'x1': '"http...esto"', 'x6': '{2}', 'x4': u'', 'x5': u''} * - 188 - { { :Bob . . } hs:corresponds_to . } log:includes {{ :Bob . . } hs:corresponds_to . } . - built-in Axiom log:includes - * - 189 - ... - parsing - * - 190 - @forAll :x0, :x1, :x2, :x3, :x4 . { :x0 c:controls_spo ( :x1 :x2 :x3 ); c:says :x4 . :x4 log:includes {:x1 :x2 :x3 . } . } log:implies {:x1 :x2 :x3 . } . - erasure from step 189 - * - 191 - { :Bob . . } hs:corresponds_to . - rule from step 190 applied to steps (170, 187, 188) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': '{2}', 'x4': '{{2} hs:corresponds_to manifesto}'} * - 192 - ... - parsing - * - 193 - @forSome :e4 . hs:corresponds_to rdfs:subPropertyOf :e4 . - erasure from step 192 - * - 194 - ... - parsing - * - 195 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 194 - * - 196 - @forSome :e4 . { . . } :e4 . - rule from step 195 applied to steps (191, 193) - {'x2': u'', 'x3': '[...]', 'x0': '{2}', 'x1': u''} * - 197 - ... - parsing - * - 198 - @forSome :e4 . :e4 owl:inverseOf c:says . - erasure from step 197 - * - 199 - ... - parsing - * - 200 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 owl:inverseOf :x3 . } log:implies {:x2 :x3 :x0 . } . - erasure from step 199 - * - 201 - c:says { :Bob . . } . - rule from step 200 applied to steps (196, 198) - {'x2': u'', 'x3': u'', 'x0': '{2}', 'x1': '[...]'} * - 202 - ... - parsing - * - 203 - @forAll :x0, :x1, :x2 . { :x0 c:says :x2; c:speaks_for :x1 . } log:implies {:x1 c:says :x2 . } . - erasure from step 202 - * - 204 - :Bob c:says { :Bob . . } . - rule from step 203 applied to steps (146, 201) - {'x2': '{2}', 'x0': u'', 'x1': u''} * - 205 - { :Bob . . } log:includes { . } . - built-in Axiom log:includes - * - 206 - ... - parsing - * - 207 - @forAll :x0, :x1, :x2, :x3 . { :x0 c:says :x1 . :x1 log:includes {:x2 :x3 . } . } log:implies {:x0 :x2 . } . - erasure from step 206 - * - 208 - :Bob . - rule from step 207 applied to steps (204, 205) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': '{2}'} * - 209 - ... - parsing - * - 210 - :subPropertyOf . - erasure from step 209 - * - 211 - ... - parsing - * - 212 - @forAll :x0, :x1, :x2, :x3 . { :x0 :x1 :x2 . :x1 rdfs:subPropertyOf :x3 . } log:implies {:x0 :x3 :x2 . } . - erasure from step 211 - * - 213 - :Bob . - rule from step 212 applied to steps (208, 210) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': u''} * - 214 - ... - parsing - * - 215 - @forAll :x0, :x1, :x2 . { :x0 a owl:SymmetricProperty . :x1 :x0 :x2 . } log:implies {:x2 :x0 :x1 . } . - erasure from step 214 - * - 216 - :Bob . - rule from step 215 applied to steps (137, 213) - {'x2': u'', 'x0': u'', 'x1': u''} * - 217 - ... - parsing - * - 218 - @forAll :x0, :x1, :x2, :x3, :x4 . { :x0 :x1 :x2; :x3 :x4 . :x1 owl:propertyDisjointWith :x3 . } log:implies {:x2 owl:differentFrom :x4 . } . - erasure from step 217 - * - 219 - :Bob owl:differentFrom :Bob . - rule from step 218 applied to steps (133, 135, 216) - {'x2': u'', 'x3': u'', 'x0': u'', 'x1': u'', 'x4': u''} * - 220 - ... - parsing - * - 221 - @forAll :x0 . { :x0 owl:differentFrom :x0 . } log:implies {:x0 owl:differentFrom :x0 . } . - erasure from step 220 - * - 222 - :Bob owl:differentFrom :Bob . - rule from step 221 applied to steps (219,) - {'x0': u''} * - 223 - :Bob owl:differentFrom :Bob . owl:differentFrom . - conjoining steps (106, 222) - Conclusion:: @prefix : . @prefix owl: . :Bob owl:differentFrom :Bob . owl:differentFrom . --=_mixed 00536508C1257690_=--