DivisionFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2220-2223 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4746-4750 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 884-887 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4742-4742 | 域 部, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4743-4743 | 域 部, 2 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5297-5297 | 身份元素 部 and 1 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4739-4739 | 例 部 and BinaryFunction |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4741-4741 | 例 部 and PartialValuedRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4744-4744 | 範圍 部 and RealNumber |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 686-686 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 688-688 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 416-416 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 80-80 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2133-2133 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 368-368 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 425-425 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 893-893 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 120-120 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 438-438 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 460-460 | |
No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 114-114 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19992-19992 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 687-687 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19991-19991 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 19990-19990 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 176-176 |
antecedent |
consequent |
statement |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7367-7369 | 等於 測量 RealNumber and 圓周角度 and 測量 乘法 RealNumber and 部 Pi and 180.0 and 弧度 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7012-7014 | 等於 測量 RealNumber and 攝氏度 and 測量 部 減法 RealNumber and 32.0 and 1.8 and 華氏度 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7239-7241 | 等於 測量 RealNumber and 杯子 and 測量 部 RealNumber and 2 and 品脫 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7248-7250 | 等於 測量 RealNumber and 盎司 and 測量 部 RealNumber and 8 and 杯子 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7230-7232 | 等於 測量 RealNumber and 品脫 and 測量 部 RealNumber and 2 and 夸脫 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7221-7223 | 等於 測量 RealNumber and 夸脫 and 測量 部 RealNumber and 4 and 美國加侖 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13333-13336 | RealNumber 等於 測量 RealNumber and OunceMass and 測量 部 RealNumber and 16.0 and 磅質量 |