| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1876-1876 | Child-care service is a subclass of maintaining |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1877-1877 | Child-care service is a subclass of service |
|
|