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