| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4539-4539 | 子類 Account and 協議 |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4540-4540 | 子類 Account and ContentBearingObject |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4541-4541 | 子類 金融賬戶 and Account |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4542-4542 | 子類 用戶帳號 and Account |
|
|