inList |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1973-1975 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3109-3111 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 605-607 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3106-3106 | The number 1 argument of in list is an instance of entity |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3107-3107 | The number 2 argument of in list is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3104-3104 | in list is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3105-3105 | in list is an instance of partial valued relation |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 131-131 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 132-132 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 87-87 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 147-147 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1914-1914 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 39-39 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 103-103 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 157-157 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 186-186 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 106-106 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 86-86 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 298-298 | |
No TPTP formula. May not be expressible in strict first order. | Music.kif 332-332 | album track is a subrelation of in list |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30193-30193 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 132-132 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30192-30192 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30191-30191 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 47-47 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 299-299 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3286-3290 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2005-2017 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1998-2003 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 503-507 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 497-501 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7582-7587 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1975-1980 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1966-1973 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2491-2498 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2483-2489 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1929-1933 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1716-1720 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1784-1788 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1750-1754 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1819-1823 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2677-2682 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1769-1775 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1860-1864 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16921-16929 |
|
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 694-710 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 771-781 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3113-3116 |
|
consequent |
No TPTP formula. May not be expressible in strict first order. | People.kif 357-390 | A year is an instance of the year the yearEAR and the male life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 403-436 | A year is an instance of the year an integer and the female life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 310-342 | A year is an instance of the year an integer and the life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 272-293 | A real number is an average of a list if and only if there exist another list and a positive integer such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all another positive integer
|
No TPTP formula. May not be expressible in strict first order. | Music.kif 280-287 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7596-7611 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4861-4872 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4874-4888 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4946-4956 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4958-4972 |
|
No TPTP formula. May not be expressible in strict first order. | Music.kif 936-946 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2005-2017 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 801-812 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1532-1547 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5369-5374 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 464-468 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2950-2955 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2957-2966 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 574-578 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4854-4859 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4939-4944 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1685-1692 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 509-517 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2940-2948 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 558-562 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |