| No TPTP formula. May not be expressible in strict first order. | Dining.kif 639-639 | 子類 Reservation and 協議 |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2819-2819 | 子類 TravelReservation and Reservation |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2832-2832 | 子類 FlightReservation and Reservation |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2837-2837 | 子類 TourReservation and Reservation |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2842-2842 | 子類 HotelReservation and Reservation |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 744-744 | 子類 DiningReservation and Reservation |
|
|