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 2390-2390 | associate in organization is a subrelation of member |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7581-7581 | group member is a subrelation of member |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16818-16818 | student is a subrelation of member |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16890-16890 | teacher is a subrelation of member |
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 3567-3569 | 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 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 3189-3194 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7589-7596 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1731-1736 |
|
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 3187-3191 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23546-23556 |
|
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 22400-22408 |
|
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 | 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 702-704 | 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 1347-1349 | 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 1225-1227 | 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 1233-1235 | 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 720-722 | 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 757-759 | 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 769-771 | 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 1306-1308 | 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 1361-1363 | 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 1247-1249 | 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 1318-1320 | 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 1411-1413 | 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 1330-1332 | 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 1457-1459 | 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 1261-1263 | 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 1428-1430 | 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 1283-1285 | 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 1275-1277 | 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 1377-1379 | 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 1472-1474 | 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 1487-1489 | 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 1396-1398 | 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 1502-1504 | 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 1517-1519 | 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 3183-3183 | Denmark is not a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3184-3184 | Sweden is not a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3185-3185 | 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 3163-3163 | 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 2867-2867 | Belgium is a member of benelux economic union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3164-3164 | Belgium is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3165-3165 | Cyprus is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3166-3166 | Estonia is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3167-3167 | Finland is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3168-3168 | France is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3169-3169 | Germany is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3170-3170 | 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 3171-3171 | Ireland is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3172-3172 | 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 3173-3173 | Latvia is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3174-3174 | Lithuania is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2869-2869 | Luxembourg is a member of benelux economic union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3175-3175 | Luxembourg is a member of european monetary union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3176-3176 | 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 2868-2868 | Netherlands is a member of benelux economic union |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3177-3177 | Netherlands is a member of european monetary union |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |