SubtractionFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2216-2219 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4731-4735 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 880-883 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4727-4727 | O argumento numero 1 de SubtractionFn e' uma instancia de Numero Real |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4728-4728 | O argumento numero 2 de SubtractionFn e' uma instancia de Numero Real |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5297-5297 | 0 e' um elemento identificador de SubtractionFn |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4724-4724 | SubtractionFn e' uma instancia de Funcao Binaria |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4726-4726 | SubtractionFn e' uma instancia de Relacao Total |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4729-4729 | O contra-dominio de SubtractionFn e' uma instancia de Numero Real |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 684-684 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 686-686 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 415-415 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 285-285 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2132-2132 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 367-367 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 424-424 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 891-891 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 322-322 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 437-437 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 459-459 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 477-477 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55856-55856 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 685-685 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55855-55855 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55854-55854 |
antecedent |
consequent |
statement |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7013-7015 | Numero Real CelsiusDegree(s) e' igual a ( Numero Real + 32.0) + 1.8 FahrenheitDegree(s) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7009-7011 | Numero Real CelsiusDegree(s) e' igual a ( Numero Real + 273.15) KelvinDegree(s) |
No TPTP formula. May not be expressible in strict first order. | Military.kif 924-937 | ReachingMilitaryAgeAnnuallyMaleFn Area Geopolitica and Ano e' igual a o numero de instancias dentro de a classe descrita por Sequencia Simbolica |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4737-4738 | Numero Inteiro ( Numero Inteiro+2) e' igual a ( Numero Inteiro + 1) |