# Generated with http://eulersharp.sourceforge.net/ version 1.4.28 on 31 Jan 2006 10:30:32 GMT
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.

(<http://www.agfa.com/w3c/euler/owl-facts.n3>!log:semantics
 <http://www.agfa.com/w3c/euler/owl-rules.n3>!log:semantics
 <http://www.agfa.com/w3c/euler/rdfs-rules.n3>!log:semantics)!log:conjunction =>
{
@prefix str: <http://www.w3.org/2000/10/swap/string#>.
@prefix p0: <http://eulersharp.sourceforge.net/2003/03swap/owl-rules#>.
@prefix q: <http://www.w3.org/2004/ql#>.
@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix : <http://www.agfa.com/w3c/euler/owl-facts#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix p1: <http://eulersharp.sourceforge.net/2003/03swap/rdfs-rules#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.

{:j owl:sameAs :i} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
{:o owl:sameAs :m} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
{{:H owl:oneOf (:s :m :t)} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_17>. 
 {{(:s :m :t) rdf:rest (:m :t)} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
  {{(:m :t) rdf:first :m} e:evidence <http://www.w3.org/2002/07/owl#kb>} => {
  {(:m :t) p0:item :m} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_228>}} => {
 {(:s :m :t) p0:item :m} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_229>}} => {
{:m a :H} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_143>}. 
{{:y owl:intersectionOf (:b :c)} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_20>. 
 {:x owl:intersectionOf (:a :b :c)} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_19>. 
 {{(:b :c) rdf:first :b} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
  {{(:a :b :c) rdf:rest (:b :c)} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
   {{(:b :c) rdf:first :b} e:evidence <http://www.w3.org/2002/07/owl#kb>} => {
   {(:b :c) p0:item :b} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_228>}} => {
  {(:a :b :c) p0:item :b} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_229>}. 
  {:b owl:equivalentClass :b} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
  {(:b :c) rdf:rest (:c)} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
  {{(:c) rdf:first :c} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
   {{(:a :b :c) rdf:rest (:b :c)} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
    {{(:b :c) rdf:rest (:c)} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
     {{(:c) rdf:first :c} e:evidence <http://www.w3.org/2002/07/owl#kb>} => {
     {(:c) p0:item :c} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_228>}} => {
    {(:b :c) p0:item :c} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_229>}} => {
   {(:a :b :c) p0:item :c} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_229>}. 
   {:c owl:equivalentClass :c} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
   {(:c) rdf:rest ()} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
   {(:a :b :c) p0:includes ()} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_234>} => {
  {(:a :b :c) p0:includes (:c)} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_235>}} => {
 {(:a :b :c) p0:includes (:b :c)} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_235>}} => {
{:x rdfs:subClassOf :y} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_123>}. 
{{:y owl:intersectionOf (:b :c)} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_20>. 
 {{(:b :c) rdf:first :b} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
  {{{:x owl:intersectionOf (:a :b :c)} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_19>. 
    {{(:a :b :c) rdf:rest (:b :c)} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
   {{(:b :c) rdf:first :b} e:evidence <http://www.w3.org/2002/07/owl#kb>} => {
   {(:b :c) p0:item :b} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_228>}} => {
  {(:a :b :c) p0:item :b} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_229>}} => {
   {:x rdfs:subClassOf :b} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_122>}. 
   {:J a :x} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_22>} => {
  {:J a :b} e:evidence <http://www.agfa.com/w3c/euler/rdfs-rules.n3#_59>}. 
  {(:b :c) rdf:rest (:c)} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
  {{(:c) rdf:first :c} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
   {{{:x owl:intersectionOf (:a :b :c)} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_19>. 
     {{(:a :b :c) rdf:rest (:b :c)} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
   {{(:b :c) rdf:rest (:c)} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
    {{(:c) rdf:first :c} e:evidence <http://www.w3.org/2002/07/owl#kb>} => {
    {(:c) p0:item :c} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_228>}} => {
   {(:b :c) p0:item :c} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_229>}} => {
  {(:a :b :c) p0:item :c} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_229>}} => {
    {:x rdfs:subClassOf :c} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_122>}. 
    {:J a :x} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_22>} => {
   {:J a :c} e:evidence <http://www.agfa.com/w3c/euler/rdfs-rules.n3#_59>}. 
   {(:c) rdf:rest ()} e:evidence <http://www.w3.org/2002/07/owl#kb>. 
   {:J p0:inAllOf ()} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_237>} => {
  {:J p0:inAllOf (:c)} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_238>}} => {
 {:J p0:inAllOf (:b :c)} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_238>}} => {
{:J a :y} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_144>}. 
{{:test43 rdfs:subClassOf :test46} e:evidence <http://eulersharp.sourceforge.net/2003/03swap/log-rules#kb>. 
 {{:test34 rdfs:subClassOf :test43} e:evidence <http://eulersharp.sourceforge.net/2003/03swap/log-rules#kb>. 
  {:test3x a :test34} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_26>} => {
 {:test3x a :test43} e:evidence <http://www.agfa.com/w3c/euler/rdfs-rules.n3#_59>}} => {
{:test3x a :test46} e:evidence <http://www.agfa.com/w3c/euler/rdfs-rules.n3#_59>}. 
{{{:test43 rdfs:subClassOf :test34} e:evidence <http://eulersharp.sourceforge.net/2003/03swap/log-rules#kb>. 
  {:test46 rdfs:subClassOf :test43} e:evidence <http://eulersharp.sourceforge.net/2003/03swap/log-rules#kb>} => {
 {:test46 rdfs:subClassOf :test34} e:evidence <http://www.agfa.com/w3c/euler/rdfs-rules.n3#_61>}. 
 {{:test43 rdfs:subClassOf :test46} e:evidence <http://eulersharp.sourceforge.net/2003/03swap/log-rules#kb>. 
  {:test34 rdfs:subClassOf :test43} e:evidence <http://eulersharp.sourceforge.net/2003/03swap/log-rules#kb>} => {
 {:test34 rdfs:subClassOf :test46} e:evidence <http://www.agfa.com/w3c/euler/rdfs-rules.n3#_61>}} => {
{:test46 owl:equivalentClass :test34} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_119>}. 
{{:R2 owl:onProperty :p2} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_28>. 
 {:R2 owl:hasValue :y2} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_29>. 
 {:x2 a :R2} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_30>} => {
{:x2 :p2 :y2} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_65>}. 
{{:Automobile rdfs:subClassOf :Car} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_33>. 
 {:Car rdfs:subClassOf :Automobile} e:evidence <http://www.agfa.com/w3c/euler/owl-facts.n3#_32>} => {
{:Automobile owl:equivalentClass :Car} e:evidence <http://www.agfa.com/w3c/euler/owl-rules.n3#_119>}. 

# Proof found in 8379 steps (93089 steps/sec) using 1 engine (312 triples)
}.