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 | O argumento numero 1 de ListOrderFn e' uma instancia de Lista |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2978-2978 | O argumento numero 2 de ListOrderFn e' uma instancia de Inteiro positivo |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2975-2975 | ListOrderFn e' uma instancia de Funcao Binaria |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2976-2976 | ListOrderFn e' uma instancia de Relacao Parcial |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2979-2979 | O contra-dominio de ListOrderFn e' uma instancia de Entidade |
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 | average Lista and Numero Real Lista Inteiro positivo comprimento de Lista e' igual a comprimento de Lista 1th elemento de Lista e' igual a 1th elemento de Lista Inteiro positivo
|
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 Entidade comprimento de (@ROW + Entidade)th elemento de (@ROW + Entidade) e' igual a Entidade |