| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11864-11864 | 服务 是 社交 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | TransportDetail.kif 143-143 | ValetParking 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3335-3335 | TransportationService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11875-11875 | 商业服务 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1780-1780 | LaundryService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1804-1804 | DryCleaningService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1821-1821 | ValetLaundryService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1850-1850 | IroningService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1866-1866 | ChildCareService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1918-1918 | RoomCleaningService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1948-1948 | TurndownService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1964-1964 | RoomService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1989-1989 | WakeUpService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2082-2082 | TourService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2096-2096 | CurrencyExchangeService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2126-2126 | PhotocopyingService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2148-2148 | CheckInService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2181-2181 | CheckOutService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2240-2240 | ExecutiveService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2255-2255 | SafetyDepositService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2275-2275 | MedicalService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2294-2294 | SecretarialService 是 服务 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 571-571 | CateringService 是 服务 的 subclass |
|
|