member |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1633-1634 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1284-1286 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 216-217 | |
No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 256-258 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1279-1279 | 组员 的 1 数量 是 物理 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1280-1280 | 组员 的 2 数量 是 群体 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1276-1276 | 组员 是 非对称关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1277-1277 | 组员 是 二元谓语 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1278-1278 | 组员 是 非传递关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1282-1282 | 组员 和 元素 是 内部相关 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1281-1281 | 组员 和 实例 是 内部相关 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 153-153 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 154-154 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 97-97 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 182-182 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1925-1925 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 49-49 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 69-69 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 185-185 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 220-220 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 116-116 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 96-96 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 358-358 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2426-2426 | 在组织中关联 是 组员 的 subrelation |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7554-7554 | 小组成员 是 组员 的 subrelation |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16791-16791 | student 是 组员 的 subrelation |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16863-16863 | teacher 是 组员 的 subrelation |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36989-36989 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 154-154 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36988-36988 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36987-36987 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 57-57 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 359-359 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3603-3605 | 物理 是 国际红十字和红新月运动 的 member 若且唯若 那个 物理 是 国际红十字会和红新月会联合会 的 member |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 506-510 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2579-2583 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2659-2663 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3231-3235 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3276-3280 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4043-4047 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3534-3543 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3528-3532 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3545-3555 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3582-3591 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3576-3580 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3593-3603 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 3207-3212 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7562-7569 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 1767-1772 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 972-976 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3223-3227 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23494-23504 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3202-3215 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3239-3259 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22348-22356 | |
No TPTP formula. May not be expressible in strict first order. | Military.kif 108-122 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 145-160 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 139-143 |
|
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. | People.kif 676-678 | 信仰团体 的 member 是 客体 的 attribute 若且唯若 那个 客体 是 那个 信仰团体 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 702-704 | 不可知 是 客体 的 attribute 若且唯若 那个 客体 是 不可知论 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1347-1349 | Ahmadiyya穆斯林 是 客体 的 attribute 若且唯若 那个 客体 是 ahmadiyya教派 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1225-1227 | 英国国教 是 客体 的 attribute 若且唯若 那个 客体 是 英国国教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1233-1235 | 英国国教 是 客体 的 attribute 若且唯若 那个 客体 是 英格兰教堂 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 720-722 | 无神论者 是 客体 的 attribute 若且唯若 那个 客体 是 无神论 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 757-759 | 巴哈 是 客体 的 attribute 若且唯若 那个 客体 是 巴哈主义 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 769-771 | 佛教徒 是 客体 的 attribute 若且唯若 那个 客体 是 佛教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1306-1308 | 儒 是 客体 的 attribute 若且唯若 那个 客体 是 儒 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1361-1363 | 德鲁兹穆斯林 是 客体 的 attribute 若且唯若 那个 客体 是 德鲁兹教派 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1247-1249 | 东正教基督教 是 客体 的 attribute 若且唯若 那个 客体 是 东正教基督教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1318-1320 | 印度教 是 客体 的 attribute 若且唯若 那个 客体 是 印度教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1411-1413 | 耆那教 是 客体 的 attribute 若且唯若 那个 客体 是 耆那教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1330-1332 | 穆斯林 是 客体 的 attribute 若且唯若 那个 客体 是 伊斯兰教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1457-1459 | Neopaganismist 是 客体 的 attribute 若且唯若 那个 客体 是 neopaganism 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1261-1263 | 新教 是 客体 的 attribute 若且唯若 那个 客体 是 新教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1428-1430 | 宗教的犹太人 是 客体 的 attribute 若且唯若 那个 客体 是 犹太教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1283-1285 | 罗马天主教徒 是 客体 的 attribute 若且唯若 那个 客体 是 罗马天主教会 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1275-1277 | 罗马天主教徒 是 客体 的 attribute 若且唯若 那个 客体 是 罗马天主教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1377-1379 | 什叶派穆斯林 是 客体 的 attribute 若且唯若 那个 客体 是 什叶派 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1472-1474 | 神道教 是 客体 的 attribute 若且唯若 那个 客体 是 神道 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1487-1489 | 锡克教 是 客体 的 attribute 若且唯若 那个 客体 是 锡克教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1396-1398 | 逊尼派穆斯林 是 客体 的 attribute 若且唯若 那个 客体 是 逊尼派 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1502-1504 | 道 是 客体 的 attribute 若且唯若 那个 客体 是 道教 的 member |
No TPTP formula. May not be expressible in strict first order. | People.kif 1517-1519 | 拜火教 是 客体 的 attribute 若且唯若 那个 客体 是 拜火教 的 member |
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. | Media.kif 1970-1978 | 有存在 时距 这样 那个 时距 是 时距 的 instance 和 那个 时距 finishes了才到 JesusOfNazareth 出现 的 time 和 那个 时距 starts了才到 TwelveApostles 出现 的 time 和 对所有 实体
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 3219-3219 | 丹麦 不 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3220-3220 | 瑞典 不 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3221-3221 | 英国 不 是 欧洲货币联盟 的 member |
appearance as argument number 0 |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3199-3199 | 奥地利 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2618-2618 | 贝克岛 是 UnitedStatesMinorOutlyingIslands 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2903-2903 | 比利时 是 比荷卢经济联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3200-3200 | 比利时 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3201-3201 | 塞浦路斯 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3202-3202 | 爱沙尼亚 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3203-3203 | 芬兰 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3204-3204 | 法国 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3205-3205 | 德国 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3206-3206 | 希腊 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2619-2619 | Howland岛 是 UnitedStatesMinorOutlyingIslands 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3207-3207 | 爱尔兰 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3208-3208 | 意大利 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2620-2620 | 贾维斯岛 是 UnitedStatesMinorOutlyingIslands 的 member |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2625-2625 | 约翰斯顿环礁 是 UnitedStatesMinorOutlyingIslands 的 member |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2621-2621 | 金曼礁 是 UnitedStatesMinorOutlyingIslands 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3209-3209 | 拉脱维亚 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3210-3210 | 立陶宛 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2905-2905 | 卢森堡 是 比荷卢经济联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3211-3211 | 卢森堡 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3212-3212 | 马耳他 是 欧洲货币联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2626-2626 | 中途岛屿 是 UnitedStatesMinorOutlyingIslands 的 member |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2622-2622 | 纳瓦萨岛 是 UnitedStatesMinorOutlyingIslands 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2904-2904 | 荷兰 是 比荷卢经济联盟 的 member |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3213-3213 | 荷兰 是 欧洲货币联盟 的 member |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |