# Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:41 GMT @prefix log: . @prefix e: . ()!log:conjunction e:constructs { @prefix e: . @prefix q: . @prefix rdfs: . @prefix log: . @prefix rdf: . # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:41 GMT @prefix log: . @prefix e: . (!log:semantics)!log:conjunction e:constructs { @prefix e: . @prefix q: . @prefix rdfs: . @prefix log: . @prefix : . @prefix rdf: . {{ :member } e:evidence . { :w3cmember } e:evidence . { :subscribed } e:evidence } e:sequent { { :authenticated } e:evidence }. # Proof found in 3 steps (300000 steps/sec) using 1 engine (4 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:42 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {{:route rdf:type owl:TransitiveProperty} e:evidence . {{:oneway rdfs:subPropertyOf :route} e:evidence . {:angers :oneway :nantes} e:evidence } e:sequent { {:angers :route :nantes} e:evidence }. {{:route rdf:type owl:TransitiveProperty} e:evidence . {{:oneway rdfs:subPropertyOf :route} e:evidence . {{:twoway rdfs:subPropertyOf :oneway} e:evidence . {:lemans :twoway :angers} e:evidence } e:sequent { {:lemans :oneway :angers} e:evidence }} e:sequent { {:lemans :route :angers} e:evidence }. {{:route rdf:type owl:TransitiveProperty} e:evidence . {{:oneway rdfs:subPropertyOf :route} e:evidence . {{:twoway rdfs:subPropertyOf :oneway} e:evidence . {:chartres :twoway :lemans} e:evidence } e:sequent { {:chartres :oneway :lemans} e:evidence }} e:sequent { {:chartres :route :lemans} e:evidence }. {{:route rdf:type owl:TransitiveProperty} e:evidence . {{:oneway rdfs:subPropertyOf :route} e:evidence . {{:twoway rdfs:subPropertyOf :oneway} e:evidence . {:parijs :twoway :chartres} e:evidence } e:sequent { {:parijs :oneway :chartres} e:evidence }} e:sequent { {:parijs :route :chartres} e:evidence }. {{:route rdf:type owl:TransitiveProperty} e:evidence . {{:oneway rdfs:subPropertyOf :route} e:evidence . {{:twoway rdfs:subPropertyOf :oneway} e:evidence . {{:twoway rdf:type owl:SymmetricProperty} e:evidence . {:parijs :twoway :orleans} e:evidence } e:sequent { {:orleans :twoway :parijs} e:evidence }} e:sequent { {:orleans :oneway :parijs} e:evidence }} e:sequent { {:orleans :route :parijs} e:evidence }. {{:route rdf:type owl:TransitiveProperty} e:evidence . {{:oneway rdfs:subPropertyOf :route} e:evidence . {{:twoway rdfs:subPropertyOf :oneway} e:evidence . {{:twoway rdf:type owl:SymmetricProperty} e:evidence . {:orleans :twoway :blois} e:evidence } e:sequent { {:blois :twoway :orleans} e:evidence }} e:sequent { {:blois :oneway :orleans} e:evidence }} e:sequent { {:blois :route :orleans} e:evidence }. {{:route rdf:type owl:TransitiveProperty} e:evidence . {{:oneway rdfs:subPropertyOf :route} e:evidence . {{:twoway rdfs:subPropertyOf :oneway} e:evidence . {:orleans :twoway :blois} e:evidence } e:sequent { {:orleans :oneway :blois} e:evidence }} e:sequent { {:orleans :route :blois} e:evidence }. {{:oneway rdfs:subPropertyOf :route} e:evidence . {{:twoway rdfs:subPropertyOf :oneway} e:evidence . {{:twoway rdf:type owl:SymmetricProperty} e:evidence . {:orleans :twoway :bourges} e:evidence } e:sequent { {:bourges :twoway :orleans} e:evidence }} e:sequent { {:bourges :oneway :orleans} e:evidence }} e:sequent { {:bourges :route :orleans} e:evidence }} e:sequent { {:bourges :route :blois} e:evidence }} e:sequent { {:bourges :route :orleans} e:evidence }} e:sequent { {:bourges :route :parijs} e:evidence }} e:sequent { {:bourges :route :chartres} e:evidence }} e:sequent { {:bourges :route :lemans} e:evidence }} e:sequent { {:bourges :route :angers} e:evidence }} e:sequent { {:bourges :route :nantes} e:evidence }. # Proof found in 1127 steps (18780 steps/sec) using 1 engine (306 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:42 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix gc: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {{{:Jos gc:childIn :dp} e:evidence . {:Maria gc:spouseIn :dp} e:evidence } e:sequent { {:Jos gc:parent :Maria} e:evidence }. {:Maria gc:sex gc:Female} e:evidence } e:sequent { {:Jos gc:mother :Maria} e:evidence }. {{{:Rita gc:childIn :dp} e:evidence . {:Maria gc:spouseIn :dp} e:evidence } e:sequent { {:Rita gc:parent :Maria} e:evidence }. {:Rita gc:sex gc:Female} e:evidence } e:sequent { {:Maria gc:daughter :Rita} e:evidence }. {{{:Bart gc:childIn :gd} e:evidence . {:Rita gc:spouseIn :gd} e:evidence } e:sequent { {:Bart gc:parent :Rita} e:evidence }. {:Bart gc:sex gc:Male} e:evidence } e:sequent { {:Rita gc:son :Bart} e:evidence }. {{{:Bart gc:childIn :gd} e:evidence . {:Rita gc:spouseIn :gd} e:evidence } e:sequent { {:Bart gc:parent :Rita} e:evidence }. {{{:Rita gc:childIn :dp} e:evidence . {:Jos gc:childIn :dp} e:evidence . {{owl:differentFrom rdf:type owl:SymmetricProperty} e:evidence . {{owl:differentFrom rdf:type owl:SymmetricProperty} e:evidence . { {:Rita log:notEqualTo :Jos} e:evidence . {:dp owl:distinctMembers (:Jos :Rita :Geert :Caroline :Dirk :Greta)} e:evidence . {{(:Jos :Rita :Geert :Caroline :Dirk :Greta) rdf:rest (:Rita :Geert :Caroline :Dirk :Greta)} e:evidence . {{(:Rita :Geert :Caroline :Dirk :Greta) rdf:first :Rita} e:evidence } e:sequent { {(:Rita :Geert :Caroline :Dirk :Greta) p0:item :Rita} e:evidence }} e:sequent { {(:Jos :Rita :Geert :Caroline :Dirk :Greta) p0:item :Rita} e:evidence }. {{(:Jos :Rita :Geert :Caroline :Dirk :Greta) rdf:first :Jos} e:evidence } e:sequent { {(:Jos :Rita :Geert :Caroline :Dirk :Greta) p0:item :Jos} e:evidence }} e:sequent { {:Rita owl:differentFrom :Jos} e:evidence }} e:sequent { {:Jos owl:differentFrom :Rita} e:evidence }} e:sequent { {:Rita owl:differentFrom :Jos} e:evidence }} e:sequent { {:Rita gc:sibling :Jos} e:evidence }. {:Jos gc:sex gc:Male} e:evidence } e:sequent { {:Rita gc:brother :Jos} e:evidence }} e:sequent { {:Bart gc:uncle :Jos} e:evidence }. # Proof found in 1804 steps (90154 steps/sec) using 1 engine (408 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:42 GMT @prefix log: . @prefix e: . (!log:semantics)!log:conjunction e:constructs { @prefix e: . @prefix q: . @prefix dc: . @prefix rdfs: . @prefix log: . @prefix : . @prefix rdf: . {_:e28423_6_ :includes _:e28431_6_} e:evidence . {_:e28455_6_ :includes _:e28463_6_} e:evidence . {_:e28475_6_ :includes _:e28483_6_} e:evidence . {_:e28503_6_ :includes _:e28511_6_} e:evidence . {_:e28523_6_ :includes _:e28531_6_} e:evidence . {_:e28551_6_ :includes _:e28559_6_} e:evidence . # Proof found in 6 steps (600000 steps/sec) using 1 engine (61 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:42 GMT @prefix log: . @prefix e: . (!log:semantics)!log:conjunction e:constructs { @prefix e: . @prefix q: . @prefix rdfs: . @prefix log: . @prefix : . @prefix rdf: . {:rec010 :year 2001} e:evidence . {:rec010 :month "May"} e:evidence . {:rec010 :city "Tel Aviv"} e:evidence . {:rec010 :film "Pokemon 2"} e:evidence . {:rec010 :cinema "Globus"} e:evidence . {:rec011 :year 2001} e:evidence . {:rec011 :month "May"} e:evidence . {:rec011 :city "Tel Aviv"} e:evidence . {:rec011 :film "Billy Elliot"} e:evidence . {:rec011 :cinema "Globus"} e:evidence . {:rec012 :year 2001} e:evidence . {:rec012 :month "May"} e:evidence . {:rec012 :city "Tel Aviv"} e:evidence . {:rec012 :film "The Mummy"} e:evidence . {:rec012 :cinema "Globus"} e:evidence . {:rec017 :year 2001} e:evidence . {:rec017 :month "May"} e:evidence . {:rec017 :city "Jerusalem"} e:evidence . {:rec017 :film "A Hard Day's Night"} e:evidence . {:rec017 :cinema "Globus"} e:evidence . {:rec018 :year 2001} e:evidence . {:rec018 :month "May"} e:evidence . {:rec018 :city "Jerusalem"} e:evidence . {:rec018 :film "15 Minutes"} e:evidence . {:rec018 :cinema "Globus"} e:evidence . # Proof found in 828 steps (82800000 steps/sec) using 1 engine (108 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:42 GMT @prefix log: . @prefix e: . (!log:semantics)!log:conjunction e:constructs { @prefix e: . @prefix q: . @prefix rdfs: . @prefix agg: . @prefix log: . @prefix : . @prefix rdf: . {_:e29730_8_ a agg:Company} e:evidence . {_:e29730_8_ agg:corporateHomepage } e:evidence . {_:e29730_8_ agg:owner _:e29750_8_} e:evidence . {_:e29750_8_ a agg:Person} e:evidence . {_:e29750_8_ agg:personalMailbox } e:evidence . {_:e29774_8_ a agg:User} e:evidence . {_:e29774_8_ agg:personalMailbox } e:evidence . {_:e29774_8_ agg:technologyInterest _:e29786_8_} e:evidence . {_:e29801_8_ a agg:Organisation} e:evidence . {_:e29801_8_ agg:corporateHomepage } e:evidence . {_:e29801_8_ agg:ethicalPolicy } e:evidence . {_:e29829_8_ a agg:Company} e:evidence . {_:e29829_8_ agg:corporateHomepage } e:evidence . {_:e29829_8_ agg:owner _:e29849_8_} e:evidence . {_:e29849_8_ a agg:Person} e:evidence . {_:e29849_8_ agg:personalMailbox } e:evidence . {_:e29873_8_ a agg:User} e:evidence . {_:e29873_8_ agg:personalMailbox } e:evidence . {_:e29873_8_ agg:technologyInterest _:e29885_8_} e:evidence . {_:e29900_8_ a agg:Organisation} e:evidence . {_:e29900_8_ agg:corporateHomepage } e:evidence . {_:e29900_8_ agg:ethicalPolicy } e:evidence . # Proof found in 123 steps (12300000 steps/sec) using 1 engine (40 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:43 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix foo: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix owl: . @prefix rdf: . {foo:a foo:b foo:c} e:evidence . {foo:a foo:d foo:e} e:evidence . {foo:f foo:g {foo:h foo:i foo:j}} e:evidence . {foo:a foo:b foo:c} e:evidence . {foo:a foo:d {foo:e foo:f foo:g}} e:evidence . {foo:a foo:b foo:c} e:evidence . {foo:a foo:b foo:d} e:evidence . {foo:a foo:b foo:e} e:evidence . {_:e30148_9_ foo:c foo:d} e:evidence . {_:e30148_9_ foo:a foo:b} e:evidence . {foo:a foo:b _:e30155_9_} e:evidence . {_:e30155_9_ foo:c foo:d} e:evidence . {_:e30178_9_ foo:g foo:h} e:evidence . {_:e30178_9_ foo:a foo:b} e:evidence . {_:e30178_9_ foo:c foo:d} e:evidence . {_:e30178_9_ foo:e foo:f} e:evidence . {_:e30193_9_ foo:g foo:h} e:evidence . {_:e30193_9_ foo:a _:e30200_9_} e:evidence . {_:e30200_9_ foo:b foo:c} e:evidence . {_:e30193_9_ foo:d _:e30203_9_} e:evidence . {_:e30203_9_ foo:e foo:f} e:evidence . {_:e30212_9_ foo:e foo:f} e:evidence . {_:e30212_9_ foo:a _:e30217_9_} e:evidence . {_:e30217_9_ foo:b _:e30221_9_} e:evidence . {_:e30221_9_ foo:c foo:d} e:evidence . {_:e30148_9_ foo:a foo:b} e:evidence . {_:e30242_9_ foo:c _:e30245_9_} e:evidence . {_:e30245_9_ foo:d foo:e} e:evidence . {_:e30242_9_ foo:a foo:b} e:evidence . {foo:c foo:b foo:a} e:evidence . {foo:c foo:b foo:a} e:evidence . {foo:a foo:d foo:e} e:evidence . {foo:a foo:b "c"} e:evidence . {foo:a foo:b "ok"@fr} e:evidence . {foo:a foo:b """c d"""} e:evidence . {foo:a foo:c "10"^^} e:evidence . {foo:a foo:c "bleu"@fr^^} e:evidence . {foo:a foo:c "blue"@en-US^^} e:evidence . {foo:a foo:c "10"^^xsd:int} e:evidence . {foo:a foo:c "bleu"@fr^^foo:mycolourspace} e:evidence . {foo:a foo:x "blue"@en-US^^_:x_9_} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {foo:jos foo:spouse _:e30307_9_} e:evidence . {_:e30307_9_ foo:firstName foo:mary} e:evidence . {foo:x foo:p _:e30375_9_} e:evidence . {_:e30375_9_ foo:q foo:z} e:evidence . {foo:foo foo:prop "<"^^rdf:XMLLiteral} e:evidence . {foo:bar foo:prop2 "0.5"^^xsd:int} e:evidence . {foo:a foo:b1 "-129"^^xsd:byte} e:evidence . {foo:a foo:b2 "-128"^^xsd:byte} e:evidence . {foo:a foo:b3 "127"^^xsd:byte} e:evidence . {foo:a foo:b4 "128"^^xsd:byte} e:evidence . {foo:a foo:i1 "-2147483649"^^xsd:int} e:evidence . {foo:a foo:i2 "-2147483648"^^xsd:int} e:evidence . {foo:a foo:i3 "2147483647"^^xsd:int} e:evidence . {foo:a foo:i4 "2147483648"^^xsd:int} e:evidence . {foo:a foo:l1 "-9223372036854775809"^^xsd:long} e:evidence . {foo:a foo:l2 "-9223372036854775808"^^xsd:long} e:evidence . {foo:a foo:l3 "9223372036854775807"^^xsd:long} e:evidence . {foo:a foo:l4 "9223372036854775808"^^xsd:long} e:evidence . {foo:a foo:s1 "-32769"^^xsd:short} e:evidence . {foo:a foo:s2 "-32768"^^xsd:short} e:evidence . {foo:a foo:s3 "32767"^^xsd:short} e:evidence . {foo:a foo:s4 "32768"^^xsd:short} e:evidence . {foo:a foo:ub1 "-1"^^xsd:unsignedByte} e:evidence . {foo:a foo:ub2 "0"^^xsd:unsignedByte} e:evidence . {foo:a foo:ub3 "255"^^xsd:unsignedByte} e:evidence . {foo:a foo:ub4 "256"^^xsd:unsignedByte} e:evidence . {foo:a foo:ui1 "-1"^^xsd:unsignedInt} e:evidence . {foo:a foo:ui2 "0"^^xsd:unsignedInt} e:evidence . {foo:a foo:ui3 "4294967295"^^xsd:unsignedInt} e:evidence . {foo:a foo:ui4 "4294967296"^^xsd:unsignedInt} e:evidence . {foo:a foo:ul1 "-1"^^xsd:unsignedLong} e:evidence . {foo:a foo:ul2 "0"^^xsd:unsignedLong} e:evidence . {foo:a foo:ul3 "18446744073709551615"^^xsd:unsignedLong} e:evidence . {foo:a foo:ul4 "18446744073709551616"^^xsd:unsignedLong} e:evidence . {foo:a foo:us1 "-1"^^xsd:unsignedShort} e:evidence . {foo:a foo:us2 "0"^^xsd:unsignedShort} e:evidence . {foo:a foo:us3 "65535"^^xsd:unsignedShort} e:evidence . {foo:a foo:us4 "65536"^^xsd:unsignedShort} e:evidence . {foo:a foo:ni1 "0"^^xsd:negativeInteger} e:evidence . {foo:a foo:ni2 "-1"^^xsd:negativeInteger} e:evidence . {foo:a foo:nni1 "0"^^xsd:nonNegativeInteger} e:evidence . {foo:a foo:nni2 "-1"^^xsd:nonNegativeInteger} e:evidence . {foo:a foo:npi1 "1"^^xsd:nonPositiveInteger} e:evidence . {foo:a foo:npi2 "0"^^xsd:nonPositiveInteger} e:evidence . {foo:a foo:pi1 "1"^^xsd:positiveInteger} e:evidence . {foo:a foo:pi2 "0"^^xsd:positiveInteger} e:evidence . {"0.3"^^xsd:float a xsd:integer} e:evidence . {foo:a foo:b "ok"@fr} e:evidence . {foo:c foo:d "100"^^xsd:int} e:evidence . {foo:e foo:f "bleu"@fr^^foo:colour} e:evidence . # Proof found in 1230 steps (17568 steps/sec) using 1 engine (395 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:43 GMT @prefix log: . @prefix e: . (!log:semantics)!log:conjunction e:constructs { @prefix e: . @prefix q: . @prefix rdfs: . @prefix log: . @prefix : . @prefix daml: . @prefix rdf: . { } e:evidence . { _:e43247_10_} e:evidence . {_:e43247_10_ } e:evidence . {_:e43247_10_ } e:evidence . {_:e43247_10_ "2"} e:evidence . { "Animal"} e:evidence . # Proof found in 7 steps (700000 steps/sec) using 1 engine (6 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:43 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix owl: . @prefix rdf: . {{:husband rdfs:subPropertyOf :spouse} e:evidence . {{:firstHusband rdfs:subPropertyOf :husband} e:evidence . {:Mary :firstHusband :Dan} e:evidence } e:sequent { {:Mary :husband :Dan} e:evidence }} e:sequent { {:Mary :spouse :Dan} e:evidence }. # Proof found in 4 steps (400000 steps/sec) using 1 engine (60 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:43 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix owl: . @prefix rdf: . {{:B rdfs:subClassOf :A} e:evidence . {:i a :B} e:evidence } e:sequent { {:i a :A} e:evidence }. # Proof found in 44 steps (4400000 steps/sec) using 1 engine (60 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:43 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix owl: . @prefix rdf: . {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdf:Alt rdfs:subClassOf rdfs:Container} e:evidence } e:sequent { {rdf:Alt a rdfs:Class} e:evidence }. {rdf:Alt a rdfs:Resource} e:evidence . {{{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdf:Alt rdfs:subClassOf rdfs:Container} e:evidence } e:sequent { {rdf:Alt a rdfs:Class} e:evidence }} e:sequent { {rdf:Alt rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdf:Bag rdfs:subClassOf rdfs:Container} e:evidence } e:sequent { {rdf:Bag a rdfs:Class} e:evidence }. {rdf:Bag a rdfs:Resource} e:evidence . {{{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdf:Bag rdfs:subClassOf rdfs:Container} e:evidence } e:sequent { {rdf:Bag a rdfs:Class} e:evidence }} e:sequent { {rdf:Bag rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . {rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence } e:sequent { {rdfs:Class a rdfs:Class} e:evidence }} e:sequent { {rdfs:Class rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { {rdfs:Class a rdfs:Class} e:evidence }. {rdfs:Class a rdfs:Resource} e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . {rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence } e:sequent { {rdfs:Class a rdfs:Class} e:evidence }} e:sequent { {rdfs:Class rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdfs:ContainerMembershipProperty rdfs:subClassOf rdf:Property} e:evidence } e:sequent { {rdfs:ContainerMembershipProperty a rdfs:Class} e:evidence }. {rdfs:ContainerMembershipProperty a rdfs:Resource} e:evidence . {{{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdfs:ContainerMembershipProperty rdfs:subClassOf rdf:Property} e:evidence } e:sequent { {rdfs:ContainerMembershipProperty a rdfs:Class} e:evidence }} e:sequent { {rdfs:ContainerMembershipProperty rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdfs:Datatype rdfs:subClassOf rdfs:Class} e:evidence } e:sequent { {rdfs:Datatype a rdfs:Class} e:evidence }. {rdfs:Datatype a rdfs:Resource} e:evidence . {{{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdfs:Datatype rdfs:subClassOf rdfs:Class} e:evidence } e:sequent { {rdfs:Datatype a rdfs:Class} e:evidence }} e:sequent { {rdfs:Datatype rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {{{rdfs:range rdfs:range rdfs:Class} e:evidence . {rdfs:comment rdfs:range rdfs:Literal} e:evidence } e:sequent { {rdfs:Literal a rdfs:Class} e:evidence }} e:sequent { {rdfs:Literal rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { {rdfs:Literal a rdfs:Class} e:evidence }. {rdfs:Literal a rdfs:Resource} e:evidence . {{{rdfs:range rdfs:range rdfs:Class} e:evidence . {rdfs:comment rdfs:range rdfs:Literal} e:evidence } e:sequent { {rdfs:Literal a rdfs:Class} e:evidence }} e:sequent { {rdfs:Literal rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . {rdf:first rdfs:domain rdf:List} e:evidence } e:sequent { {rdf:List a rdfs:Class} e:evidence }} e:sequent { {rdf:List rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { {rdf:List a rdfs:Class} e:evidence }. {rdf:List a rdfs:Resource} e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . {rdf:first rdfs:domain rdf:List} e:evidence } e:sequent { {rdf:List a rdfs:Class} e:evidence }} e:sequent { {rdf:List rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . {rdfs:domain rdfs:domain rdf:Property} e:evidence } e:sequent { {rdf:Property a rdfs:Class} e:evidence }} e:sequent { {rdf:Property rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { {rdf:Property a rdfs:Class} e:evidence }. {rdf:Property a rdfs:Resource} e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . {rdfs:domain rdfs:domain rdf:Property} e:evidence } e:sequent { {rdf:Property a rdfs:Class} e:evidence }} e:sequent { {rdf:Property rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . {rdfs:comment rdfs:domain rdfs:Resource} e:evidence } e:sequent { {rdfs:Resource a rdfs:Class} e:evidence }} e:sequent { {rdfs:Resource rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { {rdfs:Resource a rdfs:Class} e:evidence }. {rdfs:Resource a rdfs:Resource} e:evidence . {rdfs:Resource rdfs:subClassOf rdfs:Resource} e:evidence . {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdf:Seq rdfs:subClassOf rdfs:Container} e:evidence } e:sequent { {rdf:Seq a rdfs:Class} e:evidence }. {rdf:Seq a rdfs:Resource} e:evidence . {{{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdf:Seq rdfs:subClassOf rdfs:Container} e:evidence } e:sequent { {rdf:Seq a rdfs:Class} e:evidence }} e:sequent { {rdf:Seq rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . {rdf:object rdfs:domain rdf:Statement} e:evidence } e:sequent { {rdf:Statement a rdfs:Class} e:evidence }} e:sequent { {rdf:Statement rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { {rdf:Statement a rdfs:Class} e:evidence }. {rdf:Statement a rdfs:Resource} e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . {rdf:object rdfs:domain rdf:Statement} e:evidence } e:sequent { {rdf:Statement a rdfs:Class} e:evidence }} e:sequent { {rdf:Statement rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdf:XMLLiteral rdfs:subClassOf rdfs:Literal} e:evidence } e:sequent { {rdf:XMLLiteral a rdfs:Class} e:evidence }. {rdf:XMLLiteral a rdfs:Resource} e:evidence . {{{rdfs:subClassOf rdfs:domain rdfs:Class} e:evidence . {rdf:XMLLiteral rdfs:subClassOf rdfs:Literal} e:evidence } e:sequent { {rdf:XMLLiteral a rdfs:Class} e:evidence }} e:sequent { {rdf:XMLLiteral rdfs:subClassOf rdfs:Resource} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdfs:comment rdfs:domain rdfs:Resource} e:evidence } e:sequent { {rdfs:comment a rdf:Property} e:evidence }. {{rdfs:comment rdfs:domain rdfs:Resource} e:evidence } e:sequent { {rdfs:domain a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdf:first rdfs:domain rdf:List} e:evidence } e:sequent { {rdf:first a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdfs:isDefinedBy rdfs:domain rdfs:Resource} e:evidence } e:sequent { {rdfs:isDefinedBy a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdfs:label rdfs:domain rdfs:Resource} e:evidence } e:sequent { {rdfs:label a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdfs:member rdfs:domain rdfs:Container} e:evidence } e:sequent { {rdfs:member a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdf:object rdfs:domain rdf:Statement} e:evidence } e:sequent { {rdf:object a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdf:predicate rdfs:domain rdf:Statement} e:evidence } e:sequent { {rdf:predicate a rdf:Property} e:evidence }. {{rdfs:comment rdfs:range rdfs:Literal} e:evidence } e:sequent { {rdfs:range a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdf:rest rdfs:domain rdf:List} e:evidence } e:sequent { {rdf:rest a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdfs:seeAlso rdfs:domain rdfs:Resource} e:evidence } e:sequent { {rdfs:seeAlso a rdf:Property} e:evidence }. {{rdf:Alt rdfs:subClassOf rdfs:Container} e:evidence } e:sequent { {rdfs:subClassOf a rdf:Property} e:evidence }. {{rdfs:isDefinedBy rdfs:subPropertyOf rdfs:seeAlso} e:evidence } e:sequent { {rdfs:subPropertyOf a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdf:subject rdfs:domain rdf:Statement} e:evidence } e:sequent { {rdf:subject a rdf:Property} e:evidence }. {{rdf:XMLLiteral rdf:type rdfs:Datatype} e:evidence } e:sequent { {rdf:type a rdf:Property} e:evidence }. {{rdfs:domain rdfs:domain rdf:Property} e:evidence . {rdf:value rdfs:domain rdfs:Resource} e:evidence } e:sequent { {rdf:value a rdf:Property} e:evidence }. # Proof found in 1179 steps (7368 steps/sec) using 1 engine (57 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:43 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {:j owl:sameAs :i} e:evidence . {:o owl:sameAs :m} e:evidence . {{:H owl:oneOf (:s :m :t)} e:evidence . {{(:s :m :t) rdf:rest (:m :t)} e:evidence . {{(:m :t) rdf:first :m} e:evidence } e:sequent { {(:m :t) p0:item :m} e:evidence }} e:sequent { {(:s :m :t) p0:item :m} e:evidence }} e:sequent { {:m a :H} e:evidence }. {{:y owl:intersectionOf (:b :c)} e:evidence . {:x owl:intersectionOf (:a :b :c)} e:evidence . {{(:b :c) rdf:first :b} e:evidence . {{(:a :b :c) rdf:rest (:b :c)} e:evidence . {{(:b :c) rdf:first :b} e:evidence } e:sequent { {(:b :c) p0:item :b} e:evidence }} e:sequent { {(:a :b :c) p0:item :b} e:evidence }. {:b owl:equivalentClass :b} e:evidence . {(:b :c) rdf:rest (:c)} e:evidence . {{(:c) rdf:first :c} e:evidence . {{(:a :b :c) rdf:rest (:b :c)} e:evidence . {{(:b :c) rdf:rest (:c)} e:evidence . {{(:c) rdf:first :c} e:evidence } e:sequent { {(:c) p0:item :c} e:evidence }} e:sequent { {(:b :c) p0:item :c} e:evidence }} e:sequent { {(:a :b :c) p0:item :c} e:evidence }. {:c owl:equivalentClass :c} e:evidence . {(:c) rdf:rest ()} e:evidence . {(:a :b :c) p0:includes ()} e:evidence } e:sequent { {(:a :b :c) p0:includes (:c)} e:evidence }} e:sequent { {(:a :b :c) p0:includes (:b :c)} e:evidence }} e:sequent { {:x rdfs:subClassOf :y} e:evidence }. {{:y owl:intersectionOf (:b :c)} e:evidence . {{(:b :c) rdf:first :b} e:evidence . {{{:x owl:intersectionOf (:a :b :c)} e:evidence . {{(:a :b :c) rdf:rest (:b :c)} e:evidence . {{(:b :c) rdf:first :b} e:evidence } e:sequent { {(:b :c) p0:item :b} e:evidence }} e:sequent { {(:a :b :c) p0:item :b} e:evidence }} e:sequent { {:x rdfs:subClassOf :b} e:evidence }. {:J a :x} e:evidence } e:sequent { {:J a :b} e:evidence }. {(:b :c) rdf:rest (:c)} e:evidence . {{(:c) rdf:first :c} e:evidence . {{{:x owl:intersectionOf (:a :b :c)} e:evidence . {{(:a :b :c) rdf:rest (:b :c)} e:evidence . {{(:b :c) rdf:rest (:c)} e:evidence . {{(:c) rdf:first :c} e:evidence } e:sequent { {(:c) p0:item :c} e:evidence }} e:sequent { {(:b :c) p0:item :c} e:evidence }} e:sequent { {(:a :b :c) p0:item :c} e:evidence }} e:sequent { {:x rdfs:subClassOf :c} e:evidence }. {:J a :x} e:evidence } e:sequent { {:J a :c} e:evidence }. {(:c) rdf:rest ()} e:evidence . {:J p0:inAllOf ()} e:evidence } e:sequent { {:J p0:inAllOf (:c)} e:evidence }} e:sequent { {:J p0:inAllOf (:b :c)} e:evidence }} e:sequent { {:J a :y} e:evidence }. {{:test43 rdfs:subClassOf :test46} e:evidence . {{:test34 rdfs:subClassOf :test43} e:evidence . {:test3x a :test34} e:evidence } e:sequent { {:test3x a :test43} e:evidence }} e:sequent { {:test3x a :test46} e:evidence }. {{{:test43 rdfs:subClassOf :test34} e:evidence . {:test46 rdfs:subClassOf :test43} e:evidence } e:sequent { {:test46 rdfs:subClassOf :test34} e:evidence }. {{:test43 rdfs:subClassOf :test46} e:evidence . {:test34 rdfs:subClassOf :test43} e:evidence } e:sequent { {:test34 rdfs:subClassOf :test46} e:evidence }} e:sequent { {:test46 owl:equivalentClass :test34} e:evidence }. {{:R2 owl:onProperty :p2} e:evidence . {:R2 owl:hasValue :y2} e:evidence . {:x2 a :R2} e:evidence } e:sequent { {:x2 :p2 :y2} e:evidence }. {{:Automobile rdfs:subClassOf :Car} e:evidence . {:Car rdfs:subClassOf :Automobile} e:evidence } e:sequent { {:Automobile owl:equivalentClass :Car} e:evidence }. # Proof found in 8379 steps (167546 steps/sec) using 1 engine (312 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:43 GMT @prefix log: . @prefix e: . (!log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix rdf: . {("a" "b" "c") str:concatenation "abc"} e:evidence . {("a" "b" "c") str:concatenation "abc"} e:evidence . {"xyz" str:equalIgnoringCase "XYZ"} e:evidence . {"xyz" str:notEqualIgnoringCase "ABC"} e:evidence . {"xyz" str:greaterThan "abc"} e:evidence . {"abc" str:notGreaterThan "xyz"} e:evidence . {"abc" str:lessThan "xyz"} e:evidence . {"xyz" str:notLessThan "abc"} e:evidence . {"xyz" str:notLessThan "xyz"} e:evidence . {"abc" str:startsWith "ab"} e:evidence . {"abc" str:endsWith "bc"} e:evidence . {"abc" str:endsWith "abc"} e:evidence . {"abcXYZ" str:contains "cX"} e:evidence . {"abcXYZ" str:containsIgnoringCase "Cx"} e:evidence . {"abracadabra" str:matches "(a|b|r|c|d)+"} e:evidence . {"" str:notMatches ".*hello"} e:evidence . {(1.2 2.3 3.5) math:sum 7.0} e:evidence . {(7.0 1) math:difference 6.0} e:evidence . {(1 2 3) math:product 6} e:evidence . {(6 3) math:quotient 2.0} e:evidence . {(7 3) math:quotient 2.3333333333333335} e:evidence . {(7 3) math:integerQuotient 2} e:evidence . {(6.0 2.0) math:remainder 0.0} e:evidence . {(7 3) math:remainder 1} e:evidence . {-5 math:negation 5} e:evidence . {-5.1 math:absoluteValue 5.1} e:evidence . {-5.7 math:rounded -6} e:evidence . {(2 10) math:exponentiation 1024} e:evidence . {(1 2) math:atan2 0.4636476090008061} e:evidence . {2 math:cos -0.4161468365471424} e:evidence . {1.0471975511966 math:cos 0.499999999999998} e:evidence . {2 math:degrees 114.59155902616465} e:evidence . {2 math:sin 0.9092974268256817} e:evidence . {0.5235987755982989 math:sin 0.5} e:evidence . {2 math:tan -2.185039863261519} e:evidence . {0.4636476090008061 math:tan 0.5} e:evidence . {("a" ("b" "c") "d") math:memberCount 3} e:evidence . {6 math:greaterThan 2.0} e:evidence . {2.0 math:notGreaterThan 6} e:evidence . {2.0 math:lessThan 6} e:evidence . {6 math:notLessThan 2.0} e:evidence . {6 math:equalTo 6} e:evidence . {2.0 math:notEqualTo 6} e:evidence . {:x log:equalTo :x} e:evidence . {:x log:notEqualTo :y} e:evidence . {{:a :b :c. :d :e :f. :g :h :i} log:includes {:d :e :f}} e:evidence . {{:a :b :c. :d :e :f. :g :h :i} log:notIncludes {:d :x :f}} e:evidence . {("2005-03-30T11:00:00" :tz) log:dtlit "2005-03-30T11:00:00"^^:tz} e:evidence . {:q log:uri "http://www.agfa.com/w3c/euler/builtins#q"} e:evidence . # Proof found in 51 steps (1699 steps/sec) using 3 engines (0 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:43 GMT @prefix log: . @prefix e: . ()!log:conjunction e:constructs { @prefix e: . @prefix q: . @prefix rdfs: . @prefix log: . @prefix rdf: . # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:43 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix owl: . @prefix rdf: . {{ rdfs:domain } e:evidence . { } e:evidence } e:sequent { { } e:evidence }. {{ rdfs:domain } e:evidence . { } e:evidence } e:sequent { { } e:evidence }. {{ rdfs:range } e:evidence . { } e:evidence } e:sequent { { } e:evidence }. {{ rdfs:range } e:evidence . { } e:evidence } e:sequent { { } e:evidence }. {{rdfs:subClassOf rdfs:domain } e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . { rdfs:domain } e:evidence } e:sequent { { a rdfs:Class} e:evidence }} e:sequent { { rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { { } e:evidence }. {{rdfs:subClassOf rdfs:domain } e:evidence . {{{rdfs:domain rdfs:range rdfs:Class} e:evidence . { rdfs:domain } e:evidence } e:sequent { { a rdfs:Class} e:evidence }} e:sequent { { rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { { } e:evidence }. {{rdfs:subClassOf rdfs:domain } e:evidence . {{{rdfs:range rdfs:range rdfs:Class} e:evidence . { rdfs:range } e:evidence } e:sequent { { a rdfs:Class} e:evidence }} e:sequent { { rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { { } e:evidence }. {{rdfs:subClassOf rdfs:domain } e:evidence . {{{rdfs:range rdfs:range rdfs:Class} e:evidence . { rdfs:range } e:evidence } e:sequent { { a rdfs:Class} e:evidence }} e:sequent { { rdfs:subClassOf rdfs:Resource} e:evidence }} e:sequent { { } e:evidence }. # Proof found in 292 steps (29170 steps/sec) using 1 engine (64 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:44 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix owl: . @prefix rdf: . { } e:evidence . { } e:evidence . {{ rdfs:subPropertyOf } e:evidence . {{ rdf:type owl:TransitiveProperty} e:evidence . { } e:evidence . { } e:evidence } e:sequent { { } e:evidence }} e:sequent { { } e:evidence }. { } e:evidence . { } e:evidence . { } e:evidence . {{ rdf:type owl:TransitiveProperty} e:evidence . { } e:evidence . { } e:evidence } e:sequent { { } e:evidence }. { } e:evidence . { } e:evidence . # Proof found in 97 steps (9700000 steps/sec) using 1 engine (299 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:44 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix owl: . @prefix rdf: . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . # Proof found in 16 steps (1600000 steps/sec) using 1 engine (299 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:44 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix owl: . @prefix rdf: . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . # Proof found in 12 steps (1200000 steps/sec) using 1 engine (299 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:44 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix owl: . @prefix rdf: . {{ rdfs:subPropertyOf } e:evidence . {{ rdf:type owl:TransitiveProperty} e:evidence . { } e:evidence . { } e:evidence } e:sequent { { } e:evidence }} e:sequent { { } e:evidence }. {{ rdf:type owl:TransitiveProperty} e:evidence . { } e:evidence . { } e:evidence } e:sequent { { } e:evidence }. # Proof found in 85 steps (8491 steps/sec) using 1 engine (299 triples) }. # Proof found in 507 steps (1236 steps/sec) using 6 engines (0 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:44 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics)!log:conjunction e:constructs { @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix p1: . @prefix rgml: . @prefix rdf: . {p0:n1 a rgml:Node} e:evidence . {{p0:e1 rgml:source p0:n1} e:evidence . {p0:e1 rgml:target p0:n2} e:evidence } e:sequent { {p0:n1 :adjacent p0:n2} e:evidence }. # Proof found in 14 steps (699 steps/sec) using 1 engine (48 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:45 GMT @prefix log: . @prefix e: . (!log:semantics)!log:conjunction e:constructs { @prefix ct: . @prefix xlink: . @prefix util: . @prefix xyz: . @prefix sl: . @prefix ont_: . @prefix e: . @prefix q: . @prefix t: . @prefix html: . @prefix ci: . @prefix log: . @prefix contact: . @prefix cact: . @prefix rdfs: . @prefix cg: . @prefix foaf: . @prefix ont: . @prefix rcs: . @prefix ctop: . @prefix apt: . @prefix cs: . @prefix ical: . @prefix pa: . @prefix pd: . @prefix : . @prefix rdf: . @prefix dc: . @prefix ctrans: . @prefix v: . @prefix cal: . @prefix nav: . { } e:evidence . # Proof found in 1 step (100000 steps/sec) using 1 engine (916 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:45 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix math: . @prefix p0: . @prefix e: . @prefix usps: . @prefix q: . @prefix xsd: . @prefix log: . @prefix p1: . @prefix c: . @prefix dt: . @prefix rdfs: . @prefix ont: . @prefix : . @prefix rdf: . @prefix map: . @prefix str: . @prefix owl: . @prefix cn: . {:DanC cn:acquaintedWith :DanBri} e:evidence . {_:www2002_25_ cn:socialParticipants :DanBri} e:evidence . {_:www2002_25_ cn:inRegion _:e802935_25_} e:evidence . {{cn:temporalBoundsIntersect owl:inverseOf cn:temporalBoundsIntersect} e:evidence . {{cn:temporallyIntersects rdfs:subPropertyOf cn:temporalBoundsIntersect} e:evidence . {{{{cn:startingDate rdfs:subPropertyOf cn:startsDuring} e:evidence . {_:webConf_25_ cn:startingDate _:e802890_25_} e:evidence } e:sequent { {_:webConf_25_ cn:startsDuring _:e802890_25_} e:evidence }. {{cn:endingDate rdfs:subPropertyOf cn:endsDuring} e:evidence . {_:webConf_25_ cn:endingDate _:e802893_25_} e:evidence } e:sequent { {_:webConf_25_ cn:endsDuring _:e802893_25_} e:evidence }} e:sequent { {_:webConf_25_ cn:temporallySubsumes (_:e802890_25_ _:e802893_25_)} e:evidence }. {{{cn:startingDate rdfs:subPropertyOf cn:startsDuring} e:evidence . {_:www2002_25_ cn:startingDate _:e802890_25_} e:evidence } e:sequent { {_:www2002_25_ cn:startsDuring _:e802890_25_} e:evidence }. {{cn:endingDate rdfs:subPropertyOf cn:endsDuring} e:evidence . {_:www2002_25_ cn:endingDate _:e802893_25_} e:evidence } e:sequent { {_:www2002_25_ cn:endsDuring _:e802893_25_} e:evidence }} e:sequent { {_:www2002_25_ cn:temporallySubsumes (_:e802890_25_ _:e802893_25_)} e:evidence }} e:sequent { {_:webConf_25_ cn:temporallyIntersects _:www2002_25_} e:evidence }} e:sequent { {_:webConf_25_ cn:temporalBoundsIntersect _:www2002_25_} e:evidence }} e:sequent { {_:www2002_25_ cn:temporalBoundsIntersect _:webConf_25_} e:evidence }. {_:webConf_25_ cn:socialParticipants :DanC} e:evidence . {_:webConf_25_ cn:inRegion _:e802935_25_} e:evidence . {{cn:temporalBoundsIntersect owl:inverseOf cn:temporalBoundsIntersect} e:evidence . {{cn:temporallyIntersects rdfs:subPropertyOf cn:temporalBoundsIntersect} e:evidence . {{{{cn:startingDate rdfs:subPropertyOf cn:startsDuring} e:evidence . {_:webConf_25_ cn:startingDate _:e802890_25_} e:evidence } e:sequent { {_:webConf_25_ cn:startsDuring _:e802890_25_} e:evidence }. {{cn:endingDate rdfs:subPropertyOf cn:endsDuring} e:evidence . {_:webConf_25_ cn:endingDate _:e802893_25_} e:evidence } e:sequent { {_:webConf_25_ cn:endsDuring _:e802893_25_} e:evidence }} e:sequent { {_:webConf_25_ cn:temporallySubsumes (_:e802890_25_ _:e802893_25_)} e:evidence }. {{{cn:startingDate rdfs:subPropertyOf cn:startsDuring} e:evidence . {_:webConf_25_ cn:startingDate _:e802890_25_} e:evidence } e:sequent { {_:webConf_25_ cn:startsDuring _:e802890_25_} e:evidence }. {{cn:endingDate rdfs:subPropertyOf cn:endsDuring} e:evidence . {_:webConf_25_ cn:endingDate _:e802893_25_} e:evidence } e:sequent { {_:webConf_25_ cn:endsDuring _:e802893_25_} e:evidence }} e:sequent { {_:webConf_25_ cn:temporallySubsumes (_:e802890_25_ _:e802893_25_)} e:evidence }} e:sequent { {_:webConf_25_ cn:temporallyIntersects _:webConf_25_} e:evidence }} e:sequent { {_:webConf_25_ cn:temporalBoundsIntersect _:webConf_25_} e:evidence }} e:sequent { {_:webConf_25_ cn:temporalBoundsIntersect _:webConf_25_} e:evidence }. # Proof found in 609 steps (60839 steps/sec) using 1 engine (375 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:45 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {:road :repair "P14M3DT10H30M"^^xsd:duration} e:evidence . {:testcase :made "2002-11-16T00:41:00Z"^^xsd:dateTime} e:evidence . {:john :birthday "1956-01-10"^^xsd:date} e:evidence . {:john :birthday "1956-01"^^xsd:gYearMonth} e:evidence . {:john :birthday "1956"^^xsd:gYear} e:evidence . {:john :birthday "--01-10"^^xsd:gMonthDay} e:evidence . {:john :birthday "---10"^^xsd:gDay} e:evidence . {:john :birthday "--01--"^^xsd:gMonth} e:evidence . {:jane :age "+10.000"^^xsd:decimal} e:evidence . {:mary :ageS "11"} e:evidence . {:john :ageS "11"} e:evidence . {:jenny :age (10 5)!math:sum} e:evidence . {"10.1"^^xsd:decimal math:greaterThan "8.4"^^xsd:decimal} e:evidence . {"P1Y2M"^^xsd:duration math:notGreaterThan "P14MT10H"^^xsd:duration} e:evidence . {"01:41:00+01:00"^^xsd:time math:lessThan "05:41:00Z"^^xsd:time} e:evidence . {"1956-01-10"^^xsd:date math:notLessThan "1956-01-10"^^xsd:date} e:evidence . {"10"^^xsd:int math:equalTo "010"^^xsd:int} e:evidence . {"a" a rdfs:Literal} e:evidence . {5 a rdfs:Literal} e:evidence . {5.0 a rdfs:Literal} e:evidence . {0.5e1 a rdfs:Literal} e:evidence . {:aaa :ppp "333"^^xsd:int} e:evidence . {:bbb :ppp " 333 "^^xsd:int} e:evidence . {:bbb :ppp "333"^^xsd:int} e:evidence . {"333"^^xsd:int a rdfs:Literal} e:evidence . {:foo :bar "chat"@fr^^rdf:XMLLiteral} e:evidence . {:foo :bar "chat"@fr^^:baz} e:evidence . {:ccc :qqq "sss"@en-US} e:evidence . {:Jane :age "15"^^xsd:decimal} e:evidence . {:JaneC :age "15"^^xsd:byte} e:evidence . {:doc :language "en-US"} e:evidence . {:doc2 :language "en-US"} e:evidence . {:doc :language "en-US"} e:evidence . {:Jeremy :ageInYears "40"^^xsd:float} e:evidence . {:JeremyC :ageInYears "40"^^xsd:float} e:evidence . {:car :engineSizeInLitres "1.3"^^xsd:float} e:evidence . {:car2 :engineSizeInLitres "1.3"^^xsd:float} e:evidence . {:doc :identifier "http://www.example.org/doc"} e:evidence . # Proof found in 65 steps (3248 steps/sec) using 1 engine (213 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:45 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {:meas47 :p1xCm 10.1} e:evidence . {(-0.06285714285714286 10.1) math:product -0.6348571428571429} e:evidence } e:sequent { {:meas47 :pL1x1Cm -0.6348571428571429} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {(1 -0.06285714285714286) math:quotient -15.909090909090908} e:evidence } e:sequent { {:meas47 :dL3m -15.909090909090908} e:evidence }. {(0 -15.909090909090908) math:difference 15.909090909090908} e:evidence } e:sequent { {:meas47 :cL3 15.909090909090908} e:evidence }. {:meas47 :p3xCm 3.6} e:evidence . {(15.909090909090908 3.6) math:product 57.27272727272727} e:evidence } e:sequent { {:meas47 :pL3x3Cm 57.27272727272727} e:evidence }. {(-0.6348571428571429 57.27272727272727) math:difference -57.90758441558442} e:evidence } e:sequent { {:meas47 :dd13Cm -57.90758441558442} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p3yCm 29.8} e:evidence . {(7.8 29.8) math:difference -22.0} e:evidence } e:sequent { {:meas47 :dy13Cm -22.0} e:evidence }. {(-57.90758441558442 -22.0) math:difference -35.90758441558442} e:evidence } e:sequent { {:meas47 :ddy13Cm -35.90758441558442} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {(1 -0.06285714285714286) math:quotient -15.909090909090908} e:evidence } e:sequent { {:meas47 :dL3m -15.909090909090908} e:evidence }. {(0 -15.909090909090908) math:difference 15.909090909090908} e:evidence } e:sequent { {:meas47 :cL3 15.909090909090908} e:evidence }. {(-0.06285714285714286 15.909090909090908) math:difference -15.97194805194805} e:evidence } e:sequent { {:meas47 :ddL13 -15.97194805194805} e:evidence }. {(-35.90758441558442 -15.97194805194805) math:quotient 2.248165615039355} e:evidence } e:sequent { {:meas47 :p5xCm 2.248165615039355} e:evidence }. {:meas47 :p3xCm 3.6} e:evidence . {(2.248165615039355 3.6) math:difference -1.351834384960645} e:evidence } e:sequent { {:meas47 :dx53Cm -1.351834384960645} e:evidence }. {(-1.351834384960645 2) math:exponentiation 1.8274562043619251} e:evidence } e:sequent { {:meas47 :sdx53Cm2 1.8274562043619251} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {:meas47 :p1xCm 10.1} e:evidence . {(-0.06285714285714286 10.1) math:product -0.6348571428571429} e:evidence } e:sequent { {:meas47 :pL1x1Cm -0.6348571428571429} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {(1 -0.06285714285714286) math:quotient -15.909090909090908} e:evidence } e:sequent { {:meas47 :dL3m -15.909090909090908} e:evidence }. {(0 -15.909090909090908) math:difference 15.909090909090908} e:evidence } e:sequent { {:meas47 :cL3 15.909090909090908} e:evidence }. {:meas47 :p3xCm 3.6} e:evidence . {(15.909090909090908 3.6) math:product 57.27272727272727} e:evidence } e:sequent { {:meas47 :pL3x3Cm 57.27272727272727} e:evidence }. {(-0.6348571428571429 57.27272727272727) math:difference -57.90758441558442} e:evidence } e:sequent { {:meas47 :dd13Cm -57.90758441558442} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p3yCm 29.8} e:evidence . {(7.8 29.8) math:difference -22.0} e:evidence } e:sequent { {:meas47 :dy13Cm -22.0} e:evidence }. {(-57.90758441558442 -22.0) math:difference -35.90758441558442} e:evidence } e:sequent { {:meas47 :ddy13Cm -35.90758441558442} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {(1 -0.06285714285714286) math:quotient -15.909090909090908} e:evidence } e:sequent { {:meas47 :dL3m -15.909090909090908} e:evidence }. {(0 -15.909090909090908) math:difference 15.909090909090908} e:evidence } e:sequent { {:meas47 :cL3 15.909090909090908} e:evidence }. {(-0.06285714285714286 15.909090909090908) math:difference -15.97194805194805} e:evidence } e:sequent { {:meas47 :ddL13 -15.97194805194805} e:evidence }. {(-35.90758441558442 -15.97194805194805) math:quotient 2.248165615039355} e:evidence } e:sequent { {:meas47 :p5xCm 2.248165615039355} e:evidence }. {:meas47 :p1xCm 10.1} e:evidence . {(2.248165615039355 10.1) math:difference -7.851834384960645} e:evidence } e:sequent { {:meas47 :dx51Cm -7.851834384960645} e:evidence }. {(-0.06285714285714286 -7.851834384960645) math:product 0.4935438756260977} e:evidence } e:sequent { {:meas47 :pL1dx51Cm 0.4935438756260977} e:evidence }. {:meas47 :p1yCm 7.8} e:evidence . {(0.4935438756260977 7.8) math:sum 8.293543875626098} e:evidence } e:sequent { {:meas47 :p5yCm 8.293543875626098} e:evidence }. {:meas47 :p3yCm 29.8} e:evidence . {(8.293543875626098 29.8) math:difference -21.506456124373905} e:evidence } e:sequent { {:meas47 :dy53Cm -21.506456124373905} e:evidence }. {(-21.506456124373905 2) math:exponentiation 462.52765502961984} e:evidence } e:sequent { {:meas47 :sdy53Cm2 462.52765502961984} e:evidence }. {(1.8274562043619251 462.52765502961984) math:sum 464.35511123398175} e:evidence } e:sequent { {:meas47 :ssd53Cm2 464.35511123398175} e:evidence }. {(464.35511123398175 0.5) math:exponentiation 21.548900464617255} e:evidence } e:sequent { {:meas47 :d53Cm 21.548900464617255} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {:meas47 :p2xCm 45.1} e:evidence . {(-0.06285714285714286 45.1) math:product -2.834857142857143} e:evidence } e:sequent { {:meas47 :pL1x2Cm -2.834857142857143} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {(1 -0.06285714285714286) math:quotient -15.909090909090908} e:evidence } e:sequent { {:meas47 :dL3m -15.909090909090908} e:evidence }. {(0 -15.909090909090908) math:difference 15.909090909090908} e:evidence } e:sequent { {:meas47 :cL3 15.909090909090908} e:evidence }. {:meas47 :p4xCm 54.7} e:evidence . {(15.909090909090908 54.7) math:product 870.2272727272727} e:evidence } e:sequent { {:meas47 :pL3x4Cm 870.2272727272727} e:evidence }. {(-2.834857142857143 870.2272727272727) math:difference -873.0621298701299} e:evidence } e:sequent { {:meas47 :dd24Cm -873.0621298701299} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {:meas47 :p4yCm 28.5} e:evidence . {(5.6 28.5) math:difference -22.9} e:evidence } e:sequent { {:meas47 :dy24Cm -22.9} e:evidence }. {(-873.0621298701299 -22.9) math:difference -850.1621298701299} e:evidence } e:sequent { {:meas47 :ddy24Cm -850.1621298701299} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {(1 -0.06285714285714286) math:quotient -15.909090909090908} e:evidence } e:sequent { {:meas47 :dL3m -15.909090909090908} e:evidence }. {(0 -15.909090909090908) math:difference 15.909090909090908} e:evidence } e:sequent { {:meas47 :cL3 15.909090909090908} e:evidence }. {(-0.06285714285714286 15.909090909090908) math:difference -15.97194805194805} e:evidence } e:sequent { {:meas47 :ddL13 -15.97194805194805} e:evidence }. {(-850.1621298701299 -15.97194805194805) math:quotient 53.22845573407923} e:evidence } e:sequent { {:meas47 :p6xCm 53.22845573407923} e:evidence }. {:meas47 :p4xCm 54.7} e:evidence . {(53.22845573407923 54.7) math:difference -1.4715442659207696} e:evidence } e:sequent { {:meas47 :dx64Cm -1.4715442659207696} e:evidence }. {(-1.4715442659207696 2) math:exponentiation 2.1654425265642967} e:evidence } e:sequent { {:meas47 :sdx64Cm2 2.1654425265642967} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {:meas47 :p2xCm 45.1} e:evidence . {(-0.06285714285714286 45.1) math:product -2.834857142857143} e:evidence } e:sequent { {:meas47 :pL1x2Cm -2.834857142857143} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {(1 -0.06285714285714286) math:quotient -15.909090909090908} e:evidence } e:sequent { {:meas47 :dL3m -15.909090909090908} e:evidence }. {(0 -15.909090909090908) math:difference 15.909090909090908} e:evidence } e:sequent { {:meas47 :cL3 15.909090909090908} e:evidence }. {:meas47 :p4xCm 54.7} e:evidence . {(15.909090909090908 54.7) math:product 870.2272727272727} e:evidence } e:sequent { {:meas47 :pL3x4Cm 870.2272727272727} e:evidence }. {(-2.834857142857143 870.2272727272727) math:difference -873.0621298701299} e:evidence } e:sequent { {:meas47 :dd24Cm -873.0621298701299} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {:meas47 :p4yCm 28.5} e:evidence . {(5.6 28.5) math:difference -22.9} e:evidence } e:sequent { {:meas47 :dy24Cm -22.9} e:evidence }. {(-873.0621298701299 -22.9) math:difference -850.1621298701299} e:evidence } e:sequent { {:meas47 :ddy24Cm -850.1621298701299} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {{:meas47 a :Measurement} e:evidence . {:meas47 :p1yCm 7.8} e:evidence . {:meas47 :p2yCm 5.6} e:evidence . {(7.8 5.6) math:difference 2.2} e:evidence } e:sequent { {:meas47 :dy12Cm 2.2} e:evidence }. {{:meas47 a :Measurement} e:evidence . {:meas47 :p1xCm 10.1} e:evidence . {:meas47 :p2xCm 45.1} e:evidence . {(10.1 45.1) math:difference -35.0} e:evidence } e:sequent { {:meas47 :dx12Cm -35.0} e:evidence }. {(2.2 -35.0) math:quotient -0.06285714285714286} e:evidence } e:sequent { {:meas47 :cL1 -0.06285714285714286} e:evidence }. {(1 -0.06285714285714286) math:quotient -15.909090909090908} e:evidence } e:sequent { {:meas47 :dL3m -15.909090909090908} e:evidence }. {(0 -15.909090909090908) math:difference 15.909090909090908} e:evidence } e:sequent { {:meas47 :cL3 15.909090909090908} e:evidence }. {(-0.06285714285714286 15.909090909090908) math:difference -15.97194805194805} e:evidence } e:sequent { {:meas47 :ddL13 -15.97194805194805} e:evidence }. {(-850.1621298701299 -15.97194805194805) math:quotient 53.22845573407923} e:evidence } e:sequent { {:meas47 :p6xCm 53.22845573407923} e:evidence }. {:meas47 :p2xCm 45.1} e:evidence . {(53.22845573407923 45.1) math:difference 8.128455734079232} e:evidence } e:sequent { {:meas47 :dx62Cm 8.128455734079232} e:evidence }. {(-0.06285714285714286 8.128455734079232) math:product -0.5109315032849803} e:evidence } e:sequent { {:meas47 :pL1dx62Cm -0.5109315032849803} e:evidence }. {:meas47 :p2yCm 5.6} e:evidence . {(-0.5109315032849803 5.6) math:sum 5.0890684967150195} e:evidence } e:sequent { {:meas47 :p6yCm 5.0890684967150195} e:evidence }. {:meas47 :p4yCm 28.5} e:evidence . {(5.0890684967150195 28.5) math:difference -23.41093150328498} e:evidence } e:sequent { {:meas47 :dy64Cm -23.41093150328498} e:evidence }. {(-23.41093150328498 2) math:exponentiation 548.0717138515012} e:evidence } e:sequent { {:meas47 :sdy64Cm2 548.0717138515012} e:evidence }. {(2.1654425265642967 548.0717138515012) math:sum 550.2371563780655} e:evidence } e:sequent { {:meas47 :ssd64Cm2 550.2371563780655} e:evidence }. {(550.2371563780655 0.5) math:exponentiation 23.45713444515475} e:evidence } e:sequent { {:meas47 :d64Cm 23.45713444515475} e:evidence }. {(21.548900464617255 23.45713444515475) math:difference -1.9082339805374957} e:evidence } e:sequent { {:meas47 :dCm -1.9082339805374957} e:evidence }. {-1.9082339805374957 math:lessThan -1.25} e:evidence } e:sequent { {:meas47 a :LLDAlarm} e:evidence }. # Proof found in 344 steps (4299 steps/sec) using 1 engine (456 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:46 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {:johnDoe a :Contact} e:evidence . {{:johnDoe :bornYear 1946} e:evidence . {:johnDoe :bornMonth 11} e:evidence . {:johnDoe :bornDay 1} e:evidence . {:johnDoe :diedYear 2001} e:evidence . { :forYear 1999} e:evidence . {1999 math:notLessThan 1946} e:evidence . {1999 math:lessThan 2001} e:evidence . {(1999 "-" 11 "-" 1) str:concatenation "1999-11-1"} e:evidence } e:sequent { {:johnDoe :happyBirthDay "1999-11-1"} e:evidence }. {:johnDoe a :Contact} e:evidence . {{:johnDoe :bornYear 1946} e:evidence . {:johnDoe :bornMonth 11} e:evidence . {:johnDoe :bornDay 1} e:evidence . {:johnDoe :diedYear 2001} e:evidence . { :forYear 2000} e:evidence . {2000 math:notLessThan 1946} e:evidence . {2000 math:lessThan 2001} e:evidence . {(2000 "-" 11 "-" 1) str:concatenation "2000-11-1"} e:evidence } e:sequent { {:johnDoe :happyBirthDay "2000-11-1"} e:evidence }. {:johnDoe a :Contact} e:evidence . {{:johnDoe :bornYear 1946} e:evidence . {:johnDoe :bornMonth 11} e:evidence . {:johnDoe :bornDay 1} e:evidence . {:johnDoe :diedYear 2001} e:evidence . {:johnDoe :diedMonth 11} e:evidence . {:johnDoe :diedDay 3} e:evidence . { :forYear 2001} e:evidence . {1 math:lessThan 3} e:evidence . {(2001 "-" 11 "-" 1) str:concatenation "2001-11-1"} e:evidence } e:sequent { {:johnDoe :happyBirthDay "2001-11-1"} e:evidence }. {:janeDoe a :Contact} e:evidence . {{:janeDoe a :LivePerson} e:evidence . {:janeDoe :bornYear 2000} e:evidence . {:janeDoe :bornMonth 4} e:evidence . {:janeDoe :bornDay 13} e:evidence . { :forYear 2000} e:evidence . {2000 math:notLessThan 2000} e:evidence . {(2000 "-" 4 "-" 13) str:concatenation "2000-4-13"} e:evidence } e:sequent { {:janeDoe :happyBirthDay "2000-4-13"} e:evidence }. {:janeDoe a :Contact} e:evidence . {{:janeDoe a :LivePerson} e:evidence . {:janeDoe :bornYear 2000} e:evidence . {:janeDoe :bornMonth 4} e:evidence . {:janeDoe :bornDay 13} e:evidence . { :forYear 2001} e:evidence . {2001 math:notLessThan 2000} e:evidence . {(2001 "-" 4 "-" 13) str:concatenation "2001-4-13"} e:evidence } e:sequent { {:janeDoe :happyBirthDay "2001-4-13"} e:evidence }. {:janeDoe a :Contact} e:evidence . {{:janeDoe a :LivePerson} e:evidence . {:janeDoe :bornYear 2000} e:evidence . {:janeDoe :bornMonth 4} e:evidence . {:janeDoe :bornDay 13} e:evidence . { :forYear 2002} e:evidence . {2002 math:notLessThan 2000} e:evidence . {(2002 "-" 4 "-" 13) str:concatenation "2002-4-13"} e:evidence } e:sequent { {:janeDoe :happyBirthDay "2002-4-13"} e:evidence }. {:janeDoe a :Contact} e:evidence . {{:janeDoe a :LivePerson} e:evidence . {:janeDoe :bornYear 2000} e:evidence . {:janeDoe :bornMonth 4} e:evidence . {:janeDoe :bornDay 13} e:evidence . { :forYear 2003} e:evidence . {2003 math:notLessThan 2000} e:evidence . {(2003 "-" 4 "-" 13) str:concatenation "2003-4-13"} e:evidence } e:sequent { {:janeDoe :happyBirthDay "2003-4-13"} e:evidence }. # Proof found in 8492 steps (169806 steps/sec) using 1 engine (310 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:46 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics)!log:conjunction e:constructs { @prefix e: . @prefix q: . @prefix xsd: . @prefix rdfs: . @prefix log: . @prefix : . @prefix owl: . @prefix rdf: . {:x log:equalTo :x} e:evidence . {:x log:notEqualTo :y} e:evidence . {{:a :b :c. :d :e :f. :g :h :i} log:includes {:d :e :f}} e:evidence . {{:a :b :c. :d :e :f. :g :h :i} log:notIncludes {:d :x :f}} e:evidence . {:foo :bar :baz} e:evidence . # Proof found in 7 steps (700000 steps/sec) using 3 engines (2 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:46 GMT @prefix log: . @prefix e: . (!log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix owl: . @prefix rdf: . {2003 a :Year} e:evidence . {{2003 a :Year} e:evidence . {(2003 19) math:remainder 8} e:evidence . {(2003 100) math:integerQuotient 20} e:evidence . {(2003 100) math:remainder 3} e:evidence . {(20 4) math:integerQuotient 5} e:evidence . {(20 4) math:remainder 0} e:evidence . {((20 8)!math:sum 25) math:integerQuotient 1} e:evidence . {(((20 1)!math:difference 1)!math:sum 3) math:integerQuotient 6} e:evidence . {((((((19 8)!math:product 20)!math:sum 5)!math:difference 6)!math:difference 15)!math:sum 30) math:remainder 26} e:evidence . {(3 4) math:integerQuotient 0} e:evidence . {(3 4) math:remainder 3} e:evidence . {((32 (2 0)!math:product (2 0)!math:product 26!math:negation 3!math:negation)!math:sum 7) math:remainder 3} e:evidence . {((8 (11 26)!math:product (22 3)!math:product)!math:sum 451) math:integerQuotient 0} e:evidence . {((26 3 (7 0)!math:product!math:negation 114)!math:sum 31) math:integerQuotient 4} e:evidence . {((26 3 (7 0)!math:product!math:negation 114)!math:sum 31) math:remainder 19} e:evidence . {(19 1) math:sum 20} e:evidence } e:sequent { {2003 :hasEasterOnDay 20} e:evidence }. {{2003 a :Year} e:evidence . {(2003 19) math:remainder 8} e:evidence . {(2003 100) math:integerQuotient 20} e:evidence . {(2003 100) math:remainder 3} e:evidence . {(20 4) math:integerQuotient 5} e:evidence . {(20 4) math:remainder 0} e:evidence . {((20 8)!math:sum 25) math:integerQuotient 1} e:evidence . {(((20 1)!math:difference 1)!math:sum 3) math:integerQuotient 6} e:evidence . {((((((19 8)!math:product 20)!math:sum 5)!math:difference 6)!math:difference 15)!math:sum 30) math:remainder 26} e:evidence . {(3 4) math:integerQuotient 0} e:evidence . {(3 4) math:remainder 3} e:evidence . {((32 (2 0)!math:product (2 0)!math:product 26!math:negation 3!math:negation)!math:sum 7) math:remainder 3} e:evidence . {((8 (11 26)!math:product (22 3)!math:product)!math:sum 451) math:integerQuotient 0} e:evidence . {((26 3 (7 0)!math:product!math:negation 114)!math:sum 31) math:integerQuotient 4} e:evidence . {((26 3 (7 0)!math:product!math:negation 114)!math:sum 31) math:remainder 19} e:evidence . {(19 1) math:sum 20} e:evidence } e:sequent { {2003 :hasEasterOnMonth 4} e:evidence }. {2004 a :Year} e:evidence . {{2004 a :Year} e:evidence . {(2004 19) math:remainder 9} e:evidence . {(2004 100) math:integerQuotient 20} e:evidence . {(2004 100) math:remainder 4} e:evidence . {(20 4) math:integerQuotient 5} e:evidence . {(20 4) math:remainder 0} e:evidence . {((20 8)!math:sum 25) math:integerQuotient 1} e:evidence . {(((20 1)!math:difference 1)!math:sum 3) math:integerQuotient 6} e:evidence . {((((((19 9)!math:product 20)!math:sum 5)!math:difference 6)!math:difference 15)!math:sum 30) math:remainder 15} e:evidence . {(4 4) math:integerQuotient 1} e:evidence . {(4 4) math:remainder 0} e:evidence . {((32 (2 0)!math:product (2 1)!math:product 15!math:negation 0!math:negation)!math:sum 7) math:remainder 5} e:evidence . {((9 (11 15)!math:product (22 5)!math:product)!math:sum 451) math:integerQuotient 0} e:evidence . {((15 5 (7 0)!math:product!math:negation 114)!math:sum 31) math:integerQuotient 4} e:evidence . {((15 5 (7 0)!math:product!math:negation 114)!math:sum 31) math:remainder 10} e:evidence . {(10 1) math:sum 11} e:evidence } e:sequent { {2004 :hasEasterOnDay 11} e:evidence }. {{2004 a :Year} e:evidence . {(2004 19) math:remainder 9} e:evidence . {(2004 100) math:integerQuotient 20} e:evidence . {(2004 100) math:remainder 4} e:evidence . {(20 4) math:integerQuotient 5} e:evidence . {(20 4) math:remainder 0} e:evidence . {((20 8)!math:sum 25) math:integerQuotient 1} e:evidence . {(((20 1)!math:difference 1)!math:sum 3) math:integerQuotient 6} e:evidence . {((((((19 9)!math:product 20)!math:sum 5)!math:difference 6)!math:difference 15)!math:sum 30) math:remainder 15} e:evidence . {(4 4) math:integerQuotient 1} e:evidence . {(4 4) math:remainder 0} e:evidence . {((32 (2 0)!math:product (2 1)!math:product 15!math:negation 0!math:negation)!math:sum 7) math:remainder 5} e:evidence . {((9 (11 15)!math:product (22 5)!math:product)!math:sum 451) math:integerQuotient 0} e:evidence . {((15 5 (7 0)!math:product!math:negation 114)!math:sum 31) math:integerQuotient 4} e:evidence . {((15 5 (7 0)!math:product!math:negation 114)!math:sum 31) math:remainder 10} e:evidence . {(10 1) math:sum 11} e:evidence } e:sequent { {2004 :hasEasterOnMonth 4} e:evidence }. {2005 a :Year} e:evidence . {{2005 a :Year} e:evidence . {(2005 19) math:remainder 10} e:evidence . {(2005 100) math:integerQuotient 20} e:evidence . {(2005 100) math:remainder 5} e:evidence . {(20 4) math:integerQuotient 5} e:evidence . {(20 4) math:remainder 0} e:evidence . {((20 8)!math:sum 25) math:integerQuotient 1} e:evidence . {(((20 1)!math:difference 1)!math:sum 3) math:integerQuotient 6} e:evidence . {((((((19 10)!math:product 20)!math:sum 5)!math:difference 6)!math:difference 15)!math:sum 30) math:remainder 4} e:evidence . {(5 4) math:integerQuotient 1} e:evidence . {(5 4) math:remainder 1} e:evidence . {((32 (2 0)!math:product (2 1)!math:product 4!math:negation 1!math:negation)!math:sum 7) math:remainder 1} e:evidence . {((10 (11 4)!math:product (22 1)!math:product)!math:sum 451) math:integerQuotient 0} e:evidence . {((4 1 (7 0)!math:product!math:negation 114)!math:sum 31) math:integerQuotient 3} e:evidence . {((4 1 (7 0)!math:product!math:negation 114)!math:sum 31) math:remainder 26} e:evidence . {(26 1) math:sum 27} e:evidence } e:sequent { {2005 :hasEasterOnDay 27} e:evidence }. {{2005 a :Year} e:evidence . {(2005 19) math:remainder 10} e:evidence . {(2005 100) math:integerQuotient 20} e:evidence . {(2005 100) math:remainder 5} e:evidence . {(20 4) math:integerQuotient 5} e:evidence . {(20 4) math:remainder 0} e:evidence . {((20 8)!math:sum 25) math:integerQuotient 1} e:evidence . {(((20 1)!math:difference 1)!math:sum 3) math:integerQuotient 6} e:evidence . {((((((19 10)!math:product 20)!math:sum 5)!math:difference 6)!math:difference 15)!math:sum 30) math:remainder 4} e:evidence . {(5 4) math:integerQuotient 1} e:evidence . {(5 4) math:remainder 1} e:evidence . {((32 (2 0)!math:product (2 1)!math:product 4!math:negation 1!math:negation)!math:sum 7) math:remainder 1} e:evidence . {((10 (11 4)!math:product (22 1)!math:product)!math:sum 451) math:integerQuotient 0} e:evidence . {((4 1 (7 0)!math:product!math:negation 114)!math:sum 31) math:integerQuotient 3} e:evidence . {((4 1 (7 0)!math:product!math:negation 114)!math:sum 31) math:remainder 26} e:evidence . {(26 1) math:sum 27} e:evidence } e:sequent { {2005 :hasEasterOnMonth 3} e:evidence }. {2006 a :Year} e:evidence . {{2006 a :Year} e:evidence . {(2006 19) math:remainder 11} e:evidence . {(2006 100) math:integerQuotient 20} e:evidence . {(2006 100) math:remainder 6} e:evidence . {(20 4) math:integerQuotient 5} e:evidence . {(20 4) math:remainder 0} e:evidence . {((20 8)!math:sum 25) math:integerQuotient 1} e:evidence . {(((20 1)!math:difference 1)!math:sum 3) math:integerQuotient 6} e:evidence . {((((((19 11)!math:product 20)!math:sum 5)!math:difference 6)!math:difference 15)!math:sum 30) math:remainder 23} e:evidence . {(6 4) math:integerQuotient 1} e:evidence . {(6 4) math:remainder 2} e:evidence . {((32 (2 0)!math:product (2 1)!math:product 23!math:negation 2!math:negation)!math:sum 7) math:remainder 2} e:evidence . {((11 (11 23)!math:product (22 2)!math:product)!math:sum 451) math:integerQuotient 0} e:evidence . {((23 2 (7 0)!math:product!math:negation 114)!math:sum 31) math:integerQuotient 4} e:evidence . {((23 2 (7 0)!math:product!math:negation 114)!math:sum 31) math:remainder 15} e:evidence . {(15 1) math:sum 16} e:evidence } e:sequent { {2006 :hasEasterOnDay 16} e:evidence }. {{2006 a :Year} e:evidence . {(2006 19) math:remainder 11} e:evidence . {(2006 100) math:integerQuotient 20} e:evidence . {(2006 100) math:remainder 6} e:evidence . {(20 4) math:integerQuotient 5} e:evidence . {(20 4) math:remainder 0} e:evidence . {((20 8)!math:sum 25) math:integerQuotient 1} e:evidence . {(((20 1)!math:difference 1)!math:sum 3) math:integerQuotient 6} e:evidence . {((((((19 11)!math:product 20)!math:sum 5)!math:difference 6)!math:difference 15)!math:sum 30) math:remainder 23} e:evidence . {(6 4) math:integerQuotient 1} e:evidence . {(6 4) math:remainder 2} e:evidence . {((32 (2 0)!math:product (2 1)!math:product 23!math:negation 2!math:negation)!math:sum 7) math:remainder 2} e:evidence . {((11 (11 23)!math:product (22 2)!math:product)!math:sum 451) math:integerQuotient 0} e:evidence . {((23 2 (7 0)!math:product!math:negation 114)!math:sum 31) math:integerQuotient 4} e:evidence . {((23 2 (7 0)!math:product!math:negation 114)!math:sum 31) math:remainder 15} e:evidence . {(15 1) math:sum 16} e:evidence } e:sequent { {2006 :hasEasterOnMonth 4} e:evidence }. # Proof found in 988 steps (2663 steps/sec) using 1 engine (7 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:46 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {{:Continent owl:oneOf (:Africa :Antarctica :Asia :Australia :Europe :NorthAmerica :SouthAmerica)} e:evidence . {{:containsLocation owl:inverseOf :containedIn} e:evidence . {{:containsLocation rdfs:domain :Continent} e:evidence . {:Continent rdfs:subClassOf :Continent} e:evidence } e:sequent { {:containsLocation rdfs:domain :Continent} e:evidence }} e:sequent { {:containedIn rdfs:range :Continent} e:evidence }. {:Finland :containedIn :NorthernHemisphere} e:evidence . {{(:Africa :Antarctica :Asia :Australia :Europe :NorthAmerica :SouthAmerica) rdf:first :Africa} e:evidence . {{owl:differentFrom rdf:type owl:SymmetricProperty} e:evidence . {:NorthernHemisphere owl:differentFrom :Africa} e:evidence } e:sequent { {:Africa owl:differentFrom :NorthernHemisphere} e:evidence }. {(:Africa :Antarctica :Asia :Australia :Europe :NorthAmerica :SouthAmerica) rdf:rest (:Antarctica :Asia :Australia :Europe :NorthAmerica :SouthAmerica)} e:evidence . {{(:Antarctica :Asia :Australia :Europe :NorthAmerica :SouthAmerica) rdf:first :Antarctica} e:evidence . {{owl:differentFrom rdf:type owl:SymmetricProperty} e:evidence . {:NorthernHemisphere owl:differentFrom :Antarctica} e:evidence } e:sequent { {:Antarctica owl:differentFrom :NorthernHemisphere} e:evidence }. {(:Antarctica :Asia :Australia :Europe :NorthAmerica :SouthAmerica) rdf:rest (:Asia :Australia :Europe :NorthAmerica :SouthAmerica)} e:evidence . {{(:Asia :Australia :Europe :NorthAmerica :SouthAmerica) rdf:first :Asia} e:evidence . {{owl:differentFrom rdf:type owl:SymmetricProperty} e:evidence . {:NorthernHemisphere owl:differentFrom :Asia} e:evidence } e:sequent { {:Asia owl:differentFrom :NorthernHemisphere} e:evidence }. {(:Asia :Australia :Europe :NorthAmerica :SouthAmerica) rdf:rest (:Australia :Europe :NorthAmerica :SouthAmerica)} e:evidence . {{(:Australia :Europe :NorthAmerica :SouthAmerica) rdf:first :Australia} e:evidence . {{owl:differentFrom rdf:type owl:SymmetricProperty} e:evidence . {:NorthernHemisphere owl:differentFrom :Australia} e:evidence } e:sequent { {:Australia owl:differentFrom :NorthernHemisphere} e:evidence }. {(:Australia :Europe :NorthAmerica :SouthAmerica) rdf:rest (:Europe :NorthAmerica :SouthAmerica)} e:evidence . {{(:Europe :NorthAmerica :SouthAmerica) rdf:first :Europe} e:evidence . {{owl:differentFrom rdf:type owl:SymmetricProperty} e:evidence . {:NorthernHemisphere owl:differentFrom :Europe} e:evidence } e:sequent { {:Europe owl:differentFrom :NorthernHemisphere} e:evidence }. {(:Europe :NorthAmerica :SouthAmerica) rdf:rest (:NorthAmerica :SouthAmerica)} e:evidence . {{(:NorthAmerica :SouthAmerica) rdf:first :NorthAmerica} e:evidence . {{owl:differentFrom rdf:type owl:SymmetricProperty} e:evidence . {:NorthernHemisphere owl:differentFrom :NorthAmerica} e:evidence } e:sequent { {:NorthAmerica owl:differentFrom :NorthernHemisphere} e:evidence }. {(:NorthAmerica :SouthAmerica) rdf:rest (:SouthAmerica)} e:evidence . {{(:SouthAmerica) rdf:first :SouthAmerica} e:evidence . {{owl:differentFrom rdf:type owl:SymmetricProperty} e:evidence . {:NorthernHemisphere owl:differentFrom :SouthAmerica} e:evidence } e:sequent { {:SouthAmerica owl:differentFrom :NorthernHemisphere} e:evidence }. {(:SouthAmerica) rdf:rest ()} e:evidence . {() p0:notItem :NorthernHemisphere} e:evidence } e:sequent { {(:SouthAmerica) p0:notItem :NorthernHemisphere} e:evidence }} e:sequent { {(:NorthAmerica :SouthAmerica) p0:notItem :NorthernHemisphere} e:evidence }} e:sequent { {(:Europe :NorthAmerica :SouthAmerica) p0:notItem :NorthernHemisphere} e:evidence }} e:sequent { {(:Australia :Europe :NorthAmerica :SouthAmerica) p0:notItem :NorthernHemisphere} e:evidence }} e:sequent { {(:Asia :Australia :Europe :NorthAmerica :SouthAmerica) p0:notItem :NorthernHemisphere} e:evidence }} e:sequent { {(:Antarctica :Asia :Australia :Europe :NorthAmerica :SouthAmerica) p0:notItem :NorthernHemisphere} e:evidence }} e:sequent { {(:Africa :Antarctica :Asia :Australia :Europe :NorthAmerica :SouthAmerica) p0:notItem :NorthernHemisphere} e:evidence }} e:sequent { {} e:evidence }. # Proof found in 49746 steps (177657 steps/sec) using 1 engine (308 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:46 GMT @prefix log: . @prefix e: . (!log:semantics)!log:conjunction e:constructs { @prefix e: . @prefix q: . @prefix rdfs: . @prefix log: . @prefix rdf: . { } e:evidence . {_:anon_37_ } e:evidence . { _:anon_37_} e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . { "simple literal"} e:evidence . { "backslash:\\"} e:evidence . { "dquote:\""} e:evidence . { "newline:\n"} e:evidence . { "return\r"} e:evidence . { "tab:\t"} e:evidence . { } e:evidence . { "x"} e:evidence . { _:anon_37_} e:evidence . { "\u00E9"} e:evidence . { "\u20AC"} e:evidence . { ""^^} e:evidence . { " "^^} e:evidence . { "x"^^} e:evidence . { "\""^^} e:evidence . { ""^^} e:evidence . { "a "^^} e:evidence . { "a c"^^} e:evidence . { "a\n\nc"^^} e:evidence . { "chat"^^} e:evidence . { "chat"@fr} e:evidence . { "chat"@en} e:evidence . { "abc"^^} e:evidence . # Proof found in 495 steps (49500000 steps/sec) using 1 engine (30 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix ont: . @prefix my: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix your: . @prefix rdf: . {{my:hasBrother ont:inverseOf your:isBrotherOf} e:evidence . {:joe my:hasBrother :bob} e:evidence } e:sequent { {:bob your:isBrotherOf :joe} e:evidence }. # Proof found in 2 steps (200000 steps/sec) using 1 engine (291 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix ont: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {{{{:all rdfs:subPropertyOf owl:intersectionOf} e:evidence . {:BigTall :all (:Big :Tall)} e:evidence } e:sequent { {:BigTall owl:intersectionOf (:Big :Tall)} e:evidence }. {{(:Big :Tall) rdf:first :Big} e:evidence } e:sequent { {(:Big :Tall) p0:item :Big} e:evidence }} e:sequent { {:BigTall rdfs:subClassOf :Big} e:evidence }. {:bill a :BigTall} e:evidence } e:sequent { {:bill a :Big} e:evidence }. {{{{:all rdfs:subPropertyOf owl:intersectionOf} e:evidence . {:BigTall :all (:Big :Tall)} e:evidence } e:sequent { {:BigTall owl:intersectionOf (:Big :Tall)} e:evidence }. {{(:Big :Tall) rdf:rest (:Tall)} e:evidence . {{(:Tall) rdf:first :Tall} e:evidence } e:sequent { {(:Tall) p0:item :Tall} e:evidence }} e:sequent { {(:Big :Tall) p0:item :Tall} e:evidence }} e:sequent { {:BigTall rdfs:subClassOf :Tall} e:evidence }. {:bill a :BigTall} e:evidence } e:sequent { {:bill a :Tall} e:evidence }. # Proof found in 1740 steps (173826 steps/sec) using 1 engine (292 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix p0owl: . @prefix rdf: . {{{:y p0owl:oneOf (:b :a :a)} e:evidence . {:x p0owl:oneOf (:a :a :b)} e:evidence . {{(:a :a :b) rdf:first :a} e:evidence . {{(:b :a :a) rdf:rest (:a :a)} e:evidence . {{(:a :a) rdf:first :a} e:evidence } e:sequent { {(:a :a) p0:item :a} e:evidence }} e:sequent { {(:b :a :a) p0:item :a} e:evidence }. {:a p0owl:equivalentClass :a} e:evidence . {(:a :a :b) rdf:rest (:a :b)} e:evidence . {{(:a :b) rdf:first :a} e:evidence . {{(:b :a :a) rdf:rest (:a :a)} e:evidence . {{(:a :a) rdf:first :a} e:evidence } e:sequent { {(:a :a) p0:item :a} e:evidence }} e:sequent { {(:b :a :a) p0:item :a} e:evidence }. {:a p0owl:equivalentClass :a} e:evidence . {(:a :b) rdf:rest (:b)} e:evidence . {{(:b) rdf:first :b} e:evidence . {{(:b :a :a) rdf:first :b} e:evidence } e:sequent { {(:b :a :a) p0:item :b} e:evidence }. {:b p0owl:equivalentClass :b} e:evidence . {(:b) rdf:rest ()} e:evidence . {(:b :a :a) p0:includes ()} e:evidence } e:sequent { {(:b :a :a) p0:includes (:b)} e:evidence }} e:sequent { {(:b :a :a) p0:includes (:a :b)} e:evidence }} e:sequent { {(:b :a :a) p0:includes (:a :a :b)} e:evidence }} e:sequent { {:x rdfs:subClassOf :y} e:evidence }. {{:x p0owl:oneOf (:a :a :b)} e:evidence . {:y p0owl:oneOf (:b :a :a)} e:evidence . {{(:b :a :a) rdf:first :b} e:evidence . {{(:a :a :b) rdf:rest (:a :b)} e:evidence . {{(:a :b) rdf:rest (:b)} e:evidence . {{(:b) rdf:first :b} e:evidence } e:sequent { {(:b) p0:item :b} e:evidence }} e:sequent { {(:a :b) p0:item :b} e:evidence }} e:sequent { {(:a :a :b) p0:item :b} e:evidence }. {:b p0owl:equivalentClass :b} e:evidence . {(:b :a :a) rdf:rest (:a :a)} e:evidence . {{(:a :a) rdf:first :a} e:evidence . {{(:a :a :b) rdf:first :a} e:evidence } e:sequent { {(:a :a :b) p0:item :a} e:evidence }. {:a p0owl:equivalentClass :a} e:evidence . {(:a :a) rdf:rest (:a)} e:evidence . {{(:a) rdf:first :a} e:evidence . {{(:a :a :b) rdf:first :a} e:evidence } e:sequent { {(:a :a :b) p0:item :a} e:evidence }. {:a p0owl:equivalentClass :a} e:evidence . {(:a) rdf:rest ()} e:evidence . {(:a :a :b) p0:includes ()} e:evidence } e:sequent { {(:a :a :b) p0:includes (:a)} e:evidence }} e:sequent { {(:a :a :b) p0:includes (:a :a)} e:evidence }} e:sequent { {(:a :a :b) p0:includes (:b :a :a)} e:evidence }} e:sequent { {:y rdfs:subClassOf :x} e:evidence }} e:sequent { {:x owl:sameClassAs :y} e:evidence }. # Proof found in 1396 steps (139460 steps/sec) using 1 engine (292 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix p0owl: . @prefix rdf: . {{:path rdf:type p0owl:TransitiveProperty} e:evidence . {:Antwerp :path :Amsterdam} e:evidence . {:Ghent :path :Antwerp} e:evidence } e:sequent { {:Ghent :path :Amsterdam} e:evidence }. # Proof found in 25 steps (2500000 steps/sec) using 1 engine (293 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix p0owl: . @prefix rdf: . {{:u p0owl:unionOf (:Student :Employee)} e:evidence . {{(:Student :Employee) rdf:first :Student} e:evidence . {:John a :Student} e:evidence } e:sequent { {:John p0:inSomeOf (:Student :Employee)} e:evidence }} e:sequent { {:John a :u} e:evidence }. # Proof found in 107 steps (10700000 steps/sec) using 1 engine (292 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix ont: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix contact: . @prefix : . @prefix log: . @prefix rdfs: . @prefix ex: . @prefix math: . @prefix owl: . @prefix rdf: . {_:e1125975_43_ ex:hairColor ex:red} e:evidence . {_:e1125975_43_ ex:birthPlace ex:KC} e:evidence . # Proof found in 2 steps (200000 steps/sec) using 1 engine (295 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix ont: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {_:e1135671_44_ :population "2688418"} e:evidence . {_:e1135671_44_ :stateBird :WesternMeadowlark} e:evidence . # Proof found in 2 steps (200000 steps/sec) using 1 engine (294 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix fred: . @prefix p0: . @prefix db: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix owl: . @prefix rdf: . {{db:KeyProperty rdfs:subClassOf owl:FunctionalProperty} e:evidence . {{db:key rdfs:range db:KeyProperty} e:evidence . {fred:Order db:key fred:customer} e:evidence } e:sequent { {fred:customer a db:KeyProperty} e:evidence }} e:sequent { {fred:customer a owl:FunctionalProperty} e:evidence }. # Proof found in 1055 steps (105394 steps/sec) using 1 engine (293 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {{:C owl:intersectionOf _:c1_47_} e:evidence . {{_:c1_47_ rdf:first :Employee} e:evidence . {{{:B owl:intersectionOf _:b1_46_} e:evidence . {{_:b1_46_ rdf:rest _:b2_46_} e:evidence . {{_:b2_46_ rdf:first :Employee} e:evidence } e:sequent { {_:b2_46_ p0:item :Employee} e:evidence }} e:sequent { {_:b1_46_ p0:item :Employee} e:evidence }} e:sequent { {:B rdfs:subClassOf :Employee} e:evidence }. {:John a :B} e:evidence } e:sequent { {:John a :Employee} e:evidence }. {_:c1_47_ rdf:rest _:c2_47_} e:evidence . {{_:c2_47_ rdf:first :Student} e:evidence . {{{:B owl:intersectionOf _:b1_46_} e:evidence . {{_:b1_46_ rdf:first :Student} e:evidence } e:sequent { {_:b1_46_ p0:item :Student} e:evidence }} e:sequent { {:B rdfs:subClassOf :Student} e:evidence }. {:John a :B} e:evidence } e:sequent { {:John a :Student} e:evidence }. {_:c2_47_ rdf:rest ()} e:evidence . {:John p0:inAllOf ()} e:evidence } e:sequent { {:John p0:inAllOf _:c2_47_} e:evidence }} e:sequent { {:John p0:inAllOf _:c1_47_} e:evidence }} e:sequent { {:John a :C} e:evidence }. # Proof found in 1443 steps (144155 steps/sec) using 1 engine (302 triples) }. # Generated with http://eulersharp.sourceforge.net/ version 1.4.18 on 30 Oct 2005 14:13:47 GMT @prefix log: . @prefix e: . (!log:semantics !log:semantics !log:semantics !log:semantics)!log:conjunction e:constructs { @prefix str: . @prefix p0: . @prefix q: . @prefix e: . @prefix xsd: . @prefix : . @prefix log: . @prefix rdfs: . @prefix math: . @prefix p1: . @prefix owl: . @prefix rdf: . {{:Man rdfs:subClassOf :Mortal} e:evidence . {:Socrates a :Man} e:evidence } e:sequent { {:Socrates a :Mortal} e:evidence }. # Proof found in 478 steps (47752 steps/sec) using 1 engine (292 triples) }. # Proof found in 82337 steps (13702 steps/sec) using 35 engines (0 triples) }.