| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15825-15825 | 子類 住宅樓 and Building |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15826-15826 | 子類 住宅樓 and 住宅 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6935-6935 | 子類 公寓樓 and 住宅樓 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6950-6950 | 子類 公寓大樓 and 住宅樓 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6977-6977 | 子類 宿舍 and 住宅樓 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15791-15791 | 子類 屋 and 住宅樓 |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 77-77 | 子類 HotelBuilding and 住宅樓 |
|
|