| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1360-1360 | Internet access point is a subclass of device |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1373-1373 | Modem is a subclass of internet access point |
|
|