| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 253-253 | Apple mac oSX is a subclass of Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 274-274 | Kodiak is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 294-294 | Cheetah is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 315-315 | Puma is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 336-336 | Jaguar is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 357-357 | Panther is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 378-378 | Tiger is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 399-399 | Leopard is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 421-421 | Snow Leopard is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 443-443 | Lion is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 464-464 | Mountain Lion is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 482-482 | Mavericks is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 504-504 | Yosemite is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 525-525 | El Capitan is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 546-546 | Sierra is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 568-568 | High Sierra is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 589-589 | Mojave is a subclass of Apple mac oSX |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 610-610 | Catalina is a subclass of Apple mac oSX |
|
|