ListFn |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1962-1963 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2831-2832 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2827-2827 | The number 1 argument of list is an instance of entity |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2825-2825 | List is an instance of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2826-2826 | List is an instance of variable arity relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2829-2829 | The range of list is an instance of list |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 261-261 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 269-269 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34609-34609 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 262-262 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34608-34608 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34607-34607 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 470-474 | |
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. | 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. | Merge.kif 505-509 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 499-503 |
|
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 2583-2588 |
|
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. | Merge.kif 15776-15784 |
|
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 692-708 |
|
consequent |
![]() |
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. | 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 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. | 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. | 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 2942-2949 |
|
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 476-486 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2844-2849 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2851-2860 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 575-579 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4671-4676 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4678-4683 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4685-4693 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4744-4749 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4751-4756 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4758-4766 |
|
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 |
|
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 2931-2934 | For all @ROW and another entity length of (@ROW and the other entity) is equal to (length of (@ROW)+1) |
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 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3198-3199 | For all @ROW and another entity (@ROW) starts (@ROW and the other entity) |
![]() |
![]() |