| No TPTP formula. May not be expressible in strict first order. | Dining.kif 639-639 | Reservation 是 协议 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2819-2819 | TravelReservation 是 Reservation 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2832-2832 | FlightReservation 是 Reservation 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2837-2837 | TourReservation 是 Reservation 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2842-2842 | HotelReservation 是 Reservation 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 744-744 | DiningReservation 是 Reservation 的 subclass |
|
|