appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1952-1956 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2878-2885 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 584-588 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2876-2876 | List is a subclass of abstract |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2918-2918 | Null list is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7581-7581 | The range of Amounts fn is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3075-3075 | The range of list concatenate is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2936-2936 | The range of list is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1978-1978 | The range of mean three second wind speed list is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3165-3165 | The range of sub-list function is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Music.kif 49-49 | Album is a subclass of list |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1910-1910 | Consecutive time interval list is a subclass of list |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1697-1697 | Measuring list is a subclass of list |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1765-1765 | Measuring result list is a subclass of list |
No TPTP formula. May not be expressible in strict first order. | Music.kif 1119-1119 | Music charts is a subclass of list |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1800-1800 | Number list is a subclass of list |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2469-2469 | Search results is a subclass of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2904-2904 | Unique list is a subclass of list |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 913-913 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1033-1033 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 589-589 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 119-119 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 122-122 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2274-2274 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 541-541 | |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 124-124 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 156-156 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 610-610 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3272-3272 | The number 1 argument of average function is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3227-3227 | The number 1 argument of first is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3207-3207 | The number 1 argument of last is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3073-3073 | The number 1 argument of list concatenate is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3074-3074 | The number 2 argument of list concatenate is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3015-3015 | The number 1 argument of list length is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2978-2978 | The number 1 argument of list order is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3241-3241 | The number 1 argument of sum of elements is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1664-1664 | The number 1 argument of maximum value is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1487-1487 | The number 1 argument of standard deviation is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3164-3164 | The number 3 argument of sub-list function is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1431-1431 | The number 2 argument of variance average function is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1454-1454 | The number 1 argument of variance function is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5361-5361 | The number 1 argument of average is an instance of list |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1296-1296 | The number 2 argument of command line arguments is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3321-3321 | The number 1 argument of identical list items is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3322-3322 | The number 2 argument of identical list items is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3108-3108 | 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 3121-3121 | The number 1 argument of sub list is an instance of list |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3122-3122 | The number 2 argument of sub list is an instance of list |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 763-763 | The number 2 argument of list of viewed items is an instance of list |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3233-3238 |
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. | Hotel.kif 2035-2053 |
|