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. | Merge.kif 131-131 | 子类别 的 1 数量 是 类 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 132-132 | 子类别 的 2 数量 是 类 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 129-129 | 子类别 是 二元谓语 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 130-130 | 子类别 是 偏序关系 的 instance |
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 5299-5299 | 子集 是 子类别 的 subrelation |
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 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1186-1201 |
|
No TPTP formula. May not be expressible in strict first order. | Biography.kif 500-510 | |
No TPTP formula. May not be expressible in strict first order. | WMD.kif 789-793 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 969-973 | |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 48-56 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 617-623 | |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 504-520 |
|
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 522-538 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13066-13077 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13035-13046 | |
No TPTP formula. May not be expressible in strict first order. | WMD.kif 950-954 | |
No TPTP formula. May not be expressible in strict first order. | WMD.kif 956-960 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2123-2132 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2167-2176 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2213-2222 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1991-2000 | |
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. | Mid-level-ontology.kif 17836-17841 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2288-2297 | |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 346-361 |
|
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 364-378 |
|
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 811-832 |
|
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 294-313 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 1886-1890 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 1874-1878 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30884-30891 | |
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. | Merge.kif 221-227 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2941-2946 | |
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. | Merge.kif 1728-1736 | |
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. | Mid-level-ontology.kif 9207-9220 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16399-16403 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3328-3332 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29534-29564 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 324-330 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 339-343 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 351-357 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20440-20447 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20493-20505 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20470-20484 | |
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 2886-2891 | |
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 | 有存在 施事体 这样 那个 施事体 是 HandToolBox 的 subclass 和 manufacturer SortimoCorp and 那个 施事体 |
appearance as argument number 0 |
![]() |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1170-1170 | AAM 是 空袭导弹 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1169-1169 | AAM 是 空中发射导弹 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1171-1171 | AAM 是 导弹 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1647-1647 | AAV 是 两栖车辆 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1646-1646 | AAV 是 军车 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1648-1648 | AAV 是 乘用车 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1649-1649 | AAV 是 动力车辆 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25834-25834 | ACPowerSource 是 能量源 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1123-1123 | AG m 是 空中发射导弹 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1124-1124 | AG m 是 地面攻击导弹 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1203-1203 | AG m114 是 AG m 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1205-1205 | AG m114 是 反装甲武器 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1204-1204 | AG m114 是 束骑导弹 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1136-1136 | AG m65 是 AG m 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1138-1138 | AG m65 是 反装甲武器 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1137-1137 | AG m65 是 红外导弹 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1889-1889 | A h1 是 直升机 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1890-1890 | A h1 是 军车 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1177-1177 | AI m9 是 AAM 的 subclass |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1178-1178 | AI m9 是 红外导弹 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25017-25017 | AMFMAlarmClock 是 AlarmClock 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25018-25018 | AMFMAlarmClock 是 无线电接收器 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 293-293 | AM广播电台 是 广播电台 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 236-236 | AM无线电系统 是 无线电系统 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3168-3168 | AOCnumber 是 符号串 的 subclass |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
![]() |
![]() |