orientation |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3786-3788 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16915-16919 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16912-16912 | 定向 的 1 数量 是 客体 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16913-16913 | 定向 的 2 数量 是 客体 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16914-16914 | 定向 的 3 数量 是 位置属性 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16910-16910 | 定向 是 空间关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16911-16911 | 定向 是 三元谓语 的 instance |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 586-586 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 590-590 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 351-351 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 204-204 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2098-2098 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 303-303 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 359-359 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 767-767 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 242-242 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 373-373 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 389-389 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 390-390 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 587-587 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 42582-42582 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 42581-42581 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 42580-42580 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 391-391 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9119-9122 | 客体 在 另一个 客体 的 外 若且唯若 那个 客体 不 是 partlyLocated 在 那个 另外 客体 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17103-17107 | 客体 在 另一个 客体 的 邻 若且唯若 那个 客体 在 那个 另外 客体 的 近 或 那个 客体 和 那个 另外 客体 是 connected |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17091-17095 | 客体 在 另一个 客体 的 下面 若且唯若 那个 另外 客体 在 那个 客体 的 上 或 那个 另外 客体 在 那个 客体 的 以上 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17028-17030 | 客体 在 另一个 客体 的 东 若且唯若 那个 另外 客体 在 那个 客体 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17045-17047 | 客体 在 另一个 客体 的 横 若且唯若 那个 另外 客体 在 那个 客体 的 横 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17018-17020 | 客体 在 另一个 客体 的 北 若且唯若 那个 另外 客体 在 那个 客体 的 南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3653-3657 | 客体 在 另一个 客体 的 东北 若且唯若 那个 客体 在 那个 另外 客体 的 北 和 那个 客体 在 那个 另外 客体 的 东 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3688-3692 | 客体 在 另一个 客体 的 西北 若且唯若 那个 客体 在 那个 另外 客体 的 北 和 那个 客体 在 那个 另外 客体 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17124-17126 | 客体 在 另一个 客体 的 右 若且唯若 那个 另外 客体 在 那个 客体 的 左 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3664-3668 | 客体 在 另一个 客体 的 东南 若且唯若 那个 客体 在 那个 另外 客体 的 南 和 那个 客体 在 那个 另外 客体 的 东 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3676-3680 | 客体 在 另一个 客体 的 西南 若且唯若 那个 客体 在 那个 另外 客体 的 南 和 那个 客体 在 那个 另外 客体 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17036-17038 | 客体 在 另一个 客体 的 垂直 若且唯若 那个 另外 客体 在 那个 客体 的 垂直 |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1838-1860 |
|
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1862-1884 |
|
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1799-1807 | |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1814-1821 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 44-59 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6126-6131 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17004-17009 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2537-2550 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2566-2580 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17065-17069 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17054-17058 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6152-6161 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 11352-11357 | |
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. | Geography.kif 3731-3733 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3755-3757 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 东南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3739-3741 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3759-3761 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 西南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3743-3745 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3763-3765 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 西北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3747-3749 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3751-3753 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 东北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3735-3737 | 客体 对于 %3 courseWRT 实际北 若且唯若 那个 客体 在 另一个 客体 的 东 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17103-17107 | 客体 在 另一个 客体 的 邻 若且唯若 那个 客体 在 那个 另外 客体 的 近 或 那个 客体 和 那个 另外 客体 是 connected |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17091-17095 | 客体 在 另一个 客体 的 下面 若且唯若 那个 另外 客体 在 那个 客体 的 上 或 那个 另外 客体 在 那个 客体 的 以上 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17028-17030 | 客体 在 另一个 客体 的 东 若且唯若 那个 另外 客体 在 那个 客体 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17045-17047 | 客体 在 另一个 客体 的 横 若且唯若 那个 另外 客体 在 那个 客体 的 横 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17018-17020 | 客体 在 另一个 客体 的 北 若且唯若 那个 另外 客体 在 那个 客体 的 南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3653-3657 | 客体 在 另一个 客体 的 东北 若且唯若 那个 客体 在 那个 另外 客体 的 北 和 那个 客体 在 那个 另外 客体 的 东 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3688-3692 | 客体 在 另一个 客体 的 西北 若且唯若 那个 客体 在 那个 另外 客体 的 北 和 那个 客体 在 那个 另外 客体 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17124-17126 | 客体 在 另一个 客体 的 右 若且唯若 那个 另外 客体 在 那个 客体 的 左 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3664-3668 | 客体 在 另一个 客体 的 东南 若且唯若 那个 客体 在 那个 另外 客体 的 南 和 那个 客体 在 那个 另外 客体 的 东 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3676-3680 | 客体 在 另一个 客体 的 西南 若且唯若 那个 客体 在 那个 另外 客体 的 南 和 那个 客体 在 那个 另外 客体 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17036-17038 | 客体 在 另一个 客体 的 垂直 若且唯若 那个 另外 客体 在 那个 客体 的 垂直 |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 939-944 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7714-7716 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2693-2704 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2665-2676 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4078-4095 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 0 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 282-282 | 非洲 在 北美 的 东南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 280-280 | 非洲 在 南美洲 的 东北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 281-281 | 亚洲 在 大洋洲 的 西北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 290-290 | 加勒比地区 在 北美 的 南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 289-289 | 加勒比地区 在 南美洲 的 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 275-275 | 欧洲 在 非洲 的 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 276-276 | 欧洲 在 亚洲 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 277-277 | 欧洲 在 北美 的 东 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 283-283 | 欧洲 在 南美洲 的 东北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6966-6966 | 爱尔兰 在 Wales 的 西方 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6965-6965 | 人岛 在 北爱尔兰 的 东 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 288-288 | 中美洲 在 北美 的 南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 287-287 | 中美洲 在 南美洲 的 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 286-286 | 中东地区 在 非洲 的 东北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 285-285 | 中东地区 在 亚洲 的 西南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 279-279 | 北美 在 亚洲 的 东 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 278-278 | 北美 在 南美洲 的 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6954-6954 | 北爱尔兰 在 England 的 西北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6953-6953 | 北爱尔兰 在 苏格兰 的 西南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6963-6963 | 北爱尔兰 在 Wales 的 西北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 284-284 | 大洋洲 在 北美 的 西南 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6951-6951 | 苏格兰 在 England 的 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6964-6964 | 苏格兰 在 Wales 的 北 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6961-6961 | Wales 在 England 的 西方 |