|
|
   Message
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2397-2399 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6211-6214 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1078-1080 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6209-6209 | CompositeUnitOfMeasure 是 函数量 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6208-6208 | CompositeUnitOfMeasure 是 测量单位 的 subclass |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6721-6721 | 安培 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7041-7041 | 贝克勒尔 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 238-238 | 每秒位数 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7350-7350 | 英国热量单位 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7342-7342 | 卡路里 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6760-6760 | 坎德拉 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6913-6913 | 库仑 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7156-7156 | 电子伏特 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6938-6938 | 法拉 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7055-7055 | 戈瑞 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6991-6991 | 亨利 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6899-6899 | 马力 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 254-254 | InstructionsPerSecond 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6880-6880 | 焦耳 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2000-2000 | 千瓦时 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3924-3924 | 结速度单位 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7019-7019 | 流明 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7029-7029 | 勒克司 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 812-812 | 每公斤微克 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 1683-1683 | 英里每小時 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6862-6862 | 牛顿 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6949-6949 | 欧姆 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 246-246 | 每秒数据包 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6871-6871 | 帕斯卡 是 CompositeUnitOfMeasure 的 instance |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7330-7330 | 磅力 是 CompositeUnitOfMeasure 的 instance |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13563-13572 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13593-13602 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13604-13613 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13532-13541 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6456-6460 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6226-6230 | |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1718-1736 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6456-6460 |
|
|
|
|