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 2981-2984 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 596-598 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2977-2977 | 域 清單順序, 1 and List |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2978-2978 | 域 清單順序, 2 and PositiveInteger |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2975-2975 | 例 清單順序 and BinaryFunction |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2976-2976 | 例 清單順序 and PartialValuedRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2979-2979 | 範圍 清單順序 and 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 268-268 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 150-150 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 169-169 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1978-1978 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 102-102 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 159-159 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 338-338 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 207-207 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 169-169 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 156-156 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 337-337 | |
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 34697-34697 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34696-34696 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34695-34695 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 108-108 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 338-338 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 476-484 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18446-18451 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18429-18434 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18463-18468 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3219-3223 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1838-1845 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2106-2113 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2093-2103 | |
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. | Weather.kif 1935-1944 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1806-1811 |
|
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 694-710 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 799-817 |
|
consequent |
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 2998-3003 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3005-3010 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3252-3256 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 295-302 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3083-3102 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3179-3188 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3190-3202 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1486-1497 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1453-1465 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2093-2103 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2075-2090 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2137-2150 | |
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. | UXExperimentalTerms.kif 2388-2404 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2210-2223 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2174-2187 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3212-3217 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2125-2134 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 519-531 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3113-3116 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2910-2915 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2198-2207 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 2161-2170 |
statement |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3042-3046 | @ROW Entity 等於 清單順序 名單 @ROW and Entity and 列表長度 名單 @ROW and Entity and Entity |