| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 627-627 | 子類 iPhone and 移動手機 |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 628-628 | 子類 iPhone and AppleComputer |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 642-642 | 子類 AppleIPhone1 and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 643-643 | 子類 AppleIPhone3g and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 644-644 | 子類 AppleIPhone3GS and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 645-645 | 子類 AppleIPhone4 and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 646-646 | 子類 AppleIPhone4s and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 647-647 | 子類 AppleIPhone5 and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 648-648 | 子類 AppleIPhone5c and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 649-649 | 子類 AppleIPhone5s and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 650-650 | 子類 AppleIPhone6 and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 651-651 | 子類 AppleIPhone6plus and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 652-652 | 子類 AppleIPhone6s and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 653-653 | 子類 AppleIPhone6splus and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 654-654 | 子類 AppleIPhonese and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 655-655 | 子類 AppleIPhone7 and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 656-656 | 子類 AppleIPhone7plus and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 657-657 | 子類 AppleIPhone8 and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 658-658 | 子類 AppleIPhone8plus and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 659-659 | 子類 AppleIPhoneX and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 660-660 | 子類 AppleIPhoneXS and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 661-661 | 子類 AppleIPhoneXSmax and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 662-662 | 子類 AppleIPhoneXR and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 663-663 | 子類 AppleIPhone11 and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 664-664 | 子類 AppleIPhone11pro and iPhone |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 665-665 | 子類 AppleIPhone11ProMax and iPhone |
|
|