No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 21751-21751 |
伏击 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13398-13398 |
攻击 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Sports.kif 757-757 |
棒球局 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Sports.kif 684-684 |
棒球演练 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 21771-21771 |
封锁 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17102-17102 |
捕 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13420-13420 |
防守机动 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
MilitaryProcesses.kif 390-390 |
直接行动活动 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Sports.kif 815-815 |
足球演练 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17020-17020 |
游戏镜头 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Sports.kif 938-938 |
高尔夫演习 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 21797-21797 |
军事演习 是 竞争招数 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1215-1215 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1651-1651 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 893-893 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 426-426 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 429-429 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2577-2577 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 845-845 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 431-431 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 465-465 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 914-914 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 430-430 |
|