# Generated with http://eulersharp.sourceforge.net/ version 1.4.7 on 29 Sep 2005 13:07:23 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) }.