average |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2284-2286 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5363-5367 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 952-954 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5360-5360 | 域 平均, 1 and List |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5361-5361 | 域 平均, 2 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5358-5358 | 例 平均 and BinaryPredicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5357-5357 | 例 平均 and PartialValuedRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5359-5359 | 例 平均 and SingleValuedRelation |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 228-228 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 227-227 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 226-226 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 9342-9342 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 9341-9341 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1847-1847 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | People.kif 272-293 | RealNumber 是 List 的 average List PositiveInteger 等於 列表長度 List and 列表長度 List 等於 清單順序 List and 1 and 清單順序 List and 1 PositiveInteger
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5369-5374 |
|
consequent |