| No TPTP formula. May not be expressible in strict first order. | Communications.kif 119-119 | 通信卫星 是 人造卫星 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 120-120 | 通信卫星 是 通讯设备 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 153-153 | 欧洲通信卫星 是 通信卫星 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 157-157 | 国际海事卫星组织 是 通信卫星 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 161-161 | INTELSAT 是 通信卫星 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 165-165 | 空间通信 是 通信卫星 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 169-169 | 欧比特 是 通信卫星 的 subclass |
|
|