subclass |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1371-1373 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 133-135 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 27-29 | |
No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 28-30 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 131-131 | The number 1 argument of subclass is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 132-132 | The number 2 argument of subclass is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 129-129 | subclass is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18557-18557 | subclass is an instance of ClosedWorldPredicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 130-130 | subclass is an instance of partial ordering relation |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 319-319 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 324-324 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 182-182 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 271-271 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2002-2002 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 134-134 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 175-175 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 419-419 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 308-308 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 202-202 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 192-192 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 463-463 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21629-21629 | sub field is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55739-55739 | sub field is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 320-320 | sub field is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55738-55738 | sub field is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55737-55737 | sub field is a subrelation of subclass |
antecedent |
consequent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31685-31692 |
|
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1478-1491 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24556-24566 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 221-227 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3006-3011 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 244-250 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 195-200 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5060-5065 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4647-4658 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5373-5380 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5147-5151 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5350-5359 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1779-1787 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3955-3960 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4078-4083 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4108-4113 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12070-12082 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4019-4024 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4049-4054 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 3987-3992 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4063-4068 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5600-5608 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18374-18382 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3508-3537 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 219-223 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
No TPTP formula. May not be expressible in strict first order. | Military.kif 886-897 | The fit for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 5170-5173 | There exists a kind of object such that a kind of object is a subclass of tool box and the maker of the kind of object is Sortimo Corporation |
appearance as argument number 0 |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1170-1170 | Air_to_air missile is a subclass of air attack missile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1169-1169 | Air_to_air missile is a subclass of air launch missile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1171-1171 | Air_to_air missile is a subclass of guided missile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1647-1647 | Amphibious Assault Vehicle is a subclass of amphibious vehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1646-1646 | Amphibious Assault Vehicle is a subclass of military vehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1648-1648 | Amphibious Assault Vehicle is a subclass of passenger vehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1649-1649 | Amphibious Assault Vehicle is a subclass of powered vehicle |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 778-778 | A branch of dorsal primary division of suboccipital nerve is a subclass of nerve |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26651-26651 | Ac power source is a subclass of power source |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3281-3281 | Attention deficit hyperactivity disorder is a subclass of psychological dysfunction |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1123-1123 | AG m is a subclass of air launch missile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1124-1124 | AG m is a subclass of ground attack missile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1203-1203 | AG m114 is a subclass of AG m |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1205-1205 | AG m114 is a subclass of anti armor weapon |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1204-1204 | AG m114 is a subclass of beam ridingG missile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1136-1136 | AG m65 is a subclass of AG m |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1138-1138 | AG m65 is a subclass of anti armor weapon |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1137-1137 | AG m65 is a subclass of infra redG missile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1889-1889 | A h1 is a subclass of helicopter |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1890-1890 | A h1 is a subclass of military vehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1177-1177 | AI m9 is a subclass of air_to_air missile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1178-1178 | AI m9 is a subclass of infra redG missile |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2130-2130 | M113A4 Armored Medical Evacuation Vehicle is a subclass of ambulance |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2129-2129 | M113A4 Armored Medical Evacuation Vehicle is a subclass of land vehicle |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2128-2128 | M113A4 Armored Medical Evacuation Vehicle is a subclass of military vehicle |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |