No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2148-2148 | Check-in service is a subclass of service |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2168-2168 | Self-service check-in is a subclass of check-in service |