| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 816-816 | 子類 iPod and AppleComputer |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 817-817 | 子類 iPod and MediaSystem |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 829-829 | 子類 iPod touch and iPod |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 842-842 | 子類 iPod nano and iPod |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 855-855 | 子類 iPod shuffle and iPod |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 868-868 | 子類 iPod classic and iPod |
|
|