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 | The number 1 argument of member is an instance of physical |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1280-1280 | The number 2 argument of member is an instance of collection |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1276-1276 | member is an instance of asymmetric relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1277-1277 | member is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1278-1278 | member is an instance of intransitive relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1282-1282 | member is internally related to element |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1281-1281 | member is internally related to instance |
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 | associate in organization is a subrelation of member |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7526-7526 | group member is a subrelation of member |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16763-16763 | student is a subrelation of member |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16835-16835 | teacher is a subrelation of member |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37001-37001 | |
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 37000-37000 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 36999-36999 | |
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 | A physical is a member of international red cross and red crescent movement if and only if the physical is a member of international federation of red cross and red crescent societies |
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 2587-2591 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2667-2671 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3239-3243 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3284-3288 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4051-4055 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3542-3551 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3536-3540 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3553-3563 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3590-3599 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3584-3588 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3601-3611 |
|
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 7534-7541 |
|
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 23443-23453 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3210-3223 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3247-3267 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22297-22305 |
|
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 702-704 | A member of a belief group is an attribute of an object if and only if the object is a member of the belief group |
No TPTP formula. May not be expressible in strict first order. | People.kif 728-730 | Agnostic is an attribute of an object if and only if the object is a member of agnosticism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1373-1375 | Ahmadiyya muslim is an attribute of an object if and only if the object is a member of ahmadiyya sect |
No TPTP formula. May not be expressible in strict first order. | People.kif 1251-1253 | Anglican is an attribute of an object if and only if the object is a member of anglicanism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1259-1261 | Anglican is an attribute of an object if and only if the object is a member of church of england |
No TPTP formula. May not be expressible in strict first order. | People.kif 746-748 | Atheist is an attribute of an object if and only if the object is a member of atheism |
No TPTP formula. May not be expressible in strict first order. | People.kif 783-785 | Bahai is an attribute of an object if and only if the object is a member of bahaism |
No TPTP formula. May not be expressible in strict first order. | People.kif 795-797 | Buddhist is an attribute of an object if and only if the object is a member of buddhism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1332-1334 | Confucianist is an attribute of an object if and only if the object is a member of confucianism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1387-1389 | Druze muslim is an attribute of an object if and only if the object is a member of druze sect |
No TPTP formula. May not be expressible in strict first order. | People.kif 1273-1275 | Eastern orthodox christian is an attribute of an object if and only if the object is a member of eastern orthodox christianity |
No TPTP formula. May not be expressible in strict first order. | People.kif 1344-1346 | Hindu is an attribute of an object if and only if the object is a member of hinduism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1437-1439 | Jain is an attribute of an object if and only if the object is a member of jainism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1356-1358 | Muslim is an attribute of an object if and only if the object is a member of islam |
No TPTP formula. May not be expressible in strict first order. | People.kif 1483-1485 | Neopaganismist is an attribute of an object if and only if the object is a member of neopaganism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1287-1289 | Protestant is an attribute of an object if and only if the object is a member of protestantism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1454-1456 | Religious jew is an attribute of an object if and only if the object is a member of judaism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1309-1311 | Roman catholic is an attribute of an object if and only if the object is a member of roman catholic church |
No TPTP formula. May not be expressible in strict first order. | People.kif 1301-1303 | Roman catholic is an attribute of an object if and only if the object is a member of roman catholicism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1403-1405 | Shia muslim is an attribute of an object if and only if the object is a member of shiite sect |
No TPTP formula. May not be expressible in strict first order. | People.kif 1498-1500 | Shintoist is an attribute of an object if and only if the object is a member of shinto |
No TPTP formula. May not be expressible in strict first order. | People.kif 1513-1515 | Sikh is an attribute of an object if and only if the object is a member of sikhism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1422-1424 | Sunni muslim is an attribute of an object if and only if the object is a member of sunni sect |
No TPTP formula. May not be expressible in strict first order. | People.kif 1528-1530 | Taoist is an attribute of an object if and only if the object is a member of taoism |
No TPTP formula. May not be expressible in strict first order. | People.kif 1543-1545 | Zoroastrian is an attribute of an object if and only if the object is a member of zoroastrianism |
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 | There exists a time interval such that the time interval is an instance of time interval and the time interval finishes the time of existence of Jesus of Nazareth and the time interval starts the time of existence of Twelve apostles and for all an entity
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 3219-3219 | Denmark is not a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3220-3220 | Sweden is not a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3221-3221 | United kingdom is not a member of european monetary union |
appearance as argument number 0 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3199-3199 | Austria is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2618-2618 | Baker island is a member of United states minor outlying islands |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2903-2903 | Belgium is a member of benelux economic union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3200-3200 | Belgium is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3201-3201 | Cyprus is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3202-3202 | Estonia is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3203-3203 | Finland is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3204-3204 | France is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3205-3205 | Germany is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3206-3206 | Greece is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2619-2619 | Howland island is a member of United states minor outlying islands |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3207-3207 | Ireland is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3208-3208 | Italy is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2620-2620 | Jarvis island is a member of United states minor outlying islands |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2625-2625 | Johnston atoll is a member of United states minor outlying islands |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2621-2621 | Kingman reef is a member of United states minor outlying islands |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3209-3209 | Latvia is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3210-3210 | Lithuania is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2905-2905 | Luxembourg is a member of benelux economic union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3211-3211 | Luxembourg is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3212-3212 | Malta is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2626-2626 | Midway islands is a member of United states minor outlying islands |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2622-2622 | Navassa island is a member of United states minor outlying islands |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2904-2904 | Netherlands is a member of benelux economic union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3213-3213 | Netherlands is a member of european monetary union |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
![]() |
![]() |