FirstFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3228-3230 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3226-3226 | 第一 的 1 数量 是 串列 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3225-3225 | 第一 是 一元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3227-3227 | 第一 的 range 是 实体 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 1012-1012 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 1011-1011 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 1010-1010 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23954-23954 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23953-23953 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 23952-23952 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 783-797 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3258-3268 | |
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. | Merge.kif 3232-3237 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1878-1886 |