# Generated with http://eulersharp.sourceforge.net/ version 1.4.7 on 29 Sep 2005 12:57:28 GMT @prefix log: . @prefix e: . (!log:semantics !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: . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_ rdf:first } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_ rdf:rest _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1050_5_} e:evidence . {{ rdfs:range } e:evidence . { owl:oneOf _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:first } e:evidence . { } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:rest _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ rdf:first } e:evidence . { } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ rdf:rest ()} e:evidence . { :reflexive ()} e:evidence } e:sequent { { :reflexive _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_} e:evidence }} e:sequent { { :reflexive _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_} e:evidence }. {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1052_5_ owl:oneOf _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:first } e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_ rdf:first } e:evidence } e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_ :item } e:evidence }. { owl:equivalentClass } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:rest _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ rdf:first } e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_ rdf:rest _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1050_5_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1050_5_ rdf:first } e:evidence } e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1050_5_ :item } e:evidence }} e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_ :item } e:evidence }. { owl:equivalentClass } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ rdf:rest ()} e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_ :includes ()} e:evidence } e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_ :includes _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_} e:evidence }} e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_ :includes _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_} e:evidence }. { rdf:type owl:InverseFunctionalProperty} e:evidence } e:sequent { { _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1052_5_} e:evidence }. {{ rdfs:range } e:evidence . { owl:oneOf _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:first } e:evidence . { } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:rest _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ rdf:first } e:evidence . { } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ rdf:rest ()} e:evidence . { :reflexive ()} e:evidence } e:sequent { { :reflexive _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_} e:evidence }} e:sequent { { :reflexive _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_} e:evidence }. { owl:oneOf _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:first } e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:first } e:evidence } e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ :item } e:evidence }. { owl:equivalentClass } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:rest _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ rdf:first } e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ rdf:rest _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_} e:evidence . {{_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ rdf:first } e:evidence } e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ :item } e:evidence }} e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ :item } e:evidence }. { owl:equivalentClass } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_ rdf:rest ()} e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ :includes ()} e:evidence } e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ :includes _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1053_85_} e:evidence }} e:sequent { {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_ :includes _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1054_85_} e:evidence }. { rdf:type owl:InverseFunctionalProperty} e:evidence } e:sequent { { } e:evidence }. {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1052_5_ _:AX2dX20b5deb6X3aX10691944472X3aXX2dX1051_5_} e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1052_5_ } e:evidence . { } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1050_5_ rdf:first } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX1050_5_ rdf:rest _:AX2dX20b5deb6X3aX10691944472X3aXX2dX104f_5_} e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX104f_5_ rdf:first } e:evidence . {_:AX2dX20b5deb6X3aX10691944472X3aXX2dX104f_5_ rdf:rest ()} e:evidence . { } e:evidence . { } e:evidence . { } e:evidence . # Proof found in 89726 steps (203918 steps/sec) using 1 engine (446 triples) }.