| No TPTP formula. May not be expressible in strict first order. | Communications.kif 119-119 | Communication satellite is a subclass of artificial satellite |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 120-120 | Communication satellite is a subclass of communication device |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 153-153 | Eutelsat is a subclass of communication satellite |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 157-157 | Inmarsat is a subclass of communication satellite |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 161-161 | Intelsat is a subclass of communication satellite |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 165-165 | Intersputnik is a subclass of communication satellite |
| No TPTP formula. May not be expressible in strict first order. | Communications.kif 169-169 | Orbita is a subclass of communication satellite |
|
|