MultiplicationFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2212-2213 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4703-4705 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 876-877 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4699-4699 | 乘法函数 的 1 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4700-4700 | 乘法函数 的 2 数量 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5294-5294 | 1 是 乘法函数 的单位元 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4695-4695 | 乘法函数 是 结合函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4694-4694 | 乘法函数 是 二元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4696-4696 | 乘法函数 是 交换函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4698-4698 | 乘法函数 是 总值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4701-4701 | 乘法函数 的 range 是 实数 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 680-680 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 682-682 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 413-413 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 196-196 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2130-2130 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 365-365 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 422-422 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 887-887 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 234-234 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 435-435 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 457-457 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 377-377 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 39183-39183 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 681-681 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 39182-39182 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 39181-39181 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 378-378 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2080-2090 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5117-5128 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2165-2176 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2125-2136 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 1107-1115 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 587-597 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 5968-5982 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 5950-5962 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13683-13687 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3912-3919 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3894-3901 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3885-3892 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3903-3910 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 625-631 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19064-19068 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8759-8763 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3844-3848 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13618-13622 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19083-19089 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13668-13672 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13591-13595 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19073-19077 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13605-13611 | 物理 的 measure 是 实数 公吨 若且唯若 那个 物理 的 measure 是 那个 实数 和 2205.0 磅质量 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 378-380 | 物理 的 measure 是 实数 圆周角度 若且唯若 那个 物理 的 measure 是 60.0 和 那个 实数 弧分 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 397-399 | 物理 的 measure 是 实数 弧分 若且唯若 那个 物理 的 measure 是 60.0 和 那个 实数 弧秒 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2092-2106 |
|
No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 204-223 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 659-669 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13566-13575 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13577-13586 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5104-5115 | |
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. | Medicine.kif 5915-5924 | |
No TPTP formula. May not be expressible in strict first order. | Food.kif 2969-2986 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 2993-3011 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 3018-3036 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 2945-2962 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 2851-2869 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5086-5091 | |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3095-3109 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1532-1547 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2178-2196 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2138-2152 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2229-2239 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 538-548 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17906-17931 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 2782-2795 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 402-402 | 实数 弧分 equal 60.0 和 那个 实数 弧秒 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 383-383 | 实数 圆周角度 equal 60.0 和 那个 实数 弧分 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7151-7153 | 实数 amu equal 那个 实数 和 1.6605402E-24 公克 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7173-7175 | 实数 埃 equal 那个 实数 和 1.0E-10 仪表 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7367-7369 | 实数 圆周角度 equal 那个 实数 和 圆周率 和 180.0 弧度 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7353-7355 | 实数 英国热量单位 equal 那个 实数 和 1055.05585262 焦耳 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7425-7427 | 实数 字节 equal 那个 实数 和 8 位元 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7345-7347 | 实数 卡路里 equal 那个 实数 和 4.1868 焦耳 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6780-6782 | 实数 厘米 equal 那个 实数 和 0.01 仪表 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7087-7089 | 实数 一天长度 equal 那个 实数 和 24 小时 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7161-7163 | 实数 电子伏特 equal 那个 实数 和 1.60217733E-19 焦耳 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7405-7407 | 实数 欧元分 equal 那个 实数 和 0.01 欧元 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7186-7188 | 实数 脚长 equal 那个 实数 和 0.3048 仪表 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7095-7097 | 实数 小时 equal 那个 实数 和 60 分钟 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7193-7195 | 实数 英寸 equal 那个 实数 和 0.0254 仪表 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7435-7437 | 实数 千位元 equal 那个 实数 和 1024 字节 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7279-7282 | 实数 公斤 equal 那个 实数 和 1000 公克 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6799-6802 | 实数 公里 equal 那个 实数 和 1000 仪表 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7445-7447 | 实数 兆位元 equal 那个 实数 和 1024 千位元 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7097-7100 | 实数 微米 equal 那个 实数 和 0.0000001 仪表 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7200-7202 | 实数 英里 equal 那个 实数 和 1609.344 仪表 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6789-6792 | 实数 毫米 equal 那个 实数 和 0.001 仪表 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7103-7105 | 实数 分钟 equal 那个 实数 和 60 第二期 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7335-7337 | 实数 磅力 equal 那个 实数 和 4.448222 牛顿 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7296-7298 | 实数 磅质量 equal 那个 实数 和 453.59237 公克 |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |