No TPTP formula. May not be expressible in strict first order. | Cars.kif 3772-3772 | Remote keyless system is a subclass of security device |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3773-3773 | Remote keyless system is a subclass of collection |