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 131-133 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 129-129 | The number 1 argument of subclass is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 130-130 | The number 2 argument of subclass is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 127-127 | subclass is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 128-128 | 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. | Merge.kif 5291-5291 | subset is a subrelation of subclass |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55683-55683 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 320-320 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55682-55682 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55681-55681 |
antecedent |
![]() |
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30754-30761 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 219-225 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2933-2938 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 242-248 |
|
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. | Merge.kif 1720-1728 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 215-219 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 204-208 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 178-182 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 225-229 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12613-12617 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16324-16328 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3320-3324 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29408-29438 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 322-328 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 337-341 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 349-355 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20353-20360 |
|
No TPTP formula. May not be expressible in strict first order. | Languages.kif 14705-14709 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 1279-1281 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 1306-1308 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2878-2883 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 1384-1387 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 1372-1375 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 1362-1365 |
|
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. | Cars.kif 5112-5115 | There exists an agent such that the agent is a subclass of tool box and the maker of Sortimo Corporation is the agent |
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. | Mid-level-ontology.kif 25719-25719 | Ac power source is a subclass of power source |
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. | Mid-level-ontology.kif 24900-24900 | Am / fm alarm clock is a subclass of alarm clock |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24901-24901 | Am / fm alarm clock is a subclass of radio receiver |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 293-293 | AM radio station is a subclass of radio station |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 236-236 | AM radio system is a subclass of radio system |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3176-3176 | AOC number is a subclass of symbolic string |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
![]() |
![]() |