| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25062-25062 | 子類 移動手機 and 接收器設備 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25063-25063 | 子類 移動手機 and 電話 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29570-29570 | 子類 SmartPhone and 移動手機 |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 627-627 | 子類 iPhone and 移動手機 |
|
|