Created
March 5, 2016 15:40
-
-
Save tillmo/d448365b048b97fd5f00 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| logic OWL.NP-ALCIN | |
| Prefix: : <http://ontohub.org/monster-blend/animalsDetailed/shared> | |
| Class: BodyPart | |
| Class: Organism | |
| ObjectProperty: has_part | |
| ObjectProperty: meets | |
| DisjointClasses: AnatomicalBoundary, | |
| CardinalBodyPart, | |
| Organism | |
| DisjointClasses: Arm, | |
| Leg, | |
| Wing | |
| DisjointClasses: Foot, | |
| Hand, | |
| Hoof, | |
| Paw, | |
| Claw | |
| DisjointClasses: Head, | |
| Trunk, | |
| Limb, | |
| LimbEnd, | |
| Tail | |
| Class: AnatomicalBoundary | |
| SubClassOf: fiat_boundary_of some BodyPart | |
| Class: AnteriorBodyPart | |
| SubClassOf: BodyPart | |
| Class: Arm | |
| SubClassOf: Limb | |
| Class: CardinalBodyPart | |
| SubClassOf: BodyPart | |
| Class: Claw | |
| SubClassOf: LimbEnd | |
| Class: DistalBoundary | |
| SubClassOf: AnatomicalBoundary | |
| Class: Foot | |
| SubClassOf: LimbEnd | |
| Class: Hair | |
| SubClassOf: BodyPart | |
| Class: Hand | |
| SubClassOf: LimbEnd | |
| Class: Head | |
| SubClassOf: CardinalBodyPart | |
| SubClassOf: has_fiat_boundary exactly 1 AnatomicalBoundary | |
| Class: Hoof | |
| SubClassOf: LimbEnd | |
| Class: LeftBodyPart | |
| SubClassOf: BodyPart | |
| Class: LeftForeLimb | |
| EquivalentTo: Limb and LeftBodyPart and AnteriorBodyPart | |
| Class: LeftForeLimbBoundary | |
| SubClassOf: AnatomicalBoundary | |
| Class: LeftForeLimbEnd | |
| EquivalentTo: LimbEnd and LeftBodyPart and AnteriorBodyPart | |
| Class: LeftForePandaLeg | |
| EquivalentTo: PandaLeg and LeftForeLimb | |
| Class: LeftForePandaPaw | |
| EquivalentTo: PandaPaw and LeftForeLimbEnd | |
| Class: LeftForeTigerLeg | |
| EquivalentTo: TigerLeg and LeftForeLimb | |
| Class: LeftForeTigerPaw | |
| EquivalentTo: TigerPaw and LeftForeLimbEnd | |
| Class: LeftHindLimb | |
| EquivalentTo: Limb and LeftBodyPart and PosteriorBodyPart | |
| Class: LeftHindLimbBoundary | |
| SubClassOf: AnatomicalBoundary | |
| Class: LeftHindLimbEnd | |
| EquivalentTo: LimbEnd and LeftBodyPart and PosteriorBodyPart | |
| Class: LeftHindPandaLeg | |
| EquivalentTo: PandaLeg and LeftHindLimb | |
| Class: LeftHindPandaPaw | |
| EquivalentTo: PandaPaw and LeftHindLimbEnd | |
| Class: LeftHindTigerLeg | |
| EquivalentTo: TigerLeg and LeftHindLimb | |
| Class: LeftHindTigerPaw | |
| EquivalentTo: TigerPaw and LeftHindLimbEnd | |
| Class: Leg | |
| SubClassOf: Limb | |
| Class: Limb | |
| SubClassOf: CardinalBodyPart | |
| SubClassOf: has_fiat_boundary some DistalBoundary | |
| SubClassOf: has_fiat_boundary some ProximalBoundary | |
| SubClassOf: has_fiat_boundary exactly 2 AnatomicalBoundary | |
| Class: LimbEnd | |
| SubClassOf: CardinalBodyPart | |
| SubClassOf: has_fiat_boundary exactly 1 AnatomicalBoundary | |
| Class: Mammal | |
| SubClassOf: Organism | |
| Class: NeckBoundary | |
| SubClassOf: AnatomicalBoundary | |
| Class: Panda | |
| SubClassOf: Quadruped | |
| Class: PandaHead | |
| EquivalentTo: Head and part_of some Panda | |
| Class: PandaLeg | |
| EquivalentTo: Leg and part_of some Panda | |
| Class: PandaPaw | |
| EquivalentTo: Paw and part_of some Panda | |
| Class: PandaTail | |
| EquivalentTo: Tail and part_of some Panda | |
| Class: PandaTrunk | |
| EquivalentTo: QuadrupedTrunk and part_of some Panda | |
| Class: Paw | |
| SubClassOf: LimbEnd | |
| Class: PosteriorBodyPart | |
| SubClassOf: BodyPart | |
| Class: ProximalBoundary | |
| SubClassOf: AnatomicalBoundary | |
| Class: Quadruped | |
| SubClassOf: Organism | |
| SubClassOf: has_part some Head | |
| SubClassOf: has_part some QuadrupedTrunk | |
| SubClassOf: has_part exactly 4 Leg | |
| Class: QuadrupedTrunk | |
| SubClassOf: has_fiat_boundary exactly 6 AnatomicalBoundary | |
| SubClassOf: Trunk | |
| SubClassOf: has_fiat_boundary exactly 1 LeftForeLimbBoundary | |
| SubClassOf: has_fiat_boundary exactly 1 LeftHindLimbBoundary | |
| SubClassOf: has_fiat_boundary exactly 1 NeckBoundary | |
| SubClassOf: has_fiat_boundary exactly 1 RightForeLimbBoundary | |
| SubClassOf: has_fiat_boundary exactly 1 RightHindLimbBoundary | |
| SubClassOf: has_fiat_boundary exactly 1 TailBoundary | |
| Class: RightBodyPart | |
| SubClassOf: BodyPart | |
| Class: RightForeLimb | |
| EquivalentTo: Limb and RightBodyPart and AnteriorBodyPart | |
| Class: RightForeLimbBoundary | |
| SubClassOf: AnatomicalBoundary | |
| Class: RightForeLimbEnd | |
| EquivalentTo: LimbEnd and RightBodyPart and AnteriorBodyPart | |
| Class: RightForePandaLeg | |
| EquivalentTo: PandaLeg and RightForeLimb | |
| Class: RightForePandaPaw | |
| EquivalentTo: PandaPaw and RightForeLimbEnd | |
| Class: RightForeTigerLeg | |
| EquivalentTo: TigerLeg and RightForeLimb | |
| Class: RightForeTigerPaw | |
| EquivalentTo: TigerPaw and RightForeLimbEnd | |
| Class: RightHindLimb | |
| EquivalentTo: Limb and RightBodyPart and PosteriorBodyPart | |
| Class: RightHindLimbBoundary | |
| SubClassOf: AnatomicalBoundary | |
| Class: RightHindLimbEnd | |
| EquivalentTo: LimbEnd and RightBodyPart and PosteriorBodyPart | |
| Class: RightHindPandaLeg | |
| EquivalentTo: PandaLeg and RightHindLimb | |
| Class: RightHindPandaPaw | |
| EquivalentTo: PandaPaw and RightHindLimbEnd | |
| Class: RightHindTigerLeg | |
| EquivalentTo: TigerLeg and RightHindLimb | |
| Class: RightHindTigerPaw | |
| EquivalentTo: TigerPaw and RightHindLimbEnd | |
| Class: Tail | |
| SubClassOf: CardinalBodyPart | |
| SubClassOf: has_fiat_boundary exactly 1 AnatomicalBoundary | |
| Class: TailBoundary | |
| SubClassOf: AnatomicalBoundary | |
| Class: Tiger | |
| SubClassOf: Quadruped | |
| Class: TigerHead | |
| EquivalentTo: Head and part_of some Tiger | |
| Class: TigerLeg | |
| EquivalentTo: Leg and part_of some Tiger | |
| Class: TigerPaw | |
| EquivalentTo: Paw and part_of some Tiger | |
| Class: TigerTail | |
| EquivalentTo: Tail and part_of some Tiger | |
| Class: TigerTrunk | |
| EquivalentTo: QuadrupedTrunk and part_of some Tiger | |
| Class: Trunk | |
| SubClassOf: CardinalBodyPart | |
| Class: Wing | |
| SubClassOf: Limb | |
| ObjectProperty: fiat_boundary_of | |
| InverseOf: has_fiat_boundary | |
| ObjectProperty: has_fiat_boundary | |
| Domain: BodyPart | |
| Range: AnatomicalBoundary | |
| ObjectProperty: part_of | |
| InverseOf: has_part | |
| Individual: h | |
| Types: TigerHead | |
| Types: PandaHead | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary h-nb | |
| Individual: h-nb | |
| Facts: meets t-nb | |
| Types: ProximalBoundary | |
| Individual: lfl | |
| Types: LeftForeTigerLeg | |
| Types: LeftForePandaLeg | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary lfl-pb, | |
| has_fiat_boundary lfl-db | |
| Individual: lfl-db | |
| Types: DistalBoundary | |
| Individual: lfl-pb | |
| Facts: meets t-lflb | |
| Types: ProximalBoundary | |
| Individual: lfle | |
| Types: LeftForeTigerPaw | |
| Types: LeftForePandaPaw | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary lfle-pb | |
| Individual: lfle-pb | |
| Facts: meets lfl-db | |
| Types: ProximalBoundary | |
| Individual: lhl | |
| Types: LeftHindTigerLeg | |
| Types: LeftHindPandaLeg | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary lhl-pb, | |
| has_fiat_boundary lhl-db | |
| Individual: lhl-db | |
| Types: DistalBoundary | |
| Individual: lhl-pb | |
| Facts: meets t-lhlb | |
| Types: ProximalBoundary | |
| Individual: lhle | |
| Types: LeftHindTigerPaw | |
| Types: LeftHindPandaPaw | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary lhle-pb | |
| Individual: lhle-pb | |
| Facts: meets lhl-db | |
| Types: ProximalBoundary | |
| Individual: rfl | |
| Types: RightForeTigerLeg | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary rfl-pb, | |
| has_fiat_boundary rfl-db | |
| Types: RightForePandaLeg | |
| Individual: rfl-db | |
| Types: DistalBoundary | |
| Individual: rfl-pb | |
| Types: ProximalBoundary | |
| Facts: meets t-rflb | |
| Individual: rfle | |
| Types: RightForeTigerPaw | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary rfle-pb | |
| Types: RightForePandaPaw | |
| Individual: rfle-pb | |
| Types: ProximalBoundary | |
| Facts: meets rfl-db | |
| Individual: rhl | |
| Types: RightHindTigerLeg | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary rhl-pb, | |
| has_fiat_boundary rhl-db | |
| Types: RightHindPandaLeg | |
| Individual: rhl-db | |
| Types: DistalBoundary | |
| Individual: rhl-pb | |
| Types: ProximalBoundary | |
| Facts: meets t-rhlb | |
| Individual: rhle | |
| Types: RightHindTigerPaw | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary rhle-pb | |
| Types: RightHindPandaPaw | |
| Individual: rhle-pb | |
| Types: ProximalBoundary | |
| Facts: meets rhl-db | |
| Individual: t | |
| Types: TigerTrunk | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary t-nb, | |
| has_fiat_boundary t-lflb, | |
| has_fiat_boundary t-rflb, | |
| has_fiat_boundary t-lhlb, | |
| has_fiat_boundary t-rhlb, | |
| has_fiat_boundary t-tlb | |
| Types: PandaTrunk | |
| Individual: t-lflb | |
| Types: LeftForeLimbBoundary | |
| Individual: t-lhlb | |
| Types: LeftHindLimbBoundary | |
| Individual: t-nb | |
| Types: NeckBoundary | |
| Individual: t-rflb | |
| Types: RightForeLimbBoundary | |
| Individual: t-rhlb | |
| Types: RightHindLimbBoundary | |
| Individual: t-tlb | |
| Types: TailBoundary | |
| Individual: thisAnimal | |
| Types: Tiger | |
| Types: Panda | |
| Individual: tl | |
| Types: TigerTail | |
| Types: PandaTail | |
| Facts: part_of thisAnimal, | |
| has_fiat_boundary tl-pb | |
| Individual: tl-pb | |
| Facts: meets t-tlb | |
| Types: ProximalBoundary |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| logic CASL.SulFOL= | |
| sorts Char, DATA, ENTITIES, ENTITY, ID, IDREF, IDREFS, Literal, | |
| NCName, NMTOKEN, NMTOKENS, NOTATION, Name, QName, Thing, | |
| XMLLiteral, anyURI, base64Binary, boolean, byte, date, dateTime, | |
| dateTimeStamp, decimal, double, duration, float, gDay, gMonth, | |
| gMonthDay, gYear, gYearMonth, hexBinary, int, integer, language, | |
| long, negativeInteger, nonNegativeInteger, nonPositiveInteger, | |
| normalizedString, positiveInteger, rational, real, short, string, | |
| time, token, unsignedByte, unsignedInt, unsignedLongS, | |
| unsignedShort | |
| sorts ENTITIES, ENTITY, ID, IDREF, IDREFS, Literal, NCName, | |
| NMTOKEN, NMTOKENS, NOTATION, Name, QName, XMLLiteral, anyURI, | |
| base64Binary, boolean, byte, date, dateTime, dateTimeStamp, | |
| decimal, double, duration, float, gDay, gMonth, gMonthDay, gYear, | |
| gYearMonth, hexBinary, int, language, long, normalizedString, | |
| rational, real, short, string, time, token, unsignedByte, | |
| unsignedInt, unsignedLongS, unsignedShort < DATA; | |
| integer < float; nonNegativeInteger, nonPositiveInteger < integer; | |
| positiveInteger < nonNegativeInteger; | |
| negativeInteger < nonPositiveInteger | |
| op '\000' : Char | |
| op '\001' : Char | |
| op '\002' : Char | |
| op '\003' : Char | |
| op '\004' : Char | |
| op '\005' : Char | |
| op '\006' : Char | |
| op '\007' : Char | |
| op '\008' : Char | |
| op '\009' : Char | |
| op '\010' : Char | |
| op '\011' : Char | |
| op '\012' : Char | |
| op '\013' : Char | |
| op '\014' : Char | |
| op '\015' : Char | |
| op '\016' : Char | |
| op '\017' : Char | |
| op '\018' : Char | |
| op '\019' : Char | |
| op '\020' : Char | |
| op '\021' : Char | |
| op '\022' : Char | |
| op '\023' : Char | |
| op '\024' : Char | |
| op '\025' : Char | |
| op '\026' : Char | |
| op '\027' : Char | |
| op '\028' : Char | |
| op '\029' : Char | |
| op '\030' : Char | |
| op '\031' : Char | |
| op '\032' : Char | |
| op '\033' : Char | |
| op '\034' : Char | |
| op '\035' : Char | |
| op '\036' : Char | |
| op '\037' : Char | |
| op '\038' : Char | |
| op '\039' : Char | |
| op '\040' : Char | |
| op '\041' : Char | |
| op '\042' : Char | |
| op '\043' : Char | |
| op '\044' : Char | |
| op '\045' : Char | |
| op '\046' : Char | |
| op '\047' : Char | |
| op '\048' : Char | |
| op '\049' : Char | |
| op '\050' : Char | |
| op '\051' : Char | |
| op '\052' : Char | |
| op '\053' : Char | |
| op '\054' : Char | |
| op '\055' : Char | |
| op '\056' : Char | |
| op '\057' : Char | |
| op '\058' : Char | |
| op '\059' : Char | |
| op '\060' : Char | |
| op '\061' : Char | |
| op '\062' : Char | |
| op '\063' : Char | |
| op '\064' : Char | |
| op '\065' : Char | |
| op '\066' : Char | |
| op '\067' : Char | |
| op '\068' : Char | |
| op '\069' : Char | |
| op '\070' : Char | |
| op '\071' : Char | |
| op '\072' : Char | |
| op '\073' : Char | |
| op '\074' : Char | |
| op '\075' : Char | |
| op '\076' : Char | |
| op '\077' : Char | |
| op '\078' : Char | |
| op '\079' : Char | |
| op '\080' : Char | |
| op '\081' : Char | |
| op '\082' : Char | |
| op '\083' : Char | |
| op '\084' : Char | |
| op '\085' : Char | |
| op '\086' : Char | |
| op '\087' : Char | |
| op '\088' : Char | |
| op '\089' : Char | |
| op '\090' : Char | |
| op '\091' : Char | |
| op '\092' : Char | |
| op '\093' : Char | |
| op '\094' : Char | |
| op '\095' : Char | |
| op '\096' : Char | |
| op '\097' : Char | |
| op '\098' : Char | |
| op '\099' : Char | |
| op '\100' : Char | |
| op '\101' : Char | |
| op '\102' : Char | |
| op '\103' : Char | |
| op '\104' : Char | |
| op '\105' : Char | |
| op '\106' : Char | |
| op '\107' : Char | |
| op '\108' : Char | |
| op '\109' : Char | |
| op '\110' : Char | |
| op '\111' : Char | |
| op '\112' : Char | |
| op '\113' : Char | |
| op '\114' : Char | |
| op '\115' : Char | |
| op '\116' : Char | |
| op '\117' : Char | |
| op '\118' : Char | |
| op '\119' : Char | |
| op '\120' : Char | |
| op '\121' : Char | |
| op '\122' : Char | |
| op '\123' : Char | |
| op '\124' : Char | |
| op '\125' : Char | |
| op '\126' : Char | |
| op '\127' : Char | |
| op -__ : float -> float | |
| op -__ : integer -> integer | |
| op 0 : nonNegativeInteger | |
| op 1 : nonNegativeInteger | |
| op 2 : nonNegativeInteger | |
| op 3 : nonNegativeInteger | |
| op 4 : nonNegativeInteger | |
| op 5 : nonNegativeInteger | |
| op 6 : nonNegativeInteger | |
| op 7 : nonNegativeInteger | |
| op 8 : nonNegativeInteger | |
| op 9 : nonNegativeInteger | |
| op False : boolean | |
| op True : boolean | |
| op __:::__ : nonNegativeInteger * nonNegativeInteger -> float | |
| op __:@:__ : Char * string -> string | |
| op __@@__ : nonNegativeInteger * nonNegativeInteger -> | |
| nonNegativeInteger | |
| op __E__ : float * integer -> float | |
| op emptyString : string | |
| op h : Thing | |
| op h-nb : Thing | |
| op lfl : Thing | |
| op lfl-db : Thing | |
| op lfl-pb : Thing | |
| op lfle : Thing | |
| op lfle-pb : Thing | |
| op lhl : Thing | |
| op lhl-db : Thing | |
| op lhl-pb : Thing | |
| op lhle : Thing | |
| op lhle-pb : Thing | |
| op rfl : Thing | |
| op rfl-db : Thing | |
| op rfl-pb : Thing | |
| op rfle : Thing | |
| op rfle-pb : Thing | |
| op rhl : Thing | |
| op rhl-db : Thing | |
| op rhl-pb : Thing | |
| op rhle : Thing | |
| op rhle-pb : Thing | |
| op t : Thing | |
| op t-lflb : Thing | |
| op t-lhlb : Thing | |
| op t-nb : Thing | |
| op t-rflb : Thing | |
| op t-rhlb : Thing | |
| op t-tlb : Thing | |
| op thisAnimal : Thing | |
| op tl : Thing | |
| op tl-pb : Thing | |
| pred AnatomicalBoundary : Thing | |
| pred AnteriorBodyPart : Thing | |
| pred Arm : Thing | |
| pred BodyPart : Thing | |
| pred CardinalBodyPart : Thing | |
| pred Claw : Thing | |
| pred DistalBoundary : Thing | |
| pred Foot : Thing | |
| pred Hair : Thing | |
| pred Hand : Thing | |
| pred Head : Thing | |
| pred Hoof : Thing | |
| pred LeftBodyPart : Thing | |
| pred LeftForeLimb : Thing | |
| pred LeftForeLimbBoundary : Thing | |
| pred LeftForeLimbEnd : Thing | |
| pred LeftForePandaLeg : Thing | |
| pred LeftForePandaPaw : Thing | |
| pred LeftForeTigerLeg : Thing | |
| pred LeftForeTigerPaw : Thing | |
| pred LeftHindLimb : Thing | |
| pred LeftHindLimbBoundary : Thing | |
| pred LeftHindLimbEnd : Thing | |
| pred LeftHindPandaLeg : Thing | |
| pred LeftHindPandaPaw : Thing | |
| pred LeftHindTigerLeg : Thing | |
| pred LeftHindTigerPaw : Thing | |
| pred Leg : Thing | |
| pred Limb : Thing | |
| pred LimbEnd : Thing | |
| pred Mammal : Thing | |
| pred NeckBoundary : Thing | |
| pred Nothing : Thing | |
| pred Organism : Thing | |
| pred Panda : Thing | |
| pred PandaHead : Thing | |
| pred PandaLeg : Thing | |
| pred PandaPaw : Thing | |
| pred PandaTail : Thing | |
| pred PandaTrunk : Thing | |
| pred Paw : Thing | |
| pred PosteriorBodyPart : Thing | |
| pred ProximalBoundary : Thing | |
| pred Quadruped : Thing | |
| pred QuadrupedTrunk : Thing | |
| pred RightBodyPart : Thing | |
| pred RightForeLimb : Thing | |
| pred RightForeLimbBoundary : Thing | |
| pred RightForeLimbEnd : Thing | |
| pred RightForePandaLeg : Thing | |
| pred RightForePandaPaw : Thing | |
| pred RightForeTigerLeg : Thing | |
| pred RightForeTigerPaw : Thing | |
| pred RightHindLimb : Thing | |
| pred RightHindLimbBoundary : Thing | |
| pred RightHindLimbEnd : Thing | |
| pred RightHindPandaLeg : Thing | |
| pred RightHindPandaPaw : Thing | |
| pred RightHindTigerLeg : Thing | |
| pred RightHindTigerPaw : Thing | |
| pred Tail : Thing | |
| pred TailBoundary : Thing | |
| pred Thing : Thing | |
| pred Tiger : Thing | |
| pred TigerHead : Thing | |
| pred TigerLeg : Thing | |
| pred TigerPaw : Thing | |
| pred TigerTail : Thing | |
| pred TigerTrunk : Thing | |
| pred Trunk : Thing | |
| pred Wing : Thing | |
| pred __<__ : DATA * DATA | |
| pred __<=__ : DATA * DATA | |
| pred __>__ : DATA * DATA | |
| pred __>=__ : DATA * DATA | |
| pred __fractionDigits__ : DATA * DATA | |
| pred __langRange__ : DATA * DATA | |
| pred __length__ : DATA * DATA | |
| pred __maxLength__ : DATA * DATA | |
| pred __minLength__ : DATA * DATA | |
| pred __pattern__ : DATA * DATA | |
| pred __totalDigits__ : DATA * DATA | |
| pred even : integer | |
| pred even : nonNegativeInteger | |
| pred fiat_boundary_of : Thing * Thing | |
| pred has_fiat_boundary : Thing * Thing | |
| pred has_part : Thing * Thing | |
| pred meets : Thing * Thing | |
| pred odd : integer | |
| pred odd : nonNegativeInteger | |
| pred part_of : Thing * Thing | |
| . false %(inconsistency)% %implied | |
| forall a : Thing . not Nothing(a) %(nothing in Nothing)% | |
| forall a : Thing . Thing(a) %(thing in Thing)% | |
| forall a : Thing . a = tl-pb => ProximalBoundary(a) %(Ax104_267)% | |
| . meets(tl-pb, t-tlb) %(Ax103_266)% | |
| . part_of(tl, thisAnimal) %(Ax102_265)% | |
| . has_fiat_boundary(tl, tl-pb) %(Ax102_265_1)% | |
| forall a : Thing . a = t-tlb => TailBoundary(a) %(Ax101_264)% | |
| forall a : Thing . a = t-rhlb => RightHindLimbBoundary(a) | |
| %(Ax100_263)% | |
| forall a : Thing . a = lhle-pb => ProximalBoundary(a) %(Ax80_344)% | |
| . meets(lhle-pb, lhl-db) %(Ax79_342)% | |
| . part_of(lhle, thisAnimal) %(Ax78_341)% | |
| . has_fiat_boundary(lhle, lhle-pb) %(Ax78_341_2)% | |
| forall a : Thing . a = lhl-pb => ProximalBoundary(a) %(Ax77_340)% | |
| . meets(lhl-pb, t-lhlb) %(Ax76_339)% | |
| forall a : Thing . a = lhl-db => DistalBoundary(a) %(Ax75_338)% | |
| . part_of(lhl, thisAnimal) %(Ax74_337)% | |
| . has_fiat_boundary(lhl, lhl-pb) %(Ax74_337_3)% | |
| . has_fiat_boundary(lhl, lhl-db) %(Ax74_337_4)% | |
| forall a : Thing . a = lfle-pb => ProximalBoundary(a) %(Ax73_336)% | |
| . meets(lfle-pb, lfl-db) %(Ax72_335)% | |
| . part_of(lfle, thisAnimal) %(Ax71_334)% | |
| . has_fiat_boundary(lfle, lfle-pb) %(Ax71_334_5)% | |
| forall a : Thing . a = lfl-pb => ProximalBoundary(a) %(Ax70_333)% | |
| . meets(lfl-pb, t-lflb) %(Ax69_331)% | |
| forall a : Thing . a = lfl-db => DistalBoundary(a) %(Ax68_330)% | |
| . part_of(lfl, thisAnimal) %(Ax67_329)% | |
| . has_fiat_boundary(lfl, lfl-pb) %(Ax67_329_6)% | |
| . has_fiat_boundary(lfl, lfl-db) %(Ax67_329_7)% | |
| forall a : Thing . a = h-nb => ProximalBoundary(a) %(Ax66_328)% | |
| . meets(h-nb, t-nb) %(Ax65_327)% | |
| . part_of(h, thisAnimal) %(Ax64_326)% | |
| . has_fiat_boundary(h, h-nb) %(Ax64_326_8)% | |
| forall a : Thing; b : Thing . part_of(b, a) <=> has_part(a, b) | |
| %(Ax63_325)% | |
| forall b : Thing | |
| . (exists a : Thing . has_fiat_boundary(a, b)) | |
| => AnatomicalBoundary(b) %(Ax62_324)% | |
| forall a : Thing | |
| . (exists b : Thing . has_fiat_boundary(a, b)) => BodyPart(a) | |
| %(Ax61_323)% | |
| forall a : Thing; b : Thing | |
| . fiat_boundary_of(b, a) <=> has_fiat_boundary(a, b) %(Ax60_322)% | |
| forall a : Thing . Wing(a) => Limb(a) %(Ax59_320)% | |
| forall a : Thing . Trunk(a) => CardinalBodyPart(a) %(Ax58_319)% | |
| forall a : Thing . TailBoundary(a) => AnatomicalBoundary(a) | |
| %(Ax57_318)% | |
| forall a : Thing | |
| . Tail(a) | |
| => (exists b : Thing | |
| . AnatomicalBoundary(b) /\ has_fiat_boundary(a, b)) | |
| /\ forall b : Thing; c : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ AnatomicalBoundary(b) | |
| => b = c %(Ax56_317)% | |
| forall a : Thing . Tail(a) => CardinalBodyPart(a) %(Ax55_316)% | |
| forall a : Thing | |
| . RightHindLimbEnd(a) | |
| <=> LimbEnd(a) /\ RightBodyPart(a) /\ PosteriorBodyPart(a) | |
| %(Ax54_315)% | |
| forall a : Thing | |
| . RightHindLimbBoundary(a) => AnatomicalBoundary(a) %(Ax53_314)% | |
| forall a : Thing | |
| . RightHindLimb(a) | |
| <=> Limb(a) /\ RightBodyPart(a) /\ PosteriorBodyPart(a) | |
| %(Ax52_313)% | |
| forall a : Thing | |
| . RightForeLimbEnd(a) | |
| <=> LimbEnd(a) /\ RightBodyPart(a) /\ AnteriorBodyPart(a) | |
| %(Ax51_312)% | |
| forall a : Thing | |
| . RightForeLimbBoundary(a) => AnatomicalBoundary(a) %(Ax50_311)% | |
| forall a : Thing | |
| . RightForeLimb(a) | |
| <=> Limb(a) /\ RightBodyPart(a) /\ AnteriorBodyPart(a) | |
| %(Ax49_309)% | |
| forall a : Thing . RightBodyPart(a) => BodyPart(a) %(Ax48_308)% | |
| forall a : Thing | |
| . QuadrupedTrunk(a) | |
| => (exists b : Thing . TailBoundary(b) /\ has_fiat_boundary(a, b)) | |
| /\ forall b : Thing; c : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ TailBoundary(b) | |
| => b = c %(Ax46_306)% | |
| forall a : Thing | |
| . QuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . RightHindLimbBoundary(b) /\ has_fiat_boundary(a, b)) | |
| /\ forall b : Thing; c : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ RightHindLimbBoundary(b) | |
| => b = c %(Ax45_305)% | |
| forall a : Thing | |
| . QuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . RightForeLimbBoundary(b) /\ has_fiat_boundary(a, b)) | |
| /\ forall b : Thing; c : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ RightForeLimbBoundary(b) | |
| => b = c %(Ax44_304)% | |
| forall a : Thing | |
| . QuadrupedTrunk(a) | |
| => (exists b : Thing . NeckBoundary(b) /\ has_fiat_boundary(a, b)) | |
| /\ forall b : Thing; c : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ NeckBoundary(b) | |
| => b = c %(Ax43_303)% | |
| forall a : Thing | |
| . QuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . LeftHindLimbBoundary(b) /\ has_fiat_boundary(a, b)) | |
| /\ forall b : Thing; c : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ LeftHindLimbBoundary(b) | |
| => b = c %(Ax42_302)% | |
| forall a : Thing | |
| . QuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . LeftForeLimbBoundary(b) /\ has_fiat_boundary(a, b)) | |
| /\ forall b : Thing; c : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ LeftForeLimbBoundary(b) | |
| => b = c %(Ax41_301)% | |
| forall a : Thing . QuadrupedTrunk(a) => Trunk(a) %(Ax40_300)% | |
| forall a : Thing | |
| . Quadruped(a) | |
| => (exists b : Thing; c : Thing; d : Thing; e : Thing | |
| . not b = c /\ not b = d /\ not b = e /\ not c = d /\ not c = e | |
| /\ not d = e /\ Leg(b) /\ Leg(c) /\ Leg(d) /\ Leg(e) | |
| /\ has_part(a, b) /\ has_part(a, c) /\ has_part(a, d) | |
| /\ has_part(a, e)) | |
| /\ forall b : Thing; c : Thing; d : Thing; e : Thing; f : Thing | |
| . has_part(a, b) /\ has_part(a, c) /\ has_part(a, d) | |
| /\ has_part(a, e) /\ has_part(a, f) /\ Leg(b) /\ Leg(c) /\ Leg(d) | |
| /\ Leg(e) | |
| => b = c \/ b = d \/ b = e \/ b = f \/ c = d \/ c = e \/ c = f | |
| \/ d = e \/ d = f \/ e = f %(Ax39_298)% | |
| forall a : Thing | |
| . Quadruped(a) | |
| => exists b : Thing . has_part(a, b) /\ QuadrupedTrunk(b) | |
| %(Ax38_297)% | |
| forall a : Thing | |
| . Quadruped(a) => exists b : Thing . has_part(a, b) /\ Head(b) | |
| %(Ax37_296)% | |
| forall a : Thing . Quadruped(a) => Organism(a) %(Ax36_295)% | |
| forall a : Thing . ProximalBoundary(a) => AnatomicalBoundary(a) | |
| %(Ax35_294)% | |
| forall a : Thing . PosteriorBodyPart(a) => BodyPart(a) %(Ax34_293)% | |
| forall a : Thing . Paw(a) => LimbEnd(a) %(Ax33_292)% | |
| forall a : Thing . NeckBoundary(a) => AnatomicalBoundary(a) | |
| %(Ax32_291)% | |
| forall a : Thing . Mammal(a) => Organism(a) %(Ax31_290)% | |
| forall a : Thing | |
| . LimbEnd(a) | |
| => (exists b : Thing | |
| . AnatomicalBoundary(b) /\ has_fiat_boundary(a, b)) | |
| /\ forall b : Thing; c : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ AnatomicalBoundary(b) | |
| => b = c %(Ax30_289)% | |
| forall a : Thing . LimbEnd(a) => CardinalBodyPart(a) %(Ax29_287)% | |
| forall a : Thing | |
| . Limb(a) | |
| => (exists b : Thing; c : Thing | |
| . not b = c /\ AnatomicalBoundary(b) /\ AnatomicalBoundary(c) | |
| /\ has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c)) | |
| /\ forall b : Thing; c : Thing; d : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ has_fiat_boundary(a, d) /\ AnatomicalBoundary(b) | |
| /\ AnatomicalBoundary(c) | |
| => b = c \/ b = d \/ c = d %(Ax28_286)% | |
| forall a : Thing | |
| . Limb(a) | |
| => exists b : Thing | |
| . has_fiat_boundary(a, b) /\ ProximalBoundary(b) %(Ax27_285)% | |
| forall a : Thing | |
| . Limb(a) | |
| => exists b : Thing . has_fiat_boundary(a, b) /\ DistalBoundary(b) | |
| %(Ax26_284)% | |
| forall a : Thing . Limb(a) => CardinalBodyPart(a) %(Ax25_283)% | |
| forall a : Thing . Leg(a) => Limb(a) %(Ax24_282)% | |
| forall a : Thing | |
| . LeftHindLimbEnd(a) | |
| <=> LimbEnd(a) /\ LeftBodyPart(a) /\ PosteriorBodyPart(a) | |
| %(Ax23_281)% | |
| forall a : Thing . LeftHindLimbBoundary(a) => AnatomicalBoundary(a) | |
| %(Ax22_280)% | |
| forall a : Thing | |
| . LeftHindLimb(a) | |
| <=> Limb(a) /\ LeftBodyPart(a) /\ PosteriorBodyPart(a) | |
| %(Ax21_279)% | |
| forall a : Thing . a = tl => PandaTail(a) %(Ax127_162)% | |
| forall a : Thing . a = thisAnimal => Panda(a) %(Ax126_161)% | |
| forall a : Thing . a = t => PandaTrunk(a) %(Ax118_152)% | |
| forall a : Thing . a = rhle => RightHindPandaPaw(a) %(Ax114_148)% | |
| forall a : Thing . a = rhl => RightHindPandaLeg(a) %(Ax109_142)% | |
| forall a : Thing . a = rfle => RightForePandaPaw(a) %(Ax105_138)% | |
| forall a : Thing . a = rfl => RightForePandaLeg(a) %(Ax100_133)% | |
| forall a : Thing . a = lhle => LeftHindPandaPaw(a) %(Ax96_257)% | |
| forall a : Thing . a = lhl => LeftHindPandaLeg(a) %(Ax91_252)% | |
| forall a : Thing . a = lfle => LeftForePandaPaw(a) %(Ax87_247)% | |
| forall a : Thing . a = lfl => LeftForePandaLeg(a) %(Ax82_242)% | |
| forall a : Thing . a = h => PandaHead(a) %(Ax78_237)% | |
| forall a : Thing | |
| . RightHindPandaPaw(a) <=> PandaPaw(a) /\ RightHindLimbEnd(a) | |
| %(Ax68_226)% | |
| forall a : Thing | |
| . RightHindPandaLeg(a) <=> PandaLeg(a) /\ RightHindLimb(a) | |
| %(Ax67_225)% | |
| forall a : Thing | |
| . RightForePandaPaw(a) <=> PandaPaw(a) /\ RightForeLimbEnd(a) | |
| %(Ax63_221)% | |
| forall a : Thing | |
| . RightForePandaLeg(a) <=> PandaLeg(a) /\ RightForeLimb(a) | |
| %(Ax62_220)% | |
| forall a : Thing | |
| . PandaTrunk(a) | |
| <=> QuadrupedTrunk(a) | |
| /\ exists b : Thing . part_of(a, b) /\ Panda(b) %(Ax42_198)% | |
| forall a : Thing | |
| . PandaTail(a) | |
| <=> Tail(a) /\ exists b : Thing . part_of(a, b) /\ Panda(b) | |
| %(Ax41_197)% | |
| forall a : Thing | |
| . PandaPaw(a) | |
| <=> Paw(a) /\ exists b : Thing . part_of(a, b) /\ Panda(b) | |
| %(Ax40_196)% | |
| forall a : Thing | |
| . PandaLeg(a) | |
| <=> Leg(a) /\ exists b : Thing . part_of(a, b) /\ Panda(b) | |
| %(Ax39_194)% | |
| forall a : Thing | |
| . PandaHead(a) | |
| <=> Head(a) /\ exists b : Thing . part_of(a, b) /\ Panda(b) | |
| %(Ax38_193)% | |
| forall a : Thing . Panda(a) => Quadruped(a) %(Ax37_192)% | |
| forall a : Thing | |
| . LeftHindPandaPaw(a) <=> PandaPaw(a) /\ LeftHindLimbEnd(a) | |
| %(Ax27_181)% | |
| forall a : Thing | |
| . LeftHindPandaLeg(a) <=> PandaLeg(a) /\ LeftHindLimb(a) | |
| %(Ax26_180)% | |
| forall a : Thing | |
| . LeftForePandaPaw(a) <=> PandaPaw(a) /\ LeftForeLimbEnd(a) | |
| %(Ax22_176)% | |
| forall a : Thing | |
| . LeftForePandaLeg(a) <=> PandaLeg(a) /\ LeftForeLimb(a) | |
| %(Ax21_175)% | |
| forall a : Thing . a = tl => TigerTail(a) %(Ax127)% | |
| forall a : Thing . a = thisAnimal => Tiger(a) %(Ax126)% | |
| forall a : Thing . a = t-rflb => RightForeLimbBoundary(a) %(Ax123)% | |
| forall a : Thing . a = t-nb => NeckBoundary(a) %(Ax122)% | |
| forall a : Thing . a = t-lhlb => LeftHindLimbBoundary(a) %(Ax121)% | |
| forall a : Thing . a = t-lflb => LeftForeLimbBoundary(a) %(Ax120)% | |
| . part_of(t, thisAnimal) %(Ax119)% | |
| . has_fiat_boundary(t, t-nb) %(Ax119_9)% | |
| . has_fiat_boundary(t, t-lflb) %(Ax119_10)% | |
| . has_fiat_boundary(t, t-rflb) %(Ax119_11)% | |
| . has_fiat_boundary(t, t-lhlb) %(Ax119_12)% | |
| . has_fiat_boundary(t, t-rhlb) %(Ax119_13)% | |
| . has_fiat_boundary(t, t-tlb) %(Ax119_14)% | |
| forall a : Thing . a = t => TigerTrunk(a) %(Ax118)% | |
| . meets(rhle-pb, rhl-db) %(Ax117)% | |
| forall a : Thing . a = rhle-pb => ProximalBoundary(a) %(Ax116)% | |
| . part_of(rhle, thisAnimal) %(Ax115)% | |
| . has_fiat_boundary(rhle, rhle-pb) %(Ax115_15)% | |
| forall a : Thing . a = rhle => RightHindTigerPaw(a) %(Ax114)% | |
| . meets(rhl-pb, t-rhlb) %(Ax113)% | |
| forall a : Thing . a = rhl-pb => ProximalBoundary(a) %(Ax112)% | |
| forall a : Thing . a = rhl-db => DistalBoundary(a) %(Ax111)% | |
| . part_of(rhl, thisAnimal) %(Ax110)% | |
| . has_fiat_boundary(rhl, rhl-pb) %(Ax110_16)% | |
| . has_fiat_boundary(rhl, rhl-db) %(Ax110_17)% | |
| forall a : Thing . a = rhl => RightHindTigerLeg(a) %(Ax109)% | |
| . meets(rfle-pb, rfl-db) %(Ax108)% | |
| forall a : Thing . a = rfle-pb => ProximalBoundary(a) %(Ax107)% | |
| . part_of(rfle, thisAnimal) %(Ax106)% | |
| . has_fiat_boundary(rfle, rfle-pb) %(Ax106_18)% | |
| forall a : Thing . a = rfle => RightForeTigerPaw(a) %(Ax105)% | |
| . meets(rfl-pb, t-rflb) %(Ax104)% | |
| forall a : Thing . a = rfl-pb => ProximalBoundary(a) %(Ax103)% | |
| forall a : Thing . a = rfl-db => DistalBoundary(a) %(Ax102)% | |
| . part_of(rfl, thisAnimal) %(Ax101)% | |
| . has_fiat_boundary(rfl, rfl-pb) %(Ax101_19)% | |
| . has_fiat_boundary(rfl, rfl-db) %(Ax101_20)% | |
| forall a : Thing . a = rfl => RightForeTigerLeg(a) %(Ax100)% | |
| forall a : Thing . a = lhle => LeftHindTigerPaw(a) %(Ax96)% | |
| forall a : Thing . a = lhl => LeftHindTigerLeg(a) %(Ax91)% | |
| forall a : Thing . a = lfle => LeftForeTigerPaw(a) %(Ax87)% | |
| forall a : Thing . a = lfl => LeftForeTigerLeg(a) %(Ax82)% | |
| forall a : Thing . a = h => TigerHead(a) %(Ax78)% | |
| forall a : Thing | |
| . TigerTrunk(a) | |
| <=> QuadrupedTrunk(a) | |
| /\ exists b : Thing . part_of(a, b) /\ Tiger(b) %(Ax71)% | |
| forall a : Thing | |
| . TigerTail(a) | |
| <=> Tail(a) /\ exists b : Thing . part_of(a, b) /\ Tiger(b) | |
| %(Ax70)% | |
| forall a : Thing | |
| . TigerPaw(a) | |
| <=> Paw(a) /\ exists b : Thing . part_of(a, b) /\ Tiger(b) | |
| %(Ax69)% | |
| forall a : Thing | |
| . TigerLeg(a) | |
| <=> Leg(a) /\ exists b : Thing . part_of(a, b) /\ Tiger(b) | |
| %(Ax68)% | |
| forall a : Thing | |
| . TigerHead(a) | |
| <=> Head(a) /\ exists b : Thing . part_of(a, b) /\ Tiger(b) | |
| %(Ax67)% | |
| forall a : Thing . Tiger(a) => Quadruped(a) %(Ax66)% | |
| forall a : Thing | |
| . RightHindTigerPaw(a) <=> TigerPaw(a) /\ RightHindLimbEnd(a) | |
| %(Ax62)% | |
| forall a : Thing | |
| . RightHindTigerLeg(a) <=> TigerLeg(a) /\ RightHindLimb(a) | |
| %(Ax61)% | |
| forall a : Thing | |
| . RightForeTigerPaw(a) <=> TigerPaw(a) /\ RightForeLimbEnd(a) | |
| %(Ax57)% | |
| forall a : Thing | |
| . RightForeTigerLeg(a) <=> TigerLeg(a) /\ RightForeLimb(a) | |
| %(Ax56)% | |
| forall a : Thing | |
| . QuadrupedTrunk(a) | |
| => (exists b : Thing; c : Thing; d : Thing; e : Thing; f : Thing; | |
| g : Thing | |
| . not b = c /\ not b = d /\ not b = e /\ not b = f /\ not b = g | |
| /\ not c = d /\ not c = e /\ not c = f /\ not c = g /\ not d = e | |
| /\ not d = f /\ not d = g /\ not e = f /\ not e = g /\ not f = g | |
| /\ AnatomicalBoundary(b) /\ AnatomicalBoundary(c) | |
| /\ AnatomicalBoundary(d) /\ AnatomicalBoundary(e) | |
| /\ AnatomicalBoundary(f) /\ AnatomicalBoundary(g) | |
| /\ has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ has_fiat_boundary(a, d) /\ has_fiat_boundary(a, e) | |
| /\ has_fiat_boundary(a, f) /\ has_fiat_boundary(a, g)) | |
| /\ forall b : Thing; c : Thing; d : Thing; e : Thing; f : Thing; | |
| g : Thing; h : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ has_fiat_boundary(a, d) /\ has_fiat_boundary(a, e) | |
| /\ has_fiat_boundary(a, f) /\ has_fiat_boundary(a, g) | |
| /\ has_fiat_boundary(a, (var h : Thing)) /\ AnatomicalBoundary(b) | |
| /\ AnatomicalBoundary(c) /\ AnatomicalBoundary(d) | |
| /\ AnatomicalBoundary(e) /\ AnatomicalBoundary(f) | |
| /\ AnatomicalBoundary(g) | |
| => b = c \/ b = d \/ b = e \/ b = f \/ b = g \/ b = (var h : Thing) | |
| \/ c = d \/ c = e \/ c = f \/ c = g \/ c = (var h : Thing) \/ d = e | |
| \/ d = f \/ d = g \/ d = (var h : Thing) \/ e = f \/ e = g | |
| \/ e = (var h : Thing) \/ f = g \/ f = (var h : Thing) | |
| \/ g = (var h : Thing) %(Ax45)% | |
| forall a : Thing | |
| . LeftHindTigerPaw(a) <=> TigerPaw(a) /\ LeftHindLimbEnd(a) | |
| %(Ax27)% | |
| forall a : Thing | |
| . LeftHindTigerLeg(a) <=> TigerLeg(a) /\ LeftHindLimb(a) %(Ax26)% | |
| forall a : Thing | |
| . LeftForeTigerPaw(a) <=> TigerPaw(a) /\ LeftForeLimbEnd(a) | |
| %(Ax22)% | |
| forall a : Thing | |
| . LeftForeTigerLeg(a) <=> TigerLeg(a) /\ LeftForeLimb(a) %(Ax21)% | |
| forall a : Thing | |
| . LeftForeLimbEnd(a) | |
| <=> LimbEnd(a) /\ LeftBodyPart(a) /\ AnteriorBodyPart(a) | |
| %(Ax20)% | |
| forall a : Thing . LeftForeLimbBoundary(a) => AnatomicalBoundary(a) | |
| %(Ax19)% | |
| forall a : Thing | |
| . LeftForeLimb(a) | |
| <=> Limb(a) /\ LeftBodyPart(a) /\ AnteriorBodyPart(a) %(Ax18)% | |
| forall a : Thing . LeftBodyPart(a) => BodyPart(a) %(Ax17)% | |
| forall a : Thing . Hoof(a) => LimbEnd(a) %(Ax16)% | |
| forall a : Thing | |
| . Head(a) | |
| => (exists b : Thing | |
| . AnatomicalBoundary(b) /\ has_fiat_boundary(a, b)) | |
| /\ forall b : Thing; c : Thing | |
| . has_fiat_boundary(a, b) /\ has_fiat_boundary(a, c) | |
| /\ AnatomicalBoundary(b) | |
| => b = c %(Ax15)% | |
| forall a : Thing . Head(a) => CardinalBodyPart(a) %(Ax14)% | |
| forall a : Thing . Hand(a) => LimbEnd(a) %(Ax13)% | |
| forall a : Thing . Hair(a) => BodyPart(a) %(Ax12)% | |
| forall a : Thing . Foot(a) => LimbEnd(a) %(Ax11)% | |
| forall a : Thing . DistalBoundary(a) => AnatomicalBoundary(a) | |
| %(Ax10)% | |
| forall a : Thing . Claw(a) => LimbEnd(a) %(Ax9)% | |
| forall a : Thing . CardinalBodyPart(a) => BodyPart(a) %(Ax8)% | |
| forall a : Thing . Arm(a) => Limb(a) %(Ax7)% | |
| forall a : Thing . AnteriorBodyPart(a) => BodyPart(a) %(Ax6)% | |
| forall a : Thing | |
| . AnatomicalBoundary(a) | |
| => exists b : Thing . fiat_boundary_of(a, b) /\ BodyPart(b) | |
| %(Ax5)% | |
| forall a : Thing . not (Head(a) /\ Trunk(a)) %(Ax4)% | |
| forall a : Thing . not (Head(a) /\ Limb(a)) %(Ax4_21)% | |
| forall a : Thing . not (Head(a) /\ LimbEnd(a)) %(Ax4_22)% | |
| forall a : Thing . not (Head(a) /\ Tail(a)) %(Ax4_23)% | |
| forall a : Thing . not (Trunk(a) /\ Limb(a)) %(Ax4_24)% | |
| forall a : Thing . not (Trunk(a) /\ LimbEnd(a)) %(Ax4_25)% | |
| forall a : Thing . not (Trunk(a) /\ Tail(a)) %(Ax4_26)% | |
| forall a : Thing . not (Limb(a) /\ LimbEnd(a)) %(Ax4_27)% | |
| forall a : Thing . not (Limb(a) /\ Tail(a)) %(Ax4_28)% | |
| forall a : Thing . not (LimbEnd(a) /\ Tail(a)) %(Ax4_29)% | |
| forall a : Thing . not (Foot(a) /\ Hand(a)) %(Ax3)% | |
| forall a : Thing . not (Foot(a) /\ Hoof(a)) %(Ax3_30)% | |
| forall a : Thing . not (Foot(a) /\ Paw(a)) %(Ax3_31)% | |
| forall a : Thing . not (Foot(a) /\ Claw(a)) %(Ax3_32)% | |
| forall a : Thing . not (Hand(a) /\ Hoof(a)) %(Ax3_33)% | |
| forall a : Thing . not (Hand(a) /\ Paw(a)) %(Ax3_34)% | |
| forall a : Thing . not (Hand(a) /\ Claw(a)) %(Ax3_35)% | |
| forall a : Thing . not (Hoof(a) /\ Paw(a)) %(Ax3_36)% | |
| forall a : Thing . not (Hoof(a) /\ Claw(a)) %(Ax3_37)% | |
| forall a : Thing . not (Paw(a) /\ Claw(a)) %(Ax3_38)% | |
| forall a : Thing . not (Arm(a) /\ Leg(a)) %(Ax2)% | |
| forall a : Thing . not (Arm(a) /\ Wing(a)) %(Ax2_39)% | |
| forall a : Thing . not (Leg(a) /\ Wing(a)) %(Ax2_40)% | |
| forall a : Thing | |
| . not (AnatomicalBoundary(a) /\ CardinalBodyPart(a)) %(Ax1)% | |
| forall a : Thing . not (AnatomicalBoundary(a) /\ Organism(a)) | |
| %(Ax1_41)% | |
| forall a : Thing . not (CardinalBodyPart(a) /\ Organism(a)) | |
| %(Ax1_42)% |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| logic CASL.SulFOL= | |
| sorts Char, DATA, ENTITIES, ENTITY, ID, IDREF, IDREFS, Literal, | |
| NCName, NMTOKEN, NMTOKENS, NOTATION, Name, QName, Thing, | |
| XMLLiteral, anyURI, base64Binary, boolean, byte, date, dateTime, | |
| dateTimeStamp, decimal, double, duration, float, gDay, gMonth, | |
| gMonthDay, gYear, gYearMonth, hexBinary, int, integer, language, | |
| long, negativeInteger, nonNegativeInteger, nonPositiveInteger, | |
| normalizedString, positiveInteger, rational, real, short, string, | |
| time, token, unsignedByte, unsignedInt, unsignedLongS, | |
| unsignedShort | |
| sorts ENTITIES, ENTITY, ID, IDREF, IDREFS, Literal, NCName, | |
| NMTOKEN, NMTOKENS, NOTATION, Name, QName, XMLLiteral, anyURI, | |
| base64Binary, boolean, byte, date, dateTime, dateTimeStamp, | |
| decimal, double, duration, float, gDay, gMonth, gMonthDay, gYear, | |
| gYearMonth, hexBinary, int, language, long, normalizedString, | |
| rational, real, short, string, time, token, unsignedByte, | |
| unsignedInt, unsignedLongS, unsignedShort < DATA; | |
| integer < float; nonNegativeInteger, nonPositiveInteger < integer; | |
| positiveInteger < nonNegativeInteger; | |
| negativeInteger < nonPositiveInteger | |
| op '\000' : Char | |
| op '\001' : Char | |
| op '\002' : Char | |
| op '\003' : Char | |
| op '\004' : Char | |
| op '\005' : Char | |
| op '\006' : Char | |
| op '\007' : Char | |
| op '\008' : Char | |
| op '\009' : Char | |
| op '\010' : Char | |
| op '\011' : Char | |
| op '\012' : Char | |
| op '\013' : Char | |
| op '\014' : Char | |
| op '\015' : Char | |
| op '\016' : Char | |
| op '\017' : Char | |
| op '\018' : Char | |
| op '\019' : Char | |
| op '\020' : Char | |
| op '\021' : Char | |
| op '\022' : Char | |
| op '\023' : Char | |
| op '\024' : Char | |
| op '\025' : Char | |
| op '\026' : Char | |
| op '\027' : Char | |
| op '\028' : Char | |
| op '\029' : Char | |
| op '\030' : Char | |
| op '\031' : Char | |
| op '\032' : Char | |
| op '\033' : Char | |
| op '\034' : Char | |
| op '\035' : Char | |
| op '\036' : Char | |
| op '\037' : Char | |
| op '\038' : Char | |
| op '\039' : Char | |
| op '\040' : Char | |
| op '\041' : Char | |
| op '\042' : Char | |
| op '\043' : Char | |
| op '\044' : Char | |
| op '\045' : Char | |
| op '\046' : Char | |
| op '\047' : Char | |
| op '\048' : Char | |
| op '\049' : Char | |
| op '\050' : Char | |
| op '\051' : Char | |
| op '\052' : Char | |
| op '\053' : Char | |
| op '\054' : Char | |
| op '\055' : Char | |
| op '\056' : Char | |
| op '\057' : Char | |
| op '\058' : Char | |
| op '\059' : Char | |
| op '\060' : Char | |
| op '\061' : Char | |
| op '\062' : Char | |
| op '\063' : Char | |
| op '\064' : Char | |
| op '\065' : Char | |
| op '\066' : Char | |
| op '\067' : Char | |
| op '\068' : Char | |
| op '\069' : Char | |
| op '\070' : Char | |
| op '\071' : Char | |
| op '\072' : Char | |
| op '\073' : Char | |
| op '\074' : Char | |
| op '\075' : Char | |
| op '\076' : Char | |
| op '\077' : Char | |
| op '\078' : Char | |
| op '\079' : Char | |
| op '\080' : Char | |
| op '\081' : Char | |
| op '\082' : Char | |
| op '\083' : Char | |
| op '\084' : Char | |
| op '\085' : Char | |
| op '\086' : Char | |
| op '\087' : Char | |
| op '\088' : Char | |
| op '\089' : Char | |
| op '\090' : Char | |
| op '\091' : Char | |
| op '\092' : Char | |
| op '\093' : Char | |
| op '\094' : Char | |
| op '\095' : Char | |
| op '\096' : Char | |
| op '\097' : Char | |
| op '\098' : Char | |
| op '\099' : Char | |
| op '\100' : Char | |
| op '\101' : Char | |
| op '\102' : Char | |
| op '\103' : Char | |
| op '\104' : Char | |
| op '\105' : Char | |
| op '\106' : Char | |
| op '\107' : Char | |
| op '\108' : Char | |
| op '\109' : Char | |
| op '\110' : Char | |
| op '\111' : Char | |
| op '\112' : Char | |
| op '\113' : Char | |
| op '\114' : Char | |
| op '\115' : Char | |
| op '\116' : Char | |
| op '\117' : Char | |
| op '\118' : Char | |
| op '\119' : Char | |
| op '\120' : Char | |
| op '\121' : Char | |
| op '\122' : Char | |
| op '\123' : Char | |
| op '\124' : Char | |
| op '\125' : Char | |
| op '\126' : Char | |
| op '\127' : Char | |
| op -__ : float -> float | |
| op -__ : integer -> integer | |
| op 0 : nonNegativeInteger | |
| op 1 : nonNegativeInteger | |
| op 2 : nonNegativeInteger | |
| op 3 : nonNegativeInteger | |
| op 4 : nonNegativeInteger | |
| op 5 : nonNegativeInteger | |
| op 6 : nonNegativeInteger | |
| op 7 : nonNegativeInteger | |
| op 8 : nonNegativeInteger | |
| op 9 : nonNegativeInteger | |
| op False : boolean | |
| op True : boolean | |
| op __:::__ : nonNegativeInteger * nonNegativeInteger -> float | |
| op __:@:__ : Char * string -> string | |
| op __@@__ : nonNegativeInteger * nonNegativeInteger -> | |
| nonNegativeInteger | |
| op __E__ : float * integer -> float | |
| op emptyString : string | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedh : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedh_unb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl_udb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl_upb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfle : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfle_upb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl_udb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl_upb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhle : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhle_upb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl_udb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl_upb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfle : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfle_upb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl_udb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl_upb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhle : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhle_upb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_ulflb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_ulhlb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_unb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_urflb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_urhlb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_utlb : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedtl : Thing | |
| op http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedtl_upb : Thing | |
| pred Nothing : Thing | |
| pred Thing : Thing | |
| pred __<__ : DATA * DATA | |
| pred __<=__ : DATA * DATA | |
| pred __>__ : DATA * DATA | |
| pred __>=__ : DATA * DATA | |
| pred __fractionDigits__ : DATA * DATA | |
| pred __langRange__ : DATA * DATA | |
| pred __length__ : DATA * DATA | |
| pred __maxLength__ : DATA * DATA | |
| pred __minLength__ : DATA * DATA | |
| pred __pattern__ : DATA * DATA | |
| pred __totalDigits__ : DATA * DATA | |
| pred even : integer | |
| pred even : nonNegativeInteger | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnteriorBodyPart : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedArm : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedBodyPart : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedCardinalBodyPart : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedClaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedDistalBoundary : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedFoot : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHair : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHand : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHoof : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftBodyPart : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimb : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimbBoundary : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimbEnd : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForePandaLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForePandaPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeTigerLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeTigerPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimb : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimbBoundary : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimbEnd : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindPandaLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindPandaPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindTigerLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindTigerPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedMammal : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedNeckBoundary : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedOrganism : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPanda : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaHead : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaTail : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaTrunk : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPosteriorBodyPart : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadruped : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightBodyPart : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimb : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimbBoundary : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimbEnd : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForePandaLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForePandaPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeTigerLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeTigerPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimb : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimbBoundary : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimbEnd : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindPandaLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindPandaPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindTigerLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindTigerPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTail : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTailBoundary : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTiger : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerHead : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerLeg : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerPaw : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerTail : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerTrunk : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTrunk : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedWing : Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedfiat_uboundary_uof : Thing * | |
| Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary : Thing * | |
| Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart : Thing * | |
| Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets : Thing * | |
| Thing | |
| pred http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof : Thing * | |
| Thing | |
| pred odd : integer | |
| pred odd : nonNegativeInteger | |
| . false %(inconsistency)% %implied | |
| forall a : Thing . not Nothing(a) %(nothing in Nothing)% | |
| forall a : Thing . Thing(a) %(thing in Thing)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedtl_upb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax104_267)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedtl_upb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_utlb) | |
| %(Ax103_266)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedtl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax102_265)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedtl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedtl_upb) | |
| %(Ax102_265_1)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_utlb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTailBoundary(a) | |
| %(Ax101_264)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_urhlb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimbBoundary(a) | |
| %(Ax100_263)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhle_upb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax80_344)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhle_upb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl_udb) | |
| %(Ax79_342)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhle, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax78_341)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhle, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhle_upb) | |
| %(Ax78_341_2)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl_upb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax77_340)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl_upb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_ulhlb) | |
| %(Ax76_339)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl_udb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedDistalBoundary(a) | |
| %(Ax75_338)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax74_337)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl_upb) | |
| %(Ax74_337_3)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl_udb) | |
| %(Ax74_337_4)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfle_upb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax73_336)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfle_upb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl_udb) | |
| %(Ax72_335)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfle, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax71_334)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfle, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfle_upb) | |
| %(Ax71_334_5)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl_upb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax70_333)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl_upb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_ulflb) | |
| %(Ax69_331)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl_udb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedDistalBoundary(a) | |
| %(Ax68_330)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax67_329)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl_upb) | |
| %(Ax67_329_6)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl_udb) | |
| %(Ax67_329_7)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedh_unb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax66_328)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedh_unb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_unb) | |
| %(Ax65_327)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedh, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax64_326)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedh, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedh_unb) | |
| %(Ax64_326_8)% | |
| forall a : Thing; b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(b, | |
| a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| b) | |
| %(Ax63_325)% | |
| forall b : Thing | |
| . (exists a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| %(Ax62_324)% | |
| forall a : Thing | |
| . (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedBodyPart(a) | |
| %(Ax61_323)% | |
| forall a : Thing; b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedfiat_uboundary_uof(b, | |
| a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| %(Ax60_322)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedWing(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| %(Ax59_320)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTrunk(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedCardinalBodyPart(a) | |
| %(Ax58_319)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTailBoundary(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| %(Ax57_318)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTail(a) | |
| => (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| /\ forall b : Thing; c : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| => b = c %(Ax56_317)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTail(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedCardinalBodyPart(a) | |
| %(Ax55_316)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimbEnd(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightBodyPart(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPosteriorBodyPart(a) | |
| %(Ax54_315)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimbBoundary(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| %(Ax53_314)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimb(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightBodyPart(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPosteriorBodyPart(a) | |
| %(Ax52_313)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimbEnd(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightBodyPart(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnteriorBodyPart(a) | |
| %(Ax51_312)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimbBoundary(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| %(Ax50_311)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimb(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightBodyPart(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnteriorBodyPart(a) | |
| %(Ax49_309)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightBodyPart(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedBodyPart(a) | |
| %(Ax48_308)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTailBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| /\ forall b : Thing; c : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTailBoundary(b) | |
| => b = c %(Ax46_306)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimbBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| /\ forall b : Thing; c : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimbBoundary(b) | |
| => b = c %(Ax45_305)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimbBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| /\ forall b : Thing; c : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimbBoundary(b) | |
| => b = c %(Ax44_304)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedNeckBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| /\ forall b : Thing; c : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedNeckBoundary(b) | |
| => b = c %(Ax43_303)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimbBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| /\ forall b : Thing; c : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimbBoundary(b) | |
| => b = c %(Ax42_302)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| => (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimbBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| /\ forall b : Thing; c : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimbBoundary(b) | |
| => b = c %(Ax41_301)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTrunk(a) | |
| %(Ax40_300)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadruped(a) | |
| => (exists b : Thing; c : Thing; d : Thing; e : Thing | |
| . not b = c /\ not b = d /\ not b = e /\ not c = d /\ not c = e | |
| /\ not d = e | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(d) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(e) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| d) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| e)) | |
| /\ forall b : Thing; c : Thing; d : Thing; e : Thing; f : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| d) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| e) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| f) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(d) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(e) | |
| => b = c \/ b = d \/ b = e \/ b = f \/ c = d \/ c = e \/ c = f | |
| \/ d = e \/ d = f \/ e = f %(Ax39_298)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadruped(a) | |
| => exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(b) | |
| %(Ax38_297)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadruped(a) | |
| => exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_upart(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead(b) | |
| %(Ax37_296)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadruped(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedOrganism(a) | |
| %(Ax36_295)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| %(Ax35_294)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPosteriorBodyPart(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedBodyPart(a) | |
| %(Ax34_293)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPaw(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| %(Ax33_292)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedNeckBoundary(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| %(Ax32_291)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedMammal(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedOrganism(a) | |
| %(Ax31_290)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| => (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| /\ forall b : Thing; c : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| => b = c %(Ax30_289)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedCardinalBodyPart(a) | |
| %(Ax29_287)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| => (exists b : Thing; c : Thing | |
| . not b = c | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c)) | |
| /\ forall b : Thing; c : Thing; d : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| d) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(c) | |
| => b = c \/ b = d \/ c = d %(Ax28_286)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| => exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(b) | |
| %(Ax27_285)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| => exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedDistalBoundary(b) | |
| %(Ax26_284)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedCardinalBodyPart(a) | |
| %(Ax25_283)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| %(Ax24_282)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimbEnd(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftBodyPart(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPosteriorBodyPart(a) | |
| %(Ax23_281)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimbBoundary(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| %(Ax22_280)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimb(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftBodyPart(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPosteriorBodyPart(a) | |
| %(Ax21_279)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedtl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaTail(a) | |
| %(Ax127_162)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPanda(a) | |
| %(Ax126_161)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaTrunk(a) | |
| %(Ax118_152)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhle | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindPandaPaw(a) | |
| %(Ax114_148)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindPandaLeg(a) | |
| %(Ax109_142)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfle | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForePandaPaw(a) | |
| %(Ax105_138)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForePandaLeg(a) | |
| %(Ax100_133)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhle | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindPandaPaw(a) | |
| %(Ax96_257)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindPandaLeg(a) | |
| %(Ax91_252)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfle | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForePandaPaw(a) | |
| %(Ax87_247)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForePandaLeg(a) | |
| %(Ax82_242)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedh | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaHead(a) | |
| %(Ax78_237)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindPandaPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaPaw(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimbEnd(a) | |
| %(Ax68_226)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindPandaLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaLeg(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimb(a) | |
| %(Ax67_225)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForePandaPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaPaw(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimbEnd(a) | |
| %(Ax63_221)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForePandaLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaLeg(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimb(a) | |
| %(Ax62_220)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaTrunk(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPanda(b) | |
| %(Ax42_198)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaTail(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTail(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPanda(b) | |
| %(Ax41_197)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPaw(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPanda(b) | |
| %(Ax40_196)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPanda(b) | |
| %(Ax39_194)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaHead(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPanda(b) | |
| %(Ax38_193)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPanda(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadruped(a) | |
| %(Ax37_192)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindPandaPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaPaw(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimbEnd(a) | |
| %(Ax27_181)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindPandaLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaLeg(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimb(a) | |
| %(Ax26_180)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForePandaPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaPaw(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimbEnd(a) | |
| %(Ax22_176)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForePandaLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPandaLeg(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimb(a) | |
| %(Ax21_175)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedtl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerTail(a) | |
| %(Ax127)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTiger(a) | |
| %(Ax126)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_urflb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimbBoundary(a) | |
| %(Ax123)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_unb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedNeckBoundary(a) | |
| %(Ax122)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_ulhlb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimbBoundary(a) | |
| %(Ax121)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_ulflb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimbBoundary(a) | |
| %(Ax120)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax119)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_unb) | |
| %(Ax119_9)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_ulflb) | |
| %(Ax119_10)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_urflb) | |
| %(Ax119_11)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_ulhlb) | |
| %(Ax119_12)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_urhlb) | |
| %(Ax119_13)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_utlb) | |
| %(Ax119_14)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerTrunk(a) | |
| %(Ax118)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhle_upb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl_udb) | |
| %(Ax117)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhle_upb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax116)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhle, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax115)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhle, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhle_upb) | |
| %(Ax115_15)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhle | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindTigerPaw(a) | |
| %(Ax114)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl_upb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_urhlb) | |
| %(Ax113)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl_upb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax112)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl_udb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedDistalBoundary(a) | |
| %(Ax111)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax110)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl_upb) | |
| %(Ax110_16)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl_udb) | |
| %(Ax110_17)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrhl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindTigerLeg(a) | |
| %(Ax109)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfle_upb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl_udb) | |
| %(Ax108)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfle_upb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax107)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfle, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax106)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfle, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfle_upb) | |
| %(Ax106_18)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfle | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeTigerPaw(a) | |
| %(Ax105)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedmeets(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl_upb, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedt_urflb) | |
| %(Ax104)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl_upb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedProximalBoundary(a) | |
| %(Ax103)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl_udb | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedDistalBoundary(a) | |
| %(Ax102)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedthisAnimal) | |
| %(Ax101)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl_upb) | |
| %(Ax101_19)% | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl, | |
| http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl_udb) | |
| %(Ax101_20)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedrfl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeTigerLeg(a) | |
| %(Ax100)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhle | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindTigerPaw(a) | |
| %(Ax96)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlhl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindTigerLeg(a) | |
| %(Ax91)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfle | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeTigerPaw(a) | |
| %(Ax87)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedlfl | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeTigerLeg(a) | |
| %(Ax82)% | |
| forall a : Thing | |
| . a | |
| = http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedh | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerHead(a) | |
| %(Ax78)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerTrunk(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTiger(b) | |
| %(Ax71)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerTail(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTail(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTiger(b) | |
| %(Ax70)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPaw(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTiger(b) | |
| %(Ax69)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTiger(b) | |
| %(Ax68)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerHead(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead(a) | |
| /\ exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedpart_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTiger(b) | |
| %(Ax67)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTiger(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadruped(a) | |
| %(Ax66)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindTigerPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerPaw(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimbEnd(a) | |
| %(Ax62)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindTigerLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerLeg(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightHindLimb(a) | |
| %(Ax61)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeTigerPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerPaw(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimbEnd(a) | |
| %(Ax57)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeTigerLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerLeg(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedRightForeLimb(a) | |
| %(Ax56)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedQuadrupedTrunk(a) | |
| => (exists b : Thing; c : Thing; d : Thing; e : Thing; f : Thing; | |
| g : Thing | |
| . not b = c /\ not b = d /\ not b = e /\ not b = f /\ not b = g | |
| /\ not c = d /\ not c = e /\ not c = f /\ not c = g /\ not d = e | |
| /\ not d = f /\ not d = g /\ not e = f /\ not e = g /\ not f = g | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(d) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(e) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(f) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(g) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| d) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| e) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| f) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| g)) | |
| /\ forall b : Thing; c : Thing; d : Thing; e : Thing; f : Thing; | |
| g : Thing; h : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| d) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| e) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| f) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| g) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| h) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(d) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(e) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(f) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(g) | |
| => b = c \/ b = d \/ b = e \/ b = f \/ b = g \/ b = h \/ c = d | |
| \/ c = e \/ c = f \/ c = g \/ c = h \/ d = e \/ d = f \/ d = g | |
| \/ d = h \/ e = f \/ e = g \/ e = h \/ f = g \/ f = h \/ g = h | |
| %(Ax45)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindTigerPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerPaw(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimbEnd(a) | |
| %(Ax27)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindTigerLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerLeg(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftHindLimb(a) | |
| %(Ax26)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeTigerPaw(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerPaw(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimbEnd(a) | |
| %(Ax22)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeTigerLeg(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTigerLeg(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimb(a) | |
| %(Ax21)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimbEnd(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftBodyPart(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnteriorBodyPart(a) | |
| %(Ax20)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimbBoundary(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| %(Ax19)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftForeLimb(a) | |
| <=> http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftBodyPart(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnteriorBodyPart(a) | |
| %(Ax18)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeftBodyPart(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedBodyPart(a) | |
| %(Ax17)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHoof(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| %(Ax16)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead(a) | |
| => (exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b)) | |
| /\ forall b : Thing; c : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedhas_ufiat_uboundary(a, | |
| c) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(b) | |
| => b = c %(Ax15)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedCardinalBodyPart(a) | |
| %(Ax14)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHand(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| %(Ax13)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHair(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedBodyPart(a) | |
| %(Ax12)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedFoot(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| %(Ax11)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedDistalBoundary(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| %(Ax10)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedClaw(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| %(Ax9)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedCardinalBodyPart(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedBodyPart(a) | |
| %(Ax8)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedArm(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| %(Ax7)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnteriorBodyPart(a) | |
| => http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedBodyPart(a) | |
| %(Ax6)% | |
| forall a : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| => exists b : Thing | |
| . http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedfiat_uboundary_uof(a, | |
| b) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedBodyPart(b) | |
| %(Ax5)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTrunk(a)) | |
| %(Ax4)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a)) | |
| %(Ax4_21)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a)) | |
| %(Ax4_22)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHead(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTail(a)) | |
| %(Ax4_23)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTrunk(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a)) | |
| %(Ax4_24)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTrunk(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a)) | |
| %(Ax4_25)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTrunk(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTail(a)) | |
| %(Ax4_26)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a)) | |
| %(Ax4_27)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimb(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTail(a)) | |
| %(Ax4_28)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLimbEnd(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedTail(a)) | |
| %(Ax4_29)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedFoot(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHand(a)) | |
| %(Ax3)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedFoot(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHoof(a)) | |
| %(Ax3_30)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedFoot(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPaw(a)) | |
| %(Ax3_31)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedFoot(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedClaw(a)) | |
| %(Ax3_32)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHand(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHoof(a)) | |
| %(Ax3_33)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHand(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPaw(a)) | |
| %(Ax3_34)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHand(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedClaw(a)) | |
| %(Ax3_35)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHoof(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPaw(a)) | |
| %(Ax3_36)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedHoof(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedClaw(a)) | |
| %(Ax3_37)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedPaw(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedClaw(a)) | |
| %(Ax3_38)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedArm(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(a)) | |
| %(Ax2)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedArm(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedWing(a)) | |
| %(Ax2_39)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedLeg(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedWing(a)) | |
| %(Ax2_40)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedCardinalBodyPart(a)) | |
| %(Ax1)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedAnatomicalBoundary(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedOrganism(a)) | |
| %(Ax1_41)% | |
| forall a : Thing | |
| . not (http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedCardinalBodyPart(a) | |
| /\ http_u_uontohub_uorg_umonster_ublend_uanimalsDetailed_usharedOrganism(a)) | |
| %(Ax1_42)% |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment