| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 209-209 | 子類 Mac OS and 操作系統 |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 210-210 | 子類 AppleMacOSSystem1 and Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 211-211 | 子類 AppleMacOSSystem2 and Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 212-212 | 子類 AppleMacOSSystem3 and Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 213-213 | 子類 AppleMacOSSystem4 and Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 215-215 | 子類 AppleMacOSSystem5 and Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 222-222 | 子類 AppleMacOSSystem6 and Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 228-228 | 子類 AppleMacOSSystem7 and Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 238-238 | 子類 AppleMacOSSystem8 and Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 239-239 | 子類 AppleMacOSSystem9 and Mac OS |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 253-253 | 子類 AppleMacOSX and Mac OS |
|
|