ListOrderFn |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1964-1966 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2875-2878 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2871-2871 | 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 2872-2872 | The number 2 argument of list order is an instance of positive integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2869-2869 | List order is an instance of binary function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2870-2870 | List order is an instance of partial valued relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2873-2873 | The range of list order is an instance of entity |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 263-263 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 271-271 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 264-264 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34621-34621 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34620-34620 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34619-34619 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17110-17115 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17094-17099 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17127-17132 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3135-3139 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2108-2115 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2095-2105 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 427-431 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 467-474 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17077-17082 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17060-17065 |
|
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 692-708 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 987-1005 |
|
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2977-2993 | A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2116-2133 | A relation is an instance of total valued relation and the relation is an instance of predicate if and only if there exists a positive integer such that the relation is an instance of relation and the relation %&has the positive integer argument(s) and
|
No TPTP formula. May not be expressible in strict first order. | People.kif 285-306 | A real number is an average of a list if and only if there exists another list 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 a positive integer
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3105-3110 | The last of a list is equal to an entity if and only if there exists a positive integer such that length of the list is equal to the positive integer and the positive integerth element of the list is equal to the entity |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2892-2897 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2899-2904 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3141-3145 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3072-3081 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3083-3095 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1092-1103 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1060-1072 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2095-2105 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2077-2092 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2134-2147 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3120-3125 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2595-2611 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2205-2218 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2170-2183 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 476-486 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 294-301 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2123-2131 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 521-533 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 535-545 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3006-3009 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2804-2809 |
|
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. | Merge.kif 2936-2940 | For all @ROW and another entity length of (@ROW and the other entity)th element of (@ROW and the other entity) is equal to the other entity |
![]() |
![]() |